Commit f85469c6 by Giuseppe Castagna

### related work on Flow

 ... ... @@ -40,9 +40,10 @@ cons?} predicate that allows them to test whether some value is a pair. It is therefore unclear whether their systems allows one to write predicates over list types (e.g., test whether the input is a list of integers), which we can easily do thanks to our support for recursive types. Further, as far as we know, a code analysis such as the one performed by Code 8 for extensible records is not handled by the current state of the art. for recursive types. %Further, as far as we know, a code analysis such as the %one performed by Code 8 for extensible records is not handled by the %current typing systems. \citet{Kent16} introduce the $\lambda_{RTR}$ core calculus, an extension of $\lambda_{TR}$ where the logical formulæ embedded in ... ... @@ -57,3 +58,29 @@ annotations (to help the external provers). While this work provides richer logical statements than those by~\citet{THF10}, it still remains restricted to refining the types of variables, and not of arbitrary constructs such as pairs, records or recursive types. \citet{Cha2017} present the design and implementation of Flow by formalizing a relevant fragment of the language. Since they target an industrial-grade implementation they must account for aspects that we could afford to postpone to future work, notably side effects and responsiveness of the type checker on very large code base. The degree of precision of their analysis is really impressive and they achieve most of what we did here and, since they perform flow analysis and use an effect system (to track mutable variables), even more. However, this results in a specific and very complex system. Their formalization includes only union types (though, Flow accepts also intersection types as in \eqref{foo2}) which are used in \emph{ad hoc} manner by the type system, for instance to type record types. This allows Flow to perform an analysis similar to the one we did for Code 8 in Table~\ref{tab:implem}, but also has as a consequence that in some cases unions do not behave as expected. In contrast, our approach is more classic and foundational: we really define a type system, typing rules looks like classic ones and are easy to understand, unions are unions of values (and so are intersections and negations), and the algorithmic part is---excepted for fix points---relatively simple (algorithmically Flow relies on constraint generation and solving). This is the reason why our system is more adapted to study and understand occurrence typing and to extend it with additional features (e.g., gradual typing and polymorphism) and we are eager to test how much of their analysis we can capture and enhance by formalizing it in our system.
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.6958103775978088, "perplexity": 1071.9721566683397}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2022-40/segments/1664030331677.90/warc/CC-MAIN-20220924151538-20220924181538-00704.warc.gz"}