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

Merge branch 'master' of

parents e4289328 dcda978a
......@@ -232,3 +232,65 @@ Finally, I took advantage of this opportunity to describe some undocumented adva
address = {New York, NY, USA},
keywords = {Racket, Refinement types, occurrence typing},
author = {Bierman, Gavin M. and Gordon, Andrew D. and Hriundefinedcu, Cundefinedtundefinedlin and Langworthy, David},
title = {Semantic Subtyping with an SMT Solver},
year = {2010},
issue_date = {September 2010},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {45},
number = {9},
issn = {0362-1340},
url = {},
doi = {10.1145/1932681.1863560},
journal = {SIGPLAN Not.},
month = sep,
pages = {105–116},
numpages = {12},
keywords = {type systems, semantic subtyping, data processing, satisfiability modulo theories}
author = {Chugh, Ravi and Rondon, Patrick M. and Jhala, Ranjit},
title = {Nested Refinements: A Logic for Duck Typing},
year = {2012},
isbn = {9781450310833},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {},
doi = {10.1145/2103656.2103686},
booktitle = {Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {231–244},
numpages = {14},
keywords = {dynamic languages, refinement types},
location = {Philadelphia, PA, USA},
series = {POPL ’12}
author = {Ambrose Bonnaire{-}Sergeant and
Rowan Davies and
Sam Tobin{-}Hochstadt},
editor = {Peter Thiemann},
title = {Practical Optional Types for Clojure},
booktitle = {Programming Languages and Systems - 25th European Symposium on Programming,
{ESOP} 2016, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands,
April 2-8, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9632},
pages = {68--94},
publisher = {Springer},
year = {2016},
url = {\_4},
doi = {10.1007/978-3-662-49498-1\_4},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {},
bibsource = {dblp computer science bibliography,}
\ No newline at end of file
......@@ -129,8 +129,8 @@
\author{Kim Nguyen}
\department{Laboratoire de Recherche en Informatique (LRI)}
\institution{Université Paris Sud}
\department{Laboratoire de Recherche en Informatique}
\institution{Université Paris-Saclay}
......@@ -9,6 +9,9 @@ defined predicates.
State what we capture already, for instance lists since we have product and recursive types.
\kim{Need to clean-up and insert at the right place.
Occurrence typing was introduced by \citet{THF08} and further advanced
......@@ -34,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{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.
......@@ -57,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