[Prev][Next][Index][Thread]
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
CMU-CS-91-205
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
bounds.
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.
------------------------------------------------------------------------
PUBLIC FTP ARCHIVES -- INSTRUCTIONS
-----------------------------------
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
anywhere.
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
1990).
merge A Record Calculus Based on Symmetric Concatenation,
Harper and Pierce, CMU-CS-90-157 (slightly revised
version).
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 128.2.222.187]
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.
Enjoy,
Benjamin Pierce