My PhD thesis manuscript is sent for review and I finally have some time to write a blog post about it! It presents a framework of coercions to describe and unify existing type systems. In particular, all erasable type system features (such as coherent polymorphism) are expressed as coercions, which can be seen as a subtyping relation between erasable typings.

The untyped lambda-calculus with constants (pairs, integers, etc.) is the simplest functional programming language and is the underlying language of different type systems such as Coq, Haskell, and OCaml for example. Each of these type systems has its own proof of soundness, and of strong normalization (in the absence of recursion). But since they share the lambda-calculus as their core language, it is interesting to study the possibility for the lambda-calculus to have a type system that would ensure the soundness and strong normalization of these other, more exciting type systems.

The soundness and normalization for strong reduction imply the soundness and normalization for all usual strategies. As a consequence, studying soundness and normalization in a strong reduction setting is enough. Studying only the pure lambda-calculus (without side effects) still gives a result for languages with side effects when the type system keeps track of side effects with a monadic encoding, as it is the case in Haskell.

To define such a general type system for the lambda-calculus with strong reduction, we generalize existing ideas: several type systems use subtyping, containments, or coercions to express some of their features. For instance, System F-sub uses subtyping to retype a term or to constrain type abstraction. GHC uses equality coercions to implement GADTs and type families from its surface type system to its kernel type system.

In this document, we introduce a framework for defining and studying type systems based on typing coercions. We define typing coercions (which we simply call coercions) as composable and erasable typing transformations. We instantiate the framework on two type systems where all features are expressed as coercions on top of the simply-typed lambda-calculus (STLC). In particular, we make a distinction between computational types (related to computation and usually called simple types) and erasable types (related to typing). Computational types are introduced and eliminated in the term typing judgment, while erasable types are introduced and eliminated in the coercion judgment and are thus seen as inclusions between typings. Congruence rules for erasable types are derivable from their introduction and elimination rules. However, congruence for computational types have to be explicitly added to the coercion judgment. Finally, we particularly study the fundamental feature of coercion abstraction, which can be seen as a form of polymorphism (bounded or coherent).

We define a type system, System Lc, that can be seen as kernel type systems. It subsumes the STLC, System F, System F-eta, MLF, System F-sub (in its most general version), System F-rec (with equi-recursive types and coinduction rules), Constraint ML. As such, the soundness and normalization of System Lc simultaneously prove the soundness and normalization of the subsumed type systems. The type systems it subsumes can be seen as associated surface type systems. For instance, type systems with inference such as MLF or Constraint ML are surface type systems for System Lc.

A side contribution is the study of step-indexed techniques in a strong reduction setting. The proof of soundness of System Lc is formalized in Coq and documented with coqdoc.