practical.tex 2.22 KB
Newer Older
Kim Nguyễn's avatar
Kim Nguyễn committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.
15

Kim Nguyễn's avatar
Kim Nguyễn committed
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
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.