practical.tex 10.4 KB
Newer Older
Giuseppe Castagna's avatar
Giuseppe Castagna committed
1
We have implemented the algorithmic system $\vdashA$. Our
Giuseppe Castagna's avatar
Giuseppe Castagna committed
2
implementation is written in OCaml and uses CDuce as a library to
Giuseppe Castagna's avatar
Giuseppe Castagna committed
3
provide the semantic subtyping machinery. Besides the type-checking
Kim Nguyễn's avatar
Kim Nguyễn committed
4
algorithm defined on the base language, our implementation supports
Giuseppe Castagna's avatar
Giuseppe Castagna committed
5
6
7
record types (Section \ref{ssec:struct}) and the refinement of
function types (Section \ref{sec:refining} with the rule of
Appendix~\ref{app:optimize}). The implementation is rather crude and
Giuseppe Castagna's avatar
Giuseppe Castagna committed
8
consists of 2000 lines of OCaml code, including parsing, type-checking
Giuseppe Castagna's avatar
Giuseppe Castagna committed
9
10
11
of programs, and pretty printing of types. We demonstrate the output
of our type-checking implementation in Table~\ref{tab:implem} by
listing some examples none of which can be typed by current
Giuseppe Castagna's avatar
Giuseppe Castagna committed
12
13
systems (even though some systems such as Flow and TypeScript
can type some of these examples by adding explicit type annotations, the code 6,
Giuseppe Castagna's avatar
Giuseppe Castagna committed
14
7, 9, and 10 in Table~\ref{tab:implem}  and, even more,  the \code{and\_} and \code{xor\_} functions at the end of this
Giuseppe Castagna's avatar
Giuseppe Castagna committed
15
section are out of reach of current systems, even when using the right
Kim Nguyễn's avatar
Kim Nguyễn committed
16
17
18
19
explicit annotations). It should be noted that for all the examples we discuss,
the the time for the type inference process is less than 5ms, hence we do not
report precise timings in the table.
 These and other examples can be tested in the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
20
\ifsubmission
21
22
anonymized
\else
Giuseppe Castagna's avatar
Giuseppe Castagna committed
23
\fi
24
25
online toplevel available at
\url{https://occtyping.github.io/}%
Kim Nguyễn's avatar
Kim Nguyễn committed
26
\input{code_table}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
27
In Table~\ref{tab:implem}, the second column gives a code fragment and the third
Kim Nguyễn's avatar
Kim Nguyễn committed
28
column the type deduced by our implementation. Code~1 is a
Giuseppe Castagna's avatar
Giuseppe Castagna committed
29
30
straightforward function similar to our introductory example \code{foo} in (\ref{foo},\ref{foo2}). Here the
programmer annotates the parameter of the function with a coarse type
31
$\Int\vee\Bool$. Our implementation first type-checks the body of the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
32
function under this assumption, but doing so it collects that the type of
Giuseppe Castagna's avatar
Giuseppe Castagna committed
33
34
35
$\texttt{x}$ is specialized to \Int{} in the ``then'' case and to \Bool{}
in the ``else'' case. The function is thus type-checked twice more
under each hypothesis for \texttt{x}, yielding the precise type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
36
$(\Int\to\Int)\land(\Bool\to\Bool)$. Note that w.r.t.\  rule \Rule{AbsInf+} of Section~\ref{sec:refining}, our implementation improved the output of the computed
Giuseppe Castagna's avatar
Giuseppe Castagna committed
37
type. Indeed, using rule~[{\sc AbsInf}+] we would obtain the
Kim Nguyễn's avatar
Kim Nguyễn committed
38
39
type
$(\Int\to\Int)\land(\Bool\to\Bool)\land(\Bool\vee\Int\to\Bool\vee\Int)$
Giuseppe Castagna's avatar
Giuseppe Castagna committed
40
with a redundant arrow. Here we can see that, since we deduced
41
the first two arrows $(\Int\to\Int)\land(\Bool\to\Bool)$, and since
Giuseppe Castagna's avatar
Giuseppe Castagna committed
42
the union of their domain exactly covers the domain of the third arrow, then
43
the latter is not needed. Code~2 shows what happens when the argument
Giuseppe Castagna's avatar
Giuseppe Castagna committed
44
of the function is left unannotated (i.e., it is annotated by the top
Giuseppe Castagna's avatar
Giuseppe Castagna committed
45
type \Any, written ``\texttt{Any}'' in our implementation). Here
46
47
type-checking and refinement also work as expected, but the function
only type checks if all cases for \texttt{x} are covered (which means
Giuseppe Castagna's avatar
Giuseppe Castagna committed
48
49
that the function must handle the case of inputs that are neither in \Int{}
nor in \Bool).
50
51
52

The following examples paint a more interesting picture. First
(Code~3) it is
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
53
easy in our formalism to program type predicates such as those
Giuseppe Castagna's avatar
Giuseppe Castagna committed
54
hard-coded in the $\lambda_{\textit{TR}}$ language of \citet{THF10}. Such type
55
56
predicates, which return \texttt{true} if and only if their input has
a particular type, are just plain functions with an intersection
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
57
type inferred by the system of Section~\ref{sec:refining}. We next define Boolean connectives as overloaded
Giuseppe Castagna's avatar
Giuseppe Castagna committed
58
functions. The \texttt{not\_} connective (Code~4) just tests whether its
59
argument is the Boolean \texttt{true} by testing that it belongs to
60
61
62
63
64
65
66
67
68
the singleton type \True{} (the type whose only value is
\texttt{true}) returning \texttt{false} for it and \texttt{true} for
any other value (recall that $\neg\True$ is equivalent to
$\texttt{Any\textbackslash}\True$). It works on values of any type,
but we could restrict it to Boolean values by simply annotating the
parameter by \Bool{} (which in CDuce is syntactic sugar for
\True$\vee$\False) yielding the type
$(\True{\to}\False)\wedge(\False{\to}\True)$.
The \texttt{or\_} connective (Code~5) is straightforward as far as the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
69
70
code goes, but we see that the overloaded type precisely captures all
possible cases. Again we use a generalized version of the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
71
\texttt{or\_} connective that accepts and treats any value that is not
72
\texttt{true} as \texttt{false} and again, we could easily restrict the
73
74
domain to \Bool{} if desired.\\
\indent
Giuseppe Castagna's avatar
Giuseppe Castagna committed
75
To showcase the power of our type system, and in particular of
76
the ``$\worra{}{}$''
Giuseppe Castagna's avatar
Giuseppe Castagna committed
77
type operator, we define \texttt{and\_} (Code~6) using De Morgan's
78
Laws instead of
Giuseppe Castagna's avatar
Giuseppe Castagna committed
79
using a direct definition. Here the application of the outermost \texttt{not\_} operator is checked against type \True. This
80
allows the system to deduce that the whole \texttt{or\_} application
Giuseppe Castagna's avatar
typos    
Giuseppe Castagna committed
81
has type \False, which in turn leads to \texttt{not\_\;x} and
Victor Lanvin's avatar
Fixes    
Victor Lanvin committed
82
\texttt{not\_\;y} to have type $\lnot \True$ and therefore both \texttt{x}
83
84
85
86
87
88
and \texttt{y} to have type \True. The whole function is typed with
the most precise type (we present the type as printed by our
implementation, but the first arrow of the resulting type is
equivalent to
$(\True\to\lnot\True\to\False)\land(\True\to\True\to\True)$).

Giuseppe Castagna's avatar
Giuseppe Castagna committed
89
All these type predicates and Boolean connectives can be used together
90
91
92
to write complex type tests, as in Code~7. Here we define a function
\texttt{f} that takes two arguments \texttt{x} and \texttt{y}. If
\texttt{x} is an integer and \texttt{y} a Boolean, then it returns the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
93
94
integer \texttt{1}; if \texttt{x} is a character or
\texttt{y} is an integer, then it returns \texttt{2}; otherwise the
95
function returns \texttt{3}. Our system correctly deduces a (complex)
Giuseppe Castagna's avatar
Giuseppe Castagna committed
96
97
intersection type that covers all cases (plus several redundant arrow
types). That this type is as precise as possible can be shown by the fact that
98
when applying
Giuseppe Castagna's avatar
Giuseppe Castagna committed
99
100
\texttt{f} to arguments of the expected type, the \emph{type} deduced for the
whole expression is the singleton type \texttt{1}, or \texttt{2},
101
102
103
or \texttt{3}, depending on the type of the arguments.

Code~8 allows us to demonstrate the use and typing of record paths. We
Giuseppe Castagna's avatar
Giuseppe Castagna committed
104
model, using open records, the type of DOM objects that represent XML
105
or HTML documents. Such objects possess a common field
Giuseppe Castagna's avatar
Giuseppe Castagna committed
106
\texttt{nodeType} containing an integer constant denoting the kind of
107
the node (e.g., \p{1} for an element node, \p{3} for a text node, \ldots). Depending on the kind, the object will have
108
109
different fields and methods. It is common practice to perform a test
on the value of the \texttt{nodeType} field. In dynamic languages such
110
111
112
as JavaScript, the relevant field can directly be accessed
after having checked for the appropriate \texttt{nodeType}, whereas
in statically typed languages such as Java, a downward cast
113
from the generic \texttt{Node} type to the expected precise type of
Giuseppe Castagna's avatar
Giuseppe Castagna committed
114
the object is needed. We can see that using the extension presented in
115
116
117
118
119
120
121
Section~\ref{ssec:struct} we can deduce the correct type for
\texttt{x} in all cases. Of particular interest is the last case,
since we use a type case to check the emptiness of the list of child
nodes. This splits, at the type level, the case for the \Keyw{Element}
type depending on whether the content of the \texttt{childNodes} field
is the empty list or not.

Giuseppe Castagna's avatar
Giuseppe Castagna committed
122
Code~9 shows the usefulness of the rule \Rule{OverApp}.
123
Consider the definition of the \texttt{xor\_} operator.
124
125
Here the rule~[{\sc AbsInf}+] is not sufficient to precisely type the
function, and using only this rule would yield a type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
126
127
128
 $\Any\to\Any\to\Bool$.
\iflongversion
Let us follow the behavior of the
129
130
 ``$\worra{}{}$'' operator. Here the whole \texttt{and\_} is requested
 to have type \True, which implies that \texttt{or\_ x y} must have
Giuseppe Castagna's avatar
Giuseppe Castagna committed
131
 type \True. This can always happen, whether \texttt{x} is \True{} or
132
133
 not (but then depends on the type of \texttt{y}). The ``$\worra{}{}$''
 operator correctly computes that the type for \texttt{x} in the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
134
 ``\texttt{then}'' branch is $\True\vee\lnot\True\lor\True\simeq\Any$,
135
and a similar reasoning holds for \texttt{y}.
Giuseppe Castagna's avatar
Giuseppe Castagna committed
136
\fi%%%%%%%%%%%%%%
137
However, since \texttt{or\_} has type
Giuseppe Castagna's avatar
Giuseppe Castagna committed
138
139
140
141
142
%\\[.7mm]\centerline{%
$(\True\to\Any\to\True)\land(\Any\to\True\to\True)\land
   (\lnot\True\to\lnot\True\to\False)$
%}\\[.7mm]
then the rule \Rule{OverApp} applies and \True, \Any, and $\lnot\True$ become candidate types for
Giuseppe Castagna's avatar
Giuseppe Castagna committed
143
\texttt{x}, which allows us to deduce the precise type given in the table. Finally, thanks to rule \Rule{OverApp} it is not  necessary to use a type case to force refinement. As a consequence, we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
144
\begin{alltt}\color{darkblue}\morecompact
Giuseppe Castagna's avatar
Giuseppe Castagna committed
145
146
  let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
  let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
Giuseppe Castagna's avatar
Giuseppe Castagna committed
147
148
\end{alltt}
for which the very same types as in Table~\ref{tab:implem} are deduced.
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
149

Giuseppe Castagna's avatar
Giuseppe Castagna committed
150
151
152
Last but not least Code~10 (corresponding to our introductory
example~\eqref{nest1}) illustrates the need for iterative refinement of
type environments, as defined in Section~\ref{sec:typenv}. As
153
explained, a single pass analysis would deduce
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
154
for {\tt x}
Giuseppe Castagna's avatar
Giuseppe Castagna committed
155
a type \Int{} from the {\tt f\;x} application and \Any{} from the {\tt g\;x}
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
156
application. Here by iterating a second time, the algorithm deduces
Giuseppe Castagna's avatar
empty    
Giuseppe Castagna committed
157
that {\tt x} has type $\Empty$ (i.e., $\textsf{Empty}$), that is that the first branch can never
Giuseppe Castagna's avatar
Giuseppe Castagna committed
158
be selected (and our implementation warns the user accordingly). In hindsight, the only way for a well-typed overloaded function to have
Giuseppe Castagna's avatar
empty    
Giuseppe Castagna committed
159
type $(\Int{\to}\Int)\land(\Any{\to}\Bool)$ is to diverge when the
Giuseppe Castagna's avatar
typo    
Giuseppe Castagna committed
160
argument is of type \Int: since this intersection type states that
Kim Nguyễn's avatar
.    
Kim Nguyễn committed
161
162
163
164
165
whenever the input is \Int, {\em both\/} branches can be selected,
yielding a result that is at the same time an integer and a Boolean.
This is precisely reflected by the case $\Int\to\Empty$ in the result.
Indeed our {\tt example10} function can be applied to an integer, but
at runtime the application of {\tt f ~x} will diverge.
166
167

Although these experiments are still preliminary, they show how the
Giuseppe Castagna's avatar
Giuseppe Castagna committed
168
combination occurrence typing and set-theoretic types, together
169
with the type inference for overloaded function types presented in
Giuseppe Castagna's avatar
Giuseppe Castagna committed
170
171
Section~\ref{sec:refining} goes beyond what languages like
TypeScript and Flow do, since they can only infer single arrow types.
172
Our refining of overloaded
Giuseppe Castagna's avatar
Giuseppe Castagna committed
173
functions is also future-proof and resilient to extensions: since it ``retypes'' functions
174
 using information gathered by the typing of occurrences in the body,
Giuseppe Castagna's avatar
Giuseppe Castagna committed
175
176
 its precision will improve with any improvement of
 our occurrence typing framework.