GADT

GADTs

Ambivalent types for Principal Type Inference with GADTs

This project is joint work with Jacques Garrigue.

This work formalizes type inference for GADTs as done in OCaml. The novelty is the introduction of ambivalent types to retain the use of equations and type conversions within the type structure. It enables a more precise definition of type ambiguities and so rule out situations that are not actually ambiguous.

GADTs, short for Generalized Algebraic DataTypes, extend usual algebraic datatypes with a form of dependent typing that has many useful applications. However, pattern matching on GADTsintroduces type equalities with limited scopes, which are a source of ambiguities that may destroy principal types---and must be resolved by type annotations. We introduce ambivalent types to tighten the definition of ambiguities and better confine them. This enables type inference with principal types and requires fewer type annotations.

See the authors PDF of the conference absract presented in in 11th Asian Symposium on Programming Languages and Systems, Melbourne, December 2013. Springer-Verlag LNCS 8301, pages 257-272, the slides of the presentation and the extended version.

See also the talk given at the IFIP-WG2.8 2013 meeting and the extended abstract of the talk given at the ML workshop.

GADTs meet subtyping

This project is joint work with Gabriel Scherer.

This work explores the interaction of GADT with subtyping and, in particular the safety of variance annotaions on GADT in the presence of subtyping, e.g. as can be found in the OCaml language.

See the extended abstract of the talk given at the ML workshop. (You may also see also the slides and video of the talk.) ).

There is also a short paper without proofs and a research report including more details and all proofs, also availble on HAL.