- 著者
- Benjamin C. Pierce
- タイトル
- Programming with Intersection Types and Bounded Polymorphism
- 日時
- December 1991
- 概要
- Intersection types and bounded quantification are complementary mechanisms for extending the expressive power of statically typed programming languages. They begin with a common framework: a simple, typed language with high-order functions and a notion of subtyping. Intersection types extend this framework by giving every pair of types o and T a greatest lower bound, o/\T, corresponding intuitively to the intersection of the sets of values described by o and T. Bounded quantification extends the basic framework along a different axis by adding polymorphic functions that operate uniformly on all the subtypes of a given type. 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; for example, the addition function is given a type showing that it maps pairs of positive inputs to a positive result, pairs of zero inputs to a zero result, etc. More familiar programming examples are presented in terms of an extension of Forsythe (an Algol-like language with intersection types), 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; in fact, even the subtype relation of pure secondorder bounded quantification is undecidable, a surprising result in its own right. 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 propose, for future study, some simpler fragments of F/\ that share most of its essential features, while recovering decidability and least upper bounds. 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 "o is a subtype of T" is read as " O is a subset of T." More refined models can be obtained using a translation from F/\ into the pure polymorphic λ-calculus; in these models, "o is a subtype of T" is interpreted by an explicit coercion function from o to T. 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.
- カテゴリ
- CMUTR

Category: CMUTR Institution: Department of Computer Science, Carnegie Mellon University Abstract: Intersection types and bounded quantification are complementary mechanisms for extending the expressive power of statically typed programming languages. They begin with a common framework: a simple, typed language with high-order functions and a notion of subtyping. Intersection types extend this framework by giving every pair of types o and T a greatest lower bound, o/\T, corresponding intuitively to the intersection of the sets of values described by o and T. Bounded quantification extends the basic framework along a different axis by adding polymorphic functions that operate uniformly on all the subtypes of a given type. 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; for example, the addition function is given a type showing that it maps pairs of positive inputs to a positive result, pairs of zero inputs to a zero result, etc. More familiar programming examples are presented in terms of an extension of Forsythe (an Algol-like language with intersection types), 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; in fact, even the subtype relation of pure secondorder bounded quantification is undecidable, a surprising result in its own right. 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 propose, for future study, some simpler fragments of F/\ that share most of its essential features, while recovering decidability and least upper bounds. 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 "o is a subtype of T" is read as " O is a subset of T." More refined models can be obtained using a translation from F/\ into the pure polymorphic λ-calculus; in these models, "o is a subtype of T" is interpreted by an explicit coercion function from o to T. 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. Number: CMU-CS-91-205 Bibtype: TechReport Month: dec Author: Benjamin C. Pierce Title: Programming with Intersection Types and Bounded Polymorphism Year: 1991 Address: Pittsburgh, PA Super: @CMUTR