Commit 6e30a5ad authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

more on the algorithms

parent a169b4ad
......@@ -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{}.
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}.
For this presentation it suffices to consider that
types are interpreted as sets of \emph{values} ({\emph{ie}, either
constants, $\lambda$-abstractions, or pair of values: see
......@@ -432,7 +432,22 @@ diverges.
\subsection{Algorithmic system}
3 ingredients:
The system we defined in the previous section implements the ideas we
illustrated in the introduction and it is sound. Now the problem is to
decide whether an expression is well typed or not, that is, to find an
algorithm that given a type environment $\Gamma$ and an expression $e$
decides whether there exists a type $t$ such that $\Gamma\vdash e:t$
is probable. For that we need to solve essentially three problems: $(i)$ how to handle the fact that it is possible to deduce several types for the same well-typed expression $(2)$ how to compute the auxiliary deduction system for paths.
The origin of multiple types are of two distinct origins that will
require two distinct technical solutions. The first origin is the rule
\Rule{Abs-} by which it is possible to deduce for every well-typed
lambda abstractions infinitely many types, that is the annotation of
the function intersected with as many negations of arrow types as it
is possible without making the type empty. To handle this multiplicity we use the technique of \emph{type schemes} defined by~\citet{Frisch2004}. Type schemes are canonical representations of the infinite set of types of $\lambda$-abstraction and they are presented in Section~\ref{sec:type-schemes}. The second origin is due to the presence of structural rules\footnote{In logic, logical rules refer to a particular connective
(here, a type constructor, that is, either $\to$, or $\times$, or
$b$), while identity rules (e.g., axioms and cuts) and structural
rules (e.g., weakening and contraction) do not.} such as \Rule{Subs} and \Rule{Intersect}. We handle it in the classic way: we define an algorithmic system that tracks the miminum type (actually, type scheme) of an expression which is obtained from the original system by eliminating the two structural rules and distrubuting checks of the subtyping relation
\begin{enumerate}
\item type of functions -> type schemes
......@@ -451,7 +466,7 @@ Next we can give the algorithmic typing rules
change the definition of typeof to take into account type-schemes for lambda abstractions
\subsubsection{Operators on types}
\subsubsection{Operators on types}\label{sec:typeops}
\paragraph{Declarative version}
......@@ -462,5 +477,5 @@ change the definition of typeof to take into account type-schemes for lambda abs
\subsection{Algorithmic typing rules}
\subsection{Algorithmic typing rules}\label{sec
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