The idea behind
gradual typing [1] is to integrate, in a unique framework, both static
typing (where the types in a program are checked against each other
before its execution) and dynamic typing (where the types are only
controlled during the execution).
The ever-growing complexity and availability of Web applications
coupled to their intensive use make the development of verification
methods more important than ever. In particular, static methods are
especially attractive since they are capable of detecting errors in a
program before its execution. Among these methods is static typing,
which, in its most widespread form, consists in adding type
annotations in a program (such as the usual types used in mathematics
such as integers, reals, and booleans), and verifying that these types
are used in a coherent manner.
However, the primary programming language used in Web development,
JavaScript, is a dynamically typed language. While this allows for
more flexibility and faster development, it also makes errors harder
to detect.
Gradual typing reconciles static and dynamic typing by allowing the
programmer to obtain the strong guarantees offered by static typing
for certain parts of a program while keeping the flexibility of
dynamic typing for other parts. Formally, this is done by adding a new
type annotation, often called dynamic, which acts as a fully
dynamic type. That is, values of this type will pass any static type
check, and their type will only be checked at runtime. What is
important is that preexisting dynamically typed code is still valid,
but can easily be upgraded with more type annotations. This is why
gradual typing has been attracting more and more interest and has been
adopted by some of the major partakers in the development of
information technology and computer science, as shown by the
development of the languages Dart by Google, TypeScript by Microsoft
and Flow by Facebook.
Regarding static typing, one of the tools that proved to be among
the most suited to Web development is the use of union and
intersection types, also known as set-theoretic
types [3,4]. The aim of set-theoretic types is to
integrate the mathematical definitions, principles, and operations of
set-theory (such as the union, the intersection, or the complement of
sets) in a type system. This allows for a much more precise control
over types, thus providing stronger static guarantees than with simple
types.
Goals
We propose three different internships on gradual-typing for
polymorphic languages, that will build upon the work we already
developed on gradual typing with set-theoretic types [6,7]:
Occurrence typing: occurrence typing is a technique
developed for Typed-Racket to use flow information for typing highly
dynamic code [2]. The idea is that when some dynamic type test is
performed on a variable, then we can refine our type inference
according to whether the test has succeeded or not. For instance, if
in an if-expression we test whether a variable x has type
integer, then we know that in the then branch x will have
type integer (intersection with its static type) and that in the else branch
it will have its static type minus the type integer. The
goal of this internship is to formalize occurrence typing in the
context of semantic subtyping so as to extract the maximum amount of
information from the flow of a program.
Code analysis for inferring intersection types:
intersection types are a key feature for a feasible typing of
dynamic languages, where the same function can be used in contexts so
different that they cannot be captured by common polymorphic type
systems. The idea is that in each context the function is used with
some given type, that, thus, the function has all these types, and, therefore, it also has the
intersection of all these types. While it is relatively easy to
check whether a function has an intersection type specified by the
programmer via an annotation, as it can be done in Flow, it is very hard
(actually, undecidable) to infer an intersection type for code
partially annotated or not annotated at all. The goal of this stage is to use the results of a
static analysis (and, time permitting, profiling information) to
drive the inference of intersection types for functions defined in dynamic
languages.
Abstract machines for cast calculi: in order to provide strong
safety guarantees, gradually-typed languages can be compiled into
intermediate versions which contain explicit type casts that
dynamically check the correctness of gradually-typed portions of a
program. The implementation of such intermediate representations is
the subject of active research and of a heated debate [5], but there
does not exist any work on the compilation of cast when these are
on set-theoretic types. The goal of the internship is to study the
current literature on the implementation of cast calculi, use it
to define an abstract machine for cast calculi with set-theoretic
types, and --time permitting-- implement it.
References
[1] Jeremy Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop (September
2006), pp. 81–92
[3] Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Pietro Abate: Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction. POPL 2015: ACM SIGPLAN Symposium on Principles of Programming Languages.
[4] Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, Luca Padovani: Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. POPL 2014: ACM SIGPLAN Symposium on Principles of Programming Languages.
[5] Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, Matthias Felleisen. Is Sound Gradual Typing Dead? POPL 16: ACM SIGPLAN Symposium on Principles of Programming Languages.
[6] Giuseppe Castagna and Victor Lanvin. Gradual typing with union and intersection types. In International Conference on Functional
Programming, 2017.
[7] Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy Siek. Gradual typing: A new perspective (subtyping and let-polymorphism). POPL 19: ACM SIGPLAN Symposium on Principles of Programming Languages, To appear