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

typos

parent 2bac800c
......@@ -14,11 +14,11 @@ In our prototype we have implemented for the inference of arrow type the followi
\Gamma\vdash\lambda x:s.e:\textstyle\bigwedge_{(s',t') \in T}s'\to t'
}
\end{array}\]
The difference w.r.t.\ \Rule{AbsInf++} is that the typing of the body
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'$,
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 make a difference for instance with Code 3
in Table~\ref{tab:implem}. The rule above is for a single arrow type:
the extension for multiple arrows is similar to the one for the
simpler case. \beppe{is it the right code Kim?}
of the function type that makes a difference for instance with the inference for the function \code{xor\_} (Code 3
in Table~\ref{tab:implem}): the old rule would have returned a less precise type. The rule above is defined for functions annotated by a single arrow type:
the extension to annotations with intersections of multiple arrows is similar to the one we did in the
simpler setting of Section~\ref{sec:refining}.
......@@ -10,33 +10,34 @@ defined predicates.
State what we capture already, for instance lists since we have product and recursive types.
}
Occurrence typing was introduced by \citet{THF08} and further advanced
in \cite{THF10} in the context of the Typed Racket language. This
latter work in particular is close to ours, with some key differences.
The work of \cite{THF10} defines $\lambda_{TR}$, a core calculus for
typed racket. In this language types are annotated by logical
propositions that records the type of the input depending on the
\citet{THF10} define $\lambda_{\textit{TR}}$, a core calculus for
Typed Racket. In this language types are annotated by logical
propositions that record the type of the input depending on the
(Boolean) value of the output. For instance, the type of the
{\tt number?} function states that when the output is {\tt true}, then
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 this
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
outside of the tests to the surrounding context. In contrast, our type
system only refine the type of variables strictly in the branches of a
test. However using semantic-subtyping as a foundation we believe our
approach has several merrits over theirs. First, in our case, 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
approach has several merits over theirs. First, in our case, type
predicates are not built-in. A user may define any type predicate she
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 (with the notable
exception of their Example~8 which uses the propgation of type
allows us to type all but one of their key examples (the notable
exception is their Example~8 which uses the propgation 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 ({\em .e.g\/} test whether the input
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.
\ No newline at end of file
for 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