Commit 37a871d3 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

chapeau to section 3

parent 04c7b218
As we recalled in the introduction, the main application of occurrence
typing is to type dynamic languages. In this section we explore how to
extend our work to encompass three features that are necessary to type
these languages.
First, we consider record types and record expressions which, in dynamic
languages, are used to implement objects. In particular, we extend our
system to cope with typical usage patterns of objects in these
languages such as adding, modifying, or deleting a field, or dynamically
test its presence to specify different behaviors.
Second, in order
to precisely type applications in dynamic languages it is
crucial to refine the type of some functions to account for their
different behaviors with specific input types. But current approaches
are bad at it: they require the programmer to explicitly specify a
precise intersection type for these function and, even with such specifications, several common cases
fail to type (in that case the only solution is to hard-code the
function and its typing discipline into the language). We show how we
can use the work developed in the previous sections to infer precise
intersection types for functions. These functions do not
require any type annotation in our system or just an annotation for
the function parameters, whereas some of them fail to type in
current alternative approaches even when they are given the full intersection type
Finally, to type dynamic language it is often necessary to make
statically-typed parts of a program coexist with dynamically-typed
ones. This is the aim of gradually typed systems that we explore in
the third extension of this section.
\subsection{Record types}
......@@ -9,18 +41,20 @@ CDuce (e.g., $X = \textsf{Nil}\vee(\Int\times X)$ is the
type of the lists of integers): see Code 8 in Table~\ref{tab:implem} of Section~\ref{sec:practical} for a concrete example. Even more, thanks to the presence of
union types it is 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.
by~\citet{hosoya00regular}. However, this is not enough to cover
records and, in particular, the specific usage patterns in dynamic
languages of records, whose field are dynamically tested, deleted,
added, and modified. This is why we extend here our work to records,
building on the record types as they are defined in CDuce.
The extension we present in this section is not trivial. Although we use the record \emph{types} as they are
defined in CDuce we cannot do the same for CDuce record
\emph{expressions}. The reasons why we cannot use the record
expressions of CDuce and we have to define and study new one are
expressions of CDuce and we have to define and study new ones are
twofold. On the one hand we want to capture the typing of record field extension and field
deletion, two operation widely used in dynamic language; on the other
hand we need to have very simple expressions formed by elementary
subexpressions, in order to limit the combinatorics of occurrence
sub-expressions, in order to limit the combinatorics of occurrence
typing. For this reason we build our records one field at a time,
starting from the empty record and adding, updating, or deleting
single fields.
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