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