Programming with intersection types and bounded polymorphism

authors: B Pierce
year: 1992
url: https://www.cis.upenn.edu/ bcpierce/papers/thesis.pdf
publisher:
abstract: This thesis unifies and extends prior work on intersection types and bounded quantification, previously studied only in isolation, by investigating theoretical and practical aspects of a typed λ-calculus incorporating both. The practical utility of this calculus, called F_∧, is established by examples showing, for instance, that it allows a rich form of “coherent overloading” and supports an analog of abstract interpretation during typechecking. More familiar programming examples are presented in terms of an extension of Forsythe, demonstrating how parametric polymorphism can be used to simplify and generalize Forsythe's design. We discuss the novel programming and debugging styles that arise in F_∧. We prove the correctness of a simple semi-decision procedure for the subtype relation and the partial correctness of an algorithm for synthesizing minimal types of F_∧ terms. Our main tool in this analysis is a notion of “canonical types,” which allow proofs to be factored so that intersections are handled separately from the other type constructors. A pair of negative results illustrates some subtle complexities of F_∧. First, the subtype relation of F_∧ is shown to be undecidable. Second, the failure of an important technical property of the subtype relation–the existence of least upper bounds–indicates that typed semantic models of F_∧ will be more difficult to construct and analyze than the known typed models of intersection types. We study the semantics of F_∧ from several points of view. An untyped model based on partial equivalence relations demonstrates the consistency of the typing rules and provides a simple interpretation for programs, where “σ is a subtype of τ” is read as “σ is a subset of τ.” More refined models can be obtained using a translation from F_∧ into the pure polymorphic λ-calculus; in these models, “σ is a subtype of τ” is interpreted by an explicit coercion function from σ to τ. The nonexistence of least upper bounds shows up here in the failure of known techniques for proving the coherence of the translation semantics. Finally, an equational theory of equivalences between F_∧ terms is presented and its soundness for both styles of model is verified. (Abstract shortened with permission of author.)