The defense took take place on December 11th, 13h30 at Inria Paris, in the Lions ampthitéâtre (48 rue Barrault, 75013 PARIS). The slides are available here
The most up-to-date pdf version is available here.
MLmodules come as an additional layer on top of a core language to offer large-scale notions of abstraction and composition. They contributed to the success of OCamland SML. While modules are easy to write for common cases, their advanced use may become tricky, as it is easy to run into edge cases and irregularities. Additionally, despite a long line of works, their meta-theory remains difficult to comprehend, with involved soundness proofs. In this thesis we propose a consolidation for the design of the type system of MLmodules.
To this aim, we developed two type systems for an OCaml-like language, including both applicative and generative functors, extended with transparent ascription signatures. The first type system is called Mωand is built on a prolific line of works that approached MLmodules by translation to Fω, the higher-order polymorphic lambda calculus. Mωproduces signatures in an OCaml-like syntax extended with Fωquantifiers. It treats abstraction and scopes via the introduction of well-placed quantifiers. We provide a reverse translation from Mωsignatures to path-based source signatures along with a characterization of signature avoidance cases. The soundness of the type system is shown by elaboration in Fω. We improve over previous encodings of sealing within applicative functors, by the introduction of transparent existential types, a weaker form of existential types that can be lifted out of universal and arrow types. This shines a new light on the form of abstraction provided by applicative functors and brings their treatment much closer to those of generative functors.
The second type system is called ZipMLand is built on the path-based, fully-syntactic line of works. Unlike previous approaches, ZipMLavoids the signature avoidance problem by introducing floating fields, which act as additional fields of a signature, invisible to the user but still accessible to the typechecker. In practice, they are handled as zippers on module signatures, and can be seen as a lightweight extension on existing signatures. Floating fields allow to delay the resolution of signature avoidance as long as possible or desired. Since they do not exist at runtime, they can be simplified along type equivalence, and dropped once they became unreachable. We give a simple equivalence criterion for the simplification of floating fields without loss of type-sharing. We present a principled strategy that implements this criterion and performs much better than OCaml. Remaining floating fields, instead of polluting the code, partially disappear at functor applications and fully disappear at signature ascription, including toplevel interfaces. Residual unavoidable floating fields can be shown to the user as a last resort, either to be explicitly resolved by the user, or kept until link time. The correctness of the type system is proved by elaboration into Mω, which has itself been proved sound by translation to Fω. The language includes module type definitions that are returned in inferred types and kept as long as possible. ZipMLhas been designed to be a specification of an improvement over OCamlwith transparent ascription, a better solution to signature avoidance, while staying close to the source language and to its implementation.