First-Class Constrained Types
Elaboration, Type Inference, Approximation, and a Characterization of Termination
Abstract
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 => tau can be used at type tau in any context where the subtyping constraint c can be discharged. We show that FCCT exhibits interesting properties. First, all well-typed FCCT terms terminate under call-by-name evaluation (CBN), which can be shown by elaboration into System F. Second, all CBN-terminating terms are well-typed in FCCT. Together, these two properties mean that typability in System FCCT characterizes call-by-name termination. Third, FCCT admits a principal type inference semi-algorithm, called FCCTI, which makes no approximations and can thus be seen as an idealized “ground truth” of type inference. We show that FCCTI indirectly simulates term reduction, shedding some light on the difficulty of bounded polymorphic type inference. Finally, we extend FCCTI to track abstracted call contexts and perform approximation by sharing polymorphic instantiations, ensuring termination on all input terms while preserving soundness. In addition to making the connection between polymorphic subtype constraint solving and term reduction, this paper also establishes a connection between constrained types and existing intersection type systems, which are known to characterize various normalization properties.
