Exploring First-Class Constrained Types
Semantics, Principal 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 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. We extend FCCTI to track abstracted call contexts, ensuring termination on all input terms. This modified algorithm, called FCCTI+, could form the basis of a new approach to higher-order context-sensitive static analysis. We show the soundness of FCCTI+ by proving that its approximation corresponds to simulating all possible reductions in nondeterministic terms. Finally, we expect that most of our results translate smoothly to the call-by-value setting. While existing intersection type systems are already known to characterize various normalization properties, including CBN termination, FCCT is the first that does so through polymorphic subtyping and constrained types, establishing a connection between term reduction and traditional subtype constraint solving.
