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

space saver

parent 809e5795
......@@ -347,10 +347,7 @@ the positive branch will have type $(\Int\to t)\setminus(\Int\to\neg
will also be the type of the whole expression in \eqref{bistwo}. Now imagine
that the application $e(42)$ reduces to a Boolean value, then the whole
expression in \eqref{bistwo} reduces to $e$; but this has type
$\Int\to t$ which, in general, is \emph{not} a subtype of $(\Int\to
t)\setminus(\Int\to\neg\Bool)$, and therefore type is not preserved by the reduction. To cope with this problem, in
Section~\ref{sec:language} we resort to \emph{type schemes} a
technique introduced by~\citet{Frisch2008} to type expressions by
$\Int\to t$ which, in general, is \emph{not} a ssions by
sets of types, so that the expression in \eqref{bistwo} will have both the types at issue.
The second corner case is a modification of the example above
......@@ -404,17 +401,16 @@ retyping the expression without that assumption (see rule
\subsubsection*{Outline} In Section~\ref{sec:language} we formalize the
ideas presented in this introduction: we define the types, the
expressions and their dynamic semantics and a type system that
implements occurrence typing together with the algorithms to decided
whether an expression is well typed in the
system. Section~\ref{sec:extensions} extends our formalism to record
ideas presented in this introduction: we define types and
expressions of our system, their dynamic semantics and a type system that
implements occurrence typing together with the algorithms that decide
whether an expression is well typed or not. Section~\ref{sec:extensions} extends our formalism to record
types and presents two applications of our analysis: the inference of
arrow types for functions and a static analysis to reduce the number
of casts inserted by a compiler of a gradually-typed
language. Practical aspects are presented in
Section~\ref{sec:practical}. Section~\ref{sec:related} presents
related work and a discussion of future work concludes the
related work. A discussion of future work concludes this
presentation.
For space reasons several technical definitions and all the proofs are
......
......@@ -2,23 +2,23 @@ In this section we formalize the ideas we outlined in the introduction. We start
\subsection{Types}
\begin{definition}[Types]\label{def:types} The set of types \types{} is formed by the terms $t$ coinductively produced by the following grammar
\begin{definition}[Types]\label{def:types} The set of types \types{} is formed by the terms $t$ coinductively produced by the grammar:\vspace{-2mm}
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
and that satisfy the following conditions
and that satisfy the following conditions\vspace{-1mm}
\begin{itemize}
\item (regularity) every term has a finite number of different sub-terms;
\item (contractivity) every infinite branch of a term contains an infinite number of occurrences of the
arrow or product type constructors.
arrow or product type constructors.\vspace{-1mm}
\end{itemize}
\end{definition}
We use the following abbreviations for types: $
We use the following abbreviations: $
t_1 \land t_2 \eqdef \neg (\neg t_1 \vee \neg t_2)$,
$t_ 1 \setminus t_2 \eqdef t_1 \wedge \neg t_2$, $\Any \eqdef \neg \Empty$.
In the definition, $b$ ranges over basic types
$b$ ranges over basic types
(e.g., \Int, \Bool),
$\Empty$ and $\Any$ respectively denote the empty (that types no value)
and top (that types all values) types. Coinduction accounts for
......@@ -38,7 +38,7 @@ and to $ \lor $, $ \land $, $ \lnot $, and $ \setminus $
as \emph{type connectives}.
The subtyping relation for these types, noted $\leq$, is the one defined
by~\citet{Frisch2008} to which the reader may refer for more details. Its formal definition is recalled in Appendix~\ref{} and a detailed description of the algorithm to decide it can be found in~\cite{Cas15}.
by~\citet{Frisch2008} to which the reader may refer. A detailed description of the algorithm to decide it can be found in~\cite{Cas15}.
For this presentation it suffices to consider that
types are interpreted as sets of \emph{values} ({i.e., either
constants, $\lambda$-abstractions, or pair of values: see
......@@ -100,8 +100,8 @@ The dynamic semantics is defined as a classic left-to-right call-by-value reduct
\]
The semantics of type-cases uses the relation $v\in t$ that we
informally defined in the previous section. We delay its formal
definition to Section~\ref{sec:type-schemes} (where it deals with some corner cases for negated arrow types). Context reductions are
defined by the following reduction contexts:
definition to Section~\ref{sec:type-schemes} (where it deals with some corner cases for negated arrow types). Contextual reductions are
defined by the following evaluation contexts:
\[
\Cx[] ::= [\,]\alt \Cx e\alt v\Cx \alt (\Cx,e)\alt (v,\Cx)\alt \pi_i\Cx\alt \tcase{\Cx}tee
\]
......@@ -164,7 +164,7 @@ core and the use of subtyping, given by the following typing rules:
\end{mathpar}
These rules are quite standard and do not need any particular explanation besides those already given in Section~\ref{sec:syntax}. Just notice that we used a classic subsumption rule (i.e., \Rule{Subs}) to embed subtyping in the type system. Let us next focus on the unconventional aspects of our system, from the simplest to the hardest.
The first one is that, as explained in
The first unconventional aspect is that, as explained in
Section~\ref{sec:challenges}, our type assumptions are about
expressions. Therefore, in our rules the type environments, ranged over
by $\Gamma$, map \emph{expressions}---rather than just variables---into
......@@ -226,7 +226,7 @@ Clearly, the expression above is well typed, but the rule \Rule{Abs+} alone
is not enough to type it. In particular, according to \Rule{Abs+} we
have to prove that under the hypothesis that $x$ is of type $\Int$ the expression
$(\tcase{x}{\Int}{x+1}{\textsf{true}})$ is of type $\Int$, too. That is, that under the
hypothesis that x has type $\Int\wedge\Int$ (we apply occurrence
hypothesis that $x$ has type $\Int\wedge\Int$ (we apply occurrence
typing) the expression $x+1$ is of type \Int{} (which holds) and that under the
hypothesis that $x$ has type $\Int\setminus\Int$, that is $\Empty$
(we apply once more occurrence typing), \textsf{true} is of type \Int{}
......@@ -248,7 +248,8 @@ Once more, this kind of deduction was already present in the system
by~\citet{Frisch2008} to type full fledged overloaded functions,
though it was embedded in the typing rule for the type-case. Here we
need the rule \Rule{Efq}, which is more general, to ensure the
property of subject reduction.\beppe{Example?}
property of subject reduction.
%\beppe{Example?}
Finally, there is one last rule in our type system, the one that
implements occurrence typing, that is, the rule for the
......@@ -278,7 +279,7 @@ $\Gamma$ with the hypothesis deduced assuming that $e\in\neg t$, that
is, for when the test $e\in t$ fails.
All it remains to do is to show how to deduce judgments of the form
$\Gamma \evdash e t \Gamma'$. For that we first have to define how
$\Gamma \evdash e t \Gamma'$. For that we first define how
to denote occurrences of an expression. These are identified by paths in the
syntax tree of the expressions, that is, by possibly empty strings of
characters denoting directions starting from the root of the tree (we
......@@ -360,7 +361,7 @@ of rules.
{ \pvdash \Gamma e t \varpi:t_1 \\ \pvdash \Gamma e t \varpi:t_2 }
{ \pvdash \Gamma e t \varpi:t_1\land t_2 }
{ }
\\
\\
\Infer[PTypeof]
{ \Gamma \vdash \occ e \varpi:t' }
{ \pvdash \Gamma e t \varpi:t' }
......@@ -371,7 +372,9 @@ of rules.
{ \pvdash \Gamma e t \epsilon:t }
{ }
\qquad
\\
\end{mathpar}
\begin{mathpar}
%\\ \\
\Infer[PAppR]
{ \pvdash \Gamma e t \varpi.0:\arrow{t_1}{t_2} \\ \pvdash \Gamma e t \varpi:t_2'}
{ \pvdash \Gamma e t \varpi.1:\neg t_1 }
......@@ -401,7 +404,6 @@ of rules.
{ \pvdash \Gamma e t \varpi:t' }
{ \pvdash \Gamma e t \varpi.s:\pair \Any {t'} }
{ }
\qquad
\end{mathpar}
These rules implement the analysis described in
Section~\ref{sec:ideas} for functions and extend it to products. Let
......
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