Programming with Intersection Types and Bounded Quantification

Date: Fri, 20 Dec 91 16:14:29 EST

My PhD thesis, "Programming with Intersection Types and Bounded
Quantification," is finished and ready to distribute.  Electronic
copies are available now and can be obtained by FTP from Internet
hosts.  Paper copies are being printed and will be available sometime
in January.  If you'd like one, please send me a note with your
mailing address.

A brief summary and FTP instructions follow.

Happy holidays to all!

	Benjamin Pierce

		 Programming with Intersection Types
		       and Bounded Polymorphism

			  Benjamin C. Pierce

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 higher-order functions and a notion of subtyping.
Intersection types extend this framework by giving every pair of types
S and T a greatest lower bound, S/\T, corresponding intuitively to the
intersection of the sets of values described by S 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 by investigating
theoretical and practical aspects of a typed lambda-calculus
incorporating both.

The practical utility of this calculus, called F-meet, 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-meet.

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-meet 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-meet.  First, the subtype relation of F-meet is shown to be
undecidable; in fact, even the subtype relation of pure second-order
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-meet will be more difficult than the
known typed models of intersection types.  We propose, for future
study, some simpler fragments of F-meet that share most of its
essential features, while recovering decidability and least upper

We study the semantics of F-meet 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 ``S is a subtype of T'' is read as ``S is a subset
of T.''  More refined models can be obtained using a translation from
F-meet into the pure polymorphic lambda-calculus; in these models, ``S
is a subtype of T'' is interpreted by an explicit coercion function
>from S 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-meet terms is presented and its soundness for both styles of
model is verified.



The directory /usr/bcp/pub on internet host proof.ergo.cs.cmu.edu
contains ftp-able postscript and dvi files (and, where appropriate,
errata sheets) for the following papers:

     File name prefix	Paper
     ----------------   -----

     thesis		Programming with Intersection Types and Bounded 
			Polymorphism, Pierce, CMU-CS-91-205.  

			This version (identical to the printed thesis) is 
			set in the Palatino font, which is not available on all 
			Postscript printers.  Apple Laserwriters have it;
			DEC printers don't.  If you have trouble printing
			it, try the files with prefix "thesiscmr" instead.  
			These are set in computer modern and should work

     fsub		Bounded Quantification is Undecidable, Pierce, 
			CMU-CS-91-161.  (Superseded by Chapter 6 
			of CMU-CS-91-205.)

     fsubpopl		Bounded Quantification is Undecidable, Pierce, 
			POPL 92.

     leap		Programming in Higher-Order Typed Lambda-Calculi, 
			Pierce, Dietzen, and Michaylov, CMU-CS-89-111.

     ui                 Preliminary Investigation of a Calculus with Intersection 
		        and Union Types, Pierce (unpublished manuscript, June

     merge		A Record Calculus Based on Symmetric Concatenation, 
			Harper and Pierce, CMU-CS-90-157 (slightly revised

     uipq		Programming With Intersection Types, Union Types, 
			and Polymorphism, Pierce, CMU-CS-91-106.

     bctcs		Basic Category Theory for Computer Scientists 
			Pierce, MIT Press.  (errata only)

     bvars		A Decision Procedure for the Subtype Relation 
			on Intersection Types with Bounded Variables,
			Pierce, CMU-CS-89-169.

The file suffix conventions are as follows:

	*.dvi.Z			compressed dvi
	*.ps.Z			compressed postscript
	*.ps.Z.uuencoded	uuencoded and compressed postscript
	*.errata		errata (plain text format)

To retrieve files, proceed as follows.  (Remember to set the
connection type to binary; otherwise compressed files will come out as
garbage on the other end!)

    ftp proof.ergo.cs.cmu.edu      [or]
    login: anonymous
    password: <your mail address>
    binary			   <-- don't forget this
    cd /usr/bcp/pub
    get <name>.dvi.Z               [or <name>.ps.Z, etc.]

Uuencoded files can be decoded with the unix "uudecode" utility.
Compressed files (those with .Z extension) can be uncompressed with
the unix "uncompress" utility.


	Benjamin Pierce