practical.tex 2.22 KB
 Kim Nguyễn committed Jul 08, 2019 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.  Giuseppe Castagna committed Jan 03, 2019 15   Kim Nguyễn committed Jul 08, 2019 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.