Sites Inria

Version française

Séminaires des équipes de recherche

Towards a syntactic type system for recursive modules

Séminaire Gallium - Moscova

  • Date : 25/02/2013
  • Place : Inria - Rocquencourt - Amphithéâtre Alan Turing
  • Guest(s) : Hyeonseung Im - LRI
  • Organiser(s) : Gallium

A type system for ML-style recursive modules should address at least two technical challenges. First, it needs to solve the double vision problem, which refers to an inconsistency between external and internal views of recursive modules. Second, and more importantly, it needs to handle cyclic type definitions caused by recursion between modules to typecheck common patterns of recursive modules including functor fixpoints.
In this talk, I will first present a syntactic type system for recursive modules without type parameters that solves the double vision problem and accounts for cyclic type definitions. Then, I will discuss how to extend our type system with type parameters in a rather simplified setting, but still allowing us to define abstract types and arbitrary recursive type definitions with type parameters. In particular, I will discuss unsound interaction between non-contractive recursive types and abstract types, and present a new
semantic notion of contractiveness for types and signatures.  Our type system with semantic contractiveness is sound with respect to the standard call-by-value operational semantics, which eliminates signature sealings. Another notable result is that while non-contractive types in signatures lead to unsoundness of the type system, they may be allowed in modules. I hopefully expect that we can extend our results to a full-fledged module system à la OCaml.

Keywords: Paris - Rocquencourt Séminaire Moscova Gallium