Commit d4dba44b authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

WIP implementation.

parent f8246980
\lstset{language=[Objective]Caml,columns=fixed,basicstyle=\ttfamily\scriptsize,aboveskip=-1em,belowskip=-1em,xleftmargin=-0.5em}
\begin{table}
{\small
\begin{tabular}{|@{\,}c@{\,}|p{0.47\textwidth}@{}|@{\,}p{0.47\textwidth}@{\,}|}
\hline
& Code & Infered type\\
\hline
\hline
1 &
\begin{lstlisting}
let basic_inf = fun (y : Int | Bool) ->
if y is Int then incr y else lnot y\end{lstlisting}
&
$(\Int\to\Int)\land(\Bool\to\Bool)$
\\\hline
2 &
\begin{lstlisting}
let any_inf = fun (x : Any) ->
if x is Int then incr x else
if x is Bool then lnot x else x
\end{lstlisting} &
$(\Int\to\Int)\land(\lnot\Int\to\lnot\Int)\land$
$(\Bool\to\Bool)\land(\lnot(\Int\vee\Bool)\to\lnot(\Int\vee\Bool))$\\
\hline
3 &\begin{lstlisting}
let is_int = fun (x : Any) ->
if x is Int then true else false
let is_bool = fun (x : Any) ->
if x is Bool then true else false
let is_char = fun (x : Any) ->
if x is Char then true else false
\end{lstlisting}
&
$(\Int\to\Keyw{True})\land(\lnot\Int\to\Keyw{False})$\newline
~\newline
$(\Bool\to\Keyw{True})\land(\lnot\Bool\to\Keyw{False})$\newline
~\newline
$(\Char\to\Keyw{True})\land(\lnot\Char\to\Keyw{False})$
\\\hline
4 &
\begin{lstlisting}
let not_ = fun (x : Any) ->
if x is True then false else true
\end{lstlisting} &
$(\Keyw{True}\to\Keyw{False})\land(\Keyw{False}\to\Keyw{True})$\\\hline
5 &
\begin{lstlisting}
let or_ = fun (x : Any) ->
if x is True then (fun (y : Any) -> true)
else fun (y : Any) ->
if y is True then true else false
\end{lstlisting}
&
$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land$\newline
$(\lnot\True\to\lnot\True\to\False)$
\\\hline
6 &
\begin{lstlisting}
let and_ = fun (x : Any) -> fun (y : Any) ->
if not_ (or_ (not_ x) (not_ y)) is True
then true else false
\end{lstlisting}
&
$(\True\to((\lnot\True\to\False)\land(\True\to\True))$\newline
$ \land(\lnot\True\to\Any\to\False)$
\\\hline
7 &
\begin{lstlisting}
let f = fun (x : Any) -> fun (y : Any) ->
if and_ (is_int x) (is_bool y) is True
then 1 else
if or_ (is_char x) (is_int y) is True
then 2 else 3
\end{lstlisting}&
$(\Int \to (\Int \to 2) \land (\lnot\Int \to 1 \lor 3) \land (\Bool \to 1) \land$\newline
\hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 3) \land
(\lnot\Bool \to 2\lor3))$\newline
$ \land$\newline
$(\Char \to (\Int \to 2) \land (\lnot\Int \to 2) \land (\Bool \to 2) \land$\newline
\hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 2) \land
(\lnot\Bool \to 2))$\newline
$ \land$\newline%
$(\lnot(\Int \lor \Char) \to (\Int \to 2) \land
(\lnot\Int \to 3) \land$\newline
\hspace*{0.2cm}$(\Bool \to 3) \land(\lnot(\Bool \lor \Int) \to 3)
\land (\lnot\Bool \to 2
\lor 3))$\newline
$\land \ldots$ (two other redundant cases ommitted)
% \newline
% $(\lnot\Char \to (\Int \to 2) \land (\lnot\Int \to 1 \lor 3) \land (\Bool \to 1 \lor 3) \land$\newline
% \hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 3) \land
% (\lnot\Bool \to 2\lor 3)) \land$\newline
% $(\lnot\Int \to (\Int \to 2) \land (\lnot\Int \to 2
% \lor 3) \land (\Bool \to 2\lor 3) \land$\newline
% \hspace*{1cm}$(\lnot(\Bool \lor \Int) \to 2
% \lor 3) \land (\lnot\Bool \to 2\lor 3))$
\\\hline
& \begin{lstlisting}
let test_1 = f 3 true
let test_2 = f (42,42) 42
let test_3 = f nil nil
\end{lstlisting}&
$1$\newline
$2$\newline
$3$
\\\hline
\end{tabular}
}
\caption{Types inferred by implementation}
\label{tab:implem}
\end{table}
\ No newline at end of file
\subsection{Adding structured types}
\label{ssec:struct}
The previous analysis already covers a large pan of realistic cases. For instance, the analysis already handles list data structures, since products and recursive types can encode them as right associative nested pairs, as it is done in the language CDuce~\cite{BCF03} (e.g., $X = \textsf{Nil}\vee(\Int\times X)$ is the type of the lists of integers). And even more since the presence of union types makes it possible to type heterogeneous lists whose content is described by regular expressions on types as proposed by~\citet{hosoya00regular}. Since the main application of occurrence typing is to type dynamic languages, then it is worth showing how to extend our work to records. We use the record types as they are defined in CDuce and which are obtained by extending types with the following two type constructors:
\[
\begin{array}{lrcl}
......
......@@ -444,7 +444,7 @@ exists a value $v$ of type $t$ such that $e\reduces^* v$.
\subsection{Algorithmic system}
\label{ssec:algorithm}
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
......
For Kim.
We have implemented a simplified version of the algorithm presented in
Section~\ref{ssec:algorithm}. In particular, our implementation does
not make use of type schemes and is therefore incomplete. In
particular, as we explained in Section~\ref{}, in the absence of type
scheme it is not always possible to prove that $\forall v, \forall t,
v \in t \text{~or~} v \not\in \not t$. However this is property does
not hold only for lambda expressions, therefore not using type schemes
only yields imprecise typing for tests of the form
\begin{displaymath}
\ifty{(\lambda^{\bigwedge_{i\in I}t_i \to s_i} x. e)}{t}{e_1}{e_2}
\end{displaymath}
This seems like a reasonable compromise between the complexity of an
implementation involving type scheme and the programs we want to
typecheck in practice.
Our implementation is written in OCaml and uses CDuce as a library to
provide the semantic subtyping 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
consits 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}.
\input{code_table}
In this table, the second column gives a code fragment and third
column the type deduced by our implementation. Code~1 is a
straightforward function similar to our introductory example. Here the
programmer annotates the domain of the function with a coarce type
$\Int\vee\Bool$. Our implementation first typechecks the body of the
function under this assumption, but doing so collects that the type of
$\texttt{x}$ is specialized to \Int in the ``then'' case and to \Bool
in the ``else'' case. The function is therefore typechecked twice more
under both hypothesis for \texttt{x} yielding the precise type
$(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t to rule [{\sc
AbsInf}+] of Section~\{sec:refining}, we further improve the computed
output type. Indeed using rule~[{\sc AbsInf}+] we would obtain the
type
$(\Int\to\Int)\land(\Bool\to\Bool)\land(\Bool\vee\Int\to\Bool\vee\Int)$
with a redundant arrow.
......@@ -15,6 +15,7 @@
\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{color}
\usepackage{listings}
\definecolor{darkblue}{rgb}{0,0.2,0.4}
\definecolor{darkred}{rgb}{0.7,0.4,0.4}
......@@ -88,6 +89,7 @@
\newcommand {\True} {\Keyw{True}}
\newcommand {\Int} {\Keyw{Int}}
\newcommand {\Bool} {\Keyw{Bool}}
\newcommand {\Char} {\Keyw{Char}}
\newcommand {\Real} {\Keyw{Real}}
\newcommand {\Complex} {\Keyw{Complex}}
\newcommand {\String} {\Keyw{String}}
......
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