Commit 97a4ea42 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files


parent d8187fc4
......@@ -15,7 +15,7 @@ In our prototype we have implemented for the inference of arrow type the followi
instead of the simpler \Rule{AbsInf+}. The difference w.r.t.\ \Rule{AbsInf+} is that the typing of the body
is made under the hypthesis $x:s\setminus\bigvee_{s'\in\psi(x)}s'$,
is made under the hypothesis $x:s\setminus\bigvee_{s'\in\psi(x)}s'$,
that is, the domain of the function minus all the input types
determined by the $\psi$-analysis. This yields an even better refinement
of the function type that makes a difference for instance with the inference for the function \code{xor\_} (Code 3
......@@ -22,7 +22,7 @@ propositions that record the type of the input depending on the
the argument has type {\tt Number}, and when the output is false, the
argument does not. Such information is used selectively
in the ``then'' and ``else'' branches of a test. One area where their
work goes further than ours is that the type informations also flows
work goes further than ours is that the type information also flows
outside of the tests to the surrounding context. In contrast, our type
system only refines the type of variables strictly in the branches of a
test. However, using semantic-subtyping as a foundation we believe our
......@@ -33,7 +33,7 @@ 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 propgation of type
exception is their Example~8 which uses 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
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