Master project description
TITLE: Gradual Typing for dynamic languages
Part of this project is proposed in collaboration with Facebook Language Research .

Context

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]:
  1. 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.

  2. 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.

  3. 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
  • [2] Occurrence typing , The Typed Racket Guide
  • [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