Commit 55aa2e99 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents 455324fe 207b925d
......@@ -194,9 +194,9 @@ system, that is, the fact that $\lambda$-abstractions can have negated
arrow types, as long as these negated types do not make the type deduced for the function empty:\vspace{-1mm}
\begin{mathpar}
\Infer[Abs-]
{\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
{ \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }
{ (t\wedge\neg(t_1\to t_2))\not\simeq\Empty }\vspace{-3mm}
{\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
{ \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }
{ ((\wedge_{i\in I}\arrow {s_i} {t_i})\wedge\neg(t_1\to t_2))\not\simeq\Empty }
\end{mathpar}
%\beppe{I have doubt: is this safe or should we play it safer and
% deduce $t\wedge\neg(t_1\to t_2)$? In other terms is is possible to
......
......@@ -179,3 +179,20 @@ Finally, I took advantage of this opportunity to describe some undocumented adva
}
@inproceedings{Kent16,
author = {Kent, Andrew M. and Kempe, David and Tobin-Hochstadt, Sam},
title = {Occurrence Typing Modulo Theories},
booktitle = {Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation},
series = {PLDI '16},
year = {2016},
isbn = {978-1-4503-4261-2},
location = {Santa Barbara, CA, USA},
pages = {296--309},
numpages = {14},
url = {http://doi.acm.org/10.1145/2908080.2908091},
doi = {10.1145/2908080.2908091},
acmid = {2908091},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Racket, Refinement types, occurrence typing},
}
......@@ -43,7 +43,7 @@
\Infer[Abs-]
{\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
{ \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }
{ (t\wedge\neg(t_1\to t_2))\not\simeq\Empty }
{ ((\wedge_{i\in I}\arrow {s_i} {t_i})\wedge\neg(t_1\to t_2))\not\simeq\Empty }
\\
\Infer[Case]
{\Gamma\vdash e:t_0\\
......
......@@ -32,13 +32,28 @@ wishes by using an overloaded function, as we have shown in
Section~\ref{sec:practical}. Second, in our setting, {\em types\/} play
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 one of their key examples (the notable
exception is their Example~8 which uses the propagation of type
allows us to type all but two of their key examples (the notable
exceptions being Example~8 and 14 which use the propagation of type
information outside of the branches of a test). 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.\beppe{On peut dire plus? More generally, while their system refines only the type of variables, and only when they occur in some chosen contexts, our approach lifts this limitation on contexts and also refines the types of arbitrary expressions.}
\beppe{Est-ce vrai que: As far as we know, a code analysis such as the one performed by Code 8 for DOM objects is out of reach of the current occurrence typing 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 state of the art.
\citet{Kent16} introduced the $\lambda_{RTR}$ core calculus, an
extension of $\lambda_{TR}$ where the logical formulæ embedded in
types are not limited to built-in type predicates, but accepts
predicates of arbitrary theories. This allows them to provide some
form of dependent typing (and in particular they provide an
implementation supporting bitvector and linear arithmetic theories).
The static invariants that can be enforced by such logic goes well
beyond what can be proven with a static ``non depdendent'' type
system, it does so at the cost of having the programmer write logical
annotations (to help the external provers). While this works provide
richer logical statements than \cite{THF10}, it still remains
restricted to refining the types of variables, and not of arbitrary
constructs such as pairs, records or recursive types.
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