We present a new, syntax-directed framework for Curry-style type systems with subtyping. It supports a rich set of features, and allows for a reasonably simple theory and implementation. The system we consider has sum and product types, universal and existential quantifiers, and inductive and coinductive types. The latter two may carry size invariants that can be used to establish the termination of recursive programs. For example, the termination of quicksort can be derived by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed polymorphism and (co-)induction. One of the key ideas is to separate the notion of size from recursion. We do not check the termination of programs directly, but rather show that their (circular) typing proofs are well-founded. Termination is then obtained using a standard (semantic) normalisation proof. To demonstrate the practicality of the system, we provide an implementation accepting all the examples discussed in the article.

We prove that system ST (introduced in a previous work) enjoys subject reduction and is complete for realizability semantics. As far as the author knows, this is the only type system enjoying the second property. System ST is a very expressive type system, whose principle is to use two kinds of formulae: types (formulae with algorithmic content) and propositions (formulae without algorithmic content). The fact that subtyping is used to build propositions and that propositions can be used in types through a special implication gives its great expressive power to the system: all the operators you can imagine are definable (union, intersection, singleton, ...).