Commit 75040132 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add the suggested references to the related work.

parent 90e5c7f7
......@@ -12,35 +12,7 @@ State what we capture already, for instance lists since we have product and recu
\kim{Need to clean-up and insert at the right place.
}
The work of \cite{Bierman10}, presents Dminor, a data oriented
language featuring a {\tt SELECT}-like constructs over
collections. Its typesystems combines semantic subtyping and
refinement types. Syntactic types are mapped to first order formula
and subtyping is expressed as logicial implication. An SMT-solver is
then used to (try to) prove the logicial implication. The refinement
types they present go well beyond what can be expressed with the set-theoretic
types we use (as they allow almost any pure expression to occur in
types). However, the system foregoes any notion of completeness
(since satisfiability of first order logic is undecidable) and the
subtyping algorithm is largely dependent on the subtle behaviour of
the SMT solver (which may timeout our give an incorrect model that
cannot be used as a counter-example to explain the type-error).
As with our work, the typing rule for the {\tt if~$e$ then $e_1$ else
$e_2$} construct
of Dminor refines the type of each branch by remembering that $e$
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) but this information
is not propagated to the outer context.
A similar approach is taken in \cite{Chugh12}, and extended to so
called nested refinement types. In these types, an arrow type may
appear in a logical formula (where previous work only allowed formulae
between ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types. As in \cite{Bierman10}, the refined typed
of a conditional does not flow to the outer context and the same
provision to using an SMT solver apply.
\kim{\cite{Bonn16} is typed racket with closure\ldots}.
Occurrence typing was introduced by \citet{THF08} and further advanced
in \cite{THF10} in the context of the Typed Racket language. This
......@@ -65,13 +37,31 @@ the role of formulæ. Using set-theoretic types, we can express the
complex types of variables without resorting to a meta-logic. This
allows us to type all but two of their key examples (the notable
exceptions being Example~8 and 14 in their paper, which use the propagation of type
information outside of the branches of a test). Also, while they
information outside of the branches of a test). While Typed Racket
supports structured data types such as pairs and records only unions
of such types can be expressed at the level of types, and even for
those, subtyping is handled axiomatically. For instance, for pairs,
the subtyping rule presented in \cite{THF10} is unable to deduce that
$(\texttt{number}\times \texttt{number}\cup\texttt{bool})\cup
(\texttt{bool}\times \texttt{number}\cup\texttt{bool})$ is a subtype of
(and actually equal to) $(\texttt{number}\cup\texttt{bool}\times\texttt{number})\cup
( \texttt{number}\cup\texttt{bool}\times\texttt{bool})$. For record
types, we also type precisely the deletion of labels, which, as far as
we know other systems cannot do. On the other hand, the propagation of
logical properties defined in \cite{THF10} is a powerfull tool, that
can be extended to cope with sophisticated language features such as
the multi-method dispatch of the Closure language \cite{Bonn16}.
\kim{Remove or merge :
Also, while they
extend their core calculus with pairs, they only provide a simple {\tt
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.
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.
......@@ -88,7 +78,35 @@ system, it does so at the cost of having the programmer write logical
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.
constructs such as pairs, records or recursive types. The idea to
defer the subtyping check to an SMT solver is not new.
The work of \cite{Bierman10}, presents Dminor, a data oriented
language featuring a {\tt SELECT}-like constructs over
collections. Its typesystems combines semantic subtyping and
refinement types. Syntactic types are mapped to first order formula
and subtyping is expressed as logicial implication. An SMT-solver is
then used to (try to) prove the logicial implication. The refinement
types they present go well beyond what can be expressed with the set-theoretic
types we use (as they allow almost any pure expression to occur in
types). However, the system foregoes any notion of completeness
(since satisfiability of first order logic is undecidable) and the
subtyping algorithm is largely dependent on the subtle behaviour of
the SMT solver (which may timeout our give an incorrect model that
cannot be used as a counter-example to explain the type-error).
As with our work, the typing rule for the {\tt if~$e$ then $e_1$ else
$e_2$} construct
of Dminor refines the type of each branch by remembering that $e$
(resp. $\lnot e$) is true in $e_1$ (resp. $e_2$) but this information
is not propagated to the outer context.
A similar approach is taken in \cite{Chugh12}, and extended to so
called nested refinement types. In these types, an arrow type may
appear in a logical formula (where previous work only allowed formulae
between ``base types''). This is done in the context of a dynamic
language and their approach is extended with polymorphism, dynamic
dispatch and record types. As in \cite{Bierman10}, the refined typed
of a conditional does not flow to the outer context and the same
provision to using an SMT solver apply.
\citet{Cha2017} present the design and implementation of Flow by formalizing a relevant
fragment of the language. Since they target an industrial-grade
......
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