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

space

parent f2ae707d
......@@ -49,6 +49,7 @@ in particular $\recdel e \ell$ deletes the field $\ell$ from $e$, $\recupd e \el
\(\erecord{...,\ell=e,...}.\ell\ \reduces\ e\).
To define record type subtyping and record expression type inference we need the following operators on record types (refer to~\citet{alainthesis} for more details):
\begin{eqnarray}
\proj \ell t & = & \left\{\begin{array}{ll}\min \{ u \alt t\leq \orecord{\ell=u}\} &\text{if } t \leq \orecord{\ell = \Any}\\ \text{undefined}&\text{otherwise}\end{array}\right.\\
t_1 + t_2 & = & \min\left\{
......
......@@ -716,10 +716,10 @@ $\Refinef$ yields for $x_1$ a type strictly more precise than the type deduced i
previous iteration.
The solution we adopt here is to bound the number of iterations to some number $n_o$.
From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (i.e., it will find all solutions) for the deductions of $\Gamma \evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$\vspace{-2mm}
From a formal point of view, this means to give up the completeness of the algorithm: $\Refinef$ will be complete (i.e., it will find all solutions) for the deductions of $\Gamma \evdash e t \Gamma'$ of depth at most $n_o$. This is obtained by the following definition of $\Refinef$\vspace{-1mm}
\[
\begin{array}{rcl}
\Refinef_{e,t} \eqdef (\RefineStep{e,t})^{n_o}\\
\Refinef_{e,t} \eqdef (\RefineStep{e,t})^{n_o}\\[-2mm]
\text{where }\RefineStep {e,t}(\Gamma)(e') &=& \left\{\begin{array}{ll}
%\tyof {e'} \Gamma \tsand
\bigwedge_{\{\varpi \alt \occ e \varpi \equiv e'\}}
......@@ -747,10 +747,11 @@ type (which is quite rare in practice)\footnote{\label{foo:typecase}The only imp
never happens since programming languages test whether a value
\emph{is} a function, rather than the type of a given function.},
but also we had to build the expression that causes the divergence in
quite an \emph{ad hoc} way which makes divergence even more unlikely: setting
an $n_o$ twice the depth of the syntax tree of the outermost type case
should be enough to capture all realistic cases \beppe{can we give an estimate
based on benchmarking the prototype?}
quite an \emph{ad hoc} way which makes divergence even more unlikely.
%: setting
%an $n_o$ twice the depth of the syntax tree of the outermost type case
%should be enough to capture all realistic cases \beppe{can we give an estimate
% based on benchmarking the prototype?}
......
......@@ -151,10 +151,8 @@ will be checked for the input types $\Int$, $\Real\setminus\Int$, and
\Bool, yielding the expected result.
It is not too difficult to generalize this rule when the lambda is
typed by an intersection type. Indeed, even if the programmer has
specified a particular intersection type for the function, we may want
to refine each of its arrows. This is exactly what the following rule
does:\vspace{-1mm}
typed by an intersection type:
\begin{mathpar}
\Infer[AbsInf+] {\forall i\in I~\Gamma,x:s_i\vdash
e\triangleright\psi_i
......
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