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

Added extended rule

parent f584c9b5
......@@ -10,7 +10,7 @@
%\documentclass[acmsmall,screen]{acmart}\settopmatter{}
\newif\ifwithcomments
\withcommentstrue
%\withcommentsfalse
\withcommentsfalse
\newif\iflongversion
\longversiontrue
\longversionfalse
......@@ -269,6 +269,11 @@
\section{Full Proofs and Definitions}
\label{sec:proofs}
\input{proofs}
\section{A more precise rule for inference}\label{app:optimize}
\input{optimize}
\section{A Roadmap to Polymorphic Types}
\label{app:roadmap}
\input{roadmappolymorphism}
......
In our prototype we have implemented for the inference of arrow type the following rule:
\[\begin{array}{l}
{\small\Rule{AbsInf++}}\\
\frac
{ \begin{array}{c}
T = \{ (s\setminus\bigvee_{s'\in\psi(x)}s',t) \} \cup \{ (s',t') ~|~
s'\in\psi(x) \land \Gamma,x:s'\vdash e:t' \}\\
\textstyle\Gamma,x:s\vdash e\triangleright\psi
\qquad
\Gamma,x:s\setminus\bigvee_{s'\in\psi(x)}s'\vdash e:t
\end{array}
}
{
\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
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?}
......@@ -20,7 +20,7 @@ Our implementation is written in OCaml and uses CDuce as a library to
provide the semantic sub-typing machinery. Besides a type-checking
algorithm defined on the base language, our implementation supports
record types (Section \ref{ssec:struct}) and the refinement of function types
(Section \ref{sec:refining}). The implementation is rather crude and
(Section \ref{sec:refining} with the rule of Appendix~\ref{app:optimize}). The implementation is rather crude and
consist of 2000 lines of OCaml code, including parsing, type-checking
of programs and pretty printing of types. We demonstrate the output of
our type-checking implementation in Table~\ref{tab:implem}.
......
......@@ -116,7 +116,7 @@ Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x
\end{array}\right.
\end{displaymath}
\noindent
\else.\fi
\else.~\fi
All that remains to do is replace the rule [{\sc Abs}+] with the
following rule
\begin{mathpar}
......@@ -166,12 +166,12 @@ does:
I}s_i\to t_i} x.e:\bigwedge_{i\in I}(s_i\to
t_i)\land\bigwedge_{(u, v)\in T_i}(u\to v) } {}
\end{mathpar}
Here, for each arrow in the declared interface of the function, we
Here, for each arrow declared in the interface of the function, we
first typecheck the body of the function as usual (to check that the
arrow is valid) and collect the refined types for the parameter $x$.
Then we deduce all the possible output types for this refined input
Then we deduce all possible output types for this refined input
types and add the resulting arrows to the type we deduce for the whole
function.
function (see Appendix~\ref{app:optimize} for an even more precise rule).
\kim{We define the rule on the type system not the algorithm. I think
......
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