Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrencetyping
Commits
7514d60a
Commit
7514d60a
authored
Jul 08, 2019
by
Kim Nguyễn
Browse files
Added all examples and discussion in practical.
parent
a007b8e9
Changes
2
Hide whitespace changes
Inline
Sidebyside
code_table.tex
View file @
7514d60a
\lstset
{
language=[Objective]Caml,columns=fixed,basicstyle=
\ttfamily\scriptsize
,aboveskip=
1
em,belowskip=1em,xleftmargin=0.5em
}
\lstset
{
language=[Objective]Caml,columns=fixed,basicstyle=
\ttfamily\scriptsize
\linespread
{
0.8
}
,aboveskip=
0.5
em,belowskip=1em,xleftmargin=0.5em
}
\begin{table}
{
\s
mall
{
\s
criptsize
\begin{tabular}
{
@
{
\,
}
c@
{
\,
}
p
{
0.47
\textwidth
}
@
{}
@
{
\,
}
p
{
0.47
\textwidth
}
@
{
\,
}

}
\hline
&
Code
&
Infered type
\\
&
Code
&
Infer
r
ed type
\\
\hline
\hline
1
&
...
...
@@ 97,7 +97,7 @@ $\land \ldots$ (two other redundant cases ommitted)
% \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
...
...
@@ 106,7 +106,39 @@ let test_3 = f nil nil
$
1
$
\newline
$
2
$
\newline
$
3
$
\\\hline
\\\hline
8
&
\begin{lstlisting}
type Document =
{
nodeType=9 ..
}
and Element =
{
nodeType=1,
childNodes = NodeList
..
}
and Text =
{
nodeType=3,
isElementContentWhiteSpace=Bool
..
}
and Node = Document  Element  Text
and NodeList = Nil  (Node, NodeList)
let is
_
empty
_
node = fun (x : Node) >
if x.nodeType is 9 then false
else if x.nodeType is 3 then
x.isElementContentWhiteSpace
else
if x.childNodes is Nil then true else false
\end{lstlisting}
&
$
\Keyw
{
Document
}
\to\False
\land
$
\newline
$
\orecord
{
\texttt
{
nodeType
}
=
1
,
\texttt
{
childNodes
}
=
Nil
}
\to\True
~
\land
$
\newline
$
\orecord
{
\texttt
{
nodeType
}
=
1
,
\texttt
{
childNodes
}
=
(
\Keyw
{
Node
}
,
\Keyw
{
NodeList
}
)
}
\to\True
~
\land
$
\newline
$
\Keyw
{
Text
}
\to\Bool
~
\land
$
(ommitted redundant arrows)
\\\hline
9
&
\begin{lstlisting}
let xor
_
= fun (x : Any) > fun (y : Any) >
if and
_
(or
_
x y) (not
_
(and
_
x y)) is True
then true else false
\end{lstlisting}
&
$
\True\to
((
\True\to\False
)
\land
(
\lnot\True\to\True
))
~
\land
$
\newline
$
(
\lnot\True\to
((
\True\to\True
)
\land
(
\lnot\True\to\False
))
$
\\\hline
\end{tabular}
}
\caption
{
Types inferred by implementation
}
...
...
practical.tex
View file @
7514d60a
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
particular, as we explained in Section~
\ref
{
ssec:algorithm
}
, 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
v
\in
t
\text
{
~or~
}
v
\not\in
\
l
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}
...
...
@@ 11,10 +11,10 @@ only yields imprecise typing for tests of the form
\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.
type

check in practice.
Our implementation is written in OCaml and uses CDuce as a library to
provide the semantic subtyping machinery. Besides a typechecking
provide the semantic sub

typing machinery. Besides a typechecking
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
...
...
@@ 25,15 +25,136 @@ our typechecking implementation in Table~\ref{tab:implem}.
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 coar
c
e type
$
\Int\vee\Bool
$
. Our implementation first typechecks the body of the
programmer annotates the domain of the function with a coar
s
e type
$
\Int\vee\Bool
$
. Our implementation first type

checks 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
in the ``else'' case. The function is therefore type

checked 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.
with a redundant arrow. Here we can see that since we deduced
the first two arrows
$
(
\Int\to\Int
)
\land
(
\Bool\to\Bool
)
$
, and since
the union of their domain exactly covers the domain the third arrow,
the latter is not needed. Code~2 shows what happens when the argument
of the function is left unannotated (that is, annotated by the top
type
\Any
written
\texttt
{
Any
}
in our implementation). Here the
typechecking and refinement also work as expected, but the function
only type checks if all cases for
\texttt
{
x
}
are covered (which means
that the function must handle the case of inputs that are neither
\Int
nor
\Bool
).
The following examples paint a more interesting picture. First
(Code~3) it is
easy in our formalism to provide type predicates such as those
hardcoded in the
$
\lambda
_{
TR
}$
language of
\cite
{
THF10
}
. Such type
predicates, which return
\texttt
{
true
}
if and only if their input has
a particular type, are just plain functions with an intersection
type. We then define Boolean combinators as overloaded
functions. The
\texttt
{
not
\_
}
combinator just tests whether its
argument is the Boolean
\texttt
{
true
}
by testing that it belongs to
the singleton type
\True
.
The
\texttt
{
or
\_
}
combinator (Code~5) is defined as a
curryfied function, that first type cases on its argument. Depending
on the type it may return either a constant function that returns
\texttt
{
true
}
for any input, or, a function that
discriminates on its argument (which is the second argument of the
\texttt
{
or
\_
}
) and returns
\texttt
{
true
}
or
\texttt
{
false
}
accordingly. Notice that we use here a generalized version of the
\texttt
{
or
\_
}
operation that accepts and treats any value that is not
\texttt
{
true
}
as
\texttt
{
false
}
. Again, we could restrict the initial
domain to
\Bool
if we wanted.
To showcase the power of our type system, and in particular
the ``
$
\worra
{}{}$
''
type operation, we define
\texttt
{
and
\_
}
(Code~6) using De Morgan's
Laws instead of
using a direct definition. Here the application of the outer
most
\texttt
{
not
\_
}
operator is checked against type
\True
. This
allows the system to deduce that the whole
\texttt
{
or
\_
}
application
has type
\False
, which in turn leads to
\texttt
{
not
\_
x
}
and
\texttt
{
not
\_
y
}
to have type
$
\lnot
\True
$
and therefore
\texttt
{
x
}
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
)
$
).
All these type predicates and Boolean combinator can be used together
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
integer
\texttt
{
1
}
. Otherwise, if
\texttt
{
x
}
is a character or
\texttt
{
y
}
is an integer, it returns
\texttt
{
2
}
and otherwise the
function returns
\texttt
{
3
}
. Our system correctly deduces a (complex)
intersection types that covers all cases (plus several redundant arrow
types). The fact that is type is precise can be shown by the fact that
when applying
\texttt
{
f
}
to arguments of the expected type, the deduced type for the
whole expression is either the singleton type
\texttt
{
1
}
,
\texttt
{
2
}
or
\texttt
{
3
}
, depending on the type of the arguments.
Code~8 allows us to demonstrate the use and typing of record paths. We
model, using open records the type of DOM objects that represent XML
or HTML documents. Such objects possess a common field
\texttt
{
nodeType
}
containing an integer constants denoting the kind of
the node (
\emph
{
e.g.
}
9 for the root element, 1 for an element node
and 3 for a text node). Depending on the kind, the object will have
different fields and methods. It is common practice to perform a test
on the value of the
\texttt
{
nodeType
}
field. In dynamic languages such
as JavaScript, the relevant field or method can directly be accessed
after having checked for the appropriate
\texttt
{
nodeType
}
. In
mainstream statically typed languages, such as Java, downward cast
from the generic
\texttt
{
Node
}
type to the expected precise type of
the object. We can see that using the extension presented in
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.
Our implementation features one last improvement that allows us
further improve the precision of the inferred type.
Consider the definition of the
\texttt
{
xor
\_
}
operator (Code~9).
Here the rule~[
{
\sc
AbsInf
}
+] is not sufficient to precisely type the
function, and using only this rule would yield a type
$
\Any\to\Any\to\Bool
$
. Lets simulate the behaviour of the
``
$
\worra
{}{}$
'' operator. Here the whole
\texttt
{
and
\_
}
is requested
to have type
\True
, which implies that
\texttt
{
or
\_
x y
}
must have
type
\True
. This can always happen, whether
\texttt
{
x
}
is
\True
or
not (but then depends on the type of
\texttt
{
y
}
). The ``
$
\worra
{}{}$
''
operator correctly computes that the type for
\texttt
{
x
}
in the
``
\texttt
{
then
}
'' branch is
$
\True\vee\lnot\True\lor\True\equiv\Any
$
,
and a similar reasoning holds for
\texttt
{
y
}
. To solve this problem,
we can first remark that even though type cases in the body of a
function are the tipping points that may change the type of the result
of the function; they are not the only ones. Indeed,
Applications of overloaded functions plays a similar role. We
therefore extend judgement
$
\Gamma
\vdash
e
\triangleright\psi
$
with
the following rule
\\
\centerline
{\(
\Infer
[
OverApp
]
{
\Gamma
\vdash
e :
\bigvee
\bigwedge
_{
i
\in
I
}
t
_
i
\to
{}
s
_
i
\\
\Gamma
\vdash
x : t
\\
\Gamma
\vdash
e
\triangleright\psi
_
1
\\
\Gamma
\vdash
x
\triangleright\psi
_
2
\\
}
{
\Gamma
\vdash
{
e
}{
~x
}
\triangleright\psi
_
1
\cup\psi
_
2
\cup\bigcup
_{
i
\in
I
}
\{
x
\mapsto
t
\wedge
t
_
i
\}
}
{}
\)}
With this rule, whenever a function parameter is applied to an
overloaded function, we record as possible types for this parameter
all the possible domains of the arrows that make the overloaded
function, restricted to the static type of the parameter. In Code~9,
since,
\texttt
{
or
\_
}
has type
\\
\centerline
{$
(
\True\to\Any\to\True
)
\land
(
\Any\to\True\to\True
)
\land
(
\lnot\True\to\lnot\True\to\False
)
$}
We consider
\True
,
\Any
and
$
\lnot\True
$
as candidate types for
\texttt
{
x
}
which, in turn allows us to deduce a precise type.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment