[Prev][Next][Index][Thread]

Thesis Announcement: Type Inference with Bounded Quantification


I am pleased to announce the availability of my (slightly misleadingly
titled) PhD thesis:

              "Type Inference with Bounded Quantification"
                              (1998)
[Abstract below]

The thesis is available electronically from the LFCS on-line
repository of technical reports:

     <http://www.dcs.ed.ac.uk/lfcsreps/>
     
Paper copies can be ordered from: 

Kendal Reid <reports@dcs.ed.ac.uk>,
Laboratory for Foundations of Computer Science (LFCS),
The University of Edinburgh,
JCMB, The Kings Buildings,
Mayfield Road,
Edinburgh EH9 3JZ,
UK.

---------------------------- Abstract --------------------------

In this thesis we study some of the problems which occur when type
inference is used in a type system with subtyping. An underlying poset of
atomic types is used as a basis for our subtyping systems. We argue that
the class of Helly posets is of significant interest, as it includes
lattices and trees, and is closed under type formation not only with
structural constructors such as function space and list, but also any of
records, tagged variants, Abadi-Cardelli object constructors, top, and
bottom. We develop a general theory relating consistency, solvability, and
solution of sets of constraints between regular types built over Helly
posets with these constructors, and introduce semantic notions of
simplification and entailment for sets of constraints over Helly posets of
base types. We extend Helly posets with inequalities of the form a <= tau,
where tau is not necessarily atomic, and show how this enables us to deal
with bounded quantification. 

Using bounded quantification we define a subtyping system which combines
structural subtype polymorphism and predicative parametric polymorphism,
and use this to extend with subtyping the type system of Laufer and
Odersky for ML with type annotations. We define a complete algorithm which
infers minimal types for our extension, using factorisations, solutions of
subtyping problems analogous to principal unifiers for unification
problems. We give some examples of typings computed by a prototype
implementation.