Sites Inria

Version française

Gallium Seminar

Gallium Seminar - Gradual Typing : A New Perspective

  • Date : 18/02/2019
  • Place : Salle JLL1, bât C
  • Guest(s) : Victor Lanvin
  • Organiser(s) : Project team Gallium

Gradual Typing: A New Perspective

Victor Lanvin, IRIF

Gradual typing is a recent approach that aims at embedding both static typing and dynamic typing inside the same language. This allows the programmer to get the best of both worlds, by finely tuning the distribution of dynamic and static type checking over a program.  However, this "gradualization" is sometimes too coarse, and an expression is often either fully dynamic or fully static. We argue that we can solve this issue by combining gradual typing with union and intersection types, and further extend this framework to a
polymorphic setting.
Unfortunately, this kind of type discipline is out of reach of current gradual type systems. Gradual type systems are often defined using syntactic notions on types, which make them difficult to extend with more semantic notions such as union and intersection types. To solve this problem, we explore a new, more semantic way to interpret gradual types, and use this new approach to define three gradual types systems: (i) Hindley-Milner, (ii) with subtyping, and (iii) with set-theoretic types. These new systems are defined both declaratively -- by simply adding two subsumption rules -- and algorithmically -- by reusing existing techniques on non-gradual types.