Polymorphic Type Inference for Languages with
Overloading and Subtyping
Geoffrey Seward Smith
Fh.D Thesis
91-1230
August 1991
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
POLYMORPHIC TYPE INFERENCE
FOR LANGUAGES WITll OVERLOADING AND
SUBTYPING
A Dissertation
Presented to the Faculty of the Graduate School
of Cornell University
in Partial Fulfillment of the Requirements for the Degree of
Doctor of Philosophy
by
Geoffrey Seward Smith
August 1991
Oc Geoffrey Seward Smith 1991
ALL RIGHTS RESERVED
POLYMORPHIC TYPE INFERENCE
FOR LANGUAGES WITH OVERLOADING AND SUBTYPING
Geoffrey Seward Smith, Ph.D.
Cornell University 1991
Many computer programs have the property that they work correctly on a
variety 0 types of input; such programs are called polymorphic. Polymorphic
type systems support polymorphism by allowing programs to be given multiple
types. In this way, programs are permitted greater flexibility of use, while still
receiving the benefits of strong typing.
One especially successful polymorphic type system is the system of Hindley,
Milner, and Damas, which is used in the programming language ML. This type
system allows programs to be given universally quantified types as a means of
expressing polymorphism. It has two especially nice properties. First, every
well-typed program has a "best" type, called the principal type, that captures
all the possible types of the program. Second, principal types can be inferred,
allowing programs to be written without type declarations. However, two useful
kinds of polymorphism cannot be expressed in this type system: overloading and
subtyping. Overloading is the kind of polymorphism exhibited by a function like
addition, whose types cannot be captured by a single universally quantified type
formula. Subtyping is the property that one type is contained in another, as, for
example int C real.
This dissertation extends the Hindley/Milner/Damas type system to incorpo-
rate overloading and subtyping. The key device needed is constrained universal
quantification, in which quantified variables are allowed only those instantiations
that satisfy a set of constraints. We present an inference algorithm and prove
that it is sound and complete; hence it infers principal types.
An issue that arises with constrained quantification is the satisfiabitity of
constraint sets. We prove that it is undecidable whether a given constraint set is
satisfiable; this difficulty leads us to impose restrictions on overloading.
An interesting feature of type inference with subtyping is the necessity of sim-
plifying the inferred types the unsimplified types are unintelligible. The sim-
plification process involves shape unification, graph algorithms such as strongly
connected components and transitive reduction, and simplifications ba??d on the
monotonicities of type formulas.
Biographical Sketch
Geoffrey Seward Smith was born on December 30, 1960 in Carmel, California.
His childhood was spent in Bethesda, Maryland. In 1982, he graduated, summa
cnm taude, from Brandeis University with the degree of Bachelor of Arts in Math-
ematics and Computer Science. In 1986, he received a Master of Science degree
in Computer Science from Cornell University. He was married to Maria Elena
Gonzalez in 1982, and in 1988 he and his wife were blessed with a son, Daniel.
iii
To Elena and Daniel
lv
Acknowledgements
My advisor, David Gries, has been a patient, encouraging teacher. His high
standards and devotion to the field have been an inspiration to me. His warmth
and humanity have made it a pleasure to work with him.
Thanks also to my other committee members, Dexter Kozen and Stephen
Chase. I have always marveled at Dexter's depth and breadth of knowledge; he
has taught me a great deal throughout my years at Cornell.
Cornell has been a wonderful place to learn and grow; I am indebted to many
people here who have taught and inspired me. Dennis Volpano discussed much
of the material in this dissertation with me, and his comments and suggestions
helped to shape this work. Bard Bloom gave me valuable insight into the shape
unification problem. Discussions with Hal Perkins, Earlin Lutz, Steve Jackson,
Naixao Zhang, and the other members of the Polya project have added greatly
to my understanding of programming languages and type systems.
I have had a very nice group of officemates during my time at Cornell. For
friendship, advice, and encouragement, I thank Amy Briggs, Jim Kadin, Daniela
Rus, and Judith Underwood.
Finally, I thank Elena and Daniel for their love and support across the years.
v
Table of Contents
2
3
Introduction
1.1 Types
1.2 Reductionist Type Correctness . . . .
1.3 Polymorphism
1.4			Axiomatic Type Correctuess			. .			. .
1.5 The Hindley/Milner/Damas Type System
1.6 Extensions to Hindley/Milner/Damas Polymorphism.
Overloading
2.1			The Type System . . . . . 			. 			.			. .			. .
2.1.1			Types and Type Schemes
2.1.2			Substitution and o -equivalence			.			. .
2.1.3			The Typing Rules
2.1.4			The Instance Relation and Principal			Types . .
2.2			Properties of the Type System
2.3			Algorithm Wo. 						. .			. .
2.4			Properties of W0 . . . . . .
2.4.1			Soundness of W0 . . 						. .			. .			. .
2.4.2			Completeness of W0 . . 			.
2.5			Limitative Results. .			. .			. .
2.5.1			A Logical Digression
2.6			Restricted Forms of Overloading						. .			. .
2.7			Conclusion
Subtyping
3.1 The Type System
3.1.1 Types and Type Schemes
3.1.2 Substitution and a -equivalence
3.1.3 The Typing Rules
3.1.4 The Instance Relation
3.2 Properties of the Type System
3.3 Algorithm W08 . . .
vi
2
3
6
8
10
13
13
14
14
17
22
24
30
35
35
38
52
57
57
60
61
61
62
62
62
64
65
69
3.4
3.5
3.6
3.7
3.8
Properties of W08
3.4.1			Soundness of W08 . . .			. . .
3.4.2			Completeness of W08
An			Example Assumption Set			.
Type Simplification
3.6.1 An Overview of Type Simplification
3.6.2 Transformation to Atomic Inclusions
3.6.3 Collapsing Strongly Connected Components
3.6.4 Monotonicity-based Instantiations
3.6.5			Function close . .			. . .			.
Satisfiability Checking . .
Conclusion			. . . .			. . .			. .
Conclusion
4.1 A Practical Look at Type Inference
4.2			Related Work . .
4.3			Future Directions . . .			. . . .
4.3.1			Satisfiability of Constraint			Sets
4.3.2			Records . . . . .			.			.
4.3.3			Semantic Issues .			.			.
4.3.4			Imperative Languages			.			.
4
A Omitted Proofs
Bibliography
vii
69
69
71
84
86
86
91
94
96
100
102
105
106
106
109
110
110
111
111
111
112
120
List of Figures
2.1
2.2
2.3
2.4
3.1
3.2
3.3
3.4
3.5
3.6
3.7
3.8
3.9
3.10
4.1
4.2
4.3
4.4
Typing Rules with Overloading
Algorithm W0
Function close			. .
Example lexicographic
Additional Rules for Subtyping 			. .			. .
Algorithm Wos 			.
Assumption Set A0. .			.
Atomic Inclusions for lexicographic
Collapsed Components of lexicographic			.			. . .
ResultofShrinking c, v, A, ?, ?, ?,and 0
Function shape-unifier . .			. .			. . .			. .
Function atomic-inclusions
Function component-collapser			.			. . .
Function close . . . . .			.
Example fast-expon
Example mergesort
Example reduce-right			.
Example another-reduce-right
viii
18
31
33
34
63
70
85
88
89
90
92
93
95
101
107
108
109
109
Chapter 1
Introduction
Over the years, the notion of types in programming languages has grown steadily
in importance and depth. In recent years, the study of types has been enriched
by the introduction of ideas from mathematical logic. Yet, many basic questions
about types remaan unresolved there is still no consensus about what exactly
types are, or about what it means for a computer program to be type correct.
What follows in this chapter, then, is an attempt to outline what is most impor-
tant about types and type systems.
1.1 Types
It seems fundamental to human intelligence to class?fy the objects of the world
based on their observed similarities and differences. This process of classifica-
tion is a basic way of dealing with the complexity of the world: by grouping
together similar objects, we may abstract away from particular objects and study
properties of the group as a whole.
In the realm of mathematics, the process of grouping together similar objects
has led to the identification of a rich diversity of mathematical structures, for
example Euclidean spaces, topological spaces, and categories. The study of a
mathematical structure leads to the development of a theory of the structure;
the theory describes the common properties of the members of the structure and
facilitates reasoning about the structure. Reasoning about a structure is further
facilitated by the establishment of specialized notation tailored to the structure.
Many mathematical structures are also useful computational structures; for
example graphs, sets, and sequences are especially useful in programming. In
computer science, we call such structures types.
A type, then, is a set of elements and operations having an associated theory
that allows reasoning about manipulations of elements of the type.
The programming process is much easier in a language with a rich collection of
types; this is perhaps the most important feature of high-level languages. Hence
2
a major consideration in the design of any such language is how types will be
supported. Type support may be divided into two relatively independent aspects:
first, to ensure that high-level types are correctly implemented in terms of the
low-level data structures available on an actual machine, and second, to ensure
that programs use types only in ways that are sensible. The first of these we call
reductionist type correctness, the second we call axiomatic type correctness. We
explore these in more detail in the next three sections.
1.2 Reductionist Type Correctness
Since actual machines have but a few types (for example, integers of various
sizes, floating-point numbers, arrays, and pointers), a major task of a compiler
is to implement the types of a high-level language in terms of low-level data
structures. The implementation of types is complicated by the fact that many
types (for example, sets) have no best implementation that is appropriate for all
situations. Instead, different implementations should be used depending on the
kind and frequency of the operations to be performed.
As a rule, programming languages have not attempted to use multiple im-
plementations for built-in types 1; instead, the usual approach is to provide a
language facility that allows the programmer to define a new type and to give
its representation in terms of other types. The key issue is how to protect the
representation from misuse.
Suppose that we wish to implement a type dictionary with operations insert
and member?. We might chose to represent the dictionary as a bit-vector. But
this should not mean that type dictionary is the same as type bit-vector! For,
outside the procedures insert and member?, there should be no access to the
underlying representation. Furthermore, just because a value has type bit-vector
we cannot conclude that the value represents a dictionary. The two concerns are
called "secrecy" and "authentication" by Morris [Mor73], and they lead him to
declare that "types are not sets". This appears to contradict our definition of
type above, but this is really not the case. Morris is discussing what is needed
for one type to represent another; he is not discussing the nature of types.
In general, it can be argued that a failure to distinguish between reductionist
and axiomatic type correctness has led to a great deal of confusion about the
nature of types.
Cardelli and Wegner follow in the reductionist style when they state,
A type may be viewed as a set of clothes (or a suit of armor) that
protects an underlying untyped representation from arbitrary or un-
intended use. [CW85, p. 474]
1 SE?TL is an exception.
3
Similarly, in the language Russell [DD85], the notion of strong typing is defined so
that the meaning of a well-typed program is independent of the representations of
the types it uses. In a similar way, Mitchell and Plotkin [MP88J suggest that an
abstract type that is represented by another type should be given an existentially
quantified type as a way of hiding the representation.
Aho, Hopcroft, and Ullman [AHU83] assert that two types should be regarded
as different if the set of operations they support is different, because the set of
operations to be supported is crucial in determining the best implementation
of a type. From the point of view of the programmer, however, this view of
types seems inappropriate: it is a case of reductionist concerns contaminating
the axiomatic view of types. A better way of understanding the situation is in
terms of partial implementations of the same type [GP85,Pri87,GV89].
In the rest of this dissertation, we will not consider reductionist type cor-
rectness further. Instead we will think of types as existing axiomatically, and
we will not worry about how they are represented. Henceforth, then, we will
focus on axiomatic type correctness. Before we do so, we consider the notion of
polymorphism.
1.3 Polymorphism
In mathematics, the study of a proof of a theorem may reveal that the theorem
can be generalized. For example, in analyzing a proof of a theorem about the
natural numbers, we might realize that the only property of the natural numbers
needed is that they form a well-ordered set. This realization would enable us
to generalize our theorem to any well-ordered set. Lakatos gives a fascinating
account of the role of proof analysis in mathematical discovery in [Lak76].
To exploit this useful principle of generalization, we rewrite our theorems
so that they refer to abstract mathematical structures (e.g. well-ordered sets,
topological spaces) that have certain properties but whose identity is not fixed.
Poincare' describes the process thus:
... mathematics is the art of giving the same name to different things
... When the language is well-chosen, we are astonished to learn that
all the proofs made for a certain object apply immediately to many
new objects; there is nothing to change, not even the words, since the
names have become the same. [Poil3, p. 375]
Indeed, a great trend in twentieth-century mathematics has been the rise of
abstract mathematical structures; rather than studying the properties of par-
ticular mathematical structures (for example Euclidean space), mathematicians
today are more likely to study properties of abstract mathematical structures (for
example metric spaces). Abstract mathematical structures are essentially proof
4
generated; that is, they are defined by abstracting out those properties needed
for certain proofs to be carried through.
In computer science, similarly, the study of a correctness proof of an algorithm
may reveal that the algorithm works for many types of objects. Suppose for
example that exponentiation is defined by
x0 =1 and x?+1 = (?)* x.
Consider the following algorithm, which uses only O(log n) multiplications:
expon(x,n) =
if n = 0 then 1
else if even?(n) then expon(x * x, n + 2)
else expon(x,n --H 1) * x
In proving the correctness of expon, we require that n be a nonnegative integer,
but we do not need to fix the type of x. All that is needed is for the type of x
to have an associative operation * with multiplicative identity 1. Hence, expon
should be applicable to many types of inputs.
The principle of generalization goes by the name of polymorphism in computer
science, except that it is common to encumber the concept of polymorphism with
irrelevant implementation cun?ideratit,ii?; iii p?rticular, it i? iiormally demanded
that a polymorphic function execute the same machine code, regardless of the
types of its inputs. 2
Following Poincare', we can say that the basis for polymorphism is the use of
the same name for different objects, which allows programs that use these names
to apply to many types of inputs. For example, we allow the identifiers cons and
* to refer to many different functions, depending on the argument types. More
precisely, we say that cons and * have many types and that they have a meaning
corresponding to each of their types:
cons : Vo.a H seq(o) H seq(a)
describes the types of cons, ? and
* : int H int H int
* : real `. real H real
* : complex H complex H complex
gives some of the types of *.
2 The discussion of Cardelli and Wegner [CW85] is typical; Prins [Pri87], in contrast, argues
against the necessity of uniform implementations for polymorphic functions.
? Throughout this dissertation, we use curryin9 to avoid the messiness of functions with mul-
tiple arguments.
5
Notice that the types of consare all described by a single universally quantified
type formula; we therefore say that cons is parametrically polymorphic. The
types of *, in contrast, cannot be uniformly described: they require many type
formulas. For this reason, * is said to be overloaded.
With respect to the generalization principle, which seems to be the true
foundation of polymorphism, there is no essential difference between paramet-
ric polymorphism and overloading. Traditionally, however, overloading has been
regarded as less genuine and significant than parametric polymorphism; indeed
overloading is often belittled as ad-hoc polymorphism.4 This disdain for over-
loading seems to stem mostly from the desire for uniform implementations it is
easy to give an implementation of C0flS that works for all kinds of sequences, but
* requires different machine code for integers than for floating-point numbers.
In fact the usual way of treating the overloaded operators in a program is to
demand that the local context determine a particnlar overloading to be used at
each point; see, for example, [ASU86]. This is even the case in the polymorphic
language ML [WB89J. But this treatment of overloading destroys the polymor-
phism of expon above: choosing a particular overloading of * to be used by expon
arbitrarily restricts expon to a single argument type.
Another common assertion is that overloaded identifiers have only finitely
many types, in contrast to parametrically overloaded identifiers, which have in-
finitely many types. This need not be so, however. Consider the operation <.
Two of its types are real real bool and char char H bool. In addition,
< may be used to compare sequences lexicographically (that is, by dictionary
order). What sequences can be compared in this way? Precisely those sequences
whose elements can be compared witii <! Hence < has the infinite collection of
types seq(char) H seq(char) bool, seq(seq(char)) .` seq(seq(char)) H bool,
and so forth. Such types can be characterized with the formula
Va with ? : CL			CL H bool. seq(a)			seq(a)			bool,
which represents all types of the form seq(r) H seq(r) H bool that satisfy the
constraint < : r r H bool.
Another kind of polymorphism is due to subtyping, the property that one
type is contained in another. For example int C real. Subtyping leads to
polymorphism in that a value in a type is also in any supertype of that type. So
if < works on type real, < also works on type int.
From our axiomatic point of view, subtyping is a matter of set inclusion. Thus
we say that int is a subtype of real because the set of integers is a subset of
the set of reals. Another viewpoint is that subtyping is based on coercion, and
that int is a subtype of real because an integer value can be coerced to a real
value. This latter view is suggested by reductionist considerations (integers and
Again, [cw85] is typical.
6
reals will probably be represented differently), but it seems better to separate
such concerns from issues of axiomatic type correctness.
A striking example of a polymorphic function is Algorithm 5.5 in [AHU74].
The algorithm is defined in terms of an abstract type called a closed semiring.
Depending on the choice of closed semiring, the algorithm computes the reflexive,
transitive closure of a graph, the shortest paths between all pairs of vertices in
a weighted graph, or a regular expression equivalent to a nondeterministic finite
automaton.
Now that we have some understanding of polymorphism, we turn to the ques-
tion of axiomatic type correctness.
1.4 Axiomatic Type Correctness
If multiplication is defined only on integers and reals, then it is meaningless to
multiply a character by a boolean. A valuable service that a language can provide
is to ensure that this sort of mistake cannot happen; this is what axiomatic type
correctness enforces.
The basic approach is to associate a type with each phrase of a program and
to give a system of rules specifying which combinations of phrases are sensible.
These rules are called the type system of the language. As a simple example, we
might have the following rule for +: "if e and ?? are phrases of type integer
expression, then e + e'is a phrase of type integer expression."
Type systems are simpler in functional languages, because they have only
one kind of phrase, namely expressions. Imperative languages in contrast, have
several kinds of phrases: expressions, commands, variables, and acceptors. We will
limit ourselves to functional languages in this dissertation; Reynolds explores the
typing of imperative languages in [Rey8O,Rey8l,Rey88] and polymorphism in
imperative languages is investigated in [Tof88] and [LW9l].
Because in a functional language every phrase is an expression, we will drop
the use of expression from the types of phrases, saying that e + e' has type int
and writing e + ?? : int. We should keep in mind, however, that there is a
difference between saying that a program has type int and saying that a value
has type int. A program has type int if it yields an integer result, but a value
has type int if it is an element of the set of integers.
Built-in operations will appear as free identifiers within programs; for this
reason the type of a program needs to be stated with respect to a type assumption
set that gives the types of the built-in operations. Hence, the form of a typing
judgement is
AHe:r,
which may be read "from type assumption set A it follows that program e has
type T". The rules for proving such judgements make up the type system of the
7
language.
For example, the type T H r? is the type of functions that accept an input
of type r and produce an output of type r'. The rule for typing a function
application e' e" (i.e. the application of function e' to argument e") is
A H e' : r r' A H e" : r
A H ?? e11 :
This rule is strikingly like the logical rule modus ponens:
r H			T
71
This is a manifestation of the remarkable propositions as types principle [GLT89],
according to which types may be viewed as logical propositions and a program
of a certain type may be viewed as an intuitionistic proof of the proposition
corresponding to the type. As a consequence of this principle, it turns out that
a type system is a system of natural deduction [vD83,Pra65].
Given a set of typing rules, a program is said to be well typed if from the
rules it can be shown that the program has some type. If the compiler can verify
that each program is well typed, the language is said to be syntactically typed.
Traditionally, syntactically typed languages require programs to be written with
type declarations; such declarations make it easy to check whether a program
is well typed. In this case the problem is referred to as one of type checking.
Other languages, such as ML, allow programs to be written without any type
information; in this case checking type correctuess requires more ingenuity and
is referred to as type inference.
There are two reasons to prefer type inference to type checking. The obvi-
ous reason is that type inference saves the programmer keystrokes. The savings
is especially great in the polymorphic type systems considered in this thesis
our type systems involve complex type formulas with constrained quantification,
which makes the job of annotating programs with type information quite cum-
bersome.
A more subtle advantage of type inference is that forcing programmers to
write type declarations may force them to overspecialize their programs. Con-
sider, for example, the procedure swap in Pascal:
procedure swap(var x, y:integer);
var z:integer;
begin z:=x; x:=y; y:=z end
There is nothing about swap that depends on integer; indeed, changing the two
declarations of integer to character produces a correct Pascal program. But there
8
is no declaration a programmer can make that allows swap to be used on both
inte?er and character. So the deeper advantage to type inference is that programs
without type declarations implicitly have all types that can be derived for them.
We will return to this point in the next section when we discuss principal t?pes.
We have so far discussed type correctness solely with respect to a given set
of typing rules, and we have said little about what it means for a program to
be type correct. This is a tricky area; the absence of non-syntactic errors (for
example, division by 0 or nontermination) cannot in general be established at
compile time, so saying that a program has type integer does not guarantee
that the program will succeed and yield an integer output. In practice, there
are tradeoffs between the difficulty of type checking and the amount guaranteed
by type correctness. A more extreme position is taken in the language Nuprl
+ 86j, where the language is restricted to less than universal computing power
for the sake of stronger type guarantees. ?
The type systems that we consider will be more modest. We will be satisfied,
for example, to give + type int int H int,ignoring the fact that + is a
partial function. Furthermore, when considering polymorphism, we will allow a
function to accept inputs of all types that `look' correct, in the sense that the
operations needed are defined on the input types. So in the example of expon, our
type system will not require that * be associative or that 1 be a multiplicative
identity. Also, we will not demand that n be nonnegative.
1.5 The Hindley/Milner/Damas Type System
We now outline the polymorphic type system due to Hindley, Milner, and Damas
[11in69,Mil78,DM82,Car87]. This type system is successfully in use in the lan-
guage ML.
The Hindley/Milner/Damas type system expresses parametric polymorphism
by means of universally quantified types. For example, the primitive LISP oper-
ation cons may be given type
V0.0 H seq(o) H seq(o)
to indicate that for every choice of o, cons has type
0 H seq(o) H seq(o).
A fundamental restriction on this type system is that all quantification must be
outerrnost; that is, types must be in prenex form.6
In particular, because Nupri is stronul? normalizing, a Nupri function of type int int is
guaranteed to be a total function from int to int.
6 In the literature, this is sometimes called the shallow types restriction.
9
Milner [Mil78] developed a type inference algorithm, called algorithm W, for
this type system that allows programs to be written with no type information at
all. In Chapter 2, we will study in detail an extension of algorithm w; for now
we will be content to show, informally, how W infers a type for the expression
Af.Ax.f(f x) .7
The expression is of the form Af.e and we don't know what the type of f
should be. So we choose a new type variable ?, make the assumption f: a, and
attempt to find a type for Ax.f(f x). Now the expression is of the form Ax.e',
so we choose a new type variable p, make the assumption x : ?, and attempt
to find a type for f(f x). This is an application, so we first find types for f and
(f x). The type of f is easy; it is just a, by assumption. To find the type of
(f x), we begin by finding types for f and x; by assumption we have f: a and
x : ?. Now we must type the application using the rule for function application,
A H e' : r H r' A ? e11 : r
A H e' e" : r
Hence we discover that a must actually be of the form P H ? for some new
type variable ?; that is, we refine our assumption about f to f: P ?. (This
inference is made using unification.) This gives (f x) : ?. Now we must use
the rule for function application again to find a type for f(f x); we discover
that p must be the same as ?, so we refine our assumptions to f: ? H ? and
x : ?, yielding f(f x) : ?. Now we can "discharge" 8 the assumption x : ? to
get Ax.f(f x) : ? H ? Next we discharge the assumption f : ? H ? to get
Af.Ax.f(f x) : (? H ?) H (? H ?) Finally, since ? is not free in any active
assumptions, we can quantify it, thereby obtaining the typing
J H Af. Ax.f(f x) : V?.(? H ?) H (? H
This turns out to be the best possible typing for this expression; formally, we say
that the typing is principal. This means that any type whatsoever of Af. Ax.f(fx)
can be derived from the type V?.(? H ?) H (? H ?) by instantiating ? suitably;
technically, we say that all the types of Af.Ax.f(fx) are instances of the principal
type.
On the expression let x = e in e' , type inference proceeds by first finding
a principal type a for x, making the assumption x : a, and then finding a type
for e'.
Observe that, semantically, let x = e in e' is the same as (Ax.e')e. They
have, however, different typing behavior: in typing let x = e in e1 , we may
give x a quantified type when we type e'; in contrast, in typing (Ax.e')e, we
7The A -calculus expression Ax.e denotes a function with one parameter, x, and with body
e. Hence Ax.x denotes the identity function.
8This terminology comes from natural-deduction theorem proving.
10
must give x an unquant4ied type when we type ?? This discrepancy, known
as the Let anomaly, is forced by the restriction to outermost quantification: if we
find the typing ?? : r under the assumption x : a, where a is quantified, then
when we discharge the assumption x : a we will obtain the typing Axe' : a
but the type a T will not be outermost quantified.
In [DM82J, it is shown that the Hindley/Milner/Damas type system has two
especially nice properties: first, every well-typed program has a principal type,
and second, principal types may be inferred using algorithm W. More precisely,
given any program e, algorithm W finds a principal type for e if e is well typed
and fails otherwise. Another way of stating this is to say that ?Y is sound and
complete with respect to the typing rules.
One might claim that Pascal, too, has principal types after all, every Pascal
program has a unique type. But, as can be seen from the discussion of swap
above, this is true for a trivial reason: the type declarations required by Pascal
force programs to be overspecialized. If, however, we erase all type declarations
from swap, then the typing rules of Pascal allow swap to be given many types,
none of which is principal.
For this reason, principal typing results must always be formulated with re-
spect to the implicitly typed version of a language; that is, with respect to the
version of the language in which all type declarations are erased. With respect
to an implicitly typed language, the existence of principal types says, intuitively,
that the set of type formulas in the language is expressive enough to capture
all the polymorphism implied by the typing rules. It follows that increasing the
power of the typing rules of the language demands a corresponding increase in
the richness of the set of type formulas; this theme will recur throughout this
dissertation.
1.6 Extensions to Hindley/Milner/Damas
Polymorphism
One line of research aims at extending Hindley/Milner/Damas polymorphism
by removing the restriction to outermost quantified types. This leads to the
polymorphic A -calculus of Girard and Reynolds [Gir72,Rey74]. It is at present
unknown whether type inference is decidable for this language; for this reason
the polymorphic A -calculus is normally defined with explicit type declarations. ?
Research into the type inference problem for this (and related) languages is de-
scribed in [Lei83,McC84,KT90]; we will not consider this extension further in
this dissertation.
9In fact, the instantiation of quantifled type variables is usually viewed as a kind of application,
suggesting that types are somehow values.
11
Instead, we will study two kinds of polymorphism that cannot be expressed
within the Hindley/Milner/Damas type system: overloading and subtyping. In
the Hindley/Milner/Damas type system, an assumption set may contain at most
one typing assumption for an identifier; this makes it impossible to express the
overloadings of <. For < has types char char boot and real real H
bool, but it does not have type
VQ.Q H OL ` boot.
So any single typing < : a is either too narrow or too broad. Also, in the Hind-
ley/Milner/Damas type system, there is no way to express subtype inclusions
such as int C real.
The goal of this dissertation, then, is to extend the Hindley/Milner/Damas
type system to incorporate overloading and subtyping while preserving the ex-
istence of principal types and the ability to do type inference. As suggested in
the discussion of principal types above, this requires a richer set of type for-
mulas. The key device needed is constrained (universal) quantification, in which
quantified variables are allowed only those instantiations that satisfy a set of
constraints.
To deal with overloading, we require t?ping constraints of the form x :
where x is an overloaded identifier. This allows us to give function expon (de-
scribed in Section 1.3) the principal type
Va with * : a H a			a, 1 : a. a H int			a
which may be understood as saying that for all choices of a such that * is
defined on a and 1 has type a, expon has type a H int H a. It is easy to see
why such constraints are necessary: since there may be many type assumptions
for * and 1, there is probably no single type formula that explicitly gives the
types of expon; it is therefore necessary to use an implicit representation.
The typing
expon: Va with * : a H a .` a, 1 : a. a H int a
may also be understood as a universal Horn clause [L1o84]:
expon : a H int H a if *: a H a H a, 1 : a.
The reader may find this viewpoint useful.
Another example is a function sort that takes as input a sequence and re-
turns the sequence in sorted order, using < to compare the sequence elements.
Assuming that < is overloaded, sort has principal type
Va with < : a H a			boot. seq(a)			seq(a).
12
To deal with subtyping, we require incluston constraints of the form T C r'
Consider, for example, the function Af.Ax.f(f x) discussed earlier. Let us give
this function the name twice. In the Hindley/Milner/Damas type system, twice
has principal type Va.(? H 0) H (0 OL). But in the presence of subtyping,
this type is no longer principal if int C real,then twice has type (real H int)
(real			int), but this type is not deducible ftom Vo.(o H 0)			(0			o). It
turns out that the principal type of twice is
V?Pwith PCO.(O???)H(O?fl).
Another example requiring inclusion constraints is
if true 21
where if : Vo.bool H 0 H 0			0; this has principal type
Vowith intCo.o?o.
An issue that arises with the use of constrained quantification is the satisfia-
bilit? of constraint sets. A type with an unsatisfiable constraint set is vacuous; it
has no instances. We must take care, therefore, not to call a program well typed
unless we can give it a type with a satisfiable constraint set. Unfortunately, we
will see that it is undecidable whether a given constraint set is satisfiable; this
difficultly will force us to impose restrictions on overloading.
We now briefly outline the remainder of the dissertation. In Chapter 2 we con-
sider overloading. We present the typing rules, give a type inference algorithm,
W0, and prove that it is sound and complete with respect to the typing rules;
hence W0 computes principal types. Next we show that checking the satisfiabil-
ity of constraint sets is undecidable. To deal with this we propose restrictions on
overloading that make the satisfiability problem decidable, and yet allow most of
the kinds of overloading that occur in practice.
In Chapter 3 we extend the type system of Chapter 2 by adding subtyp-
ing. We give another inference algorithm, W08, and prove that it is sound and
complete. An interesting feature of type inference with subtyping is the neces-
sity of simplifying the inferred types the unsimplified types are so complex that
they are unintelligible. The simplification process involves a variant of unification
called shape unification, graph algorithms such as strongly connected components
and transitive reduction, and simplifications based on the monotonicities of type
formulas.
In Chapter 4 we give a number of examples of type inference, survey related
work, and indicate some future research directions. 10
10The reader impatient for more examples may wish to look ahead to Chapter 4 now.
Chapter 2
Overloading
In this chapter, we develop the theory of polymorphism in the presence of over-
loading. We begin in Section 2.1 by presenting a type system that extends the
Hindley/Milner/Damas type system by allowing overloading in type assumption
sets and by allowing polymorphic types to have constraint sets as a way of ex-
pressing a kind of bounded polymorphism. In Section 2.2 we study properties of
the type system and prove a normal-form theorem for derivations in our system.
In Section 2.3 we address the type inference problem for our system, present-
ing algorithm W0, which generalizes Milner's algorithm W [Mi178,DM82]. In
Section 2.4 we establish the soundness and completeness of W0, showing that
our type system has the principal typing property. In Section 2.5 we address a
problem deferred from consideration in Sections 2.3 and 2.4, namely the prob-
lem of checking the satisfiability of a constraint set. We show that the problem
is undecidable in general and, indeed, that the typability problem for our type
system is undecidable in general. Section 2.6 attempts to cope with these lim-
itations by proposing restricted forms of overloading for which the satisfiability
and typability problems are decidable.
2.1 The Type System
In order to study polymorphism in the presence of overloading in as clean a
setting as possible, we take as our language the core-ML of Damas and Milner
[DM82]. Given a set of identifiers (x, y, a < 1 .. ), the set of expressions
is given by
e			x Axe			let x = e in e
As usual, we assume that application e ???? left associative and that application
binds more tightly than A or let.
The expression let x = e in e' is evaluated by evaluating e in the cur-
rent environment, binding the value of e to x, and then evaluating e1. Notice
13
14
therefore that let does not permit recursive definitions. When we wish to make
recursive definitions, we will use an explicit fixed-point operator, fix.
The basic assertions of any type system are typings of the form e : a. The
typing e : a asserts that expression e has type a. In the next three subsections,
we present our type system, first defining the set of types and type schemes, and
then presenting the rules for proving typings.
2.1.1 Types and Type Schemes
Given a set of type variables (Q, P, ?, ?,...) and a set of type constructors (int,
boot, char, set, seq, ... ) of various arities, we define the set of (unquantified)
types by
T ::= Ir H r'
where ? is an n -ary type constructor. If ? is 0-ary, then the parentheses are
omitted. As usual, ?? is taken to be right associative. Types will be denoted by
T, ?, p, ?, or
Next we define the set of quantified types, or type schemes, by
a:: Vai,...,o? with xl :Th,...,xm:Tm.T
We call toi,.. ,anl the set of quantified variables of a, txi : ri,... ,Xm : Tm1
the set of constraints of a, and r the body of a. The order of the quantified
variables and of the constraints is irrelevant, and we assume that they are written
without duplicates. If there are no quantified variables, "V" is omitted. If there
are no constraints, the with is omitted. Type schemes will always be denoted by
a.
We will use overbars to denote sequences. Thus c is an abbreviation for
a1...., a?. The length of the sequence will be determined by context.
If a = Va with C. ? ,then a variable p occurring in C or r is said to
occur bound in a if p is some aj and to occur free in a otherwise. We use the
notation fr(a) to denote the set of type variables that occur free in a.
2.1.2 Substitution and ot -equivalence
A substitution is a set of simultaneous replacements for type variables:
,rn]
where the Qj `5 are distinct. The substitution ....... , a? := T1...., rnj is ap-
plied to a type r by simultaneously replacing all occurrences of each aj by the
corresponding Tj. Substitutions are applied on the right, so the application of
substitution S to type r is denoted by rS. A substitution S may be applied
15
to a typing x: r to yield the typing x: (rS), and a substitution may be applied
to a set of typings by applying it to each typing in the set.
A type variable ? is said to occur (free) in the substitution
[oi,...,on :=ri,...,rn]
if P is one of the oj `s or if p occurs in some Tj
Defining the application of a substitution to a type scheme is rather com-
plicated, since we must deal with the usual worries about bound variables and
capture [HS86]. In the interest of simplicity, we adopt a definition that does more
renaming of bound variables than is strictly necessary. Suppose that we are given
a type scheme
a V?1,...,on with C.T
and a substitution S, where we assume that the o? `s are distinct. Let Pi,...,Pn
be the alphabetically first distinct type variables of the universe of type variables
that occur free in neither S nor a. (We demand the alphabetically first such
variables simply so that aS will be uniquely determined. 1) Now we can define
(V?withC.r)S=VPwithC[o:=PThS.r[a:=ThS
The composition of substitutions 5 and T is denoted by 5 T. It has the
property that for all a, (aS)T = a(S T).
We sometimes need to modify substitutions. The substitution 5 O [a
is defined by
Tj,			if p is some a?,
PS,			otherwise.
The names of bound variables in type schemes are unimportant; the notion
of a -equivalence [HS86J formalizes this idea. We say that
(Vai,...,anwithC.r)=?a(VPi,...,PnwithC[a:=Th.r[a?:=Th)
(assuming that the a? `s are distinct and the pi `s are distinct) if no Pj is free in
Va? with C. r . If a =a ??, we say that ?? is an a -variant of a.
Lemma 2.1 =a is an equivalence relation.
Proof:
o+ Letting p be a?, we see that =a is reflexive.
1 Tofte [Tof88] avoids such an arbitrary choice by defining substitution to be a relation on type
schemes, rather than a function, but this decision leads to a great deal of syntactic awkwardness.
16
Suppose V?with C.r =aa. Then a= V?with C[?:=Th.r[a:=Th,
for some ? not free in Va with C. r . Now, a are not free in a, since
each oLj has been replaced by bound variable Pi Hence
a =a Va with C[a			PTh[P			a]. r[a			?][?
Since [a:=Th[P:=a]= [],it follows that a=a Va with C.r. So =a
is symmetric.
o+ Suppose (Va? with C. r) a a and a a ?? Then for some ? not free
in Va?withC.r,
QED
a V? with C[a? :--H--H P]. r[a?
and for some ? not free in a,
a'			V?with C[a:=Th[P:=?.r[a:=Th[P:=?.
Because the oLj `5 are distinct, the Pi's are distinct, and the ? `s are dis-
tinct,
Also, ? are not free in (Va? with C. r). So Va with C. r --H=a a'. Hence
--Ha is transitive.
Lemma 2.2 a -equivalence is preserved under substitution. That is, if a =a
then aS a
Proof: Let a= Va with C.r and a'= VPwithC[a:=Th.r[a-:=Th. In
fact we will show that aS --H a'S which of course implies that aS =a a'S. Let
? be the alphabetically first distinct type variables not occurring free in 5 or
a. Because a and a' have the same free variables, ? are also the first distinct
type variables not occurring free in 5 or a'. Hence
aS
--H ? definition of a »
(Va with C.r)S
--H ? definition of substitution»
V? with C[a ?S. r[a
--H since [a:=?= [a:=PTh[P:=? »
V? with C[a:= P][P :=?S.r[a? P][? :=S
--H definition of substitution»
(VP with C[a:=Th.r[a:=Th)5
--H definition of a' »
a'S
17
QED
Lemma 2.3 If ? are distinct type variables that do not occur free in S or in
Va? with C.T, then
(Va with C.r)S =<x V?withC[a:=?S.r[a:=?S.
Proof: Let P be the alphabetically first distinct type variables not occurring
free in S or Va with C. T . Note that the ? are not free in
VP with C[a := P]S. r[a := P]S.
(If ? occurs in C[a := P]5 or r[a P]S, then since ? does not
occur in 5, ? occurs in C(a? P] or ?[a := P] Since ? is not free
in Va with C. r ,this means that ? is some ??, which is bound in
VP with C[a ThS.?[a
Also,
since neither P nor ? occur in 5. Hence
QE?
(Va with C.T)S
definition of substitution»
VP with C[a P]s r[a := P]s
definition of =a, ? not free in above»
V? with C[a := P]S[P . r[a P]5[P :=
since s[P = [P :=
V? with C[a:=Th[P :=?S.r[a? :=Th[P:=?S
since [a			P][P			= [a?			?
V? with C[a?			?S. ?[a :=
2.1.3 The Typing Rules
The purpose of a type system is to prove typings e : a. In general, however, the
typing e : a depends on typings for the identifiers occurring free in e, so typing
judgements are valid only with respect to a type assumption set.
A type assumption set A is a finite set of assumptions of the form x : a. A
type assumption set A may contain more than one typing for an identifier x;
in this case we say that x is overloaded in A. We next define some terminology
regarding assumption sets. A typing of the form x : r is called a r -assumption.
If there is an assumption about x in A, or if some assumption in A has a
18
(hypoth)
(H -intro)
(?-elim)
(let)
(V-intro)
(V-elim)
A ? x : a, if x : a e A
A u fx : rl ? e : Y
A H Ax.e: r H Y
(x does not occur in A)
A H e: r r1
A ? : T
A F e e' :
AHe:a
A u fx : a? H ?? : r
A F let x = e in e1 : r (x does not occur in A)
AuC? e: T
A H C[o := ir]
A?e: V?with C.r (a notfreein A)
AFe: Va?with C.r
A F C[a
A F e: ir?]
AFe:a
a =a a'
A H e : a'
Figure 2.1: Typing Rules with Overloading
constraint x : r,then we say that x occnrs in A. We use the notation id(A) to
denote the set of identifiers occurring in A. Finally, we use the notation fr(A)
to denote the set of type variables occurring free in A.
The type inference rules given in Figure 2.1 allow us to prove typing?dgements
of the form
AHe:a,
which asserts that from A it follows that expression e has type a. If C is a
set of assumptions x : a, then we use the notation
AFC
to represent
A H x : a, for all x : a in C.
This notation is used in rules (V-intro) and (V-elim). If A F e: a for some a
then we say that e is well typed with respect to A.
19
Here is an example of a derivation. Suppose that
A-
: char H char H boot,
_ Va with < : a H a boot. seq(a) . seq(a) H boot,
c: seq(char)
We will derive the typing
AHiet f=Ax.(x?<x) in f(c) boot.
We have
by (hypoth),
by (hypoth),
AU (? ?H ?H boot,x pJ H? : ?H ? H boot
Au f? :			H			H boot,x :			H x :
Au f<--H : H . boot,x : F< (x) : boot
by (?-elim) on (2.1) and (2.2),
Au f< : H H boot,x : H x <x: boot
by (? elim) on (2.3) and (2.2),
Au f<--H : H H booti H Ax.(x ? : boot
by (H -intro) on (2.4),
A F? :			H			boot)[P			char]
by (hypoth), and
A H Ax.(x ? x): VP with <:P ) P?? boot.P boot
by (V-intro) on (2.5) and (2.6). Now let
B=AUff: VP with ?:P?P? boot.PHbootl.
Then
B H f: VP with ? : H H boot.P H boot
by (hypoth),
B H? : Va with < : a .` a boot. seq(a) H seq(a) boot
by (hypoth),
(2.1)
(2.2)
(2.3)
(2.4)
(2.5)
(2.6)
(2.7)
(2.8)
(2.9)
B F? : char H char H boot
(2.10)
20
by (hypoth),
B F< : seq(char) H seq(char) H boot
by (V-elim) on (2.9) and (2.10) with 0: char,
B H f: seq(char) H boot
by (V-elim) on (2.8) and (2.11) with ? scq(char),
B H c: seq(char)
by (hypoth),
B H f(c) : boot
by (H -elim) on (2.12) and (2.13), and
A H let f = Ax.(x <x) in f(c) : boot
(2.11)
(2.12)
(2.13)
(2.14)
(2.15)
by (let) on (2.7) and (2.14).
Rules (hypoth), (H -intro), (H -elim), and (let) are the same as in [DM82],
except for the restrictions on (H -intro) and (let), which we discuss at the end
of this section. Rules (V-intro) and (V-elim) are different, since they must deal
with constraint sets. Notice in particular that rule (let) cannot be used to create
an overloading for an identifier. Hence, the only overloadings in the language are
those given by the initial assumption set.
Rule (=a) is not included in [DM82], but it should be, for it is needed to
correct a defect of natural deduction. The problem is that without (=?a), the
names chosen for bound variables can make a difference, contrary to what we
would expect. For example, without rule (=a), if
then
but
A = ff : V?.a H x :
AHf(x) :VP.P
AVf(x) :Vo.o,
because 0 is free in A. More seriously, with rule (=?a) we can prove that if
AH e : a, then AS He: aS, but without (=a) this fails. For if
A= tf :VQ.o? ?H ?, x :01, 5 =			:=
then
A H f(x) : Vp.p H
but AS = : V&o H .` ?, x: 0), (VP.Q H ?)S = Vo.o H ?? and
AS V f(x) : Vo.o H
21
The second hypothesis of the (V-intro) rule says that a constraint set can
be moved into a type scheme only if the constraint set is satisfiable the typing
A F e : Vo with C. r cannot be derived unless we know that there is some
way of instantiating the a so that C is satisfied. This restriction is crucial in
preventing many nonsensical expressions from being well typed. For example, if
A = f+ : int H jut H jut, + : real H real real, true : booti,
then without the satisfiability condition we would have
AF (true + true) : with + : boot H boot H boot.boot
even though + doesn't work on boot!
Overloading has also been investigated by Kaes [Kae88] and by Wadler and
Blott [WB89]. Their systems do not require the satisfiability of constraint sets
in type schemes, with the result that certain nonsensical expressions, such as
true + true, are well typed in their systems. 2
The restrictions on (H -intro) and (let) forbid the rebinding of an identifier
using A or let. Hence to get the usual block structure in expressions, we would
need to define the notion of a on expressions to allow the renaming of bound
identifiers. For simplicity only, we will not bother to do this.
The usual rules [DM82] for (H -intro) and (let) are
and
Ax u (x : r] H e :
A H Ax.e: T T
AHe:a
Ax u [x : a) H e' : T
A H let x = e in e' : T
where Ax denotes A with any assumptions about x deleted. It turns out that
under these rules, a number of obviously desirable properties fail. For example,
one would imagine that if AUB He: a and A H B, then A He: a. But if
A=(y: Va with x:a.a, x:iutj,
B =			: int),
then with respect to the usual (H -intro) rule, A U B H Ax.y : boot H jut and
AH B, but A VAxy: boot ?int
2 In Kaes' system, true + true isn't well typed, but examples like it are.
22
2.1.4 The Instance Relation and Principal Types
Given a typing A F e: a, other types for e may be obtained by extending the
derivation with the (V-elim) rule. The set of types thus derivable is captured by
the instance relation, >?A.
Definition 2.1 (Va with C. r) >A r' if there is a s?bstitution [a? := 7r] such
that
o+ AHC[a:=r] and
o+ r[c := =
Furthermore we say that a >A a' if for all r, a' >A T implies a >A T. In this
case we say that a is an instance of a with respect to A.
This definition has the property that if a >A T, then for any e, A H e : a
implies A H e : r, because the derivation of A H e : a can be extended using
(V-elim).
Like the >A relation of Wadler and Blott [WB89], our >?A relation general-
izes the > relation of Damas and Milner [DM82]. Unlike Wadler and Blott,
however, we follow the approach of Mitchell and Harper [MH88] in defining
a >?A a' .3 It is easy to see that >A is reflexive and transitive and that a >?A r
is well defined.
In a polymorphic type system, an expression e may have many typings, and
it is therefore desirable to have some "best" typing, which in some way subsumes
all other typings. The notion of a principal typing makes this precise.
Definition 2.2 The typing A ? e : a is said to be principal if for all typings
A H e a', a >A a'. In this case a is said to be a principal type for e with
respect to A
Principal types in our system cannot be understood by themselves; they de-
pend upon the assumption set A. If we say that the principal type with respect
to A of the exponentiation function expon is
Va with * : a			a			a, 1 : a. a . int			a
we must look at A to discover what overloadings of * and 1 are available. Only
then do we know how expon can be used.
3The Damas/Milner approach to defining ff > j' is syntactic; roughly speaking, it says that
?`ifa derivation of A He: ? can be extended to a derivation of A He: a' using (Velim)
followed by (V-intro). The Mitchell/Harper approach, in contrast, is semantic. On > the two
approaches are equivalent, but on >A the syntactic approach (adopted by Wadler and Blott) is
weaker.
23
Because one must look to the assumption set A to determine what overload-
ings are available, overloaded symbols do not have very satisfying principal types.
For example, suppose that A contains the following assumptions:
: char H char H boot,
: real H real			boot,
_ : V? with ? : a			0 H boot. seq(a) H seq(a) H boot
Then one principal type for < with respect to A is
Va with <: 0.0,
which obviously doesn't convey anything! A somewhat better principal type is
Va with <: a			a			boot. a			a H boot
but this isn't very informative either. 4 In practice, of course, one is seldom
interested in the principal types of overloaded symbols; it is the principal types
of compound programs, like expon, that are of interest, and such programs have
principal types that seem reasonable.
In Damas and Milner's system principal types are unique up to a; in our
system, because of the constraint sets in type schemes, there can be more inter-
esting non-unique principal types. Above, we gave two different principal types
for <. Similarly, if
A = (f: ?nt, f: boot, g : boot, g: chari,
then if Va with f: a, g : a. a is a principal type for some expression e with
respect to A,then so is boot, because the only way to satisfy the constraint set
: a, g : aJ is to let a be boot.
The reader may be uneasy about the existence of multiple principal types,
especially since, under our definition of >A, they are not all interderivable. In
the inference aigorithm, however, it is only necessary to generate r types from
a principal type, not j types. Further, any principal type of an expression can
be used to derive all the r types of the expression. So multiple principal types
are not a problem.
These two principal types for < help to explain why we use the semantic approach to defining
>A. Under the syntactic definition,
Va with <:a a H boot.a a boot ?A Va with <:a a
so it would appear that
Va with < : a			a			boot. a			a			boot
be a principal type of < so they have
_ type Va with <:a. a . Besides being
is not principal. But Wadler and Blott want this to
arranged their type system so that < does nol have
unreasonable, this clutters the type system.
24
2.2 Properties of the Type System
In this section we establish a number of useful properties of the type system. We
begin by showing that, roughly speaking, typing derivations are preserved under
substitution. This property will be used many times in what follows.
Lemma 2.4 If A H e : a then AS H e: aS. Furthermore, g?en any derivation
of A H e : a, a derivation of AS H e : aS can be constructed that uses the same
sequence of steps except that it inserts a (=a) step after each (V-intro) step.
Proof: By induction on the length of the derivation of A H e : a. Consider the
last step of the derivation:
(hypoth) The derivation is simply A H x : a where x : a e A. So x : aS E AS,
and ASHx:aS.
(? -intro) The derivation ends with
A u (x : ri H e' :
A H Ax.e' : r
where x does not occur in A. By induction, (A u fx : rl)S H : YS.
Since (Au fx : Ti)5 = AS u (x : rS?, and since x does not occur in AS -
(H -intro) can be used to give
AS H ????? : rS H T'S
and TS T'S = (r H
(? -elim) The derivation ends with
A H e': r H
A H e" : r
A H e' e" : r1
By induction, AS F e' : (r H T')S and AS ? e" : rS. Since (r H r')S =
rS H T?5, (H -elim) can be used to give AS H ?I??! : r15.
(let) The derivation ends with
AFe' ??
A U (x : a?? H e" : r
A F let x = e' in ??? : T
where x does not occur in A. By induction, AS H : ??5 and (A U fx:
? e" : TS. Since (A U (x : a'?)S = AS U fx : a'Si and since x does
not occur in AS, it follows from (let) that AS F let x = e'in e" : rS.
25
(V-intro) The derivation ends with
AUCH e:r
A H C[Q? := ir]
AHe: Vowith C.r
where Q are not free in A. Let ? be distinct type variables occurring free
in neither S,nor Va with C. r ,nor A. By induction,
(A u C)[a := ?S H e: r[a :=
and
AS H C[a? := ir?]S.
Now (A u C)[a? := ?S = AS u C[a? := ?S, since the a are not free in A.
Also, [a:=ir?jS and [a:=?S[?:=ir?S] agree on
(Both substitutions take a? `?` irjS. On any other variable ? in
C, both substitutions take ?:.` 65, as no can occur in 65.)
Hence
and
AS u C?- := ?S F e: r[a? :=
AS H C[a := ?S[? := irS]
So, since ? are not free in AS, by (V-intro)
ASHe: V?with CW:=?S.r[a:=?S
By Lemma 2.3,
V? with C[a :=?S.r[a :=?S a (Va with C.r)S,
so by inserting an extra (=a) step we obtain
ASFe:(Vawith C.T)S.
(V.elim) The derivation ends with
AHe: Va with C.T
A H C[a? := ir?]
A H e : ?[a? := ir?]
By induction,
ASFe:(Va-with C.T)S
and
26
AS H C[a
Let J3 be the alphabetically first distinct type variables occurring free in
neither 5 nor Vo with C. T. Then
(Vo?with C.T)S= VP with C[a:=PThS.?[o-:=ThS-
By the same argument used in the (V-intro) case above,
C[o? := r?]S = C[o			Th?[P :=
So by (V-elim),
and as above,
AS H e: T[o := Th?[P irS],
r[o? := ThS[P			irS] =			ir]
(=?a) The derivation ends with
QED
AH e:a
a =? a
AHe:a
By induction, AS H e: a'S, and by Lemma 2.2, a'S a aS. So by (=a),
AS He: aS.
We now begin the development of the main result of this section, a normal-
form theorem for derivations in our type system. Let (V elim') be the following
weakened (V-elim) rule:
(V-elim')
(x: Va?with C.r)eA
A H C[o? := ir?]
A H x : r[o := ir].
Write A H' e : a if A H e: a is derivable in the system obtained by deleting the
(V-elim) rule and replacing it with the (V-elim') rule. Obviously, A H' e : a
implies A H e : a. We will see that the converse holds as well, so H' derivations
may be viewed as a normal form for H derivations. A similar normal-form result
for Damas and Milner's type system appears in [CDDK86] and is discussed in
[Tof88j.
The usefulness of the restricted rules is that if A H? e : r, then the form of e
uniquely determines the last rule used in the derivation: if e is x the derivation
ends with (V?elim?), if e is Axe' the derivation ends with (H -intro), if e is e? e?
the derivation ends with (H -elim), and if e is let x = e'in e" the derivation
27
ends with (let). In contrast, a derivation of A H e : r is much less predictable:
at any point in the derivation there may be a use of (V-intro) followed by a use
of (V-elim).
Observe that since a (V-elim') step is equivalent to a (hypoth) step followed
by a (V-elim) step, it follows immediately from Lemma 2.4 that ?` derivations
are also preserved under substitution:
Corollary 2.5 If A ?` e : a then AS F' e : aS. Furthermore, given any deriva-
tion of A H' e : a, a derivation of AS ?` e : aS can be constructed that uses the
same sequence of steps except that it inserts a (=?) step after each(V-intro) step.
Before proving the normal-f6rm theorem, we show a number of auxiliary
lemmas. These auxiliary lemmas, like Lemma 2.4, are proved by induction on
the length of the derivation. Because the proofs are tedious, we relegate them to
Appendix A.
Lemma 2.6 If x does not occur in A, x ? y, and A u (x : aJ ?? y : r, then
A H' y : r
Proof: See Appendix A. QED
Lemma 2.7 If A ?` e : a then A u B F' e : a, provided that no identifier
occurring in B is A -bound or let-bound in e.
Proof: See Appendix A. QED
Lemma 2.8 Let B be a set of r-assumptions. If A u B H' e : a and A ?` B,
then A ?` e : a
Proof: See Appendix A. QED
With the above lemmas in hand, we can prove the normal-form theorem for
derivations:
Theorem 2.9 AH e: a if and only if A F' e: a
Proof: It is immediate that A H' e : a implies A H e : a, since a (V elim?)
step can be replaced by a (hypoth) step followed by a (V-elim) step. We prove
that A H e : a implies A H' e: a by induction on the length of the derivation of
A ? e : a. All cases follow immediately from the induction hypothesis except for
(V-elim).
(V-elim) The derivation ends with
AHe: V??with C.r
A H C[? :--H--H 7r]
A H e : := 7r]
28
By induction we have
A H' C[? := 7r-J.
Now, the derivation of A ? e Va with C. r ends with (hypoth), (V-
intro), or
(hypoth) We can simply use (Velim') to get AF' e: ?[a :=
(V-intro) The derivation ends with
AUCH e: r
A H C[o :=
AHe: Va?withC.r
where a are not free in A By induction, A u C H' e : r. By
Corollary 2.5,
(A u C)[a := ? H' e : r[a? := 7r].
Since a are not free in A,
(A u C)[a ir] = A u C[a ir].
Since A H' C[a ir], by Lemma 2.8 we have
A F' e : r[a? := ir?].
(=a) The derivation ends with
A H e : a'
a' =? Va with C. T
AFe: Va with C.r
where for some P not free in Va? with C. r
a' = VP with C[a? := . r[a? :=
Note that
and
C[a? := ?][? := ir?] = C[a := ir?]
r[a := Th[P := ir] = r[a := ir],
so the (=a) step can be dropped and we can instead use the derivation
A H e: VP with C[a := P] r[a? :=
AFC[a?:=P][P:=ir]
A H e : T[a := Th[P := ir]
This is a shorter derivation, so by induction,
A F' e : r[a? := ir].
29
QED
Theorem 2.9 leads to a number of immediate corollaries:
Corollary 2.10 If x does not occur in A, x $ y, and Au fx : a) H y: T, then
AHy:r
Corollary 2.11 If A H e : a then A u B H e : a, provided that no identifier
occurring in B is A -bound or let-bound in e.
Corollary 2.12 Let B be a set of T -assumptions. If A u B F e: a and A F B,
then A ? e: a.
Henceforth we will be fairly casual about the distinction between F and H'
Lemma 2.13 If A H e : a then no identifier occurring in A is A -bound or
let-bound in e.
Proof: See Appendix A. QED
This lenima gives us the following variant of Corollary 2.11. The variant will
be used in proving algorithm W0 sound.
Corollary 2.14 If A F e : a then A U B H e : a, provided that all identifiers
occumng in B also occur in A.
We conclude this section by introducing a property that is needed to ensure
that a type assumption set is, in a certain sense, well-behaved. The property
is motivated by the following observation: the satisfiability condition of the (V-
intro) rule prevents the derivation of `vacuous' typings A H e : VQ with C. T
where C is unsatisfiable, but such vacuous typings could be present in A itself.
Definition 2.3 A has satisfiable constraints if whenever (x: Vo- with C. r
there exists a substitution [? := 7r?] such that A H C[? := 7r]
Note that it is no real restriction to limit ourselves to assumption sets with
satisfiable constraints, since any assumption with an unsatisfiable constraint set
is basically useless. The essential property of assumption sets with satisfiable
constraints is that any well-typed program has unquantified types; no well-typed
program has only quantified types.
Lemma 2.15 If A has satisfiable constraints and A H e : a, then there exists a
type r such that A H e : r
30
Proof: If cr is a 7-type, there is nothing to show. Otherwise, we can strip off
any final (=?) steps in the derivation A H e: a to obtain a derivation A H e : a'
ending with either (hypoth) or (V-intro).
In the (hypoth) case, the derivation is simply A ? x : a' where x : a' fA. Say
a'is of the form VQ with C. ? ; since A has satisfiable constraints it follows
that there is a substitution [Q ?] such that A ? ir]. Hence the
derivation may be extended using (V-elim), giving A H x: 7[0? := 7r?]
In the (V-intro) case, the derivation must end with
AUC He :7
A H C[&
AHe: Va?withC.?
where 0 are not free in A. Again the derivation may be extended using (V-elim),
giving A H e: 7[0 7r]. QED
Lemma 2.16 If A has satisfiable constraints and there exists a substitution [0
it] such that A H C[a- it?], then A u fx : Va with C 7 ? has satisfiable
constraints.
Proof: By Corollary 2.11, we have A u tx: Va with C. 7] H C[o := it]. And
if y : V? with ?1 71 f A, then since A has satisfiable constraints there exists
pw\ such that A H C'[p := p?]. Using Corollary 2.11 again, we get that
Au fx: Va with C.7] H C'[p := p]. QED
In proving the completeness of algorithm W0 below, we must restrict our
attention to assumption sets with satisfiable constraints.
2.3 Algorithm wo
A fairly straightforward generalization of Milner's algorithm W [Mil78,DM82]
can be used to infer principal types for expressions in our language. Algorithm
W0 is given in Figure 2.2.
W0(A, e) returns a triple (5, B, 7), such that
ASUB He :7
Informally, 7 is the type of e, B is a set of 7-assumptions that describe all
the uses of overloaded identifiers in e, and 5 is a substitution that contains
refinements to the typing assumptions in A.
? We informally discussed the refinement of A by Milner's algorithm W in Chapter 1.
31
W0(A, e) is defined by cases:
1. e is x
if x is overloaded in A with icy Vo?.r,
return ([],fx:r[a:=Th1,r[a:=Pi) where p arenew
else if (x: Vo?with C.r)eA,
return ([],C[a:=Th,r[a:=Th) where p arenew
else faiL
2. e is Ax.e'
if x occurs in A, fail.
let (Si,Bi,ri)=W0(Aufx:o?,e') where o is new;
return (S1,B1,?S1 H ri)
3. e is ?I??I
let (S1,B1,r1) = W0(A,e');
let (S2,B2,r2) = W0(AS1,e11);
let S3 = unify(riS?,r? HO) where c is new;
return (Sis2s3, B15253 U B2S3, 053)
4. e is let x = e' in ???
if x occurs in A, faiL
let (S1,B1,r1) =W0(A,e');
let (B1,,a1)= ctose(ASi,Bi,ri);
let (S2,B2,T2) = W0(AS1 U fx : ail,e");
return (5152, B1152 u B2, T2).
Figure 2.2: Algorithm W0
32
Case 1 of algorithm W0 makes use of the least common generalization (lcg)
of an overloaded identifier. 6 The lcg of an overloaded identifier x captures
any common structure among the overloadings of x. For example, given the
overloadings
char H char H bool,
real			real			bool,
VQ with < : 0			0 H bool. seq(o) H seq(o)			bool,
Va,P with <: o? 0 H bool, < : H			bool
(OL x			H (o x			bool,
the lcg of < is V0.o H 0 H bool, which tells us that in all of its instances <
takes two arguments of the same type and returns a bool
Formally, we say that r is a common generalization of Pi,... , p? if there
exist substitutions Si,.. , S? such that TSj = p? for all i, and we say that r is
a least common generalization of Pi,... , p? if
1. T is a common generalization of pi,..?, p?, and
2. if r1is any common generalization of pi,... , p?, there exists a substitution
S such that ??5=?
Finally, we say that Vo?.r is an lcg of an identifier x that is overloaded in A
if r is a least common generalization of the bodies of those type schemes a
with x : a E A, and 0 are the variables of r. Least common generalizations
are discussed in [Rey7O], which gives an algorithm for computing them, and in
[McC84j under the name least general predecessors.
The "new" type variables called for in algorithm W0 are produced by a new
type variable generator, which produces an unbounded sequence of distinct type
variables. Before W0(A, e) is called, the new type variable generator is initialized
so that it does not generate any type variables occurring free in A.
Function unify, used in case 3 of W0, returns the most general unifler [Rob65,
Kni89] of its arguments. That is, unify(r, r') returns a substitution U such that
= r'U, failing if no such substitution exists; furthermore U has the property
that for any V such that rV = r'V, V can be factored into ?V? for some V'.
Function close, used in case 4 of W0 , is defined in Figure 2.3. The idea behind
close is to take a derivation
AuBH cr
where B is a set of assumptions about overloaded identifiers and, roughly speak-
ing, to apply (V-intro) as much as possible, yielding an assumption set B' and
a type scheme a such that
A u B' ? e : a.
6In fact the soundness and completeness of W0 do not rely on the use of the least common
generalizations of the overloaded identifiers; any common generalization will do. In particular,
the type Va.c can always be used, but this leads to less informative principal types.
close(A, B, r):
33
let a be the type variables free in B or T but not in A;
let B" be the set of constraints in B in which some oj occurs;
if A has no free type variables,
then if satisflable(B, A)
then B' = fJ
else fail
else B' =
return (B', Va with B". T).
Figure 2.3: Function close
If A has no free type variables, B' will be empty.
Function satisfiable(B, A) used in close checks whether B is satisfiable with
respect to A, that is, whether there exists a substitution 5 such that A H BS.
We defer discussion of how satisfiable might be computed until Section 2.5.
Actually, there is a considerable amount of freedom in specifying the exact
behavior of close. It is possible to give fancier versions of close that try to do
more simplification of the generated type a. We have, therefore, extracted the
properties of close needed to prove the soundness and completeness of W0 into
two lemmas, Lemma 2.17 and Lemma 2.19; this allows us to replace the simple
close of Figure 2.3 by any other close that satisfies the lemmas.7
If A has no free type variables, a principal typing for e can be obtained as
follows: W0(A,e) yields (S,B,7) such that AS u B H e : r. Since A has no
free type variables, this means that A u B H e : T. If (B', a) = close(A, B, T)
succeeds, then we will have AUB' He: a and ?? = f?, so AH e: a, and this
typing will be principal.
In particular, under the reasonable assumption that there are no free variables in the initial
assumption set, we may weaken the condition "A has no free type variables" on the third line of
ciose, replacing it with the condition "no type variable in B is free in A". The weaker condition
has the advantage of allowing certain type errors to be detected sooner.
34
fix Aleq.Ax.Ay.
if (null? x)
true
if (null? y)
false
if (= (carx) (cary))
(teq (cdr x) (cdr y))
(< (carx)(cary))
Figure 2.4: Example lexicographic
Here is an example of a type inference using W0. Suppose that
fix : Va.(a H a) H a,
if : Va.boot H a a H a,
--H : Va.a a H boot,
true : boot,
A =			false : boot,
car : Va.seq(a) H a,
cdr : Va.seq(a)			seq(a),
null? : Va.seq(a) H boot,
: char H char			boot,
_ : Va with < : a H a H boot. seq(a) H seq(a) H boot
Identifier fix denotes a least fixed-point operator, which allows us to express
recursion without the use of an explicit letrec construct. 8 Let lexicographic be
the expression given in Figure 2.4. Function lexicographic takes two sequences x
and y and tests whether x lexicographically precedes y, using ? to compare
the elements of the sequences.
The call W0(A, lexicographic) returns
:= seq(A1), n := boot, () := boot boot H boot e o+--H boot, t
boot H boot ? --H seq(A1), j' := boot, v := boot H boot H boot, ,:
boot, ? := boot			boot, ? := A1, a			:= A1, p := A1, r := A1 H boot,
A := A1, ? := A1, v: A1, ?			boot, ? := boot			boot? boot,
:= A1, a? := seq(A1), ? := seq(A1) H seq(A1) H boot, w := A1,
:= seq(A1), P1 := seq(A1) H boot, e := boot, ? := boot			boot,
:= A1, C1 := A1, ?1 := A1, tci := A1 H boot, ni := A1, [1 := A1,
vi			:= boot, 0 := boot, ?? := boot, 01 := boot, ri := boot, a :=
seq(A1) H seq(A1) H boot, Pi := seq(A1) H seq(A1) .` boot
: A1 H A1 H bootj,
seq(A1) H seq(A1) H boot
More precisely, "letrec x = e in e',, is equivalent to "let x = fix Ax.e in e',,. See [Rey85j
for further discussion of fix.
35
Then the call ctose(A, f? : A1 A1 boot?, seq(A1) H seq(Ai) boot)
returns
(fJ, VA1 with ? : A1 A1 H boot.seq(A1) H seq(A1) boot),
giving the principal typing
A H lexicographic: VA1 with < : A1 H A1 H boot. seq(Ai) H seq(A1) boot.
2.4 Properties of W0
2.4.1 Soundness of W0
First we have a lemma giving the properties needed of close in proving that W0
is sound.
Lemma 2.17 If (B', a) = cThse(A,B,?) succeeds, then for any e, if AUB He: r
then A u B' H e : a. Atso, every identifier occurring in B' or in the constraints
of a occurs in B
Proof: Suppose that (B', a) = close(A, B, r) succeeds and that A u B H e: r -
There are two cases to consider:
1. A has no?free type variables.
In this case satisflabte(B, A) is true, so there exists a substitution S such
that A H BS. The only variables occurring in B are the a?, so we may
write 5 = := 7r] without loss of generality. Since B" C B we have
A H Th'[o := 7r] and A H (B --H B")[o := 7r]. Now by the definition of B",
the a do not occur in B --H B", so in fact we have A H B --H B". Then, by
Corollary 2.11, wehave AUB"HB--HB". Since AUB11U(B--HB11)He:?,
we may apply Corollary 2.12 to yield A u B" H e : r. The a are by
definition not free in A, so (V-intro) may be applied:
A u B" H e: r
A H B11[a? :=
AHe: Va?with B".r
showing that AUB' He: a.
2. Ahasfreetypevariables.
Let ? be new type variables not occurring in A, B, or T. By Lemma 2.4,
we have (A u B)[a := p] H e : r[a := ?]. Then by Corollary 2.14, (A u
36
B)[?:=ThuBHe:r[?:=Th. Now(AuB)[a:=ThuB=AuBuB11[a:=
Pi? by the definitions of ? and B". Hence (V-intro) may be applied:
AuBuB11[? :=Th He: r[a := Pi
AUB H B11[a? :=Pi[P :=
AUB He: VP with B11[o :=
since the P are not free in A u B Finally, since
V? with B11[a? := ?. := a Va with B". r,
we may use (--Ha) to get A u B H e: Va with B". r
As for the second part of the lemma, it follows immediately from the fact that
B' and B" are subsets of B. QED
Theorem 2.18 If (5, B, r) = W0(A, e) succeeds, then AS u B H e : r. Fur-
thermore, every identifier occurring in B is overloaded in A or occurs in some
constraint of some assumption in A
Proof: By induction on the structure of e.
1. eisx
Then W0(A,e) isdefinedas:
if x is overloaded in A with lcg Va?.r
return ([],?x:r[a:=P]J,r[a-:=P?) where ? are new
else if (x: Vc? with C.r)cA,
return ([],C[o := ?], r[o Pi) where p- are new
else fail.
If x is overloaded in A, then (S,B,T) = ([i,fx : T[a? := Th?,r[a := Th)?
so ASuB=Au(x:?[o-:=Thi. Soby(hypoth), ASuBHx:r[a:=Th.
Also, every identifier occurring in B is overloaded in A.
If x is not overloaded in A, then (S,B,r) = ([i,C[a := Pi,r[a? := Th)?
so ASu B = AU C[a := P] By (hypoth), ASu B H x: Va? with C.r
and AS U B H C[a := P]. So by a (possibly trivial) use of (V-elim),
AS U B H x : r[o := Pi. Also, every identifier occurring in B occurs in a
constraint of an assumption in A.
2. eisAx.e'
Then W0(A,e) isdefinedas:
if x occurs in A faiL
let (S1, B1, Ti) w0(A U fx : 0), e') where a is new;
retun? (S1, B1, oSi ri)
37
By induction, (A u fx : ai)Si u B1 H e' : ri. Also, every identifier in B1 is
overloaded in A u (x : a) or occurs in some constraint of some assumption
in A u (x : a). Since x does not occur in A, and since the type a has no
constraints, this means that every identifier in B1 is overloaded in A or
occurs in some constraint of some assumption in A. In particular, x does
not occur in B1 and, therefore, x does not occur in AS1 u B1. So, since
(AUtx : a))S? UB1 = AS1UB1 Ufx :aS?), we can use (?Antro) to get
AS1 u B1 H Ax.e' : aS1 H
3. eise1e',
Then W0(A, e) is defined as:
let (51, B1, ri) =
let (52, B2, r2) = w0(A51,?11)
let 53 = nnify(r152, r2 a) where a is new
return (515253, B15253 u B253, as3).
By induction, AS1 U B1 H e' : Ti and AS1S2 u B2 H e" : T2, and every
identifier occurring in B1 or in B2 is overloaded in A or occurs in some
constraint of some assumption in A. Hence every identifier occurring in
B1 5253 U B2 53 is overloaded in A or occurs in some constraint of some
assumption in A. By Lemma 2.4, A515253 U B15253 ? : T15253 and
AS1 5253 U B2S3 H e" : T2S3. So by Corollary 2.14,
and
AS1 5253 U B15253 U B253 H e' : T15253
A515253 U B15253 U B253 F e" : T253.
By the definition of un?j??, T1S2S3 = T2S3 H a5?. Hence by (H -elim), we
have
A515253 U B15253 U B253 F e'e" : aS?.
4. eisletx=e1ine"
Then W0(A,e) is defined as:
if x occurs in A, faiL
let (5i, B1, ri) = w0(A, e');
let (B1,,ai) = close(A5i, B1, r1)
let (52, B2, r2) = ?v0(A51 U ?x ai),e")
return (5152, B1152 U B2, r2).
By induction, AS1 U B1 F e' : T1, and every identifier occurring in B1 is
overloaded in A or occurs in some constraint of some assumption in A.
So by Lemma 2.17, AS1 U B11 H e' : a1 and every identifier occurring in
38
B11 is overloaded in A or occurs in some constraint of some assumption
in A. In particular, since x does not occur in A, x does not occur in
B11 . Also by induction, (AS1 u tx : ,a1))52 u B2 F e" r2, which is the
same as AS1S2 u B2 u fx : a?S?l ? e : r2, and every identifier occurring
in B2 is overloaded in AS1 u ? x : a?l or occurs in some constraint of
some assumption in AS1 u (x : a?J. Now x does not occur in A, and by
Lemma 2.17 every identifier occurring in the constraints of al occurs in
B1. Hence every identifier occurring in B2 is overloaded in A or occurs in
some constraint of some assumption in A. In particular, then, x does not
occur in B2. Now Lemma 2.4 and Corollary 2.14 may be applied to give
AS1S2 u P11S2 u B2 F e' : a?S?
and
AS1S2 u P1,S2 uP2 U fx : a?S?? H e', : T2.
So, since x does not occur in AS1S2 u P11S2 uP2, (let) may be used to get
AS1S2uP11S2uP2Flet x=e' in e11 :r?.
QED
2.4.2 Completeness of W0
Ultimately, we will prove the following principal typing result.
Theorem Let A be an assumption set with satisfiable constraints and no free type
variables. If e is well typed with respect to A, then (5, P, r) = W0(A, e) succeeds,
(B', a) = close(A, P, r) succeeds, and the typing A ? e : a is principal.
Reaching this result will take some time, however.
We start with a lemma that gives the properties of close needed to establish
the completeness of W0
Lemma 2.19 If AS ? PS, then (B',a) = close(A,P,r) succeeds and a is of
the form Va with B". T . In addition,
o+ if A has no free type variables then B' =
o+ fr(a) C fv(A), and
o+ B' u B" C P
Proof: If A has free type variables, then close(A, P, r) succeeds. If A has
no free type variables, then the assumption AS F PS becomes A F BS. Hence
satisfiable(B, A) is true, and close(A, P, r) succeeds.
39
The remaining parts of the lemma are immediate from the definition of
close(A, B, r). QED
Lemma 2.20 If (5, B, r) = W0(A, e) succeeds, then every type variable occurring
in 5, B, or r occurs free in A or else is generated by the new type variable
generator.
Proof: A straightforward induction on the structure of e, using properties of
uni? and Lemma 2.19. QED
Definition 2.4 Let A and A' be assumption sets. We say that A is stronger
than A', written A ? A', if
1. A' H x: r implies A H x : r, and
2. id(A) C id(A')
Roughly speaking, A ? A' means that A can do anything that A' can. One
would expect, then, that the following lemma would be true.
Lemma If A' H e: r, A' has satisfiable constraints, and A ? A', then A H e: T
Given this lemma, we can prove the following completeness theorem for W0:
Theorem If AS H e : r and AS has satisfiable constraints, then (5o, B0, ro) =
W0(A, e) succeeds and there exists a substitution T such that
1. 5 = S0T, except on new type variables of W0(A, e),
2. ASHB0T,and
3. r=r0T
Unfortunately the lemma appears to defy a straightforward inductive proof.
The essential difficulty is in the (V-intro) case. Consider the case where the
derivation A' H e: r ends with (let):
A' H ?? : a
A' u tx : al F e11 : r
A' H let x = e' in ??? : 7
We would need to use induction somehow to show that A ? e' : ?? for some
such that
A u fx : ? A' u fx : al,
40
allowing us to use induction on the second hypothesis. Suppose that the deriva-
tion of A' H e' : a is by (V-intro):
A' u C ? :
A' F C[o? :=
A'He': Va?with C.r'
Now we would like to use induction to show that A u C H ?? : 71 But we have
a serious problem: it need not be the case that A u C ? A' u C! And in fact, it
need not be the case that AUC ? e' : r'. For example, let A= fx: int,y: inti
and A' = tx: Va with y : a.a,y: int). Then A ? A'. But AU (y : ?) ?
A'U fy : ?), and also AU fy : ?) Vx : ? although A' U fy : ?) H x :
The point is that the derivation of A H e: r may have to have a very different
structure from the derivation of A' H e : T, 50 it does not seem possible to `locally'
modify the derivation of A' F e : T to arrive at a derivation of A H e: r. How,
then, can we find a derivation of A H e : 7? The answer is to use W0 to find it.
But we haven't yet shown the completeness of W0, and indeed the whole reason
for introducing the lemma above was to prove the completeness theorem! So it
appears necessary to combine the lemma and theorem above into a single theorem
that yields both as corollaries and that allows both to be proved simultaneously.
We shall now do this.
Theorem 2.21 Suppose A' H e : T, A' has satisfiable constraints, and AS ? A'.
Then (5o, B0, ?o) = W0(A, e) succeeds and there exists a substitution T such that
1. 5 = S0T, except on new type variables of W0(A, e),
2. ASHB0T, and
3. r = r0T
Proof: By induction on the structure of e. By Theorem 2.9, A' H' e : 7
eisx
By the definition of AS ? A', we have AS ?` x : 7. The last (non-trivial)
step of this derivation is either (hypoth) or (V-elim'); we may write the
derivation so that the last step is a (possibly trivial) use of (V-elim'). If
(x:Vawiil1C.p)eA,then(x:VPwiThC[a:=ThS.p[a:=P?JS)eAS,
where ? are the first distinct type variables not free in Va with C. p or
in 5. Hence the derivation AS H' x: 7 ends with
(x: VP with C[a:=ThS.p[a-:=ThS)eAS
AS F' C[a? := ThS[P :--H--H
AS H' x : p[a? := flJS[fl :=
where p[a := ThS[P? := =
We need to show that (5o, B0, ro) = W0(A, x) succeeds and that there
exists T such that
41
1. 5 = S0T, except on new type variables of W0(A, x),
2. ASHB0T,and
3. T = r0T
Now, W0(A,x) is defined by
if x is overloaded in A with tcg Va.r,
return ([],fx:r[c:=P]J,r[?:=P?]) where ? are new
else if (x: Va with C.T)fA,
return ([],C[a? P], r[a Th) where ? are new
else fail.
If x is overloaded in A with lcg V?.p0 then (50,B0,T0) = W0(A,x)
succeeds with So = [], B0 = fx po[? := ?), and To = po[? :=
where ? are new. Since V?.p0 is the lcg of x, ? are the only vari-
ables in po and there exist ? such that po[? := = p. Let T be
S?[?:=?[?:=ThS[P:=ir]]. Then
So
1.
T0T
definition»
po[? := ?(S ? := := P]S[P := 7rjj
only ? occur in poK :=
poK? := := := ThS[P :=
only ? occur in po »
poK? := := ThS[P := ir]]
only ? occur in po »
poK? := 4)Th[a := ThS[P := ir]
by above»
:=fl]S[P:=ir?]
by above»
S0T = 5 ? := := ThS[P := irfi = 5, except on ?. That is,
S0T = 5, except on the new type variables of W0(A, x)
2.			Since B0T= fx : ToTi =			: ri, it follows that ASH B0T.
3. r0T =
If x is not overloaded in A, then (So, B0, To) = W0(A, x) succeeds with
So = [], B0 = := ?, and To = p[a? := ?, where ? are new. Observe
that [?:=?(S?[?:=ir-]) and [?:=ThS[P:=ir] agree on C and on p.
(The only variables in C or p are the a and variables e not
among or ?. Both substitutions map a? i,' irj and ?
42
Let T be S?[S:=?. Then
1. SoT=S?[?:=?=S,excepton ?. That is, SoT=S,excepton
the new type variables of W0(A, x).
2. Also,
Hence AS H B0T
3. Finally,
B0T
definition»
? by above observation»
ThS[P :=
T0T
definition»
? by above observation»
eisAx.e'
The last (non-trivial) step of the derivation of A' F' e : r must be (H -
intro):
A' u (x : T11 H' e' :
A' F' Ax.e' : H T11
where x does not occur in ??
We must show that (5o, B0, To) = W0(A, Ax.e') succeeds and that there
exists T such that
1 5 = S0T, except on new type variables of ?V0(A, Ax.e'),
2. AS?B0T,and
3. T1 H T11 = T0T.
Now, W0(A,Ax.e') is defined by
if x occurs in A, fail.
let (S1, B1, r1) = w0(A U ?x : aJ, e') where a is flew;
return (S1,B1,aS1 ri)
Since x does not occur in A' and (by AS ? A') ?d(AS) c id(A'), it
follows that x does not occur in AS This implies that x does not occur
in A, so the first line does not fail.
43
Now we wish to use induction to show that the recursive call succeeds. The
new type variable OL is not free in A, so
AS u fx : r'J (A u fx: oJ)(S ? [a
By Lemma 2.16, A'Ufx : r'J has satisfiable constraints. Next we argue that
ASUfx : ? A'Ufx : Y). Clearly, id(ASUfx : C ?ct(A'ufx :
Now suppose that A'u (x : r1i H y: p. If y # x, then by Corollary 2.10,
A' H y : p. Since AS ? A' we have AS H y : p and then by Corollary 2.11,
AS u fx : r'J H y : p. On the other hand, if y x,then the derivation
A' u fx : Y? F' y : p must be by (hypoth) hence p = r' So by (hypoth),
ASU tx : Y? H y : p. We have shown that
--H A' u fx Y? F : r11,
--H A' u tx : r'i has satisfiable constraints, and
--H (Aufx : ai)(S? [0= r']) ? A'u fx : r'1
So by induction, (Si, B1, ri) = W0(AUfx : a), e') succeeds and there exists
T1 such that
1.			5 ? [a :=			= S1T1, except on new variables of H70(A u (x : a), e'),
2. (AUfx:a))(S?[a:=Y1)FBiTi,and
3. Y' = r1T1
So (50,B0,r0) = W0(A,Ax.e') succeeds with So = Si, B0 = B1, and
To = aS? H
Let T be T1. Then
1.			Observe that
S0T
--H			<? definition»
S1T1
--H by part 1 of inductive hypothesis above»
5 Q [a := r'j, except on new variables of W0(A U fx : a), e?)
--H definition of ?
5, except on a.
Hence S0T = 5, except on the new type variables of W0(A U fx
a), e') and on a. That is, S0T = 5, except on the new type variables
of W0(A, Ax.e')
44
2.
B0T = B1T1 and we have AS u (x Y? H B1T1. By Theorem 2.18,
every identifier occurring in B1 is overloaded in A u fx: c) or occurs
in some constraint of some assumption in A u fx : at. Since x does
not occur in A and a has no constraints, this means that x does not
occur in B1. Hence Corollary 2.10 may be applied to each member
of Bi T1, yielding
3. Finally,
roT
ASH B1T1.
definition»
(aSi H r1)T1
? by part 3 of the use of induction above»
aSiTi			r11
a is not a new variable of W0(A U fx : at, e?) »
a(S e [a			:=			H
definition of ?
T H T
o+ eise?e11
The last (non-trivial) step of the derivation of A' H' e : r must be (H -
elim):
?? H' e' : H T
A' H' e11 :
A' ?? e' e" : r
We need to show that (5o, B0, r0) = W0(A, e'e") succeeds and that there
exists T such that
1. 5 = S0T, except on new type variables of W0(A, e'e11),
2. ASHB0T,and
3. r = r0T
Now, W0(A,e'e") isdefinedby
let (5i, B1, Ti) W0(A,e')
let (52, B2, r2) = `v0 (AS1, e11)
let 53 = nnifr(r152, T2 a) where a is new;
return (515253, B15253 u B253, a5?)
By induction, (5i, B1, ri) = w0(A, e') succeeds and there exists T1 such
that
1. 5 = S1T1, except on new type variables of W0(A, e'),
45
2. ASFB1T1,and
3. T1 H T = r1T1.
Now AS = A(S1T1) = (A51)T1, as the new type variables of W0(A, e') do
not occur free in A. So by induction, (52, B2, r2) = W0(AS1, e") succeeds
and there exists T2 such that
1. T1 = S2T2, except on new type variables of W0(A51, e")
2. (AS1)T1 H B2T2, and
3. r' = r2T2
By Lemma 2.20, the new variable c does not occur in A, Si, B1, ri,
52, B2, or T2. So consider T2 e := rj:
(riS2)(T2 e :=
a does not occur in TlS2 »
T1S2T2
<? no new type variable of W0(AS1, e") occurs in r1 »
r1T1
--H by part 3 of first use of induction above»
T H T
In addition,
(r2			o)(T2 ? [a :=
--H			 a does not occur in T2 »
r2T2 H T
--H			by part 3 of second use of induction above»
I			______
T			T
Hence by Robinson's unification theorem [Rob65], 53 = unify(r1 S2,r2 H a)
succeeds and there exists T3 such that
T2 ? [a := = S3T3.
So (S0,B0,r0) = W0(A,e'e") succeeds with So = S1S2S3, B0 = B1S2S3 u
B2S3, and To = aS?
Let T be T3. Then
46
1. Observe that
S0T
definition»
51 S2S3T3
by above property of unifier 53 »
5152(T2 e [a :=
 a does not occur in 5152 »
S1S2T2, except on a
by part 1 of second use of induction and since the»
new variables of W0(AS1, e11) don't occur in Si »
S1T1, except on the new type variables of w0(A51, e")
by part 1 of the first use of induction above»
5, except on the new type variables of W0(A, e?)
Hence we see that S0T = 5 except on a, on the new type variables
of W0(A51, e"), and on the new type variables of W0(A, e'). That is,
S0T = 5 except on the new type variables of W0(A, e'e11).
2. Next,
B0T
--H definition»
B15253T3 u B253T3
--H by above property of unifier 53 »
B152(T2 ? [a := T]) U B2(T2 Q [a := rj)
--H  a does not occur in B152 or in B2 »
B152T2 u B2T2
--H by part 1 of second use of induction and since the»
new variables of W0(A51, ?t?) don't occur in B1 »
B1T1 u B2T2
By part 2 of the first and second uses of induction above, AS H B1T1 u
B2T2, and so AS H B0T
Finally,
3.
r0T
definition»
a53T3
by above property of unifier 53 »
a(T2 e [a 7])
definition of ?
7
47
o+ eisletx=e'ine"
The last (non-tnvial) step of the derivation of A' F' e : r must be (let):
A' H' e' : a
A' u fx : al H' e'1 : T
A' ?? let x = e1 in e11 : T
where x does not occur in A'.
We need to show that (5o, B0, ro) = W0(A, let x = e'h? e") succeeds and
that there exists T such that
1. 5 = S0T, except on new type variables of ?Y0(A,let x = ?? in e"),
2. ASFB0T,and
3. T=T?T.
Now, W0(A, let x = e'in e") is defined by
if x occurs in A, faiL
let (S1, B1, r1) = w0(A, e');
let (B1,,ai) = cThse(ASi, B1, ri)
let (S2, B2, r2) = w0(As1 U ?x : u1J, e")
return (s1s2, BjS2 U B2, r2)
Since AS ? A' x does not occur in AS or in A. So the first line does
not fail.
Since A' has satisfiable constraints, by Lemma 2.15 there exists ?? such
that A' H e' : r'. Hence by induction, (Si, B1, ri) = W0(A, e?) succeeds
and there exists T1 such that
1. 5 = S1T1, except on new type variables of W0(A, e'),
2. ASHB1T1,and
3. T1 = r1T1
By 1 and 2 above, we have (A51)T1 F B1T1, so by Lemma 2.19 it fol-
lows that (B1,, ai) = close(A51, B1, ri) succeeds and al is of the form
V? with B1,, . ri . Also fv(a1) C fv(ASi) and B1, u B1,, C B1
Now, in order to apply the induction hypothesis to the second recursive call
we need to show that
ASu fx : aiTij ? A'u fx : a).
There are two parts to this:
1. A' u tx : a) H y : p implies AS u fx : a1T1) H y : fi, and
48
2. id(AS u fx : a1T1 1) c id(A' u tx : al)
The second part is quite simple; we show it first. By Lemma 2.17 and
Theorem 2.18, id(a1) C id(Bi) C id(A). Hence
showing 2.
c
c
id(AS u tx: a1T1))
? by above»
id(AS) u fx)
? AS ? A'»
?d(A') u fx)
?(A' u fx: a)),
Now we show 1. Suppose that A' u fx : a) H y p. If y # x, then by
Corollary 2.10, A' F y: p. Since AS ? A' we have AS F y : p and then
by Corollary 2.11, ASu fx : a1T1) H y :
If, on the other hand, y = x,then our argument will begin by establishing
that A' H e' : p. By Theorem 2.9 we have A' u (x : a) H' x : p and the
derivation ends with (hypoth) or (V-elim'). If the derivation ends with
(hypoth), then a = p and so A' H e' : p. If the derivation ends with
(V-elim'), then a is of the form VP with C. p' and the derivation is of
the form
x : V? with C.p' ?A'u fx: a)
A' u fx : a) F' C[p :=
A' u fx : a) H' x : p'[? :=
where p = p'[? := ir?]. It is evident that x does not occur in C (if x occurs
in C,then the derivation of A' u tx : a) H' C[? := r] will be infinitely
high), so by Corollary 2.10 applied to each member of C[P := 7r?, it follows
that A' H C[p := 7r]. Now the derivation A' H e': V? with C. p' may be
extended using (V-elim):
A'He': VP with C.p'
A' F c[P := ir]
A' H e' : ?`[P := 7r?],
giving that A' H e' :
So by induction there exists a substitution T2 such that
1. 5 = S1T2, except on new type variables of W0(A, e'),
2. ASHB1T2,and
3. p=riT?.
49
The new type variables of W0(A, e') are not free in A, so A51T1 = AS =
A51T2. Hence T1 and T2 are equal when restricted to the free variables
of AS1. Since, by Lemma 2.19, fr(a1) C fv(ASi), it follows that a1T1 =
a1T2. Now, al is of the form Va? with B111 r? , so a?T? (= a?T?) is of
the form
V? with B111[a? := ?T2. T1[?			?T2,
where ? are the first distinct type variables not free in T2 or al.
Consider the substitution [? := aT?]. We have
B111[a := ?T2[? := ?T2] = B111I'2
and
r1[a := ?T2K := Q?T2] = r1T2.
By 2 above, we have AS H B1T2. Since by Lemma 2.19 we have B111 C B1,
it follows that AS H B111I'2. By Corollary 2.11, then, we have AS u fx
a1 T1 J H B111T2. Hence we have the following derivation:
AS u (x: a1T1i H x: V? with B111[? := ?7'2 T1[a?? :=
by (hypoth) since a1T1 = V? with B111[Q := ?T2 := ?T2
ASU fx : aiTil F B111[a := ?]T2[? := o?T2]
by above since B111[? := ?T2[? := oT2] = B111T2, and hence
AS u (x : a?T?l H x : T1T2,
by (V-elim) since r?[a := ?T2[? := ?T2] r1T2. Since by 3 above,
r1T2 = p, we have at last that
ASufx : a1T1i Hx :p.
This completes that proof that AS u fx : a?T?? ? A' u fx : al, which is
the same as
(AS1 u tx : ai))Ti ? A' u fx : a).
Because A' H e' : a and A' has satisfiable constraints, it is easy to see
that the constraints of a are satisfiable with respect to A'. Hence by
Lemma 2.16, A' u fx : a) has satisfiable constraints.
This allows us to apply the induction hypothesis again, which shows that
(52, B2,r2) = W0(ASiUfx : ail, e") succeeds and that there exists T3 such
that
1. 7'1 = S2T3 , except on the new type variables of W0(AS1Ufx : aij, e")
50
2. ASu (x : a1T1i ? B2T3, and
3. r = r2T3.
So (So, B0, To) = w0(A, let x = e'in e") succeeds with 5o = 5152, B0 =
B1,52 u B2, and To = T2.
Let T be T3. Then
1. Observe that
S0T
--H definition»
S1S2T3
--H part 1 of third use of induction; the new variables»
of W0(AS1 u fx : ai),e11) don't occur in Si »
S1T1, except on new type variables of W0(A51 u fx :
--H by part 1 of first use of induction above»
5, except on new type variables of W0(A, e').
So S0T = 5, except on new variables of W0(A, let x = e'in e").
2. Next,
c
B0T
definition»
B1,52% u B2T3
Lemma 2.19»
B152T3 u B2T3
part 1 of third use of induction; the new variables»
of W0(A51 u fx : ail,e") don't occur in L?i »
B1T1 u B2T3
Now by part 2 of the first use of induction above, AS H B1T1. And
by part 2 of the third use of induction above, ASu (x : a1T1) ? B2T3
By Theorem 2.18, every identifier occurring in B1 is overloaded in A
or occurs in some constraint of some assumption in A. Since x does
not occur in A, it follows that x does not occur in B1 either. Now by
Lemma 2.19, the constraints of ai are a subset of B1. Hence x does
not occur in the constraints of ai. By Theorem 2.18, every identifier
occurring in B2 is overloaded in AS1 U (x : ail or occurs in some
constraint of some assumption in AS1 U (x : a?l. Since x does not
occur in AS1 or in the constraints of a1, it follows that x does not
occur in B2. Hence Corollary 2.10 may be applied to each member
of B2T3, yielding AS H B2T3. So AS ? B0T
51
3. Finally,
r0T
<? definition»
r2T3
? by part 3 of the third use of induction above»
QED
At long last, we get the completeness of W0 as a simple corollary:
Corollary 2.22 If AS F e : r and AS has satisfiable constraints, then
(5o, B0, ro) = W0(A, e) succeeds and there exists a substitution T such that
1. 5 = S0T, except on new type variables of W0(A, e),
2. ASFB0T,and
3. r=r0T.
Proof: Follows immediately from Theorem 2.21 by letting A' be AS, and
noting that ? is reflexive. QED
Also, we can now prove the stubborn ? -lemma:
Corollary 2.23 If A' F e : r, A' has satisfiable constraints, and A ? A', then
AHe:r.
Proof: Letting 5 be [],we see from Theorem 2.21 that (5o, B0, ro) = W0(A, e)
succeeds and there exists a substitution T such that
1. [j = S0T, except on new type variables of W0(A, e),
2. AHB0T,and
3. r = r0T
Now by Theorem 2.18, AS0UB0 ? e : To , so by Lemma 2.4, AS0TUB0T H e: r0T.
Using 1 and 3 above, this gives us A u B0T F e: r. Since by 2 above A H B0T,
we may use Corollary 2.12 to show that A H e: r QED
Finally, we obtain as a corollary the following principal typing result:
Corollary 2.24 Let A be an assumption set with
free type variables. If e is well typed with respect to
succeeds, (B?, ?) = close(A, B, r) succeeds, and the
satisfiable constraints and no
A, then (S,B,r) = W0(A,e)
typing A H e: a is principal.
Proof: Since e is well typed with respect to A and since A has satisfiable
constraints, by Lemma 2.15 there exists r such that A ? e : 7r. Hence we see
from Corollary 2.22 that (5, B, r) = W0(A, e) succeeds and there exists T such
that
52
1. [j = ST, except on the new type variables of W0(A, e),
2. AHBT,and
3. r=rT
Since AT ? BT, by Lemma 2.19 (B', a) = ctose(A, B, T) succeeds, a is of the
form Vo with B". r , and
o+ B' = (1
o+ a has no free type variables, and
o+ B" C B
By Theorem 2.18 and Lemma 2.17, we have A H e : a
Now let a' be an arbitrary type scheme such that A F e : ?? We need to
show that a >A a'. Suppose that a' >A p. Then by the definition of >A it
follows that (V-elim) may be used to derive A H e p. So by Corollary 2.22
again, there exists T' such that
1. [? = ST', except on the new type variables of W0(A, e),
2. A H BT', and
3. p = rT'.
Since B" C B we have A H B"T'. Notice also that all of the variables occurring
in B11 or in 7 are among the ??, so by restricting T' to the ? we obtain a
substitution [? := ? such that A H B11[c? := ? and p = r[a := ?. This
shows that VQ with B". r >A p, and hence that Vo with B" r >A a'. So
AHe: Va with B".r is principal. QED
2.5 Limitative Results
Recall that in our definition of close(A, B, r) in Section 2.3, we made use of
a function satisfiable(B, A) without indicating how it might be computed. We
address that omission in this section.
Given a set B of r-assumptions and an assumption set A, satisfiable(B, A)
returns true if B is satisfiable with respect to A (that is, if there exists a
substitution 5 such that A H BS) and returns false otherwise. Unfortunately,
the satisfiability problem turns out to be undecidable.
Theorem 2.25 Given an assumption set A and a set B of r -assumptions, it is
undecidable whether B is satisfiabte with respect to A
53
Proof: It is easy to reduce the Post Correspondence Problem (PCP) [HU79]
to the satisfiability problem. We present the reduction by means of an example.
Suppose we are given the PCP instance
xi			= 10			yi = 101
X2 = 011 Y2 = 11
X3 = 110 y? =
where ? denotes the empty string. We will use type constants 0, 1, and $ and a
right-associative binary type constructor ??. Define
Apcp =
p: (1			0)			(1 H 0 H 1),
p : (0			1 H 1)			(1			1),
p: (1 H 1 H 0 $) H
p: Va,Pwithp:??P.
p: V?,P with p: ? H
p: Vo,P with p: Q H
0 H a) H (1 H 0 H 1 H
1 H 1			a) H (1			1 H
1			0 H a) H
Now consider whether fp: a a) is satisfiable with respect to Apep
This will be true if and only if there is some r such that Apep ? p : r H
r But Apcp gives p precisely all types of the form 7r H iri, where 7r is
obtained by concatenating various Xj `5 and 7r? is obtained by concatenating the
corresponding y? ???9 Hence ?p : a H a) is satisfiable with respect to Apcp
precisely when the given PCP instance has a solution. QED
It is conceivable that there is some way to do type inference without using
function satisflable(B, A), but such hopes are quickly dashed by the following
corollary.
Corollary 2.26 Given an assumption set A and an expression e, it is undecid-
able whether e is well typed with respect to A
Proof: Again we use a reduction ftom PCP. Define Apcp as above, and
consider whether the expression (Af.Ax.f(f x)) p is well typed with respect to
Apcp.
Now, Af. Ax.f(f x) has principal type Va.(a H a) H (a H a). Hence
(Af.Ax.f(f x)) p is well typed with respect to Apcp if and only if p has some
type of the form r r, which in turn holds if and only if the given PCP instance
has a solution. 10 QED
Another easy corollary is that the instance relation >?A is undecidable.
Possibly ir and Ir' have a $ tacked on the end.
10We remark in passing that the expression (AJ.Ax.f(f x))p cannot be replaced by the simpler
expression Ax.p(p x) in this proof. The problem with the simpler expression is that the two
occurrences of p are not forced to have the same type.
54
Corollary 2.27 Given A, a, and r, it is undecidable whether a >?A T
Proof: Define Apcp as above; then
Va with p: a H a bool >Apcp bool
if and only if the given PCP instance has a solution. QED
It might appear that the key to all of these undecidability results is the neces-
sity of `guessing': for example, to determine whether fp : a H al is satisfiable
we must guess how a should be instantiated. This suggests that if we arrange
to eliminate such guessing, perhaps undecidability will be avoided.
To this end, we can define the class of coupled type schemes: a type scheme
Va? with C. r is said to be coupled if every type variable occurring in C occurs
also in r. For example, the type Va with p: a . a. bool used in the proof of
Corollary 2.27 is uncoupled. We furthermore say that an assumption set A is
coupled if it contains only coupled assumptions.
We also require the notion of a nonoverlapping assumption set. We say that
type schemes a and a' overlap if (after renaming to eliminate any common
bound type variables) their bodies are unifiable. Then we say that an assumption
set A is nonoverlapping if A contains no two assumptions x: a and x: ?? with
a and a' overlapping.
Finally we say that a type T is ground if it contains no occurrences of type
variables, and an assumption x: r is ground if r is ground.
If A is coupled and nonoverlapping and B contains only ground assumptions,
then no guessing is involved in verifying the satisfiability of B with respect to
A since B contains only ground assumptions, B is satisfiable if and only if
A ? B, and we can verify A ? B by "working backwards" in a completely
deterministic manner. For example, if
A = (c: char, c: Va with c: a seq(a))
then we can reason
A H (c: seq(seq(char))J
A ? (c: seq(char)?
A F fc: chari.
More formally, we can verify that A H B as follows:
55
while B $ f? do
choose x: T ill B
find an assumption x: V? with C . p in A
such that for some 5, PS =
if none, then answer `no';
B			--H			: ?J)uCS;
od;
answer `yes'.
Because of the restriction to nonoverlapping and coupled assumptions, there is
always a unique assumption to apply next, and B always contains only ground
assumptions. Notice, however, that if A = fc: V? with c: seq(c) . c ?, then an
infinite branch will be generated when we attempt to verify that A H tc: chari,
so our procedure is not guaranteed to terminate. One might imagine that such
infinite branches can somehow be detected and avoided, but, surprisingly, this is
not so.
Theorem 2.28 Given a coupThd, nonovertapping assnmption set A and a gro?nd
assumption x : T, it is undecidable whether A F x : T.
Proof: We reduce the problem of determining whether a deterministic Turing
Machine halts on empty input [HU79] to this problem. Suppose we are given a
Turing Machine M = (Q,?(),1?,to,1,B?,?qo,B,?q??), where
o+ Q is the set of states,
o+ ?O, 1? is the input alphabet,
o+ t(),1,B) is the tape alphabet,
o+ ?:QxtQ1,BJ?QxtQ1,B1xtL,R1,
o+ qo is the start state,
o+ B is the blank symbol,
o+ q? is the unique halting state.
The idea is to encode instantaneous descriptions (IDs) of M as types and to
define a set of type assumptions Ahalt so that Ahalt H h : p if and only if p
encodes an ID from which M eventually halts. We need just one identifier h, a
binary type constructor ??, and a set of type constants Q u to, 1, B, ?J.
We encode IDs as follows: OlBqlO is encoded as
H 1 H 0 H			q H (1			0			?),
56
and in general, for cr1 and cr? in ?O, 1, Bi*, crlqcr2 is encoded as
reverse			H
cri			q			T2,
where if OL = ....... Xn, n > 0, then cr = X1 X2 ...
Next, we observe that M eventually halts from ID if and only if either
o+ ID is a halting ID, or
o+ M eventually halts from the successor of ID.
We include assumptions in Ahalt to deal with these two possibilities. First, to
deal with halting IDs, we include
h : Vcr,P.cr H q?
Next we want to express" h : ID if h : successor( ID)". Suppose that ?q, X) =
Y, R). We model this by including
h : OL H q H			H ?) if h :			H cr) H H
which in our official syntax is
h: VQ? with h (YH cr) Hq' H ?.cr? q? H fi)
In addition, if x = B then we also include
h : cr H q H ? if h: (Y H 0)			H e.
Similarly, if ?(q, X) = (q', Y, L), then for each Z in the tape alphabet we include
h: (Z H cr) q (X H p) if h : cr H H Y H
and, if X =
h: (Z H cr) q e if h : cr			H Y H
It follows, then, that Ahalt F h : e H e if and only if M halts on e.
Furthermore, Ahalt is coupled and nonoverlapping. QED
In Section 2.6 we present a set of restrictions that do make the satisfiabil-
ity problem decidable. First, however, we digress to mention an application of
Theorem 2.28 to logic and logic programming.
57
2.5.1 A Logical Digression
As we remarked earlier, our type assumptions can be rephrased as Horn clauses
[Llo84J. For each identifier x, we introduce a unary predicate symbol Tx with
the intention that Tx(r) means x : r. Then the type assumption
x: Va with x: a, y : a H a. set(a)
is represented by the Horn clause
Tx(set(a)) & T?(a) A T?(a H a).
The essential property of the translation is this: if A* denotes the translation of
A, then
AH x:r
if and only if
A* U ffalse & Tx(r)i is unsatisfiable.
Furthermore, our definitions of coupled and nonoverlapping can be applied in the
obvious way to Horn clauses. So we have the following corollary to Theorem 2.28.
Corollary 2.29 It is undecidable whether a set of coupled, nonoverlappiny Horn
clauses is satisfiable.
This corollary has consequences for logic programming as well: the set of all
logic programs that never require backtracking in their execution includes the
class of all sets of coupled, nonoverlapping Horn clauses. Hence the possibility
of nontermination cannot be avoided in logic programming, even in situations
where no backtracking can arise.
2.6 Restricted Forms of Overloading
In this section, we impose restrictions on the forms of overloading allowed; our
goal is to make the satisfiability problem decidable, which in turn will make the
typability problem decidable.
We saw in Section 2.5 that our assumption sets are expressive enough to
encode the Post Correspondence Problem and the Halting Problem. But the
examples of overloading that we care about in practice do not require nearly so
much power. Consider the assumptions for ? our typical interesting example
of overloading:
char H char H bool,
real H real H bool,
?: Va with ? : a			a H bool. seq(a) H seq(a)			bool
<:Va,? with <: a Ha H bool, < : H bool.
(a x ?) H (a x ?) H bool
58
The effect of these assumptions may be stated thus: the types of < are of the
form r H T H bool; by the first rule r may be char, by the second rule r may
be real, by the third rule r may be seq(r') if r may be r1, and by the fourth
rule r may be r? x r11 if r may be T1 and T11. That is < has exactly those types
of the form T H T H bool where r is any type built from the constructors real,
char, seq, and x. In this situation, we can do better than our usual implicit
representation of the types for < in fact we could use the explicit representation
Vajchar,real,seq,xj?? H a H bool,
associating the constructor set (char, real, seq, x 1 with a to express the fact
that a may only be instantiated with types built from those constructors. Fur-
thermore, we will see that this explicit representation of the types of < is very
useful in solving the satisfiability problem. We now make these ideas precise.
Definition 2.5 We say that x is overloaded by constructors in A if the lcg of
x in A is of the form Va.r and if for every assumption x : V? with C. p in
A,
o+ p = r[a := x(P)], for some type constructor ?, and
o+ C = tx : r[a := PieP1.
Furthermore, we say that the type constructor set of x in A is
I A contains an assumption x: V? with C. T[a := x(P)] 1
For example, under the assumptions given above < is overloaded by constructors
and has type constructor set f char, real, seq,
Lemma 2.30 If x is overloaded by constructors in A with lcg Va.r and type
constructor set X,then A H x : p if and only if p is of the form r[a := 7r] and
7r is a type built from the constructors in X
Proof: The `if' direction is a straightforward induction on the structure of ir.
The `only if' direction is a straightforward induction on the length of the
derivation of A H' x : p. QED
Definition 2.6 We say that A is an overloading by constructors if
o+ every identifier overloaded in A is overloaded by constructors and
o+ for every constraint x : p in an assumption in A, x is overloaded in A and
p ? an tnstance of the lcg of x
59
We now argue that if A is an overloading by constructors, then the satis-
fiability problem can be solved efficiently. For simplicity, however, we restrict
satisfiable(B, A) to constraint sets B generated by W0; this is justified by the
fact that close calls satisfiable only on constraint sets generated by W0. Now,
if A is an overloading by constructors, then a simple inductive argument shows
that if (5, B, r) = w0(A, e), then B contains only constraints of the form x : p
where x is overloaded in A and p is an instance of the lcg of x. Hence we
restrict our attention to constraint sets of this form.
Let B be a constraint set containing only constraints of the form x : p where
x is overloaded in A and p is an instance of the lcg of x. Let x : p be a
constraint in B. By assumption, p = rx[a := 7r] where Va.rx is the icg of x in
A, so by Lemma 2.30, A H x : pS if and only if 7r5 is a type constructed from
Xx,the type constructor set of x. Examine ir; if it contains any type constructor
not in Xx, then B is unsatisfiable. Otherwise, 5 satisfies x : p if and only
if 5 instantiates all variables in ir to types constructed from the constructors
in Xx. In this way, the constraint x : p in B associates the constructor set
Xx with each variable occurring in p. Now, for each variable P in B, take
the intersection of all the constructor sets thus associated with P; this gives
explicitly the set of possible instantiations of p that satisfy B in particular,
there is some satisfying instantiation of p if and only if the intersection contains
a 0-ary type constructor. Hence, B is satisfiable if and only if every variable in
B has an associated constructor set containing a 0-ary type constructor. Clearly,
this procedure can be done in polynomial time.
There is a natural example of overloading for which the restriction to over-
loading by constructors is too severe. The example, due to Dennis Volpano, is
matrix multiplication: for matrices to be multiplied it is necessary that the el-
ements of the matrices can be multiplied and also added, for we need to form
inner products. Hence we would like to use the assumption
* : Va with + : a H a H a, * : a H a H a
matrnx(a) H matmx(a) H matrnx(a),
but this is not an overloading by constructors.
We conjecture, however, that the satisfiability problem remains decidable
when the second part of the definition of `overloaded by constructors' is relaxed
to
C?(x:r[a:=Pj] PiePi,
which permits the above matrix multiplication assumption. Further research into
the satisfiability problem is described in [VS91].
60
2.7 Conclusion
We have shown that overloading may be combined with Hindley-Milner-Damas
polymorphism in a natural way that preserves the principal typing property and
type inference. However, certain restrictions on overloading need to be imposed
to avoid undecidability.
Chapter 3
subtyping
In this chapter we develop the theory of polymorphism in the presence of both
overloading and subtyping. Our new type system is an extension of the type
system of Chapter 2, so this chapter will parallel the development of Chapter 2,
preserving as many of the results as possible.
3.1 The Type System
One approach to subtyping is to use explicit type conversions, thereby eliminating
the need to change the type system at all. For example, we can indicate that int
is a subtype of real simply by defining a conversion function c: int real. The
trouble with this approach is that it limits polymorphism. Consider, for example,
the function twice, defined as Af.Ax.f(fx). Intuitively, the application of twice to
a function g: real H int should be well typed. But if subtyping is achieved solely
through explicit type conversion, this is not so; indeed, for the application twiceg
to be well typed, we must change the definition of twice to Af.Ax.f(c(f x)). But
now twice cannot be applied to a function of type char H char. In general, the
use of explicit type conversions forces programs to be overspecialized.
Instead, our approach to subtyping is to augment the type system with a new
kind of assertion. In addition to typings e : a, we have inctusions r C r1. The
inclusion T C T1 asserts that r is a subtype of r'. Inclusions are incorporated
into the type system in four ways:
1. Inclusions may occur in constraint sets of type schemes.
2. Inclusions may occur in assumption sets.
3. There are new rules for proving judgements of the form A ? r C ??
4. Finally, the new typing rule
61
62
AFe:?
A ? r C T1
A H e:
links the inclusion sublogic with the typing sublogic.
3.1.1 Types and Type Schemes
Types are just as in Chapter 2; type schemes are now defined by
a:: Vo1,...,?n with Cl,...,Cm.T,
where each constraint Ci is either a typing x : p or an inclusion p C p'.
We say that a type is atomic if it is a type constant (that is, a 0-ary type
constructor) or a type variable.
3.1.2 Substitution and a -equivalence
A substitution 5 may be applied to an inclusion r C r', yielding the inclusion
(rS) C
All the lemmas about a -equivalence given in Section 2.1.2 carry over to our
richer set of type schemes, without modification.
3.1.3 The Typing Rules
A type assumption set A may now contain inclusions r C r' as well as typings
x : a. The notion of r -assumption is extended to include inclusions T C r1 as
well as typings of the form x : T.
All the typing rules given in Figure 2.1 are retained in the new system. In
addition, there are new rules given in Figure 3.1. The first five rules allow in-
clusion judgements to be proved. Rule (hypoth) allows inclusion assumptions
to be used; rules (reflex) and (trans) assert that C is reflexive and transitive.
Next, there are rules expressing the well-known monotonicities of the various
type constructors [Rey80,Car84,Rey85]. For example, H is antimonotonic in its
first argument and monotonic in its second argument. The name ((--H) H
compactly represents this information. Additional rules, such as (set(+)), will
be introduced as needed. The last rule, (C?), says that an expression of type r
has any supertype of r as well.
As an example, we derive the principal typing
fJHAf.Ax.f(fx): Va,Pwith ?C?a.(a?P)?(a?P).
We have
tP C a, f: a			?, x: a) H f: a H
(3.1)
63
(hypoth)
(reflex)
(trans)
A H r C r', if (r C T') E A
AFTCT
A H T C r'
A F r1 C r11
A H T C T11
A F T1 C r
A H p C p'
A F (r H p) C (T' H p1)
A H r C r1
A H seq(r) C seq(Y)
A ? r C T1
A F e : r1
Figure 3.1: Additional Rules for Subtyping
64
by (hypoth),
by (hypoth),
C a, f : a x : aJ H x a
fPCQ f:a?P, x:alH(fx):P
by (? -elim) on (3.1) and (3.2),
by (hypoth),
C a, f: a H			x: aJ H p c a
Ca, f: a H x: a) H (f x) : a
by (C?) on (3.3) and (3.4),
fPCQ f:a??, x:a)Hf(fx):p
by (H -elim) on (3.1) and (3.5),
fPCQ f:a?PJFAx.Afx):a?P
by (?? -intro) on (3.6),
fP C a) F Af.Ax.f(f x) (a P) H (a H
by (H -intro) on (3.7),
by (reflex), and finally
f)FAfAx.f(fx):V?PwithPC?a.(a?P)?(a?P)
(3.2)
(3.3)
(3.4)
(3.5)
(3.6)
(3.7)
(3.8)
(3.9)
(3.10)
by (V-intro) on (3.8) and (3.9).
Recall that, without subtyping, the principal type of Af. Ax.f(f x) is simply
Va.(a H a) H (a a). This illustrates that adding subtyping to a type system
has more pervasive effects than does adding overloading the principal type of
a program that uses no overloaded identifiers is unaffected by the presence of
overloading, but the principal type of every program is potentially changed by
the presence of subtyping.
3.1.4 The Instance Relation
The instance relation >A needs to be refined to account for subtyping. What
we want, essentially, is that a r if and only if A u (x: a) H x : r, where x
is any identifier not occurring in A.
Definition 3.1 (Va? with C. r) >A T1 ?f there ? a substitvtThn [a? r-] such
that
o+ AHC[a:=ir] and
o+ A H r[a? 7r] C r1.
65
3.2 Properties of the Type System
In this section we show that the properties of the type system of Chapter 2 are
not disturbed by the addition of subtyping.
We begin by showing a number of useful properties of the inclusion sublogic;
fortunately, inclusions have simpler behavior than do typings, so the proofs are
easier.
Lemma 3.1 If A H T C r', then AS H TS C T'S. Furthermore, the demvation of
AS H rS C r1S uses the same sequence of steps as the dernvat?on of A H r C r1.
Proof: By induction on the length of the derivation of A F T C r1. Consider
the last step of the derivation:
(hypoth) The derivation is simply A ? r C r' where (T C T') E A. So (TS C
r'S) ? AS, and AS F rS C YS by (hypoth).
(reflex) By (reflex), AS F rS C TS
(trans) The derivation ends with
A ? r C r'
A H r' C r'1
A H T C r"
By induction, AS F rS C r'S and AS H T'S C r11S, so by (trans),
AS F TS C r"S
(+)) The derivation ends with
A H r1 C r
A H p C PI
A H (r H p) C (r' H PI)
By induction, ASH T'S Cr5 and ASH pS C p'S, so by ((--H) H
AS H (rS H p5) C (r'S H p15)
Other type constructors are handled in the same way. QED
Lemma 3.2 If A u fx : al H r C r1, then A H r C r1
Proof: By a straightforward induction on the length of the derivation of Au (x:
a) H r C r1. QED
Lemma 3.3 If A H r C r',then			A u B H r C r'
66
Proof: By induction on the length of the derivation of A H 7 ? r'. QED
Lemma 3.4 If AUB ? 7 C 7' and A H B, then A H 7Cr'
Proof: Yet another straightforward induction, this time on the length of the
derivation of AuBHrCr'. QED
Now we show that the properties proved in Section 2.2 still hold in our new
system with subtyping.
Here is the counterpart to Lemma 2.4:
Lemma 3.5 If A H e : CT then AS H e: aS. Furthermore, gtven any derivation
of A H e : CT, a derivation of AS H e : CTS can be constructed that uses the same
sequence of steps except that it inserts a (=a) step after each (V -intro) step.
Proof: The proof of Lemma 2.4 suffices, except that we must consider the case
when the derivation of A H e : CT ends with (C).
(c?) The derivation ends with
QED
AHe:r
A H r C r'
A F e :
By induction, AS H e : 75, and by Lemma 3.1, AS H rS C r'S. So by
(c), ASHe:r'S
Again, our major goal is to prove a normal-form theorem for derivations.
Define rule (V-elim') as in Chapter 2 (see page 26), and say A H' e : CT and
A H' r C r' if these can be derived in the system obtained by deleting (V-
elim) and replacing it with (V-elim'). Because H' does not restrict the inclusion
sublogic in any way, the following lemma is immediate.
Lemma 3.6 A H r C r' if and only if A F' r C r'.
Here is the counterpart to Corollary 2.5:
Corollary 3.7 If A H' e : CT then AS H' e : CTS. Furthermore, given any deriva-
tion of A H' e : CT, a derivation of AS ?` e : CTS can be constructed that uses the
same sequence of steps except that it inserts a (--H=?) step after each (V-intro) step.
The counterparts to Lemmas 2.6, 2.7, and 2.8 are given next; their straight-
forward proofs are given in Appendix A.
Lemma 3.8 If x does not occur in A, x ? y, and A u (x : a? K' y : 7, then
A ?` y : 7.
67
Lemma 3.9 If A H' e : a then A u B H' e : a, provided that no identifier
occurring in B is A -bound or let-bound in e.
Lemma 3.10 Let B be a set of r -assumptions. If A u B Y e : a and A F' B,
then A ?? e : a.
With these lemmas, we can now show the counterpart to Theorern 2.9.
Theorem 3.11 AH e : a if and only if AH' e: a
Proof: The proof of Theorem 2.9 suffices, except that when the derivation
of A H e : a ends with (c?), we use the fact that A H r C r' if and only if
AH'rCr' QED
As in Chapter 2, we get the following corollaries:
Corollary 3.12 If x does not occur in A, x $ y, and A u fx : al H y : r,then
A?y:r
Corollary 3.13 If A ? e : a then A u B F e : a, provided that no identifler
occurring in B is A -bound or let-bound in e
Corollary 3.14 Let B be a set of r -assumptions. If A u B H e : a and A H B
then A ? e: a.
Lemma 3.15 If A F e : a then no identifier occurring in A is A -bound or
let-bound in e.
Corollary 3.16 If A H e : a then A u B F e : a, provided that all identifiers
occurnng in B also occur in A.
As in Chapter 2, we define the notion of an assumption set with satisfiable
constraints; both of the lemmas about assumption sets with satisfiable constraints
carry over without change.
Lemma 3.17 If A has satisfiable constraints and A ? e : a, then there exists a
type r such that A F e: r
Lemma 3.18 If A has satisfiable constraints and there exists a substitution [ot
r] such that A ? C[? 7r], then A u tx : Va? with C. r ? has satisfiable
constraints.
Algorithm Wos and the new close given below make certain demands about
the inclusions in the assumption sets that they are given. In particular, they
disallow assumptions like int C (int H int) in which the two sides of the inclusion
do not have the same `shape'. Furthermore, they disallow `cyclic' sets of inclusions
such as bool C int together with int C bool. The precise restrictions are given in
the following definitions. A constant inclusion is an inclusion of the form c C d
where c and d are type constants (i.e. 0-ary type constructors).
68
Definition 3.2 An asstmption set A is said to have acceptable inclusions if
o+ A contains only constant inclusions and
o+ the transitive closure of the inclusions in A is antisymmetric.
We now establish a few properties of assumption sets with acceptable inchi-
510115. Recall that atomic types are type constants or type variables.
Definition 3.3 Types T and r' have the same shape if either
o+ r and r' are atomic or
o+ r=x(ri,...,Tn), Y=?(???...?r?I)? where ? isan n-arytypeconstruc-
tor n > 1, and for all i, ri and ?j? have the same shape.
This definition appears in [Mit84] under the name `matching', and also in [Sta88J
and [FM9oj. Note that the `same shape' relation is an equivalence relation.
Define an atomic inclusion to be an inclusion of the form r C r1 where r and
TI are atomic. Any constant inclusion is an atomic inclusion, so the following
lemmas apply to any assumption set with acceptable inclusions.
Lemma 3.19 If A contains only atomic inclusions and A H T C r' then r and
r' have the same shape.
Proof: By induction on the length of the derivation of A H r C r1. QED
Lemma 3.20 If A contains only atomic inclusions and A H r p C T1 . PI
then A ? r' C r and A H p C PI
Proof: By induction on the length of the derivation of A F T H p C r'
p'. Consider the last step of the derivation. Since A contains only atomic
inclusions, the last step cannot be (hypoth). Hence the last step is (reflex),
(trans), or ((--H) H (+)). In the (reflex) and ((--H) H (+)) cases, the result
follows immediately. Suppose the derivation ends with (trans):
A ? (T H P) C ?
A H ? C (T1 H
A H (r H P) C (r1 H
By Lemma 3.19, T H P and ir have the same shape, so 7r is of the form irI H
By induction, we have A ? ?` C r, A H P C ?ll, A F T1 C 7rI and A H irIl c P1
Hence by (trans) we have A H TI C T and A ? P C P1. QED
In the same way, one can prove similar lemmas for the other type constructors.
Lemma 3.21 If A has acceptable inclusions, A ? T C T1 and A H r1 C r then
T = T1
69
Proof: Since A contains only atomic inclusions, r and TI have the same
shape. Hence we may use induction on the structure of r and r'. If r and r'
are atomic, then both r C r' and T1 C r are in the reflexive transitive closure of
the inclusions in A. Since by assumption the transitive closure of the inclusions
in A is antisymmetric, it follows that r =
Now suppose that T = T1 H T2 and r' = H T21 By Lemma 3.20, we have
A H 4 C ri, A ? r2 C r21, A ? Ti C r11, and A H r21 C r2. So by induction,
ri = 4 and T2 = r21.
Other type constructors are handled similarly. QED
3.3 Algorithm W05
Algorithm Wos is given in Figure 3.2. The algorithm differs from W0 in two
ways. First, there is a small change to the let case; close(A, B, r) now returns
a substitution 5 as well as a constraint set B' and a type scheme a. The
idea is that close may discover that some of the type variables in B can be
instantiated in only one way if B is to be satisfied; any such instantiations are
returned in the substitution ? ? The major departure from W0 is in the case
of an application e1c". Intuitively, W08 returns the smallest possible type for
an expression. Normally, such a type can be used in a derivation in place of a
larger type. The one exception is in the (H -elim) case, where the type of the
argument e" is required to be the same as the domain of the function e'; in this
case, it may be necessary to pass from the type found by W08 for the argument
e" to a supertype.
We now discuss close. For now, we trivially modify the close of Figure 2.3
so that it always returns the identity substitution. In Section 3.6 we will give
a fancy close and prove that it satisfies the two lemmas needed to establish the
soundness and completeness of W08
3.4 Properties of W05
3.4.1 Soundness of W08
The soundness of close is given by the following lemma.
Lemma 3.22 If (5, B', a) = close(A, B, r) succeeds, then for any e, if A u B H
e : r then AS u B' H e : a. Also, every identifier occurring in B' or in the
constraints of a occurs in B
1 ?0 could also be modified to use a version of close that returns a substitution, but without
subtyping it doesn't seem important to do so.
70
W08(A, e) is defined by cases:
1. e is x
if x is overloaded in A with lcg Va.?,
return ([],tx:r[c-:=PJ1,r[?:=Th) where p arenew
else if (x: V?with C.T)EA,
return ([],C[?:=Th,r[?:=Th) where ? are new
fail.
else
2. e is ?????
if x occurs in A, fail.
let (Si,Bi,ri) = Wos(AU (x : al,e') where o is new;
return (Si,Bi,aSi H ri)
3. e is e'e"
let (Si,Bi,ri) = W0s(A,e');
let (52, B2, r2) = W08(AS1, e");
let 53 = unifit(T152,? H ?) where ? and ? are new;
return (s1s2s3,B1s253uB2s3u fr253 C ?531,P?3)
4. e is let x = e' in e'1
if x occurs in A, faiL
let (51,B1,r1) =
let (52,B11,ai) = close(AS1,Bi,ri);
let (53, B2, T2) = Wos(ASiS2 U fx : ?`), e11)
return (S1S2S3,B1,S3 uB2,r2).
Figure 3.2: Algorithm ??os
71
Next we give the soundness of W08; the proof is very similar to the proof of
Theorem 2.18.
Theorem 3.23 If (5, B, r) = W08(A, e) succeeds, then AS u B F e : r. Fur-
thermore, every identifler oCcurring in B is overloaded in A or occurs 2n some
constraint of some assumption in A
3.4.2 Completeness of Wos
The properties of close needed to prove the completeness of W05 are extracted
more carefully here than they were in Chapter 2, thereby giving close more
freedom to do type simplification. This freedom will be exploited in Section 3.6.
Lemma 3.24 Suppose that A has acceptable inclusions and AR H BR. Then
(5, ??, a) = close(A, B, r) succeeds and
o+			if A			has no free type variables then B' =
o+ fv(a) C fv(AS), and
o+ there exists T such that
1.			R=ST,
2.			ARHB'T,and
3.			aT>??TR.
The next two lemmas have straightforward inductive proofs.
Lemma 3.25 If (5, B', a) = close(A, B, r) succeeds, then every type variable oc-
curring free in 5, B', or a occurs free in A, B, or T or else is generated by
the new type variable generator.
Lemma 3.26 If (5, B, T) = Wos(A, e) succeeds, then every type variable occur-
ring in 5, B. or r occurs free in A or else is generated by the new type variable
generator.
The definition of A ? A' needs to be revised to account for inclusions; we
simply demand that A and ?? contain the same inclusions.
Definition 3.4 Let A and A' be assumption sets. We say that A is stronger
than A', written A ? A', if
1. A' H x: r implies A F x : r,
2. id(A) c id(A'), and
3. A and A' contain the same inclusions.
We now show the completeness of W05
72
Theorem 3.27 Suppose that A' H e : r, A' has satisfiable constraints, AS ? A'
and A has acceptable inclusions. Then (5o, B0, ro) = Wos(A, e) succeeds and there
exists a substitution T such that
1. 5 = S0T, except on new type variables of Wos(A, e),
2. ASHB0T,and
3. AS ? r0T C r
Proof: By induction on the structure of e. By Theorem 3.11, A' H' e: r
eisx
By the definition of AS ? A', we have AS ?` x r. Without loss of gener-
ality, we may assume that the derivation of AS H' x : r ends with a (possi-
bly trivial) use of (V-elim') followed by a (possibly trivial) use of (c?). If
(x:VcwithC.p)eA,then(x:VPwitbC[o?:=ThS.p[a:=ThS)?AS,
where ? are the first distinct type variables not free in Va with C. p or
in 5. Hence the derivation AS ?? x: T ends with
(x: VP with C[a-:=ThS.p[o-:=ThS)eAS
AS F' C[a := P]S[P :=
AS H' x : p[a? := P]S[P :=
AS H' p[a := ThS[P :=			r
AS F' x :
We need to show that (5o, B0, ro) = W08(A, x) succeeds and that there
exists T such that
1. 5 = S0T, except on new type variables of ??os(A, x),
2. ASHB0T,and
3. AS?r0TCr
Now, Wos(A,x) is defined by
if x is overloaded in A with Icg Vc.r,
return ([],?x: P]), r[a? Pi) where ? are new
else if (x: Va? with C.r)?A,
return ([],C[?			P], r[a			P]) where ? are new
else faiL
If x is overloaded in A with lcg V?.p0, then (50,B0,r0) = Wos(A,x)
succeeds with So = [], B0 = tx : po[? := ??, and ro = po[? := ?, where
are new. Since V?.p0 is the lcg of x, ? are the only variables in po and
there exist ? such that po[? := = p. Let
73
Then
So
1.
To',
<? definition»
po[?			6J(S ?			ThS[P :=
only ? occur in po[? :=
po[?			ThS[P :=
only ? occur in po »
poW :=			:= ThS[P
only ? occur in po »
po[?			ThS[P :=
by above»
p[o? := P]S[? :=
S0T = 5 e			ThS[P :=			= 5, except on ?. That is,
S0T = 5, except on the new type variables 0 Wos(A, x)
2. Since B0T = fx : ToTi = fx : p[c := ThS[P := r]J, it follows that
AS H B0T
3. We have ToT = p[a ThS[P r] and AS F p[a ThStp? ? c ?,
so AS H ToT C T
If x is not overloaded in A, then (5o, B0, To) = Wos(A, x) succeeds with
So = [], B0 = := ?, and To = p[a? := ?, where ? are new. Observe
that [a?:=?(S?[?:=?) and [a:=ThS[P?:=?-] agree on C and on p.
(The only variables in C or p are the o and variables e not
among or ?. Both substitutions map oj :, 7rj and e'.'
Let T be S?[?:=?]. Then
1. SoT=S?[?:=r?]=S,excepton ?. That is, SoT=S,excepton
the new type variables of Wos(A, x)
2. Also,
Hence AS H B0T
B0T
definition»
by above observation»
C[Q := ThS[P :=
74
3. Finally,
r0T
<? definition»
? [6
 by above observation »
p[Q? := ThS[P
Since AS H p[a? := ThS[P := 7r?] C T, we have AS ? r0T C r
o+ eisAx.e'
Without loss of generality, we may assume that the derivation of ?` H' e : r
ends with a use of (?+ -intro) followed by a (possibly trivial) use of ( C?):
A' u tx ??J ?? :
A' H' Ax.e' : r' H r1,
A' ?? (Y			r11) C r
A' ??			: r
where x does not occur in A'
We must show that (5o, B0, ro)			W0s(A, Ax.e') succeeds and that there
exists T such that
1. 5 = S0T, except on new type variables of W0s(A, Ax.e'),
2. ASHB0T,and
3. ASHr0TCr
Now, W08(A, Ax.e') is defined by
if x occurs in A, fail.
let (S1,B1,r1) w08(A U ?x : a),c') where a is new;
return (5i, B1, aS? ri).
Since x does not occur in A' and (by AS ? A') id(AS) C id(A'), it
follows that x does not occur in AS. This implies that x does not occur
in A, so the first line does not fail.
Now we wish to use induction to show that the recursive call succeeds. The
new type variable a is not free in A, so
AS u (x : r'1 = (A u fx : &?)(S e [a :=
By Lemma3.18, A'Ufx : r?? has satisfiable constraints. Next we argue that
ASu(x:YJ?A'ufx:Y1. Clearly, ?d(ASufx:Y1)c?id(A'ufx:Y1),
and AS u tx : r?) and A' u fx : ??? contain the same inclusions. Now
suppose that A' u tx : r'i H y : p. If y # x, then by Corollary 3.12,
75
A' H y : p. Since AS ? A' we have ASH y : p and then by Corollary 3.13,
AS u fx : 7'J H y : p On the other hand, if y = x, then the derivation
A' u tx : T'? H' y : p must be by (hypoth) followed by a (possibly trivial)
useof(C):
u fx: 711 H' x
A' u fx : ?`l H' r' C p
A' u tx: ?`1 H' x : p
Since AS ? A' AS and A' contain the same inclusions. Therefore,
ASu fx : r'J H' 7' c p, so by (hypoth) followed by (C), ASu fx: Y? H'
x : p. Finally, A u (x : aJ has acceptable inclusions. So we have
--H A' u fx : 7?J H e' : 7",
--H A' u (x : 7'1 has satisfiable constraints,
--H (AU(x :a))(Se[a:= r']) ? A'U(x : ?1, and
--H A u fx : a) has acceptable inclusions.
So by induction, (S1,B1,r1) = Wos(A u fx : a),e') succeeds and there
exists T1 such that
1.			Se[a :=			= S1T1, except on new variables of Wos(AU fx
2. (AUfx :a))(S?[a:=Y])HB1T1, and
3. (A u fx : a))(S e [a := 7'j) H r1T1 C r"
So (So,Bo,ro) = W08(A,Ax.e') succeeds with So = St, B0 = B1, and
= aSi H
Let T be T1. Then
1. Observe that
S0T
--H			? definition»
S1T1
by part 1 of the use of induction above»
5 e [a := 7'], except on new variables of Wos(A u (x: a), e')
definition of ?
5, except on a.
Hence S0T = 5, except on the new type variables of Wos(A U fx
a), e') and on a. That is, S0T = 5, except on the new type variables
of W08(A, Ax.e').
76
2.
3.
B0T = B1T1 and, by part 2 of the use of induction above, we have
AS u fx : T1) ? B1T1. By Theorem 3.23, every identifier occurring
in B1 is overloaded in A u (x : al or occurs in some constraint of
some assumption in A u fx : aJ. Since x does not occur in A and a
has no constraints, this means that x does not occur in B1. Hence
Corollary 3.12 and Lemma 3.2 may be applied to each member of
B1T1, yielding AS F B1T1.
Finally,
r0T
definition»
aS1T1 H r1T1
 a is not a new type variable of W08(A u fx: al, e') »
a(S ? [a := r'J) T1T1
definition of ?
r1T1.
Now by part 3 of the use of induction above, ASufx: r'1 H r1T1 C r",
so by Lemma 3.2, AS ? r1T1 C r". Since by (reflex), AS F r' C T1
it follows from ((--H) H (+)) that AS F (r' H riT1) C (r' H r"). In
other words, AS H r0T C (r' H r"). Next, because ?? H H ?1?) c
r and AS ? ??, we have AS H (Y H r") C r. So by (trans) we have
ASHT0TCT
o+ eise'e11
Without loss of generality, we may assume that the derivation of A' H' e : r
ends with a use of (H -elim) followed by a use of (C?):
A' H' e' : H T11
?? ?? e11 : r1
A' ?? e' e" : T11
?? ?? T11 C T
A' ?? e' e" : r
We need to show that (5o, B0, ro) = Wos(A, e'e") succeeds and that there
exists T such that
1. 5 = S0T, except on new type variables of Wos(A, e'e"),
2. AS?B0T,and
3. ASHr0TCr.
Now, Wos(A, e'e") is defined by
77
let (S1,B1,r1) = W08(A,e');
let (S2, B2, r2) = W08(AS1, e")
let S3 = ttnif?(riS??,a P) where Q and P are new;
return (sis2s3, B1S2S3 u B2S3 u fr2S3 c aS3J, PS3)
By induction, (Si, B1, r1) = W08(A, e') succeeds and there exists T1 such
that
1. 5 = S1T1 except on new type variables of Wos(A, e'),
2.			ASHB1T1,and
3.			AS H r1T1 C			H
Since A has acceptable inclusions, AS contains only atomic inclusions.
Hence by Lemma 3.19, r1T1 is of the form p H p'? and by Lemma 3.20,
we have AS H r1 C p and AS F p' C r1,
Now AS = A(S1T1) = (AS1)T1, as the new type variables of W0s(A, e') do
not occur free in A. So by induction, (52, B2, r2) = Wos(ASi, etl) succeeds
and there exists T2 such that
1. T1 = S2T2, except on new type variables of Wos(ASi, e"),
2. (A51)T1 ? B2T2, and
3. (A51)T1 H T2T2 C r1
By Lemma 3.26, the new type variables a and ? do not occur in A, Si,
B1, Ti, 52, B2,or r2. So consider T?O[a,P:=?,?1]:
(r152)(T2 ? [a,P := P,P1J)
--H ? a and P do not occur in r1S2 »
r152T2
--H ? no new type variable of W0s(ASi, e") occurs in Ti »
T1T1
--H <? by above»
P
In addition,
(a H P)(T2 ? [a,P :=
--H			? definition of 0
p H p1
Hence 53 = unify(rjS2, a ?) succeeds and there exists T3 such that
T2o [a,p := P,P1J = S3T3.
So (50,B0,r0) = W08(A,c1e11) succeeds with So = 515253, B0 = B15253u
B253 u (T2S3 C aS?l, and To = PS3.
Let T be T3. Then
78
1. Observe that
S0T
definition»
51 S2S3T3
by above property of unifier 53 »
5152(T2 ? [a,P
 a and p do not occur in S1S2 »
S1S2T2, except on a and ?
by part 1 of second use of induction and since the»
 new variables of W0s(ASi, e") don't occur in Si »
S1T1, except on the new type variables of ??os(AS1, e")
by part 1 of the first use of induction above»
5, except on the new type variables of Wos(A, e').
Hence we see that S0T = 5 except on a, on ?, on the new type vari-
ables of Wos(ASi, e?), and on the new type variables of W08(A, e').
That is, S0T = 5 except on the new type variables of ?V08(A, e'e").
2. Next,
3.
B0T
definition»
B15253T3 u B253T3 u tT253T3 C aS3T3i
by above property of unifier 53 »
B152(T2 ? [a, P := p, p']) u B2(T2 ? [a, P := p,
Ufr2(T2 ? [a,P := p,p']) C a(T2 ? [a,P := P,P1])1
a and p donotoccurin B152, B2,or T2 »
B1S2T2 u B2T2 u fr2T2 C pJ
by part 1 of second use of induction and since the»
new variables of Wos(ASi, e") don't occur in `3i »
B1T1 u B2T2 u fT2T2 C
By part 2 of the first and second uses of induction above, AS H B1T1
and AS H B2T2. By part 3 of the second use of induction above,
AS H T2T2 C r1. Also, we found above that AS H r' C p So by
(trans), AS H r2T2 C p. Therefore, AS H B0T
Finally,
r0T
definition»
p53T3
by above property of unifier 53 »
p(T2 ? [a,P :=
definition of ?
PI
79
Now, AS H p? C r', and, since A' F r" C T and AS ? ??, also
AS H r" C r. So it follows from (trans) that AS F T0T C r
o+ eisletx=e1ine11
Without loss of generality we may assume that the derivation of A' H1 e : r
ends with a use of (let) followed by a (possibly trivial) use of (C?):
A' F' e' : a
A' u fx a) F' e" : r1
A! H' let x = e1 in e11 : T1
A' H1 r' C r
A' H' let x = e1 in e" : r
where x does not occur in ??
We need to show that (5o, B0, ro) = W0s(A, let x = e' in e") succeeds
and that there exists T such that
1. 5 = S0T, except on new type variables of ?V03(A, let x = e? in e'1),
2. ASHB0T,and
3. ASFr0TCr.
Now, W0?(A,let x=e'in e") is defined by
if x occurs in A, fail.
let (S1,B1,ri) = Wos(A,c')
let (S2, B11,a1) = close(AS1, B1, ri)
let (S3, B2,r2) = W0?(As1s2 U fx : uil,e11)
return (S15253,B1,83 uB2,r2).
Since AS ? A' x does not occur in AS or in A. So the first line does
not fail.
Since ?? has satisfiable constraints, by Lemma 3.17 there exists r'1 such
that A' H e' : ril. Hence by induction, (5i, B1, r1) = W0s(A, e') succeeds
and there exists T1 such that
1. 5 = S1T1, except on new type variables of ??os(A, e'),
2. ASHB1T1,and
3. AS H r1T1 C r"
By 1 and 2 above, we have (A51)T1 H B1T1. Since AS1 has acceptable
inclusions, by Lemma 3.24 it follows that (52,B1,,a1) = close(ASj,B1,r1)
succeeds, fi;(ai) C fv(A5152), and there exists a substitution T2 such that
T1 = S2T2 and (A51)T1 H B1,T2.
80
Now, in order to apply the induction hypothesis to the second recursive call
we need to show that
ASu (x : a1T21 ? A'u (x : a).
There are three parts to this:
1. A'U(x : a) H y : p implies ASu fx : a1T2) H y : p
2. id(ASUfx:a1T2))C id(A'ufx:a)),
3. AS u fx : a1T2) and A' u fx : a) contain the same inclusions.
The second and third parts are quite simple; we show them first. By
Lemma 3.22 and Theorem 3.23, td(ai) C id(B1) C ?d(A). Hence
c
c
?d(AS u fx : a1T2))
? by above»
id(AS) u fx)
AS ? A'»
id(A') u fx)
id(A'u tx: a)),
showing 2.
Since AS ? A' it follows that AS u fx : a?T2) and A' u fx : a) contain
the same inclusions, showing 3.
Now we show 1. Suppose that A' u fx : a) H y : p. If y # x, then by
Corollary 3.12, A' H y: p. Since AS ? A' we have AS H y : p and then
by Corollary 3.13, ASU (x : aiT2) H y :
If, on the other hand, y = x, then our argument will begin by establishing
that A' He': p. By Theorem 3.11 we have A'u tx : a) H' x : p and we
may assume that the derivation ends with a use of (V-elim') followed by
a use of ( C): if a is of the form Vp- with C. p' then we have
x : V? with C. p' e A' u fx : a)
A' u fx : a) H' C[P := 7r?]
A' u (x : a) F' x : p'[P := 7r]
A' u (x: a) H' p'[? := 7r?] C p
A' u fx : a) H' x : p
It is evident that x does not occur in C (if x occurs in C, then the
derivation of A' u fx a) H' C[P := ir] will be infinitely high), so by
Corollary 3.12 applied to each member of C[P := ir], it follows that A' H
7r?]. Also, by Lemma 3.2, A' H p'[P := 7r?] C p. Therefore the
81
derivation A' ? : V? with C. p' may be extended using (V -elim) and
A'He': VP with C.p'
A' H C[p :=
A' ? e' : p'[? 7r--H]
A' H p'[p 7r?j C p
A' H e' : p
So by induction there exists a substitution T3 such that
1. 5 = S1T3, except on new type variables of H%s(A, e'),
2. ASHB1T3,and
3. ASHr1T3Cp.
By 1 and 2 above, we have (AS1)T3 ? B1T3, so by Lemma 3.24 it follows
that there exists a substitution T4 such that
1. T3=S2T4,
2. AS1ThFB1,T4,and
3. a1T4 >As1Th T1T3
Now,
AS1 S2T2
by first use of Lemma 3.24 above»
AS1T1
by part 1 of the first use of induction above»
AS
by part 1 of the second use of induction above»
A51T3
by second use of Lemma 3.24 above»
AS1 S2T4
Hence T2 and T4 are equal when restricted to the free variables of AS1 52.
Since, by Lemma 3.24, fr(a?) C fv(AS1S2), it follows that a1T2 = a?Th.
So, by part 3 of the second use of Lemma 3.24 above,
a1T2 >?As r1T3.
Write a1T2 in the form Va with D. ?. Then there exists a substitution
? such that
AS H D[a :=
and
AS ? := C r1T3.
82
Using Corollary 3.13 and Lemma 3.3, then, we have the following derivation:
ASUfx:a1T2JHx: VQwith D.?
by (hypoth),
by above,
by (V-elim),
by above,
by(C?),
AS u (x : a1T21 F D[? :=
ASu fx : a1T21 F x:			:= ff1
AS u fx : a1T21 H ?[a := C r1T3
AS u fx : a1T21 F x : r1T3
AS u fx : a1T2? F T1T3 C p
by part 3 of the second use of induction above, and finally
ASu fx :a1T2lF x:p
by (C). This completes that proof that AS u (x : a1T2i ? A' u fx : al,
which is the same as
(AS1S2 u fx : a1J)T2 ? A' u fx : a).
Because A' F e' : a and A' has satisfiable constraints, it is easy to see
that the constraints of a are satisfiable with respect to A'. Hence by
Lemma 3.18, A' u fx : a) has satisfiable constraints.
Finally, AS1S2 u (x : a?) has acceptable inclusions.
This allows us to apply the induction hypothesis a third time, showing that
(S3,B2,r2) = Wos(A5152 u fx : ai),e") succeeds and that there exists T5
such that
1. T2 = S3T5, except on new variables of W08(AS?S2 U fx : a?),e11),
2. ASU (x : aiT2) H B2T5, and
3. AS u tx : aiT2) H T2T5 C T'.
So (So,Bo,r0) = W08(A,let x = e'in e") succeeds with So = 515253,
B0 = B1,53 u B2, and r0 =
Let T be T5. Then
83
1. Observe that
S0T
<? definition»
Si S2S3T5
? part 1 of third use of induction; the new variables»
of Wo8(ASiS?Ufx:ai1,e11) don't occur in S1S2 »
S1S2T2, except on new variables of W08(AS1S2 u fx : aij, e")
by the first use of Lemma 3.24 above»
S1T1
--H by part 1 of first use of induction»
5, except on new variables of Wos(A, e').
So S0T = 5, except on new variables of W08(A, let x = e' in e11).
2. Next,
3.
B0T
definition»
B11S3% u B2T5
by part 1 of third use of induction and Lemma 3.25»
B11T2 u B2T5
By the first use of Lemma 3.24 above, AS F B11T2. By part 2 of the
third use of induction above, AS u fx : a1T21 F B2T5. By Theo-
rem 3.23, every identifier occurring in B1 occurs in A. So, since x
does not occur in A, x does not occur in B1. By Lemma 3.22, ev-
ery identifier occurring in the constraints of ?? occurs in B1 . Hence
x does not occur in the constraints of ??. By Theorem 3.23, every
identifier occurring in B2 is overloaded in AS1S2 u tx : ?? or occurs
in some constraint of some assumption in AS1S2 U f x : ail Since
x does not occur in AS1S2 or in the constraints of aj, it follows
that x does not occur in B2. Hence Corollary 3.12 and Lemma 3.2
may be applied to each member of B2T5, yielding AS H B2T5. So
AS H B0T
Now, r0T = r2T5 and by part 3 of the third use of induction above
and by Lemma 3.2, we have AS H r0T C T1 Also since ?? H r1 C r
and since AS ? A' it follows that AS F ?` c T So by (trans),
AS H T0T C T
QED
Theorem 3.27 gives as an immediate corollary the completeness of W0?:
Corollary 3.28 If AS F e : r, AS has sat?sflable constraints, and A has ac-
ceptable inclusions, then (5o, B0, To) = Wos(A, e) succeeds and there exists a sub-
stitution T such that
84
1. 5 = S0T, except on new type variables of Wos(A, e),
2. AS?B0T,and
3. ASHr0TCr.
Finally, we get the following principal typing result:
Corollary 3.29 Let A be an assumption set with satisfiable constraints, accept-
able inclusions, and no free type variables. If e is well typed with respect to A,
then (5, B, r) = W08(A, e) succeeds, (5', ??, a) = close(A, B, r) succeeds, and the
typing A ? e: a is principal.
3.5 An Example Assumption Set
In this section we define an example assumption set, A0, which will be used in
a number of examples in the remainder of the thesis. A0 is given in Figure 3.3.
We make a few remarks about A0.
o+ A0 has satisfiable constraints, acceptable inclusions, and no free type vari-
ables, so Wos can be used to infer principal types with respect to A0.
o+ Type matrix is intended to denote the set of all real 2 x 2 matrices. The
operators +, --H and * denote matrix addition, subtraction, and multipli-
cation respectively. 0 denotes the zero matrix and 1 denotes the identity
matrix.
o+ Because of the undecidability of equality of functions, it is common to give
--H a weaker type then we have given. Using overloading, one can give =
precisely those types for which equality is decidable. 2 Whether applying
--H to functions should be viewed as a type error or not is debatable.
o+ The presence of int C real makes fewer overloadings necessary. In partic-
ular, it is not necessary to include the overloadings 0 : real and 1 : real,
since these typings follow from 0 : int and 1 : int. Note however that
both + : int int H int and + : real H real H real are still
needed. (From int C real and + : real H real H real, it follows that
+ : int H int H real, but it does not follow that + : int H int H int.)
2 For example, equality is decidable on sequences provided that it is decidable on the type of
the elements of the sequences. This fact is reflected by the typing
= : Va with = : a			a			bool. seq(a)			seq(a)			boot
85
?nt C real
fix :			H a)			a,
if : Va.bool H OL H a H a,
--H : Va.a H a bool,
0: int, 0: matrix,
1 : int, 1 : matrix,
2: int,
o+ real,
+ : int H int H int, + : real H real real,
+ : matrix H matrix H matrix,
--H : int H int int, --H : real H real real,
--H : matrix matrix matrix,
A0 = * : int H int H int, * : real H real real,
* : matrix H matrix H matrix,
o+ : int ?int ?int,
: real real real,
even? : int H bool,
true : bool, false : bool,
cons : Va.a			seq(a) H seq(a),
car : Va.seq(a) H a,
cdr : Va.seq(a)			seq(a),
nil : Va.seq(a),
null? : Va.seq(a) H bool,
real H real H bool < char H char H bool,
_ Va with < : a H a bool. seq(a) H seq(a) H bool
Figure 3.3: Assumption Set A0
86
We use two different symbols for division: + denotes truncating integer
division; I denotes real division. One might propose instead that / be
overloaded to denote both truncating integer division and real division,
but it would be a design mistake to do so. For consider the expression 3/2
as a real value. Since 3 and 2 are integers, we could use truncating integer
division, yielding the integer 1, which gives the real value 1. But we could
also take 3 and 2 as reals and use real division, yielding the real value 1.5,
so the expression would be ambiguous. Reynolds discusses these design
issues in [Rey80].
3.6 Type Simplification
Let textcographic be the program of Figure 2.4 for comparing sequences lexico-
graphically. As shown in Corollary 3.29, the computation
(S,B,r) = W0s(A0,texicographic);
(5', B', a) = cThse(A0,B,r).
produces a principal type a for lexicographic. But if we use the simple close of
Figure 2.3 we discover, to our horror, that we obtain the principal type
Va,?, ?, e, 6, (),7?, A, ic, ?, i', ?, 7r, p, a, C, T, V, 4) with
C seq(?), bootC ? 6 c seq(()), boot C ?, ? C seq(A),
A C 6 c seq(?), ? C ,:, ? C seq(v), seq(u) C ?,
6 c seq(r), seq(ir) C p, a t _ T T H bool,
C seq(v), v C r 6 c seq(4)), 4) C T, bool C t, t C ?,
C e, (? ?4 p H a) H (? .6 H ?) C (a H a)
a
Such a type is clearly useless to a programmer, so, as a practical matter, it is
essential for close to simplify the types that it produces.
3.6.1 An Overview of Type Simplification
We begin with an informal overview of the simplification process, showing how
type simplification works on lexicographic.
The call Wos(Ao, lexicographic) returns ([?, 0 := H fi H a, p H a], B, a),
where
C seq(?), boot C bool, boot C e 6 c seq(()), boot C ?, ? C seq(A),
B = A c ? 6 C seq(?), it C ?, ? C seq(v), seq(u) C ?, 6 c seq(r),
seq(r) C p, aCt, < : r H T boot, ? C seq(v), v Cr 6 C seq(4)),
4) C r,boot C t t C ?, ? C e, (? H p .` a) `. (? H 6 H e) C (a H a)
This means that for any instantiation 5 of the variables in B such that A0 H
BS, lexicographic has type aS. The problem is that B is so complicated that it
87
is not at all clear what the possible satisfying instantiations are. But perhaps we
can make (generally partial) instantiations for some of the variables in B that
are in a certain sense optimal, in that they yield a simpler, yet equivalent, type.
This is the basic idea behind type simplification.
There are two ways for an instantiation to be optimal. First, an instantiation
of some of the variables in B is clearly optimal if it is `forced', in the sense that
those variables can be instantiated in only one way if B is to be satisfied. The
second way for an instantiation to be optimal is more subtle. Suppose that there
is an instantiation T that makes B no harder to satisfy and that makes the
body (in this example, a) no larger. More precisely, suppose that A0u B H BT
and A0 u B ? aT C a. Then by using rule (C?), BT and aT can produce the
same types as can B and a, so the instantiation T is optimal. We now look at
how these two kinds of optimal instantiation apply in the case of texicographic.
We begin by discovering a number of forced instantiations. Now, A0 has
acceptable inclusions, so by Lemma 3.19, A0 can prove only inclusions of the
form r C ?? where r and r1 have the same shape. So the constraint ? C seq(?)
in B can be satisfied only if ? is instantiated to some type of the form seq(x);
the partial instantiation [? seq(x)] is forced. There is a procedure, shape-
unifter, that finds the most general substitution U such that all the inclusions
in BU are between types of the same shape. In this case, U is
seq(x),
seq(?),
seq(w),
p			seq(ai),
a			seq(?) H seq(?i) H Pi
The instantiations in U are all forced by shape considerations; making these
forced instantiations produces the constraint set
seq(x) C seq(?) boot C boot, boot C e seq(?) C seq(()),
boot C ?, seq(?) C seq(A), A C tc seq(V') C seq(jt),
it C ic, seq(?) C seq(v), seq(v) C seq(w) , seq(?) C seq(ir),
seq(?) C seq(ai) a C t ? : r H T H boot, seq(?) C seq(v),
v C r seq(?) C seq(?), ? C r, boot C t, c ?, fl C e,
(seq(w) H seq(ai) H a) H (seq(?) H seq(?) H e) C
(seq(6i) seq(?i) H ?`) H (seq(?) H seq(?i) H
and the body
seq(?) H seq(?i) H Pi.
We have made progress; we can now see that texicographicis a flinction that takes
two sequences as input and returns some output.
88
: r H T H boot
t			t
body: seq(?) H seq(?i) H Pi
o+ Pi
Figure 3.4: Atomic Inclusions for lexicographic
The new constraint set contains the complicated inclusion
(seq(w) H seq(?i) H a) H (seq(x) H seq(?) e) C
(seq(?i) H seq(?i) H Pi) H (seq(?i) H seq(?i) H Pi).
However, by Lemma 3.20 and rule ((--H) H (+))? we have
A0 H T			p C			.. PI
if and only if
A0 H 71 ? r and A0 F p C p'
Hence our complicated inclusion is equivalent to the simpler inclusions
(seq(?) seq(?i) H Pi) C (seq(w) H seq(a1) H a)
and
(seq(x) H seq(?) H e) C (seq(?) H seq(?i) H Pi).
These simpler inclusions, too, can be broken down into still simpler inclusions.
The result of this process is to convert the constraint set into an equivalent set
containing only atomic inclusions. The result of this transformation is shown
graphically in Figure 3.4, where an inclusion ?i ? 72 is denoted by drawing an
arrow from ?i to ?2 Below the representation of the constraint set we give the
body.
Now notice that the constraint set in Figure 3.4 contains cycles; for example
w and v lie on a common cycle. This means that if s is any instantiation that
89
: T H T ` boot
body: seq(?) H seq(?i) H
Figure 3.5: Collapsed Components of texzcograph?c
boot
satisfies the constraints, we will have both A0 H wS C vS and A0 F vS C wS.
Hence, by Lemma3.21, it follows that wS = vS. In general, any two types within
the same strongly connected component must be instantiated in the same way.
If a component contains more than one type constant, then, it is unsatisfiable; if
it contains exactly one type constant, then all the variables must be instantiated
to that type constant; and if it contains only variables, then we may instantiate
all the variables in the component to any chosen variable. We have surrounded
the strongly connected components of the constraint set with dotted rectangles
in Figure 3.4; Figure 3.5 shows the result of collapsing those components and
removing any trivial inclusions of the form p C p thereby created.
At this point, we are finished making forced instantiations; we turn next to
instantiations that are optimal in the second sense described above. These are
the monotonicity-based instantiations.
Consider the type boot a. By rule ((--H) (+)), this type is monotonic
in a: as a grows, a larger type is produced. In contrast, the type a H boot
is antimonotonic in a: as a grows, a smaller type is produced. Furthermore,
the type fi H P is both monotonic and antimonotonic in a: changing a has no
effect on it. Finally, the type a H a is neither monotonic nor antimonotonic in
a: as a grows, incomparable types are produced.
Refer again to Figure 3.5. The body seq(?i) H (seq(?i) H t) is antimono-
tonic in ?i and ?i and monotonic in t. This means that to make the body
smaller, we must boost ?i and ?i and shrink t. Notice that i has just one type
smaller than it, namely boot. This means that if we instantiate t to boot, all
the inclusions involving t will be satisfied, and t will be made smaller. Hence
the instantiation [c := bootj is optimal. The cases of ?i and ?i are trickier
they both have more than one successor, so it does not appear that they can
90
H T H boot
body: seq(?) H seq(?) H boot
Figure 3.6: Result of Shrinking t, v, A, ?, b, tt, and ()
be boosted. If we boost ?i to v, for example, then the inclusions ?i C A and
? may be violated.
The variables v, A, ?, b, it and (), however, do have unique predecessors.
Since the body is monotonic (as well as antimonotonic) in all of these variables,
we may safely shrink them all to their unique predecessors. The result of these
instantiations is shown in Figure 3.6.
Now we are left with a constraint graph in which no node has a unique
predecessor or successor. We are still not done, however. Because the body
seq(?i) H seq(?i) H boot is both monotonic and antimonotonic in ?, we can
instantiate tc arbitrarily, even to an incomparable type, without making the
body grow. It happens that the instantiation [tc := r] satisfies the two inclusions
? and ?i C ,c. Hence we may safely instantiate ? to r
Observe that we could have tried instead to instantiate r to tc, but this would
have violated the overloading constraint < : T H r H boot. This brings up a
point not yet mentioned: before performing a monotonicity-based instantiation of
a variable, we must check that all overloading constraints involving that variable
are satisfied.
At this point, ?i and ?i have a unique successor, T, 50 they may now be
boosted. This leaves us with the constraint set
: r H T H booti
and the body
seq(r) H seq(?) H boot.
At last the simplification process is finished; we can now use the simple close of
Figure 2.3 to produce the principal type
Vr with < : r H T H boot. seq(r) H seq(r) H boot,
which happens to be the same as the type obtained in Chapter 2 without sub-
typing.
91
In the next three subsections, we present in more detail the transformation
to atomic inclusions, the collapsing of strongly connected components, and the
monotonicity-based instantiations. We then present the complete function close
and prove that it satisfies Lemmas 3.22 and 3.24.
3.6.2 Transformation to Atomic Inclusions
In this subsection we describe the part of close(A, B, r) that transforms the
inclusions in B to atomic inclusions. We begin by developing the theory of
shape unification.
First we recall certain definitions about ordinary unification. Given a set ?
of pairs (r, r'), we say that substitution U unifies T' if for every pair (r, T') in
?, rU = r'U; if there exists such a U we say that ? is uniflable. We say that
U is a most general unifler for P if
o+ U unifies ? and
o+ any V that unifies T' can be factored into UV', for some
There are efficient algorithms for computing most general unifiers [Kni89].
Now, given a set ? of pairs (r, r'), we say that substitution U shape unifies
? if for every pair (r, T') in ?, rU and r'U have the same shape; in this case
we say that ? is shape un4iable. We say that U is a most general shape unifier
for ? if
o+ U shape unifies ? and
o+ any V that shape unifies ? can be factored into UV', for some V'.
For example,
f((a?P)?a, ??seq(?)?
has most general shape unifier
seq(e)			?, a			seq(?)]
and
((seq(a)?P, PHO))
has no shape unifier.
Computing most general shape unifiers turns out to be more subtle than
computing most general unifiers.3 Fuh and Mishra [FM90] give a rather com-
plicated algorithm. We can, however, give a simpler algorithm with the help of
the following lemma, which is due to Bard Bloom.
The difficulty is that, unlike equality, the `same shape' relation is not preserved under suh?
stitution; hence building up a shape unifier from partial solutions is more awkward.
92
shape-unifier(?):
if Pc is not unifiable, fail;
Q
5
while Q does not contain only atomic pairs do
choose peQ nonatomic;
case p:
or
let
R = [OL := fresh4eaves(r)];
Q := QR;
5			SR;
(X(ri,...,rn),x(m',...,r?')):
Q:=(Q--HfpJ)uf(ri,r1,),...,(r?,r?')J;
return 5, restricted to the variables of P
Figure 3.7: Function shape-unifier
Lemma 3.30 Let Pc denote the result of replacing all occurrences of type con-
stants in P by the type constant c. Then P is shape unifiable if and only if P,
is unifiable.
Proof: (?) If rcU = rc'U, then rU and r'U have the same shape.
(?) If r and r' are shape unifiable, then they have a shape unifier [a := 7r]
where, without loss of generality, ? has no occurrences of type constants. Hence
m[c := 7rJ5 = rc'[a := 7r]S, where 5 is a substitution that maps all type variables
to c. QED
Lemma 3.30 gives us a way to use ordinary unification to test whether a set
P of pairs is shape unifiable, allowing us to use an algorithm for constructing
most general shape unifiers that works only when P is in fact shape unifiable.
Algorithm shape-unifler is given in Figure 3.7. The call fresh-leaves(r) in shape-
unifier returns r with all occurrences of type variables and type constants re-
placed by new type variables; for example, fresh-leaves(seq(a) H int a) is
seq(P) H ?, where P, ?, and ? are new type variables. The important
properties of shape-unifler are given in the following lemma.
Lemma 3.31 If P is shape unifiable, then shape-unifier(P) succeeds and returns
a most general shape unifier for P; otherwise, shape-unifier(P) fails.
Proof: The loop invariant is
1. If U shape unifies P, then U = SU' for some U' and Ut shape unifies
2. If V shape unifies Q,then SV shape unifies P
93
atomic-inclusions(B) = B, if B contains only atomic inclusions;
atomic-inclusions(B u (r p C r' H p')) =
atomic-inclusions(B u (r' C r, p C p'));
atomic-inclusions(B u (seq(r) C seq(r'))) =
atomic-inclusions(B u fr C
Figure 3.8: Function atomic-inclusions
From 1, if ? has a shape unifier U, then U = SU'; it follows that 5 cannot
grow without bound and hence the loop terminates. QED
One might wonder whether the test of the uiiifiability of ?c at the start of
shape-unifier could be made unnecessary by adding an "occurs" check to the
(0, r) case that fails if o occurs in r, and by adding an "else" case that fails
when p is of the form (x(...)?x'(...)) and ? ? ?1. Unfortunately, this is not
good enough: if ? is ((seq(a) ?? H o)),then even with the proposed
tests the while loop will not terminate.
Now we turn to the problem of converting a set of inclusions between types
of the same shape into an equivalent set of atomic inclusions. This is accom-
plished by function atomic-inclusions, given in Figure 3.8. Each clause in the
definition of atomic-inclusions takes care of one type constructor and is based on
the monotonicities of that constructor in each argument position. The soundness
and completeness of atomic-inclusions are shown in the following lemmas.
Lemma 3.32 If C = atomic.inclusions(B) succeeds, then C contains only
atomic inclusions and C H B.
Proof: This follows easily from the rules ((--H) H (t)) and (seq(Q)). QED
Lemma 3.33 If B contains only inclusions between types with the same shape,
then atomic-inclusions(B) succeeds. Furthermore, if A contains only atomic in-
clusions, then for any 5 A H BS implies A H (atomic-inclusions(B))S
Proof: Follows from Lemma 3.20. QED
Given shape-unifler and atomic-inclusions, we can now state precisely the
transformation to atomic inclusions, which is the first part of close(A, B, r):
let Aci be the constant inclusions in A,
Bi be the indusions in B,
Bt be the typings in B;
let U = shape-unifier(((?, ?) I (? C
let Ci = atomic-inclusions(BjU) U Aci,
Ct = BtU;
94
(The reason for including Aci in Ci will be given later, in the discussion of
monotonicity-based instantiations.) The soundness and completeness of the trans-
formation are shown in the following two lemmas.
Lemma 3.34 If the transformation to atomic inclusions succeeds, then Ci con-
tains only atomic inclusions. Also, if A u B ? e: r,then AU U (Ci U Ct) H e : TU
and id(Ct) = id(Bt)
Proof: By Lemma 3.32 and the fact that Aci contains only constant inclusions,
Ci contains only atomic inclusions.
By Lemma 3.5, AU u BjU U BtU F e: rU. By Lemma 3.32, Ci H BjU, and
so by Lemmas 3.3, 3.13, and 3.14, AU U Ci U BtU F e: rU. Since Ct = BtU, we
have AU U (Ci U Ct) H e : rU and also id(Ct) = id(Bt). QED
Lemma 3.35 If A has acceptable inclusions and AR F BR, then the transfor
mation to atomic inclusions succeeds and there exists a substitution ?? such that
R = UR' and AUR' H (Ci U Ct)R'
Proof: By Lemma 3.2 and the fact that A contains only constant inclusions we
have Aci?BiR. So by Lemma3.19, R shapeunifies f(?,?) I (?C?)EBi1.
Hence by Lemma 3.31, U = shape-unifier(((?, ?) I (? c ?)eBi1) succeeds and
U is a most general shape unifier for f(?, 4)') I (4) c 4)')eBi1, so there exists R'
such that R = UR'.
Now BiU contains only inclusions between types of the same shape, so
by Lemma 3.33, atomic-inclusions(BiU) succeeds. Furthermore, since Aci H
(BiU)R', by Lemma 3.33 we have Aci H (atomic-inclusions(BjU))R', and hence
AUR' H (Ci U Ct)R'. QED
3.6.3 Collapsing Strongly Connected Components
As discussed in the overview of type simplification, types belonging to the same
strongly connected component of Ci must be instantiated in the same way, so
each strongly connected component can be collapsed to a single type. To this end,
component-collapser(Cj) returns the most general substitution that collapses the
strongly connected components of Ci. Function component-collapser is given in
Figure 3.9. The strongly connected components of G may be found in linear
time using depth-first search [AHU74j.
Let nontrivial-inclusions (B) be the set of inclusions in B not of the form
ir C ir. Now if V = component-collapser(Cj), then the only cycles in CjV
are trivial inclusions; hence nontrivial-inclusions (CiV) is acyclic. An acyclic
graph can be further simplified by taking its transitive reduction [AGU72J. The
transitive reduction of an acyclic graph G is the unique minimal graph having
the same transitive closure as G; it may be found by deleting redundant edges
95
component-collapser( C):
1. Bnild a directed graph G with a vertex for each type in C and
with an edge r r1 whenever (r C r')eC.
2. Find the strongly connected components of G
3. V:=[];
for each strongly connected component C of G do
if C contains more then one type then
if C contains more than one type constant, fail;
let ?`,... , a? be the type variables in c;
if C contains a type constant c then
V			V[a1,c2, ..			:= c,c,. . .
else
V: V[c?,a?,...,an
4. Return V.
Figure 3.9: Function component-collapser
from C using an algorithm that is essentially the inverse of Warshall's transitive
closure algorithm [GMvdSU89].
It will be seen in the discussion of monotonicity-based instantiation that the
use of the transitive reduction has significance beyond mere simplification.
We can now state precisely the next part of close(A, B, T), which is the
collapsing of strongly connected components:
let V = component-collapser(Ci);
let S=UV,
Di = transitive-reduction ( nontrn'rnal-inclusions (Cj V)),
Dt = CtV;
The soundness and completeness of these statements are shown in the following
two lemmas, whose proofs are straightforward.
Lemma 3.36 If the collapsing of strongly connected components succeeds then Di
is acyclic and reduced; that is, transitive-reduction(Di) = Di. Also, if AU U (Ci U
Ct)Fe:rU,thenASU(D?UDt)Fe:r5 and id(Dt)=id(C1)
Lemma 3.37 If A has acceptable inclusions and AUR' H (Ci U Ct)R',then the
collapsing of strongly connected components succeeds and there exists a substitution
R" such that R' --H VR11 and ASR" H (Di U D1)R11
96
3.6.4 Monotonicity-based Instantiations
The final simplifications performed in ctose(A, B, r) are the monotonicity-based
instantiations. Monotonicity-based simplification was earlier explored by Curtis
[Cur9O] and by Fuh and Mislira [FM89].
Monotonicity-based instantiations, in contrast to the instantiations made dur-
ing shape unification and the collapsing of strongly connected components, are
not in general forced. Because of this, there is a restriction on monotonicity-based
instantiations: they may be applied only to variables that are not free in AS.
This is because the instantiations of type variables free in AS may be forced in
subsequent type inference, so to preserve the completeness of W05 such variables
must not be instantiated unnecessarily.
At this point in the simplification process, we have transformed the original
typing A u B H e : r to the typing AS u (Di U Dt) H e : rS. Now, given
a variable a not free in AS, we may (by Lemma 3.5) transform the typing
ASu(DiuDt)Fe:rS to the typing ASu(DiuD?)[a:=r] He:rS[a:=?,
but we may lose information by doing so. We will not lose information, however,
if the instantiation [a ir] makes (Di U Dt) no harder to satisfy and makes rS
no bigger; precisely we require that
and
AS u (Di U D1) F (Di U Dt)[a			ir]
AS U (Di U Dt) H rS[a := ir] C rS.
To see why no information is lost by the transformation in this case, suppose that
T is an instantiation of variables not free in AS such that AS H (Di U Dt)T,
allowing the original typing to produce AS H e : rST. Then AS H (Di U
Dt)[a irJT and AS ? rS[a ir]T C rST, so the new typing can produce
first AS ? e : rS[a ir]T and then AS F e : rST by (C).
We now give the precise formulation of the monotonicity-based instantiat?ons:
E?:=D?; Et:--H--HDt; p:--H--HTS;
a variables free in Di or Dt or TS but not AS;
while there exist a in a and ir different from a such that
AS U (Ei U Et) F (Ej U E1)[a ir] u fp[a ir] C
do
Ej : = trans?tive-redttction( nontrnrn'al-inclusions (Ej [a =
Et			Et[a			ir];
p			p[a			ir];
a a --H a;
od
It is straightforward to show that the while loop has the following invariant:
97
1. ffASU(DiuD1)Fe:rS,then ASU(EiUEi)?e:p and id(Ei)=id(Dt)
2. AS u (Di U Dt) F Ej U E1 u fp C rSJ.
3. Ej is acyclic and reduced; that is, transitive-redttction(E?) = Ej
4. If A has acceptable inclusions, then AS u (Ej U E1) ? C ? if and only if
It was to achieve part 4 of the invariant that we included Aci in Ci in the
transformation to atomic inclusions.
Notice that the monotonicity-based instantiations ahvays succeed.
The soundness and completeness of the monotonicity-based instantiations are
given in the next two lemmas, both of which follow immediately from the loop
invariant.
Lemma 3.38 If AS u (Di U Di) H e : rS, then AS U (Ei u E1) ? e : p and
id(Et) = id(Dt)
Lemma 3.39 If ASR" H (Di U D1)1?" then ASR" H (Ej U E1)R" and ASR" H
pR" C rSR"
At this point the only question is how to implement efficiently the guard of
the while loop: given a variable a in a, we want to determine whether there is
a ir not equal to a such that
AS u (Ej U E1) F (Ej U Et)[a := r] U (p[a := 7r] C
We begin by determining under what circumstances
ASU(EiUE1) Fp[a:=? C?p;
the monotonicity of p in a turns out to be the key.
Definition 3.5 We say that p is monotonic in a if
o+ p is atomic,
o+ P = Pi H 02, Pi is antimonotonic in a, and P2 is monotonic in a, or
o+ p = seq(pi) and pi is monotonic in a
Similarty, p is antimonotonic in a if
o+ p is atomic and p # a,
o+			0 = Pi			02, pi is monoton?c ? a, and P2 is antimonotonic in a, or
o+ 0 = seq(pi) and pi is antimonotonic in a
98
Notice that if p is both monotonic and antimonotonic in a,then a does not oc-
cur in p. The importance of monotonicity and antimonotonicity is demonstrated
by the following lemma.
Lemma 3.40 Let A have acceptable inclusions and let a and it be distinct. Then
A H p[a itj C p if and onlg if one of the following hold:
o+ p is monotonic but not antimonotonic in a and A H ? C a
o+ p is antimonotonic but not monotonic in a and A H a C it or
o+ p is both monotonic and antimonoton?c tn a.
Aided by Lemma 3.40, we now return to the implementation of the guard of
the while loop. Given a in a?, the first step is to check the monotonicity and
antimonotonicity of p in a; we discuss in turn what to do for each of the four
possible outcomes.
If p is neither monotonic nor antimonotonic in a,then by Lemma 3.40 there
is no it distinct from a such that AS U (Ej U Et) H p[a it] C p. Hence a
cannot be instantiated.
If p is monotonic but not antimonotonic in a, then a must be shrunk by
Lemma 3.40 we have
if and only if
AS U (Ei U Et) H p[a :--H--H it] C p
ASU(EiUEt) H it Ca.
Now, if A has acceptable inclusions, then by part 4 of the invariant of the while
loop, this will hold if and only if Ej H it a. Siiice Ej contains only atomic
inclusions, by Lemma 3.19 it must be atomic; hence Ej H it C a if and only if
there is a path of length at least 1 from it to a in Ej. This implies that a must
have a predecessor in E?; that is, there must be a type ? such that (? C a)EEi,
for otherwise, there are no nontrivial paths to a in Ej.
Suppose now that
AS U (Ej U Et) H Ei[a := it].
Then AS u (Ei U Et) H ? c it so by part 4 of the invanant of the while loop,
Ej ? ? C it hence there is a path from ? to it iii Ej. So we have the following
picture:
a
99
One possibility is that ? = ?; in fact this is the only possibility! For suppose
that			? ? ?. Then since Ej is acyclic, neither the path ?			7r nor the path
a contains the edge ?			a. Therefore, the edge ?			a is redundant,
contradicting the fact that Ej is reduced, which is part 3 of the invariant of the
while loop. It follows, then, that if a has more than one predecessor in Ej then
there is no 7r such that
AS u (Ej u E?) H Ei[a := ir] u fp[a := 7r] C pJ.
If, on the other hand, ir is the ?niqte predecessor of a in Ej, then one sees
readily that
AS u (Ej U Et) F Ei[a := 7r] U (p[a := 7r] C pJ.
This gives us an efficient implementation of the guard of the while loop in
the case when p is monotonic but not antimonotonic in a. First check whether
a has a unique predecessor in E?; if not, a cannot be instantiated. ? If a has a
unique predecessor ?,then it suffices to check that ASu (Ej U Et) H Et[a :=
(We will discuss the implementation of this check in Section 3.7.)
Next we turn to the case where p is antimonotonic but not monotonic in a;
in this case a must be boosted. By an analysis just like that of the previous
case, one can show that a can be instantiated if and only if it has a unique
siccessor 7r in Ej (that is, there is a unique type 7r such that (a C ?)?Ei) and
ASU(EiUEt) FEj[a:=?.
Finally, we must consider the case where p is both monotonic and anti-
monotonic in a, which implies that a does not occur in p. In this case
AS u (Ei U Et) H p[a := 7r] C p holds for every 7r, so we must do some searching.
(Of course, the fact that 7r can be chosen so freely has benefits as well as costs
it is what makes possible the instantiation of ? in the example of lexicographic
discussed in the overview.)
If a occurs in Ej, then we can limit the search for 7r to types occurring in
Ej. For suppose that (a C ?)eEi. Then if
AS U (Ej U Et) K (Ej U Et)[a := 7r],
then (by part 4 of the while loop invariant) we have Ej H ? c ?, so there is a
path in Ej from ir to ?; that is, ?r must occur in Ej.
If, however, a does not occur in Ej, then it is not clear that the search for
7r can be bounded at all. Indeed, this case amounts to a search for a satisfying
assignment for a set of overloading constraints, which is of course undecidable in
general. Two solutions may be considered. First, by limiting overloading we may
be able to bound the search. Second, we may limit the search for ? arbitrarily,
? Of course, later in the simplification process, after other variables have been instantiated, it
may become possible to instantiate a
loo
perhaps to types occurring in Ei; if we do this we will still produce principal
types, we just may not produce the simplest possible types. This approach seems
to work well in practice.
We conclude the discussion of monotonicity-based instantiation with two ex-
amples that show the necessity of taking transitive reductions.
The call
returns
W0s(A0,if true 2 7r)
([1, (bool C bool int C CL real C CLi, CL),
so if Aci were not included in Ci or if Ej were not reduced, then the analysis
requiring that CL have a unique predecessor would be wrong and we would arrive
at the principal type
rather than real.
The example
VCL with int C CL real C CL. CL
if fr?e ((Ax.x)2) ?
shows the need for taking transitive reductions repeatedly. In this example, the
initial value of p is CL and the initial value of (Ej U Et) is
CL
which is reduced. If the monotonicity-based instantiations begin by boosting P
to CL, then we will be stuck unless we take another transitive reduction, because
CL will be left with two predecessors, int and real.
3.6.5 Punction close
At last, we can put all the pieces together and give the new function close.
Function close performs the transformation to atomic inclusions, the collapsing
of strongly connected components, the monotonicity-based instantiations, and
finally the simple close of Figure 2.3. The complete flinction close is given in
Figure 3.10.
Finally, we can combine the soundness and completeness lemmas of the pre-
vious three subsections to prove Lemmas 3.22 and 3.24.
101
dose(A, B, ?):
let
Aci be the constant inclusions in A,
Bi be the inclusions in B,
Bt be the typings in B;
let U = shape-unifler(f(?, ?) I (? c
let Ci = atomic??nclnsions(B?U) U Aci,
Ct = BtU;
let V = component-collapser(C?);
let S=UV,
Di = transitive-reduction( nontrnv?at-inctttsions (CjV)),
Dt = CtV;
E?:=D?; Et:=Dt; p:--HrS;
a := variables free in Di or Dt or rS but not AS;
while there exist a in a and ? different from a such that
AS u (Ej U Et) H (Ej U Et)[a := 7r] U (p[a := 7r] C
do Ej := frafls%t?ve-reduct?on(nontriviat-inclusions(Ei[a :=
Et := Et[a :=
p := p[a :=
a := a --H a
od
let E= (EiUEt) --H fC ASF Ci;
let E" be the set of constraints in E in which some a in a occurs;
if AS has no free type variables,
then if satisfiable(E,AS) then E' := (1 else fa?l
else E' :=
return (5, E', Va with E"
Figure 3?10: Function close
102
3.7 Satisfiability Checking
real H real H boot
seq(reat) seq(reat) H boot
seq(tnt) H seq(?nt) H boot
A0 F?:			(hypoth)
A0 F<:			(Velim)
A0 F?:
(hypoth)
(V-elim).
H boot
In general, the derivation of a typing x : 7, where x is overloaded and r is an
instance of the tcg of x may be written so that all uses of (C?) precede all uses
of (V-elim).
As a result of this property, we can simplify typing assumptions in a con-
straint set by "unwinding" them. For example, the constraint ? : seq(seq(fl))
seq(seq(P)) H boot can be replaced by the constraint < : H boot. In gen-
eral, we can work backwards from the original constraint, eventually either failing
or arriving at a set of atomic instantiations of the tcg. We can incorporate this
simplification into close by changing the initialization of E1 from "Et := Dt" to
nnwind(Dt)".
Now we can give a way of checking that
AS u (Ei U Et) H Et[o := ir],
which is required on page 99. For each x : 7 in Et[o := ir], it suffices to check
that there is some typing x : ? in AS U (Ei U Et) sud? that
ASU(EiUEt)? ?c? ?.
Next we consider the satisfiability problem. We are given a set E of atomic
inclusions and overloading constraints; for example, we might have
E = (a C p, int C a <: (3H (3H boot)
In this section, we give some thoughts on the problem of checking the satisfi-
ability of constraint sets, which may now contain inclusions as well as typings.
In addition, we consider the related problem of checking whether an overloaded
identifier has a particular type.
In Section 2.5, however, we saw that these problems are undecidable, even in
the absence of subtyping. We therefore restrict ourselves again to the case where
the assumption set A is an overloading by constructors, as defined in Section 2.6.
An important consequence of the restriction to overloading by constructors
is that, roughly speaking, (V-elim) and (c?) steps can be exchanged within
derivations. For example, the derivation
can be replaced by the derivation
A0 F< : real H real H boot
A0 F? : int int H boot
A0 F< : seq(int) H seq(int)
103
We model E as a graph with a node for each type variable or constant in E
and with edges corresponding to the inclusions in E. In addition, we associate
a set of possible type constructors with each node, indicating that the node may
only be instantiated to a type built from those type constructors. We use U to
denote the set of all type constructors. For example, the first two constraints in
the above E are modeled by
Next we must model typing constraints. We are again aided by the exchangeabil-
ity of (V-intro) and (c?) steps in derivations, which allows us to assume that all
uses of (V-elim) precede all uses of ( C?). This allows us to characterize the set of
all typesof <. Indeed < has all supertypes of types of the form ? boot,
where ? is a type built from the type constructor set for ?, (reat,char,seq).
Since ? H boot is antimonotonic in ?,this means that < : H H boot
if and only if p is a subtype of some type ? built from (reat,char,seq?. Hence
we can model the constraint < : H H boot as
p
where ? is a new type variable.
In general, if an overloaded identifier x has tcg V?.r?, we must consider
the monotonicity of Tx in o in order to determine how to model a constraint
x : Tz[Q P]. If Tx is monotonic in c, then p must be a supertype of some
type ? built from the type constructor set of x. If Tx is neither monotonic nor
104
antimonotonic in a, then ? must itself be built from the type constructor set
of x.
Given the graph representation of , we now try to characterize the possible
satisfying instantiations of E. Observe that if any node has an associated type
constructor set that is empty, then E is unsatisfiable. Hence, we can make
progress by making deductions that allow us to shrink the type constructor sets.
First, we can restrict the type constructor sets to type constants. This is a
consequence of the rules of subtyping. For example, if the constraint a C p is
satisfied by [a, p := seq(r), seq(r')],then it is also satisfied by [a, P r, r'] .?
Next, we can work "locally", eliminating type constants that can be seen not
to work. We have the following picture:
p
a
must be a subtype of
some type constructor here
? must be a supertype of
some type constructor here
If x is not a subtype of any of the possible type constructors of p or if ? is not a
supertype of any of the possible type constructors of ?, then a certainly cannot
be instantiated to ?. We can repeatedly eliminate useless type constructors,
stopping when no further constructors can be eliminated, or when some type
constructor set becomes empty.
Fuh and Mishra [FM88], in their investigation of a type system with subtyping
but no overloading, propose the above local algorithm. They conjecture that,
for any unsatisfiable constraint set, the local algorithm eventually produces an
empty type constructor set. Unfortunately, this is not so, as may be seen by the
following counterexample. Suppose that we are given the constraint set
C a, ? C a, ? C p, s c
and that each type variable has a choice of two type constructors whose inclusions
are as indicated in the following picture.
? If there are any purely antimonotonic type constructors, a bit more work needs to be done.
105
p
Then no type constructors may be eliminated locally, yet the constraint set is
unsatisfiable.
In fact, Wand and O'Keefe [WO89] show that the satisfiability problem with
subtyping but no overloading is NP-complete. They also show that if the subtype
relation has the property that any set of types with an upper bound has a least
upper bound, then the satisfiability problem can be solved in polynomial time.
In the case of a type system with both overloading and subtyping, more
research needs to be done. At worst, we can first apply the local algorithm to
shrink the set of possible type constructors; if an empty type constructor set
is produced, then the constraint set is unsatisfiable. If not, then we can do a
brute-force search for a satisfying instantiation.
An alternative approach is to restrict the subtype relation somehow; perhaps
one can show that if the subtype relation has some reasonable property, then the
local algorithm works.
3.8 Conclusion
The introduction of constrained quantification has allowed subtyping to be added
smootMy to the Hindley/Milner/Damas type system with overloading. The sub-
type relation needs to be restricted somewhat; roughly speaking, we allow only
those type inclusions implied by inclusions among type constants. Also, restric-
tions on overloading are required for the satisfiability and typability problems to
be decidable.
Chapter 4
Conclusion
4.1 A Practical Look at Type Inference
In the last two chapters, we have given a formal account of polymorphic type
inference in the presence of overloading and subtyping. The main result is that
the inference algorithms W0 and Wos are sound and complete and can therefore
be used to infer principal types. Formal results, however, do not give much feel
for how type inference works in practice; it would be nice to know that type
inference tends to produce types that are understandable.
An implementation of algorithm W05 and the close of Figure 3.10 has been
written in Scheme. The implementation is not especially efficient, but it is ade-
quate for our purposes.
Define function type as the type of expression e under the initial assumptions
A, as determined using our algorithms W08 and close:
type(A,e):
let (S,B,r) = W05(A,e);
let (5', B', a) = close(A, B, r);
return a
As shown in Corollary 3.29, type(A, e) computes a principal type for e with
respect to A provided that A has satisfiable constraints, acceptable inclusions,
and no free type variables. Let A0 be the assumption set given in Figure 3.3.
We now show the result of type(A0, e) on various expressions e
o+ fast-expon
Function fast-e?pon is given in Figure 4.1; type(A0,fast-expon) is
Va with 1 : a, * : a a a. a H int H a
This is the same as the type arrived at without subtyping.
106
107
fix Aexp.
Ax.An. if
n 0)
if
(even? n)
(exp (* xx) (+ n 2))
(* x exp x n 1)))
Figure 4.1: Example fast-expon
Function fast-expon can be used to raise 2-by-2 matrices to powers. It
can be used, for example, to calculate the n th convergent to a periodic
continued fraction in logaritlimic time.
o+ max
Function max is Ax.Ay. if (< y x) x y. The result of type(Ao, max) is
VQ?,?? with o C ? a C ? C ? < ? H H boot.
aH?H?.
This surprisingly complicated type cannot, it turns out, be further simpli-
fied. A simpler type can be found under stronger assumptions about the
subtype relation: if we assume that any two types with an upper bound
have a least upper bound, then the type of max can be simplified to
V? with <: ? H H boot. ? H
o+ mergesort
Function mergesort is given in Figure 4.2; t?pe(Ao, mergesort) is
Va? with < : a? H H boot. seq(a?) H seq(a?).
The type computed for split is
V?.seq(?) H seq(seq(?))
and the type computed for merge is
Vt1,91,ij1,? with ()i C tc, ?i C ?11, Ci C tc, t? C ?i, ? : tc H ? H boot
seq(ti) H seq(()i) H seq(?i),
which is very much like the type of max above.
108
let split=
fix A split.
A 1st. if (null? 1st)
(cons nil (cons nil nil))
if (null? (cdr 1st))
(cons 1st (cons nil nil))
let pair split ( cdr ( cdr 1st)) in
(cons ( cons ( car 1st) ( car pair))
(cons (cons?(car (cdrlst)) (car (cdrpair)))
nil)) iii
let merge
fix Amerge.
A lstl. A lst2.
if (null? lstI)
1st2
if (null? lst2)
lstl
if(?? (carlstl) (carlst2))
(cons (carlstl) (merge (cdrlstl) lst2))
(cons (car lst2) (merge lstl (cdr lst2))) in
fix A mergesort.
A 1st. if (null? 1st)
nil
if (null? (cdr 1st))
1st
let lstllst2--H split 1st in
merge (mergesort (car
( mergesort ( car
lstllst2))
(cdr lstllst2)))
Figure 4.2: Example mergesort
109
fix A reduce.
Af.Aa.Al. if (null? 1)
a
(f(carl)
(reducefa (cdrl)))
Figure 4.3: Example reduce-right
fix Areduce.
Af.Aa.Al. if (null? 1)
a
if (null? (cdr 1))
(car 1)
(f(carl) (reducefa (cdrl)))
Figure 4.4: Example another-reduce-right
Interestingly, when I first wrote mergesort I neglected to test for the case
when 1st has length 1; that is, I wrote
fix A mergesort.
AIst. if(null? 1st)
nil
let lstilst2= split 1st in
merge (mergesort ( car lstilst2))
(mergesort ( car (cdr lstilst2)))
The type constructed for this version of mergesort was
Vr3, ?? with < : 73 H 73 H bool. seq(a?) H seq(m),
which showed me that something is wrong!
o+ reduce-right
Function reduce-right is given in Figure 4.3; type(Ao, reduce-right) is
Vp1,?(p1 H?H? ?+?H seq(Pi)?Q
o+ another-reduce-right
Function another-reduce-right is given in Figure 4.4; it has type
VPi,?withP1C??.(?1????????seq(?1)??
110
4.2 Related Work
Overloading had long been a neglected topic, but recently it has been addressed in
papers by Kaes [Kae88] and, as part of the Haskell project, by Wadler and Blott
[WB89j. Kaes' work restricts overloading quite severely; for example he does
not permit constants to be overloaded. Both Kaes' and Wadler/Blott's systems
ignore the question of whether a constraint set is satisfiable, with the consequence
that certain nonsensical expressions are regarded as well typed. For example, if
+ is overloaded with types int H int int and real real real, then in
Wadler/Blott's system the expression true + false is well typed, even though +
does not work on booleans. Kaes' system has similar difficulties.
There is a much larger body of literature on subtyping, spurred recently by
excitement about object-oriented programming. None of the work of which I am
aware considers the problem of type inference in the presence of both overloading
and subtyping, but a number of papers do address the problem of type inference
with subtyping. Most notable are the papers of Stansifer [Sta88], Curtis [Cur90J,
and Fuh and Mishra [FM89,FM90J.
Stansifer gives a type inference algorithm and proves its completeness, but
unfortunately his language does not include a let expression, which we saw to be
a major source of difficulty. He also does not address type simplification or the
problem of determining the satisfiability of constraint sets.
Curtis studies a very rich type system that is not restricted to shallow types,
i.e. to types where all quantification is outermost. Largely because of the richness
of his system, he is unable to characterize formally much of what he does. He gives
an algorithm for the satisfiability problem but leaves its correctness as a conjec-
ture. He gives an inference algorithm but does not address completeness at all.
He performs elaborate type simplification, including some monotonicity-based
instantiation, but does not completely prove the correctness of his algorithm.
Fuh and Mishra give a type inference algon.thm and prove its completeness,
but, like Stansifer's, their language does not include let. They also perform some
type simplification.
4.3 Puture Directions
We conclude by mentioning a few areas for fliture research.
4.3.1 Satisfiability of Constraint Sets
The problem of checking the satisfiability of a constraint set needs more study,
especially in the case where both overloading and subtyping are present. In
particular, it would be valuable to identify a restriction on the subtype relation
that, combined with the restriction to overloading by constructors, allows the
111
satisfiability problem to be solved efficiently. Also, the possibility of relaxing
somewhat the restriction to overloading by constructors should be explored.
4.3.2 Records
A recordis a labeled collection of fields. The subtype relation is more complicated
on record types than on the types we have considered so far; for example, adding
extra fields to a record type produces a subtype. What changes are needed to
incorporate record types into our type system?
4.3.3 Semantic Issues
Our type system has the property that a typing A H e : r can have more than
one derivation. For example, using the assumption set A0 of Figure 3.3, the
typing A0 H 1 + 1 : real can be derived in two ways:
as well as
A0 H 1 : int			(hypoth)
A0 H + : int int H int			(hypoth)
A0 Hi + 1: int			(?-ehm)
A0 H int C real			(hypoth)
A0 H 1+1: real
A0 H lint			(hypoth)
A0 H int C real			(hypoth)
A0 H 1 : real
A0 H + : real H real H real			(hypoth)
A0 Hi + 1: real			(?-elim).
For the language to be unambiguous, it is crucial that these two derivations lead
to the same meaning.
In general, the semantics of an expression e of type r should be independent
of the choice of derivation of e: r. This property has been explored by Reynolds
[Rey80], and, more recently, by Breazu-Tannen et al. [BTCGS89], who call the
property coherence.
4.3.4 Imperative Languages
Finally, we would like to extend our results to an imperative language. Unfortu-
nately, extending polymorphic type inference to imperative languages has proved
difficult, because the obvious typing rules turn out to be unsound in the presence
of assignment. Proinising approaches to this problem have been proposed by
Tofte [Tof88J and by Leroy and Weis [LW91J; it should be possible to adapt their
approaches to our type system.
Appendix A
Omitted Proofs
In this appendix we give the inductive proofs omitted from Sections 2.2 and 3.2.
Lemma 2.6 If x does not occur tn A, ? ? y, and A u (x : al ?` y : r, then
A H' y : r
Proof: By induction on the length of the derivation of Au fx : al ?` y : r. The
only possible (non-trivial) last steps are (hypoth) and (V-elim'). ((V-intro) and
(=?a) could be used trivially.)
(hypoth) The derivation is simply A U (x : al H' y ? where y r cAu fx :
Since x ? y, y : r eA, and so A F' y : r.
(V-elim') The derivation ends with
y: V?with C.T' eAufx:a)
AUfx :al H' C[?:=r]
A u (x : al H' y: Y[o ir]
Since x ? y, y : V? with C. T1 C A. Since x does not occur in A, no
constraint in C[c ir] is of the form x : p. So the induction hypothesis
may be applied to each member of C[Q ir?], giving A F' C[a ir]. So
by (V-elim'),
QED
A H' y :			ir?].
Notice that the derivation of AS H' e : aS given by Corollary 2.5 can be
longer than the derivation of A H' e : a, because of the necessity of inserting an
(=a) step after each (V-intro) step. In the proof of Lemma 2.7 below, however,
we will need the property that applying a substitution to a derivation does not
lengthen the derivation. This can be achieved by defining the notion of a padded
derivation: a derivation is padded if every (V-intro) step is followed by a (possibly
112
113
identity) (=?a) step. Any derivation can be padded, of course, and applying a
substitution to a padded derivation does not lengthen it, since the extra (=a)
steps introduced by the substitution can be combined with the padding (=a)
steps that have been provided.
Lemma 2.7 If A H' e : a then A u B H' e : a, provided that no identifier
occurring in B is A -bound or let-bound in e
Proof:
By induction on the length of the derivation of A H' e : a, which we
assume without loss of generality to be padded. Consider the last step of the
derivation:
(bypoth) The derivation is simply A H' x : a where x : aeA. So x: aeAuB,
and A u B F' x : a.
(H -intro) The derivation ends with
A u fx : rJ ?? e' : r1
A ?? Ax.e' : r H
where x does not occur in A. No identifier occurring in B is A -bound or
let-bound in ??, so by induction,
(A u fx : r1) u B H' e' : Y
Since x is A -bound in Ax.e', x does not occur in B, so x does not occur
in AUB. So, since (AUfx : TJ)UB =(AuB)ufx : r?, (?4ntro) may
be used to give
A u B H' ????? : T H T1
(? -elim) The derivation ends with
A ?? e' : r H
A H1 e11 : r
A H1 e' e'1 : T1
No identifier occurring in B is A -bound or let-bound in e' or e", so by
induction, A u B ?? e' : T H T? and A u B H1 e" : T, and so by (H -elim),
A u B ?? e1 e"
(let) The derivation ends with
A H' e'
A u fx: a'? H' e11 : r
A H1 let x e1 in e11 : r
114
where x does not occur in A. No identifier occurring in B is A -bound
or let-bound in ?? or e11, so by induction, A u B ?? e' : ?? and (A u fx
a?)) u B H1 e11 : r Since x is let-bound in let x in e1, x does not
occur in B, so x does not occur in A u B. So (let) may be used to give
A u B ?? let x =			in e11 :
(V-intro) A padded derivation cannot end with (V-intro).
(V-elim') The derivation ends with
x: V? with C. r e A
A H' C[?
A H' x : := 7r?]
Now x : Va with C. r e A u B, and by induction on each member of
C[a := ?j,(using the fact that for any y : p in C[a := ir], no identifier
in B is A-bound or let-bound in y,) A u B H' C[a := ir]. Hence by
(V-elim'),
A u B H' x: T[a :=
(?=a) The derivation ends with
A H' e
a a a
A ?? e : a
If the derivation of A F' e: a' is padded, then by induction A u B H' e: a',
so by (=a),
A u B H' e : a.
If, on the other hand, the derivation of A F' e : a' is not padded, then it
ends with (V-intro):
A u C H' e: r
A F' C[a := ir]
A H' e: Va with C. r
where a are not ftee in A, and where ?? = Va with C. r . Let p be
distinct type variables not occurring free in a', A, or B. By Corollary 2.5,
(AuC)[a:=Th H' e:r[a-:=Th,
and (by our padding assumption) the derivation is no longer than the
derivation of A u C ?? e : T. Since no identifier occurring in B is A -bound
115
or let-bound in e, by induction we have (Auc)[? P]uB H' e : r[a
Since a are not free in A, (AuC)[a			= AuC[o			?, sowe have
AuBu C[& ?j Ye: r[a :=
Also by induction on each member of C[o			7r], we have A u B H' C[a
?. Since C[a:=?=C[a:=Th[?:=?,wehave
AUB H' C[a			Th[P? :=
So by (V-intro),
AUB F'e: VP with C[a? := Th.r[a			Th.
Since
VP with C[o? := ?. r[a := Pi a a' --Ha a,
it follows by (=a) that
AUBF' e:a.
QED
Lemma 2.8 Let B be a set of T -assttmptions. If A u B H' e : a and A H' B,
then A H' e : a
Proof: By induction on the length of the derivation of A U B ?` e : a. Consider
the last step:
(hypoth) The derivation is simply A u B H' x : a where x : a e A u B. If
x : a e A then A H' x : a. If x : a e B then by the assumption A ??
again AH' x:a.
(? -intro) The derivation ends with
(A u B) u fx : rt H' e' : T1
A u B ??			: r H T
where x does not occur in A u B. By Lemma 2.7 applied to each member
of B, AUfx : r? Fl B. Now (AUB)Ufx : = (AUfx : rl)uB, soby
induction
A u fx : rl ?? e' :
Since x does not occur in A u B, it does not occur in A, so by (H -intro),
A H' Ax.e' : T H
116
(? -elim) The derivation ends with
A u B H1 ?` : r H
A u B ?? e11 : T
A u B H' e1 e" T
By induction, A ?` ?` : r H Y and A H' e" : T, 50 by (H elim),
A H' c1e11 :
(let) The derivation ends with
A u B H' e' : a'
(A u B) u fx : a') H' e" :
A u B H' let x = e' in e" : T
where x does not occur in A u B. By induction, A H' e' : a'. By
Lemma 2.7 applied to each member of B, A u fx : a?) ?? B. Since
(A u B) u ?x : a') = (A u tx a')) u B, the induction hypothesis may be
applied to give
A u (x &) H' e" :
Since x does not occur in A u B, it does not occur in A, so by (let),
A ?? let x = ?? in e11 :
(V-intro) The derivation ends with
(A u B) u C H' e r
AuB?' C[a :=?J
AuB?'e: V?with C.T
where ? are not free in A u B By Lemma 2.7 on each member of B,
A u C H' B. Since (A u B) u C = (A u C) u B,the induction hypothesis
may be applied to give
AUCH' e:r.
Also by induction,
A H' C[o :=
Since a are not free in A, (V-intro) gives
A H' e: Vc? with C. r
117
(V-elim') The derivation ends with
x: V? with C. r e A u B
AuBH' C[a:=ir]
A u B H' x : :=
Since B contains only r -assumptions,
x: Va with C. T ? A,
and by induction, A H' C[c := 7r?]. So by (V-elim'),
A H' x : r[o
(=a) The derivation ends with
QED
(AuB)H' e: a'
a			a a
(A u B) H' e : a
By induction, A H' e: a', so by (--Ha),
A F' e: a.
Lemma 2.13 If A H e : a then no identifier occurring in A is A -bound or
let-bound in e
Proof: By induction on the length of the derivation of A H e : a. Consider the
last step of the derivation:
(hypoth) The derivation is simply A H x : a where x : a e A. Nothing is
A -bound or let-bound in x
(? -intro) The derivation ends with
A u (x : H e' :
A H ????` : T H
where x does not occur in A. By induction, no identifier in A u fx : r? is
A -bound or let-bound in e'. So no identifier in A is A -bound or let-bound
in ?? And since x does not occur in A, no identifier in A is A -bound or
let-bound in ?????
118
(H -elirn) The derivation ends with
A H ?? r H
A H e" 7
A H e' e'1 : 71
By induction, no identifier in A is A -bound or let-bound in e' or e'1.
Hence no identifier in A is A -bound or let-bound in e' e".
(let) The derivation ends with
I			?
AHe a
A u fx : a') F e" : 7
A ? let x e' in e" : 7
where x does not occur in A By induction, no identifier in A is A -bound
or let-bound in e' and no identifier in A u fx : a') is A -bound or let-bound
in e". Since x does not occur in A, no identifier in A is A -bound or
let-bound in let x = e1 in e11
(V-intro) The derivation ends with
AUCH e: 7
A H C[a			7r]
AHe: Va with C.7
where a are not free in A. By induction, no identifier in AUC is A -bound
or let-bound in e; hence no identifier in A is A -bound or let-bound in e.
(V-elim) The derivation ends with
AHe: Va with C.7
A H C[a :=
A H e : ?[a :=
By induction, no identifier in A is A -bound or let-bound in e
(=a) The derivation ends with
AHe:a'
I--H
a =a a
AHe:a
By induction, no identifier in A is A -bound or let-bound in e.
QED
Now we give the proofs from Section 3.2.
119
Lemma 3.7 If x does not occur in A, x ? y, and Au fx al H' y : r, then
A H' y : r.
Proof: The proof of Lemma 2.6 suffices, except that we must consider one more
possible last step of the derivation of A u fx : a? H' y : r
(c?) The derivation ends with
QED
Au fx : al H' y : 7'
A u fx : al H' 71 ? 7
Au fx : at H' y : 7
By induction, A H' y : 7' and by Lemma 3.2, A ?` 71 ? ?. So by (C?),
A ?` y : 7
Lemma 3.8 If A H' e : a then A u B H' e : a, provided that no identifier
occumny in B is A -bound or let-bound in e.
Proof: The proof of Lemma 2.7 suffices, except that we must consider the case
when the derivation of A H' e: a ends with (C).
(c?) The derivation ends with
QED
A H1 e: 7
A F' ? C 71
A H' e: 71
By induction, A U B H' e: 7 and by Lemma 3.3, A U B H1 ? C 71 So by
(c?), A u B H' e: 7'.
Lemma 3.9 Let B be a set of 7-assumptions. If AU B H' e : a and A H' B -
then A ?? e : a
Proof: The proof of Lemma 2.8 suffices, except that we must consider the case
when the derivation of A u B H' e a ends with (C?).
(C?) The derivation ends with
A u B H1 e : 7
A u B ?l 7 C 71
A u B H' e : 71
By induction, A ?` e : 7 and by Lemma 3.4, A F1 7 c ?`. So by (C?),
A H' e:
QED
Bibliography
[ACU72]
[AHU74]
[AHU83]
[ASU8G]
[BTCGS89]
[C+86]
[Car84]
[Car87j
Alfred V. Aho, Michael R. Garey, and Jeffrey D. Ullman. The tran-
sitive reduction of a directed graph. SIAM Journal on Computing,
1(2):131--H137, June 1972.
Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The De-
sign and Analysis of Computer Algorithms. Addison-Wesley Pub-
lishing Company, 1974.
Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. Data
Structures and Algorithms. Addison-Wesley Publishing Company,
1983.
Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compil-
ers: Principles, Techniques, and Tools. Addison-Wesley Publishing
Company, 1986.
v. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov.
Inheritance and explicit coercion (preliminary report). In lEEF
Fourth Annual Symposium on Logic in Computer Science, pages
112--H129, 1989.
Robert L. Constable et a'. Implementing Mathematics with the
Nupri Proof Development System. Prentice-Hall, Inc., 1986.
Luca Cardelli. A semantics of multiple inheritance. In G. Kahn,
D. B. MacQueen, and G. Plotkin, editors, Semantics of Data Types,
volume 173 of Lecture Notes in Computer Science, pages 51--H67.
Springer-Verlag, 1984.
Luca Cardelli. Basic polymorphic typechecking. Science of Com-
puter Programming, 8:147--H172, 1987.
Dominique Clement, Joe?lle Despeyroux, Thierry Despeyroux, and
Gilles Kahn. A simple applicative language: Mini-ML. In ACM
Conference on LISP and Functional Programming, pages 13--H27,
1986.
[CDDK86]
120
121
[Cur9O]
[CW85j
[DD85j
[DM82]
[FM88]
[FM89]
[FM9o]
[Gir72j
[GLT89]
[GMvdSU89]
[GP85]
Pavel Curtis. Constrained Quantification in Polymorphic Type
Analysis. Ph.D. dissertation, Cornell University, January 1990.
On understanding types,
A CM Computing Surveys,
Luca Cardelli and Peter Wegner.
data abstraction, and polymorphism.
17(4):471--H522, December 1985.
James Donahue and Alan Demers. Data types are values. ACM
Transactions on Programming Languages and Systems, 7(3):426--H
445, July 1985.
Luis Damas and Robin Milner. Principal type-schemes for func-
tional programs. In 9th ACM Symposium on Principles of Program-
ming Languages, pages 207--H212, 1982.
You-Chin Fuh and Prateek Mishra. Type inference with subtypes.
In II. Ganzinger, editor, ESOP `88, volume 300 of Lecture Notes in
Computer Science, pages 94--H114. Springer-Verlag, 1988.
You-Chin Fuh and Prateek Mishra. Polymorphic subtype infer-
ence: Closing the theory-practice gap. In J. Dfaz and F. Orejas,
editors, TAPSOFT `89, volume 352 of Lecture Notes in Computer
Science, pages 167--H183. Springer-Verlag, 1989.
You-Chin Fuh and Prateek Mishra. Type inference with subtypes.
Theoretical Computer Science, 73:155--H175, 1990.
et elimination des
These de doctorat
Jean-Yves Girard. Interpre'tation fonctionnelle
coupures dans l'arithme'tique d'ordre supe'neur.
d'etat, Umversite' Paris VII, 1972.
Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types.
Cambridge University Press, 1989.
David Gries, Alain J. Martin, Jan L. A. van de Snepscheut, and
Jan Tijmen Udding. An algoritlim for transitive reduction of
an acyclic graph. Science of Computer Programming, 12:151--H155,
1989.
David Gries and Jan Prins. A new notion of encapsulation. In
Proceedings ACM SICPLAN Symposium on Language Issues in Pro-
gramming Environments, pages 131--H139, 1985.
David Cries and Dennis Volpano. The transform a new language
construct. Technical Report TR 89-1045, Department of Computer
Science, Cornell University, October 1989.
[CV89]
122
[Hin69j
[11586]
[HU79j
[Kae88]
[Kni89]
[KT9O]
[Lak76]
[Lei83]
[Llo84]
[LW9l]
[McC84]
J. Roger Hindley. The principal type-scheme of an object in corn-
binatory logic. Transactions of the American Mathematical Society,
146:29--H60, December 1969.
J. Roger Hindley and Jonathan P. Seldin. Introduction to Combi-
nators and A -Calculus. Cambridge University Press, 1986.
John E. Hopcroft and Jeffrey D. Uliman. Introduction to Automata
Theory, Languages, and Computation. Addison-N\'esley, 1979.
Stefan Kaes. Parametric overloading in polymorphic programming
languages. In 11. Ganzinger, editor, ESOP `88, volume 300 of Lec-
ture Notes in Computer Science, pages 131--H144. Springer-Verlag,
1988.
K. Knight. Unification: A multidisciplinary survey. ACM Com-
puting Surveys, 21(1):93--H124, March 1989.
A. J. Kfoury and Jerzy Tiuryn. Type reconstruction in finite-rank
fragments of the polymorphic A -calculus. In Fifth IEEE Sympo-
sium on Logic in Computer Science, pages 2--H11, 1990.
Imre Lakatos. Proofs and Refutations: Ti?e Logic of Mathematical
Discovery. Cambridge University Press, 1976. Edited by John
Worrall and Elie Zahar.
Daniel Leivant. Polymorphic type inference. In 10th ACM Sympo-
s?um on Principtes of Programming Languages, pages 88--H98, Austin,
Texas, 1983.
John Wylie Lloyd. Foundations of Logic Programming. Springer-
Verlag, Berlin/New York, 1984.
Xavier Leroy and Pierre Weis. Polymorphic type inference and
assignment. In 18ll? ACM Symposium on Principles of Programming
Languages, pages 291--H302, 1991.
Nancy McCracken. The typechecking of programs with implicit
type structure. In G. Kalrn, D. B. MacQueen, and G. Plotkin,
editors, Semantics of Data Types, volume 173 of Lecture Notes in
Computer Science, pages 301--H315. Springer-Verlag, 1984.
John C. Mitchell and Robert Harper. The essence of ML. In 15th
A CM Symposium on Principles of Programming Languages, pages
28--H46, 1988.
[M1188]
123
[Mil78]
[Mit84]
[Mor73j
[MP88]
[Poil3]
[PraOS]
[Pri87]
[Rey7O]
[Rey74j
[Rey8O]
[Rey81]
Robin Milner. A theory of type polymorphism in programming.
Journal of Computer and System Sciences, 17:348--H375, 1978.
John C. Mitchell. Coercion and type inference (summary). In
Eleventh A CM Symposium on Priciples of Programming Languages,
pages 175--H185, 1984.
James II. Morris, Jr. Types are not sets. In ACM Symposium
on Principles of Programming Languages, pages 120--H124, Boston,
Massachusetts, 1973.
John C. Mitchell and Gordon D. Plotkin. Abstract types have
existential type. A CM Transactions on Programming Languages
and Systems, 10(3):470--H502, July 1988.
Henri Poincare'. The Foundations of Science. The Science Press,
Lancaster, Pennsylvania, 1913. Authorized English translation by
G. B. Halsted.
Dag Prawitz. Natural Deduction. Almqvist and Wiksell, Stock-
holm, 1965.
Jan F. Prins. Partial Implementations in Program Derivation.
Ph.D. dissertation, Cornell University, August 1987.
John C. Reynolds. Trausformational systems and the algebraic
structure of atomic formulas. Machine Intelligence, 5:135--H151,
1970.
John C. Reynolds. Towards a theory of type structure. In Program-
ming Symposium, vdume 19 of Lecture Notes in Computer Science,
pages 408--H425. Springer-Verlag, 1974.
John C. Reynolds. Using category theory to design implicit conver-
sions and generic operators. In Semantics-Directed Compiler Gen-
eration, volume 94 of Lecture Notes in Computer Science, pages
211--H258. Springer-Verlag, 1980.
John C. Reynolds. The essence of ALGOL. In de Bakker and van
Vliet, editors, Algorithmic Languages, pages 345--H372. IFIP, North-
Holland Publishing Company, 1981.
John C. Reynolds. Three approaches to type structure. In Math-
ematical Foundations of Software Development, volume 185 of Lec-
ture Notes in Computer Science, pages 97--H138. Springer-Verlag,
1985.
[Rey8S]
124
[Rey88]
[Rob65]
[Sta88]
[Tof88]
tvD83]
[VS91j
[WB89]
John C. Reynolds. Preliminary design of the programming lan-
guage Forsythe. Technical Report CMU-CS-88-159, Department
of Computer Science, Carnegie Mellon University, June 1988.
J. A. Robinson. A machine-oriented logic based on the resolution
principle. Journal of the ACM, 12(1):23--H41, January 1965.
Ryan Stansifer. Type inference with subtypes. In Fifleenth ACM
Symposium on Prnnciples of Programming Languages, pages 88--H97,
1988.
Mads Tofte. Operational Semantics and Polymorphic Type Infer-
ence. Ph.D. dissertation, University of Edinburgh, 1988.
Dirk van Dalen. Logic and Structure. Springer-Verlag, 1983.
Dennis M. Volpano and Geoffrey 5. Smith. On the complexity of
ML typability with overloading. In Conference on Functional Pro-
gramming Languages and Computer Architecture, Cambridge, Mas-
sachusetts, August 1991. To appear.
Philip Wadler and Stephen Blott. How to make ad-hoc pAymor-
phism less ad hoc. In 16th A CM Symposium on Principles of Pro-
gramming Languages, pages 60--H76, 1989.
Mitchell Wand and Patrick O'Keefe. On the complexity of type
inference with coercion. In Confrrence on Fanctional Programming
Languages and Computer Architecture, 1989.
[WO89]