Commit f85469c6 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

related work on Flow

parent 2114badf
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment