Florent Ferrari

First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination

We study a first-class treatment of constrained types, which were previously confined mostly to ML-style polymorphism. We define System FCCT, an extension of System F with polymorphic subtyping and constraint abstraction in types. A value of type c ⇒ τ can be used at type τ in an...