Tofte1988
Tofte1988
Tofte1988
(e.g. PhD, MPhil, DClinPsychol) at the University of Edinburgh. Please note the following
terms and conditions of use:
• This work is protected by copyright and other intellectual property rights, which are
retained by the thesis author, unless otherwise stated.
• A copy can be downloaded for personal non-commercial research or study, without
prior permission or charge.
• This thesis cannot be reproduced or quoted extensively from without first obtaining
permission in writing from the author.
• The content must not be changed in any way or sold commercially in any format or
medium without the formal permission of the author.
• When referring to this work, full bibliographic details including the author, title,
awarding institution and date of the thesis must be given.
Operational Semantics and
Polymorphic Type Inference
Mads Tofte
Ph. D.
University of Edinburgh
1987
Abstract
Three languages with polymorphic type disciplines are discussed, namely the
A-calculus with Milner's polymorphic type discipline; a language with imperative
features (polymorphic references); and a skeletal module language with struc-
tures, signatures and functors. In each of the two first cases we show that the
type inference system is consistent with an operational dynamic semantics.
On the module level, polymorphic types correspond to signatures. There is
a notion of principal signature. So-called signature checking is the module level
equivalent of type checking. In particular, there exists an algorithm which either
fails or produces a principal signature.
Contents
1 Introduction 1
I An Applicative Language 8
2.1 Notation 10
2.2 Dynamic Semantics 11
II An Imperative Language 26
5 Proof of Soundness 47
5.1 Lemmas about Substitutions 47
5.2 Typing of Values using Maximal Fixpoints 51
5.3 The Consistency Theorem 62
8.4.3 Programs 98
Bibliography 201
Chapter 1
Introduction
Since early days in programming the concept of type has been important. The
basic idea is simple; the values on which a program operates have types and
whenever the program performs an operation on a value the operation must be
consistent with the type of the value. For example, the operation "multiply x by
7" makes sense if x is a value of type integer or real, but not if x is a day in the
week, say.
Any programming language comes with some typing rules, or a type discipline,
if you like, that the programmer keeps in mind when using the language. This is
true even of so-called "untyped" languages.'
There is an overwhelming variety of programming languages with different
notions of values and types and consequently also a great variety of type disci-
plines.
Some languages have deliberately been designed so that a machine by just
examining the program text can determine whether the program complies with
the typing rules of the language. In our example, "multiply x by 7", it is a
simple matter, even for a computer, to check the well-typedness of the expression
assuming that x has type int, say, without ever doing multiplications by 7. This
kind of textual analysis, static type checking, has two advantages: firstly, one can
discover programming mistakes before the program is executed; and secondly, it
can help a compiler generate code.
For these languages one can factor out the static semantics from the dynamic
semantics. The former deals with type checking and possibly other things a com-
piler can handle, while the latter deals with the evaluation of programs provided
- 'Every LISP programmer knows that one should not attempt to add an integer and a list
although this is not always conceived as a typing rule
1
CHAPTER 1. INTRODUCTION 2
they are legal according to the static semantics. Let us refer to this class of lan-
guages as the statically typed languages. It includes ALGOL [4], PASCAL [44],
and Standard ML [18, 20].
But there are also languages where such a separation is impossible. One
example is LISP [26] which has basically one data type. The "type errors" one
can commit are of such a kind that they cannot in general be discovered statically
by a mere textual analysis.' Similarly, there can be no separation in languages
where types can be manipulated as freely as values. Let us call such languages
dynamically typed.
At first sight it seems a wonderful idea that a type checker can find program-
ming mistakes even before the program is executed. The catch is, of course, that
the typing rules have to be simple enough that we humans can understand them
and make the computers enforce them. Hence we will always be able to come up
with examples of programs that are perfectly sensible and yet illegal according
to the typing rules. Some will be quick to say that far from having been offered
a type discipline they have been lumbered with a type bureaucracy.
The introduction of polymorphism [27] in functional programming must have
been extremely welcome news to people who believed in statically typed lan-
guages because the polymorphic type checker in some ways was a lot more tol-
erant than what had previously been seen. A monomorphic type system is one
where every expression has at most one type. By contrast, in Milner's poly-
morphic type discipline there is the distinction between a generic type, or type
scheme, and all the instances of the generic type. One of the typing rules is that
if an expression has a generic type, then it also has all instances of the generic
type. So the empty list, for example, has the generic type Va.a list and all its
instances int list, (bool list) list, (int --> bool) list, and so on. In fact, Va.a list
is said to be the principal type of the empty list, because all other types of the
empty list can be obtained from it by instantiation.
Polymorphism occurs naturally in programming in many situations. For ex-
ample the function that reverses lists is logically the same regardless of the type of
list it reverses. Indeed, if all lists are represented in a uniform way, one compiled
version of the reverse function will suffice.
Milner's polymorphic type discipline has been used in designing the functional
2Even in statically typed languages there will normally be kinds of "type errors" that cannot
be discovered. Taking the head of the empty list is one example; index errors in arrays is
another.
CHAPTER 1. INTRODUCTION 3
language ML, first in "Old ML", which was a "meta language" for the proof
system LCF [15], and later in Standard ML [18].
The main purpose of this thesis is to demonstrate that the basic ideas in
Milner's polymorphism carry over from the purely applicative setting to two quite
different languages. Because these languages have different notions of values and
types, the objects we reason about are different. But there is still the idea of
types that are instances of type schemes, there are still notions of principal types,
and using different kinds of unification algorithm one can get new type checkers
that greatly resemble the one for the applicative case. Perhaps some category
theorist will tell us that these different type systems are all the same, but I find
it interesting that this kind of polymorphism "works" in languages that are not
the same at all.
Unfortunately, polymorphism does not come for free. The price we have to
pay is that we have to think pretty hard when we lay down the typing rules.
First and foremost, typing rules must be sound in the sense that if they admit
a program then (in some sense) that program must not be bad. Whereas in
monomorphic type disciplines one would not feel compelled to invest lots of en-
ergy in investigating soundness, one has to be extremely careful when considering
polymorphism. Indeed Part II of this thesis has its root in the historical fact that
people have worked very hard to extend the purely applicative type discipline to
one that handles references (pointers) as values. Polymorphic exceptions were in
ML for years before it quite recently was discovered that the "obvious" typing
rules are unsound.
Clearly we do not want to launch unsound type inference systems. Perhaps
we do not want to undertake the task of proving the soundness of typing rules
for a big programming language, such as ML, but the least we can do is to make
sure that the big language rests on a sound base. Then we want to formulate the
typing rules for the small language in a way that is convenient for stating and
proving theorems.
It so happens that there is a notation that is extremely convenient for defin-
ing these polymorphic type disciplines (and others as well, I trust). It started
as "Structural Operational Semantics" [34], the French call it "Natural Seman-
tics" [9]- I shall use the term "operational semantics". The idea is to borrow
the concept of inference rule and proof from formal logic. The typing rules are
CHAPTER 1. INTRODUCTION 4
has type r-' then you may infer that the application of el to e2 has type r." Such
rules need not be deterministic (r is not a function of e, not even when e contains
no free variables) and that makes them very suitable for defining polymorphism.
Given a type inference system in the form of a collection of type inference
rules, how do we investigate soundness?
The first soundness proofs used denotational semantics [14, 13]. Types are
seen as ideals of values in a model of the lambda calculus and it is proved that
if by the type inference system an expression has a type then the value denoted
by the expression is a member of the ideal that models the type.
It seems a bit unfortunate that we should have to understand domain theory
to be able to investigate whether a type inference system admits faulty programs.
The approach to soundness I take is different in that I also use operational seman-
tics to define the dynamic semantics and then prove that, in a sense that is made
precise later on, the two inference systems are consistent. This only requires
elementary set theory plus a simple powerful technique for proving properties of
maximal fixpoints of monotonic operators.
Milner [27] independently discovered essentially the same result but he was
able to extend the type inference rules so that a function, once declared, can be
applied to objects of different types. For instance, the expression
1.2 Outline
There are three parts. In Part I we review Milner's polymorphic type discipline
for a purely applicative language and we formulate and prove a consistency result
using operational semantics.
In Part II we extend the language to have references (pointers) as values. We
present a new polymorphic type discipline for this language and compare it with
one due to Luis Damas [13]. The soundness of the new type inference system is
proved using operational semantics.
Part III is concerned with a polymorphic type discipline for modules. The lan-
guage has structures, signatures and functors as in ML. Signatures will be seen to
correspond to structures as type schemes correspond to types in the applicative
setting. We present a unification algorithm for structures that generalizes the
ordinary first order unification algorithm used for types, and we present a "sig-
CHAPTER 1. INTRODUCTION 7
nature checker" (the analogue of a type checker) and prove that it finds principal
signatures of all well-formed signature expressions.
In the conclusion I shall comment on the role of operational semantics partly
based on the proofs I have done, and partly based on the experience we as a
group had of using operational semantics to write the full ML semantics [20].
Part I
An Applicative Language
Chapter 2
We define a dynamic and a static semantics for a little functional language and
show that, in a sense to be made precise below, they are consistent.
The type discipline is essentially Milner's discipline for polymorphism in func-
tional languages [27, 14]. However, we formulate and prove soundness of the type
inference system with respect to an operational dynamic semantics instead of a
denotational semantics.
I apologize to readers who already know this type discipline for bothering
them with the differences between types and type schemes, substitution and in-
stantiation, the role of free type variables in the type environment, and so on.
However, I cannot bring myself to copy out the technical definitions without some
examples and comments, mostly because I have a feeling that many have some
experience of polymorphism through the use of ML without being used to think-
ing of the semantics in terms of inference rules. Moreover, a good understanding
of the inference rules is essential for the understanding of the type disciplines in
Part II and III.
The soundness of the type inference system is not hard to establish using
operational semantics. The proof therefore serves as a simple illustration of a
proof method that will be put to more heavy use in the later parts.
We are considering the following little language, Exp. Assuming a set, Var,
of program variables
x E Var = {a,b,...,x,y,...}.
9
CHAPTER 2. MILNER'S POLYMORPHIC TYPE DISCIPLINE 10
2.1 Notation
Throughout this thesis we shall give inference rules that allow us to infer sequents
of the form
A I- phrase --i B
where phrase is a syntactic object and A and B are so-called semantic objects.
Semantic objects are always defined as the least solution to a collection of set
equations involving Cartesian product (x), disjoint union (+), and finite subsets
and maps. When A is a set then Fin(A) denotes the set of finite subsets of A. A
finite map from a set A to a set B is a partial map with finite domain. The set
of finite maps from A to B is denoted
fin
A B.
The domain and range of any function, f, is denoted Dom(f) and Rng(f), and
f 1 A means the restriction of f
to A. When and g are (perhaps finite) maps f
then f + g, called f modified by g, is the map with domain Dom(f) U Dom(g)
and values
(f + g)(a) = if a E Dom(g) then g(a) else f (a).
f
The symbol + is a reminder that + g may have a larger domain than (hence f
the +) and also that some of the values of f may "disappear" because they are
superseded by the values of g (hence the -).
When Dom(f) fl Dom(g) = write g for + g. We say that
0 we g is f I f f I
f
the simultaneous composition of and g. Note that for every a E Dom(f g) we I
I f
have that either (f g)a = (a) or (f g)a = g(a). I
f
We say that g extends f, written C g if Dom(f) C Dom(g) and for all x in
f
the domain of we have (x) = g(x). f
Any E Af fin
B can be written in the form
>
x E Dom E
EI-x-E(x)
x Dom E
EI- x -p wrong
Eo ±{xo " E
vo}
I-
I-
e2
eo -' r vo
EI-ele2-r
E I- el -p [xo, eo, Eo] E I- e2 -p wrong
E I- el e2 -p wrong
EI- el -p borwrong
E I- el e2 ) wrong
By using the conclusion of one rule as the premise of another one can build
complex evaluations out of simpler ones. More precisely, an evaluation is regarded
as a special case of a proof tree in formal logic.
Then the set of types, Type, ranged over by r and the set of type schemes,
TypeScheme, ranged over by o are defined by
T 7r aI Tl-3T2
a T Va.ol
The -p is right associative. Note that types contain no quantifiers and that type
schemes contain outermost quantification only. This is necessary to get a type
checking algorithm based on first order term unification. A type environment is
a finite map from program variables to type schemes:
fin
TE E TyEnv = Var TypeScheme
A type scheme or = dal. ... Van.T written dal ... an.T. We say that
is
al, ... an are bound in o and that a type variable is free in o if it occurs in r
and is not bound. Moreover, we say that a type variable is free in TE if it is free
in a type scheme in the range of TE.
The map tyvars : Type -p Fin(TyVar) maps every type T to set set of type
variables that occur in T. More generally, tyvars(o) and tyvars(TE) means the
set of type variables that occur free in o and TE, respectively. Also, o and TE
are said to be closed if tyvars o = 0 and tyvars TE _ 0 and r is said to be a
monotype if tyvars(T) = 0-
A total substitution is a total map S : TyVar -p Type. A finite substitution
is a finite map from type variables to types. Every finite substitution can be
extended to a total substitution by letting it be the identity outside its domain,
and we shall often not bother to destinguish between the two. However, to deal
CHAPTER 2. MILNER'S POLYMORPHIC TYPE DISCIPLINE 14
Reg(S) = U tyvars(S(a))
oEDom(S)
Definition 2.1 Let al = dal ... an-Ti and v2 = Vf31... 13m..7-2 be type schemes
and S be a substitution. We write of _S__+ 0'2 if
1. m = n, and {a, H f3t I 1 < 2 < n} is a bijection, no at is in Reg(So), and
where so
S
tyvars al. Moreover, we write TE
,
-* TE' if Dom TE
DomTE' and for all x E DomTE, TE(x) -S-+ TE'(x).
We write al = v2 as a shorthand for vl D > o2. Note that this is the familiar
notion of a-conversion.
c'
The operation of putting Va. in front of a type or a type scheme is called gen-
eralization (on a), or quantification (of a), or simply binding (of a). Conversely,
T' is an instance of o = Val ... an-T, written
U>T1,
if there exists a finite substitution, S, with domain {al, ... , an} and S(T) = T'.
The operation of substituting types for bound variables is called instantiation.
Instantiation to type schemes as follows: o2 is an instance of o ,
is extended
written vl > v2i if for all types T, if o2 > T then vl > T. Write v2 = df3l ... P..7-2-
One can prove that vl > v2 if and only if vl > T2 and no /3, is free in o 1. (This,
in turn, is equivalent to demanding that vl > T2 and tyvars(vl) C tyvars(o2)).
Finally,
C1osTET
means Val ... an-T, where {a1, ... , an} = tyvars T \ tyvars TE.1
CHAPTER 2. MILNER'S POLYMORPHIC TYPE DISCIPLINE 15
I TEI- e:T
x EDomTE TE(x)>T
TEF-x:T
TE±{xHT'}F-e1:T
(2.10)
TEFAx.e1:T'->T
TEF-e1:T1 TE±{xHC1osTET1}F-e2:T
(2.12)
TE F-let x = el in e2 : r
This is all we need to give the static semantics, see Figure 2.3.2
The following examples illustrate the use of the system. Skip them if you
know the type inference system.
Example 2.2 (Shows a simple monomorphic type inference). Consider the ex-
pression
((7x.Ay.y x)z)(Ax.x).
Assume TEo(z) = int, let TE1 = TEo ±{x H ant} and TE2 = TE1 ±{y H int -->
int}. We then have the inference
TE2 F- y : int -> int TE2 F- x : int
TE2F-yx:int
TE1 F- Ay.y x : (int -> int) -r ant
TEo F Ax.Ay.y x : ant -> ((ant -> ant) -> int)
'Throughout, the symbol \ is used for set difference, i.e., A \ B means {x E A x B}. I
2The reader familiar with the type inference system of [14] will note that our version does
not have an instantiation and a generalization rule Instead instantiation is done precisely when
variables are typed and generalization is done explicitly by the closure operation in the let rule
Also note that the result of a typing is a type rather than a general type scheme. Although
it is not trivial to prove it, the two systems admit exactly the same expressions. Our system
has the advantage that whenever TE I- : r, the form of e uniquely determines what rule was
applied.
CHAPTER 2. MILNER'S POLYMORPHIC TYPE DISCIPLINE 16
where the form of the expressions always tells us which rule is used. Thus
TEo I- Ax.Ay.y x : int -- (int -- int) -- int TEo I- z : int
(2.13)
(Ax.Ay.y x)z: (int -4 int) -- int
We have
TE1 I- x int :
TEo I- (Ax.Ay.y x)z: (znt -- int) -- znt TEo I- Ax.x : int -- int
TEo I- ((Ax.Ay.y x)z)(Ax.x) : znt
as we suspected. Notice that we had to "guess" the right types for the lambda
bound variables x and y, but there exists an algorithm that can do this job (see
Section 2.4).
Example 2.3 (Illustrates instantiation of type schemes). For the sake of this
and following examples let us extend Type with lists:
Let TE1 = TEo ±{x i-* (znt list) list} and TE2 = TE1 ±{g i-* int int int}
and consider
e = g(hd(rev(hd x))).
Here hd is a polymorphic function used once to take the head of a list of integer
lists and then once to get the head of an integer list. Thus in the following type
inference, two different instances of the type scheme of hd are used:
TE2 I- hd : (int list) list -- int list TE2 I- x : (znt list) list
(2.14)
TE2 I- hd x : int list
TE2 I- rev : int list -- znt list TE2 I- hd x : int list by (2.14)
(2.15)
TE2 I- rev(hd x) : int list
CHAPTER 2. MILNER'S POLYMORPHIC TYPE DISCIPLINE 17
Here it was the instantiations we had to guess because of the type of g the
instantiations we chose are the only ones that make the term well-typed.
Example 2.4 (Illustrates free type variables in the type environment). Take
TEo as in the previous example, but let TE1 = TEo ±{x i- (t' list) last} and
TE2 = TE1 ±{g'--p t' --> Q. Thus t and t' are free in TE2. Now the inference for
the same expression becomes
Example 2.5 (Illustrates the let rule, in particular the role of type variables free
in the type environment when types are generalized). We continue the previous
example. From (2.21) we get
Note that t' is free in TE1 and in the resulting type, whereas t is not free in TE1.
Now consider the expression (where first has type Vtlt2.t1 --a t2 --a t1)
(f first) 7
(f first) true.
(f cons) nil...
in TEi. The let rule (rule 2.12) requires that the body be checked in the type
environment
TEi=TE1±{f:`dt.(t'-->t)-->t}
since C1osTE1((t' --> t) --> t) _ Vt.(t' --> t) --> t. That we must not generalize on
t' is not too surprising, if we think of t' as a type constant (c.f. Example 2.4).
In the body of the above expression we use the following instantiations for f:
The following two lemmas are essential for the later proofs:
Lemma 2.6 For any S, if o > T' and o -S--+ 0'2 then Q2 > S T'.
Proof. Let o = `dal ... a,,.T and let I be the instantiation substitution,
I= fee, HT,I1<i<n}
with I T = T'. Now 0'2 ... j3,,.(So la, H 0,})T where {a, H /3,}
is of the form Vol I
J((So I la,
H Ns})T) = S(IT). (2.22)
J((So {a,
I -* /3 })a) = J(So a) = J(S a) = S a,
since Reg so nip,,..., /3,} = 0. But S a = S(I a), since a is not in {at, ... , an},
showing that (2.23) holds in this case as well. Thus we have (2.22) and since
IT = T', this gives the desired 02 > ST,
Lemma 2.7 IfTEH e : T andTE - TE'thenTE'H e : Sr.
We have already seen one application of this lemma, namely that the proof
in Example 2.3 could be obtained from the proof in Example 2.4.
TE I- el : r1 TE ±{x i- * ClosTETl } H e2 : T
(2.24)
TE H let x = e1 in e2 : T
Let {al.... an} be tyvars Tl \ tyvars TE. Let {,Ql, ... , ,Qn} be such that {a{
,
No ,Q, TE' (since TE --> TE' and /3 54 Reg(So)). Moreover, any type
is free in
Since TE -
on el and the first premise of (2.24) we have
C1osTET1 -S--+ C1osTEs
Moreover, we have
-
succeeds and there exists a substitution So and a type envzronment TEo such that
TE TEo and TE
Sow TE1 and So ClosTE0 TO > 7-1.
The proofs of Theorems 2.9 and 2.10 are by structural induction on e and use
Lemma 2.7.
CHAPTER 2. MILNER'S POLYMORPHIC TYPE DISCIPLINE 21
W (TE, e) = case e of
x = if x Dom TE then fail
else let t1a1... a,,.7- = TE(x)
/31 i ... , be new
,13,E
relating 5 to int, true to bool, and so on. In order to ensure that the definitions
really define something, we define the relation between values, v, and types T in
stages. We start with monotypes, y:
F-
e = Ax.el Here the type inference must have been of the form
by Lemma 2.7. Now let v' be such that = v' : S r' and assume
By induction on el, using (2.29), (2.30), and (2.31) we have rl 54 wrong and
r1:ST.
This proves = [x, el, E] : S7-'--+ S T, i.e., = r : S7-'--+ S7-.
Since this holds for any S, we have proved = r : T' -i T as desired.
e=el e2 Here the type inference must have been of the form
Let S be any total, ground substitution. There exists a TE° such that
TE + TE°. By Lemma 2.7 on the premises of (2.32) we have
By Definition 2.11, rl must be a closure, [xo, eo, Eo], say. Thus E F el e2 ---> r
was not by rule (2.6) i.e., it must have been by rule (2.4) or (2.5). Therefore,
there exists an r2 so that E I- e2 r2. -)
Using induction on e2 together with (2.34) we get that
Thus r2 is a value, vo, say. In particular, it must have been rule (2.4) that
was used.
Hence Eo ±{xo F---> vo} F- eo --> r.
Since I= [xo, eo, Eo] : S7-' -i S r and
vo : S T', we must therefore have that r # wrong and I= r : S7-.
Since this holds for any S, we have proved I= r : T.
Let S be any total, ground substitution. Let {al, ... , an} = tyvars T1
tyvars TE, let Sl = S ,j, tyvars TE and let So = S ,j, tyvars ClosTETl. Let
{01, . , On} be such that {a, F--> f,} is a bijection and no 0, is in Reg Sl. Then
no 0, is in Reg So, so
TE°F-e1:S'T1. (2.38)
Inspecting the evaluation rules we see that there must exist an r1 such that
E I- el ---, r1. Since = E : TE we have J
E : TE° so by induction on e1,
using (2.38), we get
r1 wrong and =r1:S'r-1.
Thus r1 is a value, v1, say. Then it must have been rule 2.7 that was applied
soE±{xHvl}I-e2--->r.
Since vl : S'7-1 we have = v1 : ClosTEo S'7-1 by Definition 2.12. Thus
Since we can do this for any S, we have proved r wrong and = r 7-.
:
I
Part II
An Imperative Language
Chapter 3
of e and ! stands for dereferencing. Notice that none of the variables have had
to be given explicit types. More importantly, this is an example of a polymor-
phic function that uses imperative features; intuitively, the most general type of
fast.severse is Vt.t list -+ t list.
The first ML [15] had typing rules for so-called letref bound variables. (Like
a PASCAL variable, a letref bound variable can be updated with an assignment
operation but, unlike a PASCAL variable, a letref bound variable is bound to a
permanent address in the store). The rules admitted some polymorphic fuctions
that used local letref bound variables.
Damas [13] went further in allowing references (or pointers, as other peo-
ple call them) as first order values and he gave an impressive extension of the
polymorphic type discipline to cope with this situation.
Yet, many more have thought about references and polymorphism without
publishing anything. Many, including the author, know all too well how easy it
is to guess some plausible typing rules that later turn out to be plain wrong.
Guessing and verifying are inseparable parts of developing a new theory. None
is prior to the other, neither in time nor in importance. I believe the reason why
the guessing has been so hard is precisely that the verifying has been hard. The
soundness of the LCF rules was stated informally, but no proof was published.'
In his thesis Damas did give a soundness proof for his system; it was based on
2There is some uncertainty as to whether a proof was carried out
CHAPTER 3. FORMULATION OF THE PROBLEM 29
e ::= x variable
Ax.el lambda abstraction
el e2 application
let x = el in e2 let expression
We assume values ref, asg, and deref bound to the variables ref, : =, and ! ,
respectively. We use the infix form e1:=e2 to mean (:= e1) e2. We introduce a
basic value done which is the value of expressions that are not meant to produce
an ordinary value (an example is e1: = e2). The objects in the dynamic semantics
are defined in Figure 3.1 and the rules appear in Figure 3.2. To reduce the
number of rules, and hence the length of our inductive proofs, we have changed
the dynamic semantics from Chapter 2 by removing wrong from the semantics.
3In the proof of Proposition 4, case INST, page 111, the requirements for using the induction
hypothesis are not met; I do not see how to get around this problem.
CHAPTER 3. FORMULATION OF THE PROBLEM 30
E Val
a E Addr
xEDomE
s, E F- -* E(x), s
s, E f- el --a asg, Si
sl,Efe2-4a,s2
S2,EI- e3-;v3,s3
s, E f- (el e2) e3 - -> done, s3 ± {a H V3}
s, E f- el - deref, sl
s,Ef-ele2- )v,s'
sl, E f- e2 ---> a, s' s'(a) = v
(3.6)
s,Ef-el->vl,sl sl,E±{xF+vl}f-e2-*v,s'
s,Ef-letx=eline2 +v,s'
TEf{x-+T'}F-61:T
TEF-Ax.ei:T'-pT
TEF-el:T'-+T TEF-e2:T'
TEI-ele2:T
However, the following example shows that with this system one can type
nonsensical programs.
let r = ref(Ax.x)
in (r:= Ax.x+1; (!r)true)
where ; stands for sequential evaluation (the dynamic and static inference rules
for ; will be given later). Also, x+1 is infix notation for (+x) and the type of l
+ is int -+ int -+ int. This program can be typed; the expression ref(Ax.x)
CHAPTER 3. FORMULATION OF THE PROBLEM 32
can get type (t --> t) ref and the body of the let expression is typable under the
assumption
{r H Vt.((t --> t) ref )} (3.8)
Now let us formulate a consistency result and see the point at which the
proof breaks down. Our starting point is the consistency result of Section 2.5,
Theorem 2.13 which read'
Theorem3.2 If a nd I - an d I -
In the presence of a store the addresses of which are values, the typing of
values becomes dependent on the store. (Obviously, the type of address a must
depend on what the store contains at address a). Thus the first step will be to
replace the relations = v : 7and = E : TE by s v : T and s = E : TE. Thus
we arrive at the following conjecture
Conjecture 3.3
s' =V:T.
Ifs = E : TE and TE f- e : T and s, E F- - v, s' then
However, it is not the case that the typing of values depends on just the
dynamic store, it also depends on a particular typing of the store. To see this,
consider the following example. Let
s = {a H nil}
E _ {x" a, yHa}
TE _ {x : (tint list) ref, y : (bool last) ref }
e = (.Az. I y) (x: = [7] )
Notice that x and y are bound to the same address. At first it might look like
we have s = E : TE -
after all, x is bound to a and s(a) has type tint list
4As we are not noncerned with wrong, this is a slight simplification of the original
theorem.
CHAPTER 3. FORMULATION OF THE PROBLEM 33
and, similarly, y is bound to a and s(a) has type bool list. But if we admitted
s E : TE, not even the above very fundamental conjecture would hold: we have
TE I- e : bool list and s, E I- e -f
[7], s', but certainly not s' [7] : bool list.
The solution to inconsistent assumptions about the types of stored objects is
to introduce a store typing, ST, to be a map from addresses to types, and replace
therelations s= v:7- ands= E:TEbys:ST= v:-rands:ST= E:TE,
respectively. Hence we arrive at the second conjecture.
The idea is that a stored object can have at most one type, namely the one given
by the store typing; formally,
With the current type inference system, conjecture 3.4 in fact false. However is
one can "almost" prove it and the one point where the proof breaks down gives
a hint how to improve the type inference system.
If we accept (3.9)
and attempt a proof of Conjecture 3.4 then we see that store
types must be able to contain free type variables. For instance, with s = ST = {}
and e = ref(Ax.x) we have TEo I- e :(t -* t) ref and Eo, {} F- e --> a, {a F-+
Ix, x, {}]}, for some a, so if we are to obtain the conclusion of the conjecture
{aH[x,x,{}]}:ST'= a:(t-*t)ref
then ST' must be {a H (t -* t)}, c.f. (3.9).
These free type variables in the store typings are extremely important. In
fact, they reveal what goes wrong in unsound inferences, as should soon become
clear. Let us attempt a proof of Conjecture 3.4 by induction on the depth of
inference of s, E I- e -)
v, s'. (It requires a definition of the relation =, of
course, but we shall soon see how that can be done). It turns out that all the
cases go through, except one, namely the case concerning let expressions
where
the proof breaks down in the most illuminating way. So let us assume that we
have defined and dealt succesfully with all other cases; we then come to the
dynamic inference rule for let expressions:
s,El-e1-->v1,s1 s1,E±{xHVI}I-e2-->v,s'
s, E I- let x = el in e2 v, s' >
(3.10)
CHAPTER 3. FORMULATION OF THE PROBLEM 34
(Recall that ClosmTl means dal ... a,,,.Tl, where feel.... , a,,} are the type vari-
ables in Tl that are not free in TE).
We now apply the induction hypothesis to the first premise of (3.10) together
with the first premise of (3.11) and the given s : ST = E : TE. Thus there exists
a ST 1 such that
sl : ST1 = Vi : Ti (3.12)
Before we can apply the induction hypothesis to the second premise of (3.10), we
must establish
sl:ST1 =E±{x-->vl}:TE±{x-->ClosTET1}
and to get this, we must strengthen (3.12) to
It is precisely this step that goes wrong, if we by taking the closure generalize on
type variables that occur free in ST1. The snag is that when we have imperative
features, there are really two places a type variable can occur free, namely (1) the
type environment and (2) the store typing. In both cases, generalization on such
a type variable is wrong. The naive extension of the polymorphic type discipline
fails because it ignores the free type variables in the store typing.
As a counter-example to conjecture 3.4, we can revisit example 3.1.5 Assum-
ing s = ST = {}, the dynamic evaluation was
from which it follows that ST1 must be {a --> (t -a t)}. The free occurrence of
t in STl expresses a dependence of the type of a on the store typing. therefore,
we cannot strengthen (3.15) to
The are various ways in which one can try to strengthen the theorem so
that the induction goes through. One approach is to try to formulate a side
condition on the let rule expressing on which type variables generalization is
admissible. But we should not be surprised that a natural condition is hard to
find - essentially it ought to involve the evolution of the store typings, but store
typings do not occur in the static semantics at all. One way out of this is to give
up having references as values and instead have updatable variables, because the
store typing then essentially becomes a part of the type environment. This was
what was done in the early version of ML used in Edinburgh LCF. Even though
generalization of the types of updatable references is prevented, one still has to
impose extra restrictions; see [15], page 49 rule (2)(i)(b) for details.
Another approach is to enrich the type inference system with information
about the store typing. To include the store typing itself is pointless since we
are not interested in the domain of the store. All that is of interest is the set
of type variables that occur free in the store typing. One way of enriching the
type inference system with information about this set is to partition the type
variables into two syntactic classes, those that are assumed to occur in the store
typing and those that are guaranteed not to occur in the store typing. Because
type checking is purely structural, the set of type variables that are assumed to
be in the store typing is in general a superset of the set of type variables that will
actually have to be in the store typing (it is undecidable to determine given an
arbitrary expression whether it generates a reference). This idea was first used
by Damas in his thesis, and I also use it in the system I shall now present.
Chapter 4
The Type Discipline
We first present the type inference system. Then we give examples of its use and
present a type checker.
The set Type of types, ranged over by r and the set TypeScheme of type schemes,
ranged over by a, are defined by
7r E TyCon = {stm, int, bool.... } type constructors
r ir a rl -a r2 rl ref
I I I types
a r Va.al
I type schemes
and type environments are defined by
fin
TE E TyEnv = Var TypeScheme.
to mean Val... an.T where {al, ... , an} = apptyvars T \ apptyvars TE is the set
of all applicative type variables in T not free in TE.
The type inference rules appear in Figure 4.1 and they allow us to infer
sequents of the form TE H e : T. We see that the first three rules are as before
but that the let rule has been split into two rules.
Notice that if TE contains no imperative type variables (free or bound) then
every type inference that could be done in the original system can also be done
in the new system. (Note that in rule 4.5 when Tl contains no imperative type
variables then taking the applicative closure is the same as taking the ordinary
closure). But in general TE will contain imperative type variables.
I TEF- e:T
(Recall that u is imperative, while t is applicative; the reason that only the type
of ref contains an imperative type variable should gradually become clear).
To give examples that have some bearing on real programming let us extend
the types with lists
T ... I Tl list
and functions
Example 4.1 As long as an expression does not have free variables whose type
contains imperative type variables, the type of the expression need not involve
imperative type variables. As an example we have
instantiations of the type scheme for !. Thus, by use of the let rule for non-
expansive expressions, rule 4.4, we get TE e2
f : stm, where
Syntax
e :.= el ; e2 sequential evaluation
while el do e2 while loop
begin el end parenthesis
( el ) parenthesis
Dynamic Semantics
s, E F- el -+ false, s'
s, E F- while el do e2 -) done, s'
s, E F- el --- true, sl
s1,EF-e2--v2,s2
S2, E F- while el do e2 -- * done, s'
s, E F- while el do e2 ----* done, s'
s,EI-e1---v,s'
S, E F- begin el end -) v, s'
s,EF-eI---v,s'
s,EF-(e1)---v,s'
Static Semantics
TEFe1:stm TEFe2:T
TEFel;e2:T
TE F e1 : boot TE F e2 : r
TE I- while el do e2: stm
TEI-e1:r
TE I- begin el end : r
TEI-e1:r
TEI-(el): r
Example 4.2 On the other hand, if the expression has a free variable whose type
(scheme) contains an imperative type variable, in particular if ref occurs free,
then the type of the expression may have to involve imperative type variables.
Hence TE I- el : u -4 u where
el = Ax.! (ref x)
el = ref ()x.x)
but not TE I- el : (t -> t) ref. Consequently, in an expression of the form
let r= ref(.\x.x) in e2
CHAPTER 4. THE TYPE DISCIPLINE 42
the let rule for expansive expressions, rule 4.5, will prohibit generalization from
(u --> u) ref to Vu.((u --+ u)) ref). Thus the faulty expression
Example 4.4 Here function that reverses lists in one single scan using iter-
is a
ation and a minimum number of applications of the :: constructor:
Note that u remains free as u after "Al." occurs free in the type environment,
namely in the type of 1. Now
let fast_reverse= el
in begin fastxeverse [1, 9, 7, 5];
fast-reverse [true, false, false]
end
is typable using rule 4.4, which allows the generalization from u list -- u list to
Vu.u list -+ u list.
As one would expect, since fast-reverse has type Vu.u list -* u list while
the applicative reverse function has type Vt.t list -* t list, there are programs
that are typable with the applicative version only. One example is
CHAPTER 4. THE TYPE DISCIPLINE 43
let reverse=
in let f = hd(reverse [Ax.x] )
in begin f(7); f(true) end
which can be typed under the assumption the reverse has type Vt.t list -> t list
but not under the assumption that reverse has the type Vu.u list -> u list.
Example 4.5 This example illustrates what I believe to be the only interesting
limitation of the inference system. The fast-reverse function is a special case
of folding a function f (e.g. cons) over a list 1 starting with initial result i (e.g.
nil).
el = Af.Ai.Al.
let data= ref 1 in
let result= ref i in
begin
while !data<>nil do
begin result:= f(hd(! data))(! result);
data:= tl(!data)
end;
!result
end
let fold= el in
begin fold cons nil [5,7,9];
fold cons nil [true, true, false]
end
because the let rule for non-expansive let expressions allows us to generalize on
ul and u2 in the type of fold.
However, we will not be able to type the very similar
let fold= el in
let fast-reverse= fold cons nil in
begin
fast-reverse [3,5,7];
fast-reverse [true, true, false]
end
CHAPTER 4. THE TYPE DISCIPLINE 44
because fold cons nil will be deemed expansive so that fast_reverse cannot
get the polymorphic type Vu.u last -f u last .
This illustrates that the syntactic classification into expansive and non-expan-
sive expressions is quite crude. Fortunately, as we shall see when we study the
soundness proof, soundness is not destroyed by taking a more sophisticated clas-
sification. Moreover, even with the simple classification we get a typable program
by changing the definition of fast_reverse to
Example 4.6 The final example is an expression which, if evaluated, would give
a run-time error, and which therefore must be rejected by the typing rules. If
you have some candidate for a clever type inference system, it might be worth
making sure that the expression e below really is untypable in your system. The
example illustrates the use of "own" variables, which form a dangerous threat to
soundness!
When applied to an argument x, the function mk_sham_id produces a function,
sham-id, which has an own variable with initial contents x. Each time sham_id
is applied to an argument it returns the argument with which it was last called
and stores the new argument.
TEI- e:r.
Any imperative type variable free in TE stands for some fixed, but unknown
type that occurs in the typing of the store prior to the dynamic evaluation of e.
Any imperative type variable bound in TE, in the type scheme ascribed to x,
say, stands for a type that might have to be added to the present store typing to
type new references that are created as a result of applying x.
Moreover, an imperative type variable that is free in r but not free in TE
ranges over types that may have to be added to the initial store typing to obtain
the resulting store typing. The "may have to be" is because, in general, more
type variables than strictly necessary may be imperative. For example we have
F- Ax.x : t -* t and also F- Ax.x : u -* u.
Finally let us discuss the let rule. The idea in the first of the two rules for
let x = el in e2 is that if TE F- el : 7-1 and el is non-expansive then the initial
and the resulting store typings are identical and so none of the imperative type
variables free in 7-1 but not free in TE will actually be added to the initial store
typing. Therefore, these imperative type variables may be quantified.
On the other hand, if el is expansive then we have to assume that the new
imperative type variables in 7-1 will have to be added to the initial store typing
and so the second let rule does not allow generalization on these.
In both cases, if 7-1 contains an applicative type variable t that is not free
in TE then t will not be added to the initial store typing simply because store
typings by definition contain no applicative type variables, and so generalization
on t is safe.
W1(TE, e) = case e of
x = if x Dom TE then fail
else let Val ... a,,.T = TE(x)
/31, ... , P. be new such that
a, is applicative if /3= is applicative
in (ID, {a, /3=}T)"
let t be a new applicative type variable
Ax.el =
(S1,T1) = W1(TE±{x i--> t},el)
in (Si, Si(t) --* T1)
el e2 = let (S1 i Ti) = Wi (TE, e1);
(S2,T2) = Wi(S1(TE), e2)
t be a new applicative type variable
S3 = Unzfy1(S2(Tl), T2 -* t)
in (S3S2S1, S3(t))
let x = e1 in e2=
let (S1,-r1) = W1(TE, e1)
v = if el is non-expansive then Clossl JTi
else AppCloss, TET1
(S2iT2) = W1(S1 TE ±{x i-r Q}, e2)
in (S2S1, T2)
Unzfyl(a,T)
{a --> if a is imperative
S(T)} U S,
provided a does not occur in T, where {a1 i ... , an} is apptyvars T and
"
{u1, ... , u,,} are new imperative type variables, and S is jai" u1,... , an un}.
That sound in the sense that (S, T) = W1(TE, e) implies that for all TE'
W1 is
with TE Si TE' we have TE' f- e T is easy to prove by structural induction on
:
e given a lemma that type inference is preserved under substitutions (this lemma
will be proved later, see lemma 5.2).
To prove that W1 is complete in the sense that it finds principal types for all
typable expressions requires more work. I have not done it simply because this
is where I had to stop, but I feel confident of the completeness of W1 because,
intuitively, W1 never has to make arbitrary choices. I believe that the proof will
be similar in spirit and simpler in detail than the proof of the completeness of
the signature checker in Part III.
Chapter 5
Proof of Soundness
We shall now prove the soundness of the type inference system. Substitutions
are at the core of all we do, so we start by proving lemmas about substitutions
and type inference. Then we shall define the quaternary relation s : ST = v :
T (discussed in Section 3.2) as the maximal fixpoint of a monotonic operator.
ImpType for all u E ImpTyVar. Substitutions are extended to types and they can
be composed. The restriction and region of a substitution is defined as before,
see Section 2.3. Similarly, we can define substitutions on type schemes and type
environments by ternary relations a1 S+ U2 and TE S+ TE':
Definition 5.1 Let a1 = Va1... a,.Tl and U2 = dtl ... #,,,.T2 be type schemes
and S be a substitution. We write o1 S--+ 0'2 if
1. m = n, and {a, i-4 i < i < n} is a bijection and at is imperative i f fli
/3, 1
The definition of instantiation (a > T) is as before but now with the new
meaning of type variables and substitutions. One can prove that if o > T and
o Sa Q' then o,' > S T. The proof is alr st identical to that of Lemma 2.6.
CHAPTER 5. PROOF OF SOUNDNESS 48
The following lemma will be used again and again in what follows.
Since TE -S + TE', no Q, is free in TE'. Moreover, any type variable that is not
a /3 but occurs in (Si I{a, "
/3 })Tl must be free in TE'. (The reason for this is
Vol ... /.3n.(Sl I{a, h-) #,})7-1 = C1osTE'(S1 I{a, h-) Qi})Tl.
Let S'= Sl I{a, " /3t}. Then we have
free in TE we have TE
is
on el, using the second premise of (5.1),
Close S'Tl.
- TE'. Thus by induction
(5.2)
By (5.2) we have
2.
1. Any applicative a in Tl which is not an a, is free in TE and TE
We have
Lemma 5.3 Assume a- -S--+ a-' and a-' > T1' and A is a set of type variables with
tyvars a C A. Then there exists a type Ti and a substitution Si such that o- > 7-1,
j
Sl Tl = Ti, and S A = Sl IA.
I V V I'
S1
Tl Ti
Write o, as Val ... a,,.T and a-' as b',131... ,6,,,,.T'. Since o Q' we have m = n,
a, is imperative if and only if ,6, is imperative, {a= i--> #,} is a bijection, no 0, is
in Reg So and (So If a, i-+ #,}) T = T', where So = S J. tyvars 0.
Since a-' > Ti there exists an
range of I' and let {Sl, ... Sk} be a set of type variables such that the renaming
,
a is free in a Here
where (*) is because {8 , ... , Sk} fl Reg(S 1 A) This shows 5.8 when a is
free in Q.
R-1(S . I
A) a, = R-1(S I A) RT(`)
T(i)
s:ST =v:T
if v = b then (v, T) E RBA;
if v = [x, el, E] then there exists a TE such that
s: ST = E:TEandTEH )x.e1:T;
if v = asg then r = rl ref -> Tl -> stm for some r1;
if v = ref then r = 0 -- 0 ref for some imperative 0;
if v = deref then r = rl ref ->
ifv=athen r=(ST(a))ref ands:STF-- s(a)
l
for some T1;
: ST(a)
s:STF-- E:TE
DomE = DomTE and Vx E DomE, s : ST = E(x) : TE(x).
The above property does not define a unique relation F--. However, it can be
regarded as a fixpoint equation
Rm'n=n{QcUIF(Q)cQ}
and
Rma'=U{Q9UIQ9F(Q)}. (5.10)
For our particular F, the minimal fixpoint Rm'n is strictly contained in the
maximal fixpoint R-' and it turns out that it is the latter we want. This is due
to the possibility of cycles in the store as illustrated by the following example.
in the empty store. At the point just before "r: s" is evaluated, the store
looks as follows
{ al F--) [x, x+1, Eo],
a2 H [y, (! r)y+2, Eo ±{r H al}]
}
CHAPTER 5. PROOF OF SOUNDNESS 54
where E0 is the initial environment; after the assignment the store becomes cyclic:
Now we would expect to have s': ST' = a1 : (int -> int) ref, where
where for simplicity I have ignored E0 and the initial type environment.
As we shall see below, one can think of this Q as the smallest consistent set
of typings containing q.
On the other hand, q is not in R""n. This can be seen as follows. There is an
alternative characterization of RI"'n, namely
Rn`n=UAFA (5.11)
where
FA = F(U,<AF') (5.12)
where ) ranges over all ordinals (see [1] for an introduction to inductive defini-
tions). In other words, one obtains Rn"n by starting from the empty set and then
applying F iteratively. It is easy to show that because q is cyclic there is no least
ordinal ) such that q E FA. Therefore q V Rn"n. 0
Let us try to explain informally why maximal fixpoints are often useful in op-
erational semantics. Let us first review the essential differences between minimal
and maximal fixpoints. In what follows, let U be a set and let F be a function
F : P(U) -> P(U) which is monotonic with respect to set inclusion.
CHAPTER 5. PROOF OF SOUNDNESS 55
and if, in order to prove claim of the form "X:On the day of the crime I was in
Paris with Y", F proceeds by investigating all claims of the form "Y: ... " then
F is never going to be able to prove either of the two claims.
The other way to interpret Q is to think of it as being the set of witnesses that
F has not proved wrong. Then F(Q) are the witnesses that cannot be proved
wrong, given that the witnesses in Q cannot be proved wrong. The monotonicity
of F now implies that the more witnesses that have been weeded out, the more
witnesses F can reject. Starting from Q = U, meaning that at the outset F
CHAPTER 5. PROOF OF SOUNDNESS 56
rejects nothing, F(U) is the set of witnesses that cannot be rejected because
they refer to witnesses in U. For example, we have (s : ST, 3, int) E F(U) but
(s : ST, 3, bool) F(U).
Using that F is monotonic we have
U D F(U) F(F(U)) D .. .
Rmax=U{QCUI QCF(Q)}.
For a set Q to have the property Q C F(Q) means that for each q E Q, q is
acceptable to F perhaps by virtue of other witnesses, but only witnesses within
Q. Each of these witnesses, in turn, are acceptable to F in the same sense. Thus,
no matter how many iterations F embarks on, no new witnesses need be called.
This motivates the following definition: Q is (F-) consistent if Q C F(Q).
To return to example 5.5 the Q we defined was the smallest F-consistent
set containing q and, as such, contained in the largest F-consistent set there is,
namely Rma".
To sum up,
the maximal fixpoint of F : U --+ U
It should now be obvious that maximal fixpoints are of interest whenever one
considers consistency properties, in particular when one wants to define relations
between objects that are inherently infinite, although they may have a finite
representation. In CCS [28], for example, observation equivalence of processes is
defined as the maximal fixpoint of a monotonic operator. As yet another example,
let us mention that the technique can be used to extend the soundness result of
CHAPTER 5. PROOF OF SOUNDNESS 57
Take = to be Rmax :
Definition 5.7 A typed store s': ST' succeeds a typed store s : ST, written
s: ST Es':ST',
if
1. STCST'
Dom ST C Dom ST' and for all x E Dom ST, ST(x) = ST'(x).
Notice that if s : ST C s' : ST' and Dom s = Dom s' then ST = ST', since
Dom ST = Dom s = Dom s' = Dom ST'.
The relation C is obviously reflexive and transitive. It is not antisymmetric.
From Property 5.4 we immediately get
U{Q9UI Q9F(Q)}
RmaX
=
is the largest set contained in its image under F.
First, take q1 = (s' : ST', v, T) E Q1; then
s : ST =v : T. (5.15)
on (5.15). Since s : ST C s': ST' this means T = (ST'(a)) ref and s : ST = s'(a)
ST'(a), i.e., (s' : ST', s'(a), ST'(a)) E Q1. Hence q1 E F1(Q).
Next, take q2 = (s': ST', v, o) E Q2. Thus
s:ST=v: a. (5.16)
The following lemma is used in the case concerning assignment (of the value
vo to the address ao).
CHAPTER 5. PROOF OF SOUNDNESS 60
Proof. Define
where ao, vo, s, s', and ST all are given and satisfy s : ST = vo : ST(ao) and
s'=s±{ao'-->vo}.
It will suffice to prove Q C F(Q).
First, take ql = (s' : ST, v, T) E Q1. Then
Finally, this lemma is crucial in the case regarding the let rule.
Proof. Define
Let A = tyvars(ST) U tyvars(a). Then by lemma 5.3 there exists a Tl and and
S1 such that a >,r1, S1 T1 =,r' and Sl I A = S j. A. In particular, S1(ST) = ST'.
hav e
This, together with S1(ST) = ST' and Sl T1 = ri gives (s : ST', v,-ri) E Q1. Since
we can do this for every Tl < a', we have q2 = (s : ST', v, a') E F2(Q) as desired.
Finally, take q3 = (s : ST', E, TE') E Q3. Let S and TE be such that
TE-S+ TE'and S(ST) = ST'and s : ST E:TE. Then Dom E = Dom TE and
Vx E DomE, s : ST E(x) : TE(x) and TE(x) --S--+ TE'(x). Thus Vx E DomE,
(s : ST', E(x),TE'(x)) E Q2 showing that q3 = (s : ST', E, TE') E F3(Q). M
The special case that is of basic concern is when the initial store is empty
(hence s = ST = {}), the only free variables in e are ref, !, and :=, and that E
and TE are the initial environments
Eo(ref) = ref
E0(') = deref
TE0(ref) = Vu.u -> u ref
TEo(!) = Vt.t ref t ref --
Eo(: _) = asg TEo(: =) = Vt.t ref t -> stm
-
:
where RBs still is the relation between basic values and types (relating 3 to int,
false to bool etc.).
Proof. The proof of 5.12 is by induction on the depth of the dynamic evaluation.
There is one case for each rule. The first case where one really sees the induction
hypothesis at work is the one for application of a closure. The crucial case is
of course the one for let expressions. Given the lemmas in the previous section,
neither assignment nor creation of a new reference offers great resistance.
CHAPTER 5. PROOF OF SOUNDNESS 63
we have s' : ST' = E(x) : TE(x), and since TE(x) < r, Property 5.4 gives
s': ST'=v:r as desired.
Lambda Abstraction, rule 3.2 Here e = .Ax.e1 and TE I- ) x.e1 : r and v =
[x, el, E] and s' = s. Let ST' = ST. Then s : ST C s' : ST'. Moreover,
S/ : ST' = [x, el, E] : r by Property 5.4.
Application of a Closure, rule 3.3 Here the situation is
and
TEo I- Ax0.eo: r'-;T. (5.24)
We now use induction on (5.26), (5.25), and the third premise of (5.20) to get
the desired ST'.
Notice that we could not have done induction on the depth of the type infer-
ence as we do not know anything about the depth of (5.24). Also note that the
present definition of what it
for a closure to have a type (which almost was
is
forced upon us because we needed F to be monotonic) now most conveniently
provides the TEo for (5.23).
Assignment, rule 3.4 Here e = (e1 e2) e3 so the inferences must have been
TEF-e1:T"-4(T'-4T) TEF-e2:T"
(5.27)
TEF-e1 e2:T'-4T
TEF-e1 e2:T'-4T TEF-e3:T'
(5.28)
TE I- (el e2) e3 : T
where s'=33±{aHv3}.
s, E F- (e1 e2) e3 -
2j EF- e 3 -->v 3) s 3
done, s3 ± {a -> v3}
(5.29)
By induction on the first premises of (5.27) and (5.29) there exists a ST1 such
that s:ST Es1:ST1and
s1 : ST1 = asg : T" -4 (T' -4 T).
and (5.29) we therefore get a ST2 such that s1 : ST1 C S2 : ST2 and S2 : ST2 =
a:T'ref.
Thus S2 : ST2 k E : TE. By induction on the second premise of (5.28) and
the third premise of (5.29) there exists an ST' such that s2 : ST2 C S3 : ST' and
S3: ST'=v3:T'. Thus we have s3: ST' =a:T'ref.
Thus we must have T' = ST'(a) so s3 : ST' V3 : ST'(a). Thus by the
assignment lemma, Lemma 5.10, we have S3: ST' C s': ST'. Since (done, stm) E
RBA we have s': ST' = done : stm, i.e., the desired s': ST' = v : T.
CHAPTER 5. PROOF OF SOUNDNESS 65
TEI-e1:T'-1T TEI-e2:T'
TE I- el e2 : 7-
s, E I- el -ref,s1 s1,EI-e2-->v2,s2
) aDoms2
s,EI- el e2-ia,s2±{aFfv2}
where s' = s2 ± {a - f v2}. By induction on the first premises there exists a ST1
such that s : ST C sl ref T' -a T. Thus by Property 5.4
: ST1 and s1 : ST1 :
TEI-e1:T'-aT TEI-e2:T'
TEI-ele2:T
s, E I- el -+ deref s1 sl, E e2 -+ a, s'
, F- s'(a) = v
s,EI-ele2) V, S'
By induction of the first premises there exists an ST1 such that s : ST C sl : ST1
and s1 : ST1 deref T' -a T. Thus T' = T ref.
Now s1 : ST1 = E : TE. Thus by induction on the second premises there is an
ST' such thatsl:ST1Es':ST'and s':ST' =a:Tref. Thuss:STEs':ST'
and s': ST'= s'(a):Ti.e.,s':ST' =v:T.
TEI-el:T1 (5.31)
and
TE ±{x --> AppClosTETi} I- e2: T (5.32)
for some T1,by rule 4.5. By induction on the first premise of (5.30) and (5.31)
there exists an ST, such that s : ST C sl : ST, and
Thus
s1:ST1 =E:TE (5.34)
contain applicative type variables. Thus T < AppClosTET1 ensures the existence
of a substitution S such that S(5T1) = ST, and S(Ti) = T. Thus, when we apply
the semantic substitution lemma, Lemma 5.11, on (5.33) we get
Since (5.36) holds for arbitrary 7- < AppClosTETi we have proved (5.35), c.f.
Property 5.4.
Then (5.34) and (5.35) give
Applying induction on the second premise of (5.30) and (5.37) and (5.32), we
get an ST' such that (s:STC)sl:ST,Cs':ST'ands':ST'J V:Tas desired.
CHAPTER 5. PROOF OF SOUNDNESS 67
TE I- el : Tl (5.38)
is a bijection and
by using lemma 5.2 on the identity substitution. Applying induction to the first
premises of (5.30) and (5.42) we get an ST1 such that s : ST C sl : ST1 and
= Dom s'
Since el is non-expansive, we have Dom s and this is the crucial -
property of non-expansive expressions. Since s : ST C sl : ST1 we have ST1 = ST
(recall the definition of C and note that Dom ST = Dom s = Dom s' = Dom ST').
Thus
sl:ST=E:TE (5.45)
and, by (5.44)
sl:ST =v1:RT1. (5.46)
sl : ST = v1 : ClosTE(Rr1). (5.47)
CHAPTER 5. PROOF OF SOUNDNESS 68
Hence T < ClosTE(R Ti) implies the existence of a substitution S with S(ST)
ST and S(RT1) = T. We now apply the semantic substitution lemma, Lemma 5.11,
to (5.46) to obtain
s1 : ST = v1 : T (5.48)
Since (5.48) holds for every T < ClosTE(R T1), we have proved (5.47), c.f.
Property 5.4.
From (5.45) and (5.47) we then get
Finally we apply induction to (5.49), the second premise of (5.30), and to (5.43)
to get the desired ST'. 0
From the proof case concerned with non-expansive expressions in let expres-
sions we learn that the important property of a non-expansive expression is that
it does not expand the domain of the store. Because of the very simple way we
have defined what it is for an expression to be non-expansive, non-expansive ex-
pressions will in fact leave the store unchanged. The proof shows that this is not
necessary; assignments are harmless, only creation of new references is critical.'
In larger languages -
ML, say -
the class of syntactically non-expansive
expressions is quite large. The class is closed under the application of many
primitive functions, and under many constructions. For instance, if e1 and e2 are
non-expansive, so is let x = e1 in e2.
the applicative system where P' is special in the sense that the type scheme for
ref is always instantiated to a monotype (i.e., a type without any type variables
at all). Then there is a proof P of TEO I- e : T in the modified inference system.
Hence corollary 5.13 gives the basic soundness of the special applicative type
inference.
Chapter 6
T ::= L I a I T ref 1 T1 -+ T2
where t ranges over primitive types and a ranges over one universal set of type
variables,
Next, type schemes, 77 are defined by
is a type scheme. The quantification binds over both Ti -+ T2 and A. The set
0 should be thought of as an addendu%to the whole of Ti -- T2, not just to r2.
CHAPTER 6. COMPARISON WITH DAMAS' INFERENCE SYSTEM 71
Roughly speaking, a function has the type (6.1) if it has the polymorphic type
Val ... a,.(T1 -r T2) and in addition 0 is an upper bound for the types of objects
to which new references will be created as a side-effect of applying the function.
For example,
TEo(ref) = Vt.t -3 t ref *{t} (6.2)
where TEo as usual means the initial type environment.
Type environments map variables to type schemes of the above kind. The
type inference rules allow us to infer sequents of the form
TEI-e:ri*0.
Since 71 can be of the form Val ... a,.Tl -3 T2 * 0' one can infer sequents of the
form
TE I- e : (VaI ... a,. T, -3 T2 * 0') * A. (6.4)
This device of nested sets of types is extremely important and provides a gen-
eralization of my rough classification of "expansive" versus "non-expansive" ex-
pressions. The rough idea in (6.3) is that 0
contains the types of all objects to
which new references may be created as a side-effect of evaluating e. In addition,
in (6.4), the set 0' contains the types of all objects to which new references will
be created when e is applied to an argument.
As an example, we will have
and so on for arbitrary levels of nesting. The present rule, however, does not
distinguish between whether it
application of the function itself, or, in
is the
the case where the result of the application is a function, the application of the
resulting function that creates the reference. For example, with the present rule
we will have
TE I- Ax.let y=ref x in \z.z :
Ti * 0
and also
TEH)x.Az.lety=refxinz:Ti*0
where q= dtl, t2.tl
-a t2 --> t2 * {t,}.
To suggest some terminology, we might call the types in the outer A-set for
the immediate store types and call the types in the inner 0-set the future store
types.
The generalization rule is
TE I- e :
Ti *,A a tyvars TE U tyvars O
(6.7)
TEHe:(Va.T)*0
Hence, if Ti has the formTl -4 T2 * 0' then a may be free in 0, the future store
types, but it must not be free in A, the immediate store types. This makes sense
following the discussion in Section 3.2 where it was demonstrated that it is the
immediate extension of the present store typing that can make generalization
unsound.
Next, the rule for application is
TEI-el:(T'-->T)*A TEI-e2:T'*0
TEI-ele2:T*0
Note that the type inferred for el has no future store types, only the immediate
store types. The point is that store types associated with el that have hitherto
been considered as belonging to the future are forced to be regarded as immediate
now that we apply el.
The rule for let expressions is
may be applied repeatedly to quantify all variables that are not in 0 and not
free in TE.
Also notice that
a type scheme whereas in the purely applicative system
772 is
the result was a type. This makes a difference in Damas' system because only
type schemes can contain store types. Thus we can infer for instance
TEo F- 7 : ant *0
TEo +{x F-> int} F- Ay.! (ref y) : (t -} t * {t}) *0
(6.10)
TEo F- let x=7in.\y.I(ref y):(t-}t*{t})*0
where t subsequently can be bound because it is a future store type only.
The distinction between immediate and future store types is finer than the
distinction between expansive and non-expansive expressions (see Section 4.1).
That variables and lambda abstraction are non-expansive corresponds to the set
of immediate store types being empty in rules (6.5) and (6.6). However, as we
saw in (6.10), the property of having an empty set of immediate store types
can be synthesized from subexpressions. This is true even when applications are
involved; for example we have TEo F- e : (t -} t * {t}) * 0, where
When doing proofs in Damas' system, one will seek to partition the store
types in such a way that as many of them as possible belong to the future so
that one can get maximal use of the generalization rule. However, in typing an
application, future store types are being forced to be considered immediate. The
inference rule that allows this transition is the instantiation rule,
The relation * 0 > 71' * 0' is defined in terms of type scheme instantiation,
77
77> 71', which in turn is defined as follows' (here 0 ranges over non-quantified
type schemes, i.e., terms of the form r or T1 -} T2 * A):
'Taken from [13], page 95
CHAPTER 6. COMPARISON WITH DAMAS' INFERENCE SYSTEM 74
2. 77is Val ... a,,.T' -4 T * 0", 77' is V0 1. .. 0,.v and, assuming the
P. do not occur free in rt nor in 0', there are types r1, ... , T
such that v = [T,/a,](T' -+ T) and is a subset of 0'.
Note that the requirement 0 C 0' allows us to increase the set of immediate
store types at any point in the proof. This will make generalization harder, of
course, but it may be needed to get identical sets of immediate store types in the
premises of rules (6.8) and (6.9).
It is condition (2) in the above definition that allows the transition from future
store types to immediate store types. For example, we have
TEo F- ref : t last --+ t last ref *{t last} TEo F- nil : t list *{t list}
TEo F- ref nil : t last ref *{t list}
in which the unsound generalization on t is prevented.
Damas' inference rules translated into our notation are repeated in Figure 6.1.
At this point, I hope that the reader agrees that Damas' system looks plausible.
At the same time it is subtle enough that the question of soundness is difficult.
2From [13], page 96
CHAPTER 6. COMPARISON WITH DAMAS' INFERENCE SYSTEM 75
TE(s)=,q
TEFx:,q *0
TE±{x"T'}fel:T*0
TEH)x.el:(T'--+T*A)*0
TE ±{ f" T'--+ T, x
f
'T'} fel : T *
TE F rec x.el : (T' -4 T * A) * 0
0
6.2 Comparison
There are expressions that Damas can type, but I cannot. An example is
TEOF-e:(Vt.t-->t*{t})*01
can contain a mixture of strong and weak type variables, store types have in
effect been included among types.
As for unification, if one unifies a against a type T in which a does not
a weak
occur, then the unifying substitution is {a R T} U R where R is a substitution
mapping the strong type variables occurring in T to new weak type variables. (In
the imperative version of the type checker, each variable has a bit for weak/strong
and the effect of applying R is achieved by overwriting this bit). It is true that
when the unification algorithm has to choose new type variables, the unifier,
So, it produces cannot be mediating for every unifier, S, because S may have a
different idea of what should happen to the new type variables. Perhaps this is
the difficulty Damas refers to. But if one wants to be precise, the proof of the
completeness of the type checker must account for what it is for a type variable
to be new and I claim that all that is needed of So is that it is mediating for all
other unifiers on the domain of used variables. The proof of the completeness of
the signature checker in Part III should give an idea of how the proof would go.
Even though Damas' system admits programs that mine rejects, there are
still sensible programs that cannot be typed by Damas. A good example is the
fold function from Example 4.5. The problem is that Damas' system too is
vulnerable to curried functions or, more generally, lambda abstractions within
lambda abstractions.
One idea to overcome this problem, due to David MacQueen, is to associate a
natural number,the rank, say, with each type variable. Moreover, type inference
is relative to the current level of lambda nesting, n, say. Intuitively, immediate
store type variables correspond to type variables of rank n; the type variables with
rank n + 1 range over types that will enter the store typing after one application
of the current expression, and so on. An applicative type variable can then be
represented as a variable with rank oo. It would be interesting to see the rules
written down and their soundness investigated using the method of the previous
chapter.
6.3 Pragmatics
Obviously, there is a tension between the desire for very simple rules that we can
all understand and very advanced rules that admit as many sensible programs as
CHAPTER 6. COMPARISON WITH DAMAS' INFERENCE SYSTEM 78
possible. In the one end of this spectrum is the system I propose - it is very easy
to explain what it is for an expression to be non-expansive and, judging from the
examples given, the system allows a fairly wide range of programs to be typed.
Then comes Damas' system. I am not convinced that the extra complexity
it offers is justified by the larger class of programs it admits. If one wants to
be clever about lambda nesting, then one might as well take the full step and
investigate MacQueen's idea further.
Part III
A Module Language
79
Chapter 7
Typed Modules
The type disciplines in the previous parts are suitable when programs are com-
piled in their entirety. A small program can simply be recompiled every time it is
changed, but this becomes impractical for larger programs. Many languages pro-
vide facilities for breaking large programs into relatively independent modules. A
module can then be compiled separately provided its interface to its surroundings
is known.
Sometimes modules are defined not as the units of separate compilation but
rather as a means of delimiting scope and protecting "private" data from the
surroundings. In any case, a module is typically a collection of components, where
a component can be a value, a variable, a function, a procedure or a data type.
Other terms for "module" are "package" [41], "object" [2] and "structure" [25].
The notion of interface varies from language to language, but typically an
interface lists names together with some specification involving these names. A
module, M, matches an interface, I, if M has the components specified in I and
if these components satisfy the specifications in I. Other terms for "interface"
are "package specification" [41], "class" [2] and "signature"[25].
One often wants to write and compile a module, M2, which depends on an-
other module, M1, before M1 is written. In that case the meaning of A12 is
relative to some assumptions about the properties of All,. Let us assume that
M2 can access M1 as specified by the interface 11. Then we want to be able to
write an abstraction of the form AM1 : Il . M2. Later, we can define an actual
argument module, M, and perform the application
(AM,: Il M2)(M)
. (7.1)
to create a module in which those components of M2 that stem from the formal
80
CHAPTER 7. TYPED MODULES 81
of a record can be significant for the type of other components). More complex
"modules" can be built using abstraction and application. Dependent sum and
dependent product suffice to give strong expressive power.
It is desirable that interface checking can be done at compile time rather than
as a part of the execution so that one can make sure that modules at least fit
AM,:I,.M2
if the interface Il postulates two modules both containing a type called stack it
might well be that the body of M2 makes sense only if the two stack types are
assumed to be identical. Thus one would find a sharing specification, perhaps
something like
sharing M.stack = M'.stack
in I,.
If by removing the distinction between small and big programs we obtain that
modules can be handled as other values it becomes impossible to tell statically
whether two modules (or types) are identical.
This leads to the idea of a stratified language: at the bottom the core lan-
guage in which we write small programs; on top a module language. The module
language may allow abstraction and application, but the operations on modules
are kept simple enough that module equality and other properties we want to
check statically remain decidable.
So the main motivation for having a stratified language is that we want more
information about modules than ordinary type checking can give us.
The languages in Part I and II are typical core languages. We shall now
present a module language which has a type discipline that handles sharing and
is very similar to the previous polymorphic type disciplines.
Chapter 8
ML semantics.
We shall first define the syntax of ModL and then give a static semantics
which enables one to infer what structures are created as a result of evaluating
a structure expression so that sharing specifications and functor applications
can be checked statically. We shall then show theorems about the semantics,
in particular that there exists an algorithm, the signature checker, that finds
so-called principal signatures of all legitimate signature expressions.
8.1 Syntax
Assume the following sets of identifiers:
dec empty
structure strid = strexp structure
decl dec2 sequential
spec empty
structure strid : sigexp structure
spec1 spec2 sequential
sharing longstrzd 1 = longstrzd 2 sharing
structure IntStack=
struct
type elt= int
val stack= ref [ ]
fun push(x: elt)= ...
fun pop( ... )_ ...
end
signature StackSig=
sig
type elt
val stack: elt list ref
fun push: elt-> ...
fun pop:...
end
end)
Example 8.2 Here is an example of how sharing can come about by construc-
tion.
structure StackUserl=
struct
structure A1= SharedStack
fun f(x)= ... Al.push( ...) ...
end
structure StackUser2=
struct
structure A2= SharedStack
fun g( ... )= ... A2.pop ...
end
end
Here StackUserl pushes SharedStack while StackUser2 pops it. The ex-
plicit dependency of both users upon the stack has been acknowledged by in-
corporating the shared stack as a substructure in each of the users, under the
identifiers Al and A2, respectively. The above structure with its three substruc-
tures matches the following signature:
CHAPTER 8. THE LANGUAGE MODL
signature Users=
sig
structure StackUserl:
sig
structure Al: sig end
end
structure StackUser2:
sig
structure A2: sig end
end
sharing StackUserl.A1 = StackUser2.A2
end
Sharing is particularly important in functor declarations since the body of
the functor may only make sense provided certain sharing constraints are met.
If, for example two stack users are mentioned in a functor parameter it might
be important that they use the same stack. Therefore one needs to be able to
declare a functor like
NameSet Fin(StrName)
Env
Str
Strld- Str
StrName x Env
Sig NameSet x Str
Funlnst Str x NameSet x Str
FunSig NameSet x Str x NameSet x Str
FunEnv FunId fin FunSig
-fin+
be +b
Here the difference between structure names and structure identifiers is obvi-
ous.
For any structure S = (n, E) we call n the structure name of S; also, the proper
substructures of S are the members of Rng E and their proper substructures. The
substructures of S are S and its proper substructures.
A signature E takes the form (N)S where the prefix (N) binds names in S.
A structure is bound in (N)S if it occurs in S and its name is in N. The set of
bound structures of E is denoted boundstrs(E).
The idea is that bound names can be instantiated to other names during
signature matching, whereas free names in the signature must be left unchanged.
In the signature from Example 8.2 all names are bound since no sharing with
structures outside the signature was specified. In diagrams, nodes with bound
names are open circles, whereas free nodes are filled out. The signature from
Example 8.2 can be drawn as follows:
CHAPTER 8. THE LANGUAGE MODL 91
StackUser
ha 6h
We now see the first sign of a correspondence with the polymorphic type
disciplines of Part I and II; a structure S corresponds to a type r, while a signature
(N)S corresponds to a type scheme Va1... an-
7-There are two important aspects of signature matching. Given a signature
This leaves open the definition of signature instantiation >. One possibility is
to define it so that it only changes names but preserves the number of components
and then leave all the widening to -<. The other extreme is to allow instantiation
to do widening so that we strengthen the requirement So -< S to So = S. The
two definitions give different semantics, but curious as it may seem, the same
CHAPTER 8. THE LANGUAGE MODL 92
inference rules can be used in both cases. We shall therefore defer the detailed
discussion of the two alternatives till we have presented the rules. In both cases,
the instantiation E > S to structures extends to instantiation to signatures:
A functor signature takes the form (N)(S, (N')S'). Here the prefix (N')
binds names over S' and the prefix (N) binds over S and also over free names
in (N')S'. Here (N)S stems from the formal parameter signature of the functor
declaration. Moreover, S' is the formal result structure of the functor; the prefix
(N') binds those names of S' that must be generated afresh upon each application
of the functor as will be explained in more detail below. Names that are free in
(N')S' and also occur in S signify sharing between the formal argument and the
formal result. An example where this occurs is
({a, b}) ((a, {Al i--> (b, {}), A2 i--> (b, {})}) , (b, {}))
ob
but again there are two natural definitions for the same inference rules, so we defer
the detailed discussion of the alternatives till later. No matter which definition
is chosen, the following functor instance matches the functor signature we drew
above.
d
d
Note how sharing between the formal argument and result has been converted
into sharing between the actual argument and result.
Finally, a basis B = M, F, G, E is the semantic object in which all phrases are
elaborated. The environments F, G and E bind semantic objects to identifiers
that occur free in the phrase. Here F is a functor environment mapping functor
identifiers to functor signatures, G is a signature environment mapping signature
identifiers to signatures and E is a (structure) environment mapping structure
identifiers to structures. Finally, M is a set of structure names. It serves two
purposes.
Firstly, M records the names of all structures that have been generated so far.
This use is relevant to the elaboration of declarations, structure expressions and
programs since these are the phrase classes that can generate "new" structures.
Whenever we need a "fresh" structure name, we simply choose it disjoint from all
names in M. In general, a name can have been used although it is not currently
accessible via the F, G, or E components of the basis. Therefore M is not just
redundant information about the other components.
Secondly, M contains all names that are to be considered as "constants" in
the current basis. This becomes important when we study the signature checker
but it is worth having in mind already when reading the rules. The type checker
CHAPTER 8. THE LANGUAGE MODL 94
8.3 Notation
Free structures and names: It is sometimes convenient to work with an arbi-
trary semantic object A, or assembly A of such objects. In general, strnames(A)
denotes the set of structure names occurring free in A. A structure is said to be
free if its name is free and strs(A) means the set of structures that occur free in
A.
We often need to change bound names in semantic objects. For arbitrary A
it is sometimes convenient to assume that all nameset prefixes N occurring in A
are disjoint. In that case we say that we are disjoining bound names in A.
Projection: We often need to select components of tuples - for example
the environment of a basis. In such cases we rely on variable names to indicate
which component is selected. For instance "E of B" means "the environment
component of B" and "n of S" means "the name of S."
Moreover, when a tuple contains a finite map we shall "apply" the tuple to
an argument, relying on the syntactic class of the argument to determine the
relevant function. For instance B(funid) means (F ofB)funid.
Finally, environments may be applied to long identifiers. For instance if
CHAPTER 8. THE LANGUAGE MODL 95
B H phrase =A
where A is some semantic object. The relation is read "phrase elaborates to A
in the basis B."
(8.2)
BH 0
CHAPTER 8. THE LANGUAGE MODL 96
B strexp
F- S
B I- structure strid = strexp = {strid H S}
(8.4) The use of ®, here and elsewhere, ensures that the names generated during
the first sub-phrase are considered used during the elaboration of the second
sub-phrase.
B I- dec E n V strnames(E) U (M of B)
B I- struct dec end (n, E)
B(longstrid) = S
B F- longstrid S
(8.5) The side condition ensures that the resulting structure receives a new
name. If the expression occurs in a functor body the structure name will
be bound by (N') in rule will ensure that for each application of
8.18. This
the functor, by rule 8.7 (last premise), a new distinct name will be chosen
for the structure generated.
(8.7) The interpretation of this rule depends of the definition of the functor
instantiation relation as will be discussed in Section 9.1. The purpose of
the last premise was explained above. It can always be satisfied by choosing
the bound names in the functor instance (S, (N')S') appropriately.
CHAPTER 8. THE LANGUAGE MODL 97
Specifications B I- spec =E
B F = {}
B H sigexp = (0) S
B F structure strid : sigexp = {strid H S}
n of B(longstrid 1) = n of B(longstrid 2)
(8.11)
B H sharing longstrzd 1 = longstrid 2 = { }
Comments:
'For each of the two definitions of signature instantiation "implied" means a different thing.
CHAPTER 8. THE LANGUAGE MODL 98
(8.11) The premise is a simple test of identity of names. The liberty that
rule 8.12 and 8.13 give to choose names can be used to achieve the sharing
before it is tested.2
BI-spec=E
(8.12)
B I- sig spec end = (0) (n, E)
B(sigid) = E
(8.13)
BI-sigid=E
(8.12) In contrast to rule 8.5, n is not here required to be new. The name n
may be chosen to achieve the sharing required in rule 8.11.
(8.15) This rule is called the znstantzation rule. It's interpretation obviously
depends on the definition of signature instantiation.3 Regardless of which
of the two definitions we take, the instance is not determined by the rule;
the generalization and instantiation rules are often used to achieve sharing
properties.
8.4.3 Programs
These rules are monomorphic in the same sense as the rules for declarations and
structure expressions.
2While humans can make such predictive choices when doing proofs in this formal sys-
tem, the signature checker will try to unify the two structures upon encountering the sharing
specification
'Exactly how, will be discussed in Section 9 1.
CHAPTER 8. THE LANGUAGE MODL 99
(8.17) The principality requirement ensures that the signature bound to sigid
has exactly the components and sharing implied by sigezp.
a a
A A
b c
The static elaboration may change the underlying assembly of semantic ob-
jects but only as long as the consistency conditions are maintained. Therefore
the rules are only part of the semantics. The foundation on which they are built
is the definition of what an admissible assembly of semantic objects is.
In this chapter we shall describe two different definitions of admissibility.
They give rise to different notions of signature instantiation and functor instan-
tiation and two quite different interpretations of the inference rules.
Definition 9.2 (Structure Equality) Two structures (n, E) and (n', E') are
equal, written (n, E) = (n', E'), if n = n' and E = E'. Two environments E and
E' are equal, written E = E, if Dom(E) = Dom(E') and for all strid E Dom(E)
one has E(strzd) = E'(strid ).
Then it will be obvious that coherence implies consistency, but not the other
way around. For instance the assembly consisting of the three structures
a a
A B
b c
9.1.1 Coherence
First let us consider signature matching. Recalling Definition 8.4, if So and S
are coherent and So -< S then So = S. Therefore S matches (N')S' precisely if
(N')S' > S. Thus the instantiation will have to do both the change of bound
names and the widening.
If two substructures Si and S'2 of S' have the same name then they must
be matched by structures S1 and S2 with n of Sl = n of S2. By coherence
n of S1 = n of S2 implies S1 = S2. Thus matching could be described by a map
from names in S' to substructures of S. By coherence of S' this is equivalent
to a map from substructures of S' to substructures of S. The change of names
together with the widening is captured by the following definition
of for all S E Str and all strid, if S(strid) exists then ('P S)strid exists and
cp(S strid) = ('p S)strzd.
{n,"n/ 11<i<k}
can first be extended to a total map on StrName by letting it be the identity
outside In,, , nk} and this map then induces a realisation map, denoted pa.
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 103
(n, Wo E) if (n, E) A,
wo(n, E)
W(n, E) if (n, E) E A.
this means that no free structure contains a bound structure). More generally, if
p (for renaming) is a finite bijection from structure names to structure names, A
is a substructure closed set of structures such that strnames(A) fl Dom(p) = 0,
and cpo is a finite realisation whose domain is A then the simultaneous compo-
sition of cpo and p, written CPo JAp is the realisation defined as follows. For all
S = (n, E) E Str,
WO(S) if S E A;
(coo IAP)S = (p(n), (coo JAP) E) if n E Domp;
(n, (coo AP) E)
I
otherwise.
It easy to check that coo JAP really is a realisation. We shall often omit the
is
subscript A in coo JAP since A has to be the domain of coo.
1. N2 fl Reg(coo) = 0, and
co co
Formally
Since performs widening as well as change of names the actual result may
(P
have more components that the formal result. For example the following functor
instance
td
A
e4 1e 4e
is an instance of the functor signature (8.1). Another example is the functor
which has the functor signature {n}((n, {}), (0)(n, {})). In any instance of this
functor signature the actual argument and result will be identical, so F acts like
the identity functor.
Now let us review the inference rules that in interesting ways depend on these
definitions.
Rule 8.7 simplifies to to
B(funid) > (S, (N')S') B I- strexp =S
N' n (M of B) = 0
(9.2)
B I- funid(strexp) S'
and the thing to note is that the actual result, S', may have more components
that the formal result, in fact no components of the actual result :a r' lost as a
result of the functor application.
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 106
Rule 8.11 concerning sharing is now effectively a test for structure identity
as the premise by coherence implies B(longstrid ) = B(longstrid 2). Structure
identity can be achieved by the generalization and instantiation rules, which now
allow widening as well as name instantiation. An example of this is the signature
expression
sig
structure A:
sig structure Al: sig end
end
structure B:
sig structure A2: sig end
end
sharing A = B
end
d c C( "b d
where A has an A2 component and B an Al component.
9.1.2 Consistency
First, let us consider signature matching. We can now allow S to match E, where
S is
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 107
and Eis
but since here we have an example of one substructure of the signature being
matched by two different substructures we can no longer describe the matching
by a realisation map from structures to structures. Instead we let realisation
simply be a map from names to names and leave the widening to the enrichment
relation -<.
Now Supp W means the set of n for which (p n 54 n and the definition of
signature instantiation becomes
1. N2 fl Reg((Po) = 0, and
However, since realisation no longer performs widening, the actual result will
always have exactly the same number of components as the formal result. So
now the functor instance
0 d
now is the functor that cuts out all the components of its argument.
As to the inference rules, we have already noted that in the rule for functor
application (8.7) the formal and actual results have the same number of compo-
nents. The instantiation rule no longer admits widening, but that is no longer
needed since the sharing rule only tests for name equality. Hence the signature
expression
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 109
sig
structure A:
sig structure Al: sig end
end
structure B:
sig structure A2: sig end
end
sharing A = B
end
Since fewer paths are present in principal signatures, fewer functor declara-
tions (rule 8.18) will be admitted.
had to coerce the number of components of the structure to which strexp elab-
orates down to the number of components mentioned in sigexp without ruining
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 110
sharing information between the full and the cut down version of the structure.
This cannot be done in the coherent semantics, but it can be done in the consis-
tent semantics.
It is dangerous to claim that the results I prove in the coherent semantics
carry over to the consistent semantics. However, I would be very surprised if
it should turn out that the main results (the existence of principal unifiers and
signatures) did not carry over.
I shall now turn to other restrictions that semantic objects must satisfy in
order to be admissible.
M-Str={SEStrInofSEM}.
Moreover, for any object or assembly, A, we define the (free) M-structures of A,
written
M-strs A,
to mean M-Str (1 strs A, i.e.,
M-strs A= IS E Str n of S E
I M and S occurs free in A}.
Proof. We first prove the implication from left to right. Assume (N)S >
(N')S'. Clearly (N') S' > S'. Thus by definition 8.5 we have (N) S > S'.
We prove N' n strnames((N)S) = 0 indirectly. Assume
n' E N' n strnames((N)S). Let n be a name different from n'. Then {n' i-* n} is
a realisation and Supp({n' i-* n}) fl strs S' C boundstrs((N')S'). Thus (N')S' >
{n' i-+ n} S'. By definition 8.5 this implies (N)S > {n' H n} S'. But that is
impossible; n' occurs free in (N)S and hence in any instance of it, but it obviously
does not occur in {n''--> n} S'. Thus N' fl strnames((N)S) = 0.
To prove the implication from right to left, assume (N)S > S' and N' n
strnames((N)S) = 0. Assume (N')S' > So and prove (N)S > So. By as-
sumption there exists a realisation 0 such that 0 S' = So and Supp 0 fl strs S' C
boundstrs((N')S'), and there exists a realisation Yo with Yo S S' and
Supp Yo n strs S C boundstrs((N)S). Thus 0 o is a realisation with ' o y(S) =
So. Moreover, if Si E strs((N)S) then 'p glides on Si so n of 'P Si = n of Si
which is not bound in (N')S' - since by assumption N' n strnames((N)S) = 0.
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 113
Corollary 9.16 If E > E' and E is well formed then strs E C strs E'.
The relation E > E' is obviously reflexive and transitive. Thus we get an
equivalence relation - defined by
E - E' E >E'andE'>E.
The following lemma gives a characterization of this equivalence. Basically,
two signatures are equivalent if and only if one can be obtained from the other
by renaming of bound names together with deletion or insertion of redundant
bound variables. More precisely, defining boundnames((N)S) to mean the set
N fl strnames S, we have
1. -
(N)S (N')S'
2. a) strnames((N)S) = strnames((N')S') and
b) There exists a bijection a : boundnames((N)S) -+ boundnames((N')S')
with au(S) = S'.
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 114
V(n', E') E strs S' an. -%(n', E') _ (n, -/ E'). (9.16)
CHAPTER 9. FOUNDATIONS OF THE SEMANTICS 115
Lemma 9.18 Given = (N1)(S1, (Nf)S,') and assume (N1)Sl > S2. Then
there exists an (N2)S2 such that > (S2, (N2)S2). Moreover, if D > (S2, (N2)S2)
and > (S2, (N2 )S2) then (N2) S2' « AN2)S2.
Chapter 10
Robustness Results
In this chapter we shall state a number of results relating realisation and elab-
oration. Just like one can get a better understanding of a program by stating
and proving properties of it, one can get a better understanding of an inference
system by stating and proving properties of it. So fundamental are the results
we shall now present that if they did not hold, we would feel that the seman-
tics would have to be changed. Moreover, we shall use most of the results in
subsequent proofs.
To avoid unreasonable punishment of readers who do not want to study the
details most of the proofs are deferred to Appendix A.
Lemma 10.1 If E is admissible and E > S' and E 0' E1 then E1 > '0 S.
Lemma 10.2
E1 > Ei.
If E - E1 and E--'-p4 Ei and E > E' and E is admissible then
In definition 9.6 we boldly claimed that we could define the relation A1- A2
for any semantic objects. Functor signatures require a bit of care, though:
116
CHAPTER 10. ROBUSTNESS RESULTS 117
Definition 10.3 Let D1 = (N1)(S1, (Nf)S') and 'D2 = (N2)(S2, (N2)S2) be well-
formed functor signatures and (p be a realisation. We write 4)1 -> D2 if there
exists a bijection pl : N1 --> N2 and a bijection p : N1 U Nl --> N2 U N2' extending
pl such that
(a) Reg cpl nN2 = 0 and (cpl 1pl) Sj = S2,
where (p1 = 'p J, strs(N1)S1.
This is stronger than requiring (Ni) Sl -+ (N2) S2 and (Ni U Ni) S1-4(N2 U
N2') S2 because having one common renaming ensures that sharing between bound
structures in (N1)S1 and free structures in (Nf)S' is preserved. When N1 = 0
definition 10.3 simplifies to the obvious definition of
Theorem 10.5 Let B = M, F, G, E and B' = M', F', G', E' be bases with
B
If
b
B'.
Recall that when we write B' F- sigexp = E' we implicitly refer to admissible
proofs only (c.f. definition 9.12). Some of the admissibility constraints listed in
that definition follow from the assumptions (10.1) and (10.4), but others have to
be ensured by (10.2),(10.3) and (10.5),(10.6).
We shall mostly use the above theorem in the situation where Yo is an M-
realisation:
{P B, PE1} is coherent
then
cpBF-spec =cpE1.
Similarly, if
B F- sigexp =:- E and E E'
M-strs(E') is substructure closed
B rb B (10.7)
But (10.7) follows from nstrnames(B) and the fact that any strictly robust
basis is also robust. As to (10.8),
In the proof of theorem 10.8 (see Appendix A) one checks for each rule that
the bases occurring on the left hand side of the F- in the premises are strictly
robust assuming that the basis on the left hand side of the F- in the conclusion
was strictly robust. Therefore we accidently prove:
Theorem 10.12 If B F- strexp = S and B b B', then for all S' E Str,
Note that this realisation is the dual of the realisation on signature inferences.
In the latter case we are mostly interested in M-realisations (Corollary 10.10)
that can be used to change structures that do not stem from the basis, whereas
in the above theorem the realisation affects structures stemming from the basis
but glides on new structures (up to the renaming of new names).
Most importantly, note that theorem 10.12 justifies the definition of functor
signatures and functor signature instantiation. Suppose for the moment that we
extend ModL programs to include
with the obvious inference rule. Moreover, assume that we allow structure dec-
CHAPTER 10. ROBUSTNESS RESULTS 122
then also
provided funid does not occur free in strexp2. The converse, that one can always
make an abstraction, does not in general hold here since strexp, may refer to
paths that are present in strexp2 but not in sigexp.
'Note that the explicit signature serves simply as a control that S matches the signature;
the decoration in no way constrains S. This choice is forced upon us in the coherent semantics.
In the consistent semantics the signature could constrain S
Chapter 11
Unification of Structures
A unifier for two structures S, S' is a realisation (p such that (p S = (p S'. More-
over, (p is said to be a principal unifier for S and S' if whenever 0 is a unifier for
S and S' there exists a realisation 0' such that 0 _ O' o W.
In this chapter we shall prove that if S and S' are coherent and have a unifier
then they have a principal unifier. We prove it by giving an algorithm, Unify,
which when given S and S' as parameters either fails or succeeds and succeeds
with principal unifier precisely if S and S' have a unifier.
a
The unification algorithm will be vital when we in the next chapter give an
algorithm for checking signature expression with sharing constraints, but the
unification we consider can also be seen as a generalisation of unification from
terms to certain directed acyclic graphs regardless of its use in the modules
semantics. The graphs we consider are those that correspond to so-called simple
subsets of Str:
S' there exists an M-realisation 0' such that 0 = O' o W. For the sake of the
semantics we are interested in M-unifiers. We shall solve the general problem of
123
CHAPTER 11. UNIFICATION OF STRUCTURES 124
determining when M-unifiers exist. The problem of deciding when unifiers exist
is a special case, namely M = 0.
Example 11.2 In the following pictures, M-nodes are filled out while the others
are little circles. There exists an M-unifier, cP, for S and S', where S =
and S' =
with wS=wS'=
c
A C
and there exists a principal M-unifier, -0, for S and S' with -0 S = 0 S' =
CHAPTER 11. UNIFICATION OF STRUCTURES 125
4f
or S' and S"', where S"' =
O r
Theorem 11.3 (Principal Unifiers) Assume that IS, S'} is coherent and that
M-strs{S, S'} is substructure closed. If S and S' have an M-unifier then they
have a principal M-unifier.
This is nice to know from a theoretical point of view. But from a practical
point of view it is also necessary to know how one finds out whether two struc-
tures are unifiable. Therefore we prove theorem 11.3 constructively by giving an
algorithm, Unify, which finds unifiers, when possible. More precisely, let us say
that an M-realisation cP is a locally principal M-unifier for S and S' if 'P S = 'P S'
and moreover, whenever 0 is an M-unifier for S and S' then there exists an
M-realisation, 0', such that
Theorem 11.4 (Unification) Assume that IS, S'} is coherent and that
M-strs{S, S'} is substructure closed. Either Unzfy(M, S, S') fails or it succeeds
with a locally principal M-unifier for S and S'. Moreover, Unify succeeds if and
only if there exists an M-unifier for S and S'.
This theorem really does imply theorem 11.3: if 'P is a locally principal M-
unifier for S and S', one obtains a principal M-unifier, 'P1, for S and S' as follows
E), if (n, E) occurs in S or in S',
Vi (n, E) - { P(n,
(n, E)
W otherwise.
Here is Unify:
CHAPTER 11. UNIFICATION OF STRUCTURES 126
Unify(M, S, S') =
let (n, E) = S; (n', E') = S' in
if n E M and n' E M then if n = n' then ID else fail
if n E M and n' M then
if Dom E' C Dom E then
let Wi = Unify(M, E, E'); c = {(n', wi E') H (n, E)}
in cowl
else fail
Unify(M, E, E') =
if Dom E fl Dom E'= 0 then ID
else let strid E Dom E fl Dom E'
{strid H Si} U El = E (disjoint union)
{strid H S'} U E' = E' (disjoint union)
wi = Unify(M, Si, Si)
Wz= Unify(M,Y'iEi,BpiEi)
in W21
For k = 1 and k = 2 there are particularly simple conditions that ensure that
{S1 -4 Si, ... , Sk -4 S'k} denotes a realisation.
For k = 1 condition is E of S1 C E of Si.1 In other words, the
a sufficient
operation of changing a given structure by perhaps changing its name and perhaps
widening it at the top is a realisation. The first e in Unify is of this kind.
For k = 2 a sufficient condition is
The conditions S strs E' and S' strs E is what in ordinary term unifi-
cation is known as the "occur check" . From the definition of realisation (defini-
tion 9.4) it is easy to see that if S and S' have a unifier, then S strs(E of S')
and S' strs(E of S).
In the case n E M and n' M we do not need an occur check "if Dom E' C
Dom E and S' strs E" because M-strs S is assumed substructure closed.
Vstrid E Dom E n Dom E', 'p E strzd = 'p E' strid (11.8)
Despair not! Among these properties (11.1) and (11.4) are the ones we pri-
marily want, whereas (11.2), (11.3), (11.5) and (11.7) are used partly to get
the induction to work and partly in the proof of the soundness of the signature
checker. Property (11.6) will give a simple termination argument in the next
section.
Note that (11.2) does not say "Supp C strs{S, S'}" for the very good reason
cp
that this inclusion is not true because cp accumulates all operations that have been
performed during the unification. This is why cp is a locally principal M-unifier,
not in general a principal unifier.
Proof. [of theorem 11.5] The proof is by induction on the length of the compu-
tation counted as the number, r, of recursive calls.
Base Case, r = 0. By the definition of Unify there are two cases, one for
structures and one for environments. The latter trivially gives (11.8)-(11.14)
and the former gives (11.1)-(11.7) using the coherence of W.
Inductive Step, r > 0. There are a number of cases corresponding to the def-
inition of the algorithm. We start by considering structures S = (n, E) and
S' = (n', E').
Proof of (11.1): (P(n',E') = e o coi(n', E') = e(n', c01 E') since (11.17) and
n' strnames{E, E'}. And (n', 01 E') = (n, E) = 0(n, E) since cP is an M-
realisation.
Proof of (11.2): Supp o f1W c Supp o1 f1W U Supp e f1W C
strs E U strs E' U ({ (n', 01 E') } fl W). By the coherence of W, { (n', 01 E') } n w C
{(n', E')}. Thus Supp co flW C strs{S, S'}.
Proof of (11.3): Inv cp C Inv 01 U Inv e C strnames{E, E'}
U strnames(n', 01 E') U strnames(n, E) C strnames{S, S'} by (11.17).
Proof of (11.5): 0 W is obtained from 01 W by replacing all occurrences of
(n', ol E') by (n, E). But (n, E) is already in ol W. It follows that cP W is finite,
coherent, and that cP W and M-strs W are substructure closed. Hence co W is
simple.
Proof of (11.6): cP is not ID. If 01 = ID then co W1 = e W1 = W1 1
I I I -
as we saw in the proof of (11.5). Otherwise, W W1 = e 01 W1 = 01 W1 1 <
I I -
JWI -1 < JWI by (11.20).
e = {(n, cot E) H (n, cot E U o1 E'), (n', o1 E') H (n, cot E U o1 E')}
and 0 =eo(P1.
By induction,
01 is an M-realisation (11.25)
Here (11.22) ensures that E1 = (1 E U (l E' really makes sense. Now n does
not occur in 'Pi E' -
since S strs E' and (11.24). Therefore S strs (l E' and
similarly, S' strs 'P1 E. It follows from the considerations in the previous section
that e is a realisation. It is clearly an M-realisation, so cp is an M-realisation
showing (11.4).
Proof of (11.1):
cPS = eco1(n,E)
= e(n, cp1 E) as (11.23) and S strs{E, E'}
e(n', (l E')
e cp1(n', E') as (11.23) and S' strs{E, E'}
= (PS'.
Proof of (11.2): Supp cp f1W C Supp cp1 f1W U Supp e f1W C
strs{E, E'} U ({(n, cpl E), (n', cpl E')} fl W) C strs{E, E'} U {S, S'} by the coher-
ence of W, so Supp cP flW C strs{S, S'}.
Proof of (11.3): Inv cp C Inv cp1 U Inv e C Inv (1 U strnames S U strnames S'
C strnames{S, S'}.
Proof of (11.5): cp W is obtained from cpl W by replacing all occurrences of
(n, cpl E) and (n', (l
E') by (n, cpl E U (1 E'). cpl W is simple by induction and
every structure in strs{cp1 E, cpl E'} is already in (l
W. Therefore cp W is simple.
Proof of (11.6): if ID then either cpl = ID and e
cp 5A ID or cp1 ID.
In the former case n J l -
n' so Jcp W _ Je W = IWI 1 as we saw in the proof
of (11.5). In the latter case,
co W l= e (P1 W
J j < jcp1 W see the proof of (11.5)
j j
01 is an M-realisation (11.32)
02 is an M-realisation (11.39)
If (p2 54 ID then 1
< (p1 W1
(p2 (p1 W1 I (11.41)
X02 does not change the name of any structure whose
(11.42)
name is in strnames{02 01 E1, CP2 o1 Ell.
Proof of (11.8): If strid = strid o then use (11.29), else use (11.36).
Proof of (11.9): Suffice to show that cp glides on every S" = (n", E") E
W \ strs{E, E'}. But cp1 glides on S" by (11.31) i.e., cp1 S" _ (n", o1 E"). Now
n" does not occur in Cpl E1 or in 01 E'1 (use (11.31)). Therefore, by (11.38), V2
glides on (n", (P1 E"). Thus 'p2 o 01 glides on (n", E").
Proof of (11.10): Inv (p C Inv 02 U Inv 01 C Inv Cpl U strnames E1
U strnames El (by (11.38)) strnames E U strnames E' by (11.31).
Next, (p is an M-realisation by (11.32) and (11.39) and (pW is simple with
respect to M by (11.40). Moreover, (11.13) follows from (11.34) and (11.41).
CHAPTER 11. UNIFICATION OF STRUCTURES 133
0 W=(1'oco)IW. (11.46)
Proof. The proof relies on theorem 11.5. In particular (11.6) and (11.13) give
a very painless proof of termination. The trick is to have an outer induction on
J W+ with an inner structural induction on the structures in W.
Outer Base Case, JWJ =0 Thus W = 0. The part of the statement regarding
structures is vacuously true. For the second part, strs{E, E'} C W implies
E = E'= {}. For every M-unifier, 0, for {} and {} (i.e., for every M-realisation)
cp = Unify(M, {}, {}) succeeds and
01 W =(OoID)I W=(OoW)IW
as desired.
Outer Inductive Step, IWI > 1 We assume that the theorem holds for all sim-
ple W' with JW'I < JWJ and prove that it holds for W by structural induction
on the structures in W.
Inner Inductive Step Let us first consider structures S = (n, E) and S' _
(n', E'). There are four, and only four, possibilities.
nEMand WE M Let 0 be an M-unifier for S and S'. Then S = 0S =
0 S' = S', W = Unify(M, S, S') returns cp = ID and 0 J, W = (0 o W. If S gyp)
and S' do not have an M-unifier we must have S 54 S' (as otherwise ID would
be an M-unifier), so n 54 n' by the coherence of W so Unify fails.
CHAPTER 11. UNIFICATION OF STRUCTURES 135
01 W=(blocpl)IW. (11.47)
As we saw in the soundness proof, {(n', Cpl E') i (n, E)} really does denote a
realisation map so it makes sense to say that Unzfy succeeds with the composition
W=Cowl.
Moreover, Cpl W is coherent and cp W is coherent and the latter is obtained
from the former by replacing all occurrences of (n', Cpl E') by (n, E). Consider an
S1 = (n1, E1) E (p W. If n1 n there exists exactly one structure, call it e-1(S1),
in (P1 W such that
e(e-1 Si) = S1.
(?1(e-1 S1)strzd = 0S
zb w by (11.47).
This proves (11.46).
Conversely, assume that S and S' have no M-unifier. If DomE' Dom E
then Unify fails, but if DomE' C DomE, there cannot be an M-unifier for
E and E' (since if W1 were one, e o (P1 would unify S and S' with e as in the
program). Therefore, by the inner induction, Unify(M, E, E') will fail so that
also Unify(M, S, S') fails.
nMandn'EMI Symmetric.
CHAPTER 11. UNIFICATION OF STRUCTURES 137
nMandn'M Similar to the two previous cases. Here are the details.
Assume 0 is an M-unifier for S and S'. Then S strs E' and S' strs E
so Unify passes the test and calls Bpi = Unify(M, E, E'). Since 0 is also an M-
unifier for E and E' we get by the inner induction that Bpi = Unify(M, E, E')
succeeds and that there exists an M-realisation z/i1 with
01 W=(b1o'p1). W. (11.48)
c = {(n,'p1 E) i-4 (n, vi E U'p1 E'), (n', pi E') '- (n, p1 E U'1 E')}
really is a realisation map, so it makes sense to say that Unify succeeds with
result V= E o 'pi.
We also saw that Bpi W is coherent, that 'p W is coherent, and that the latter is
obtained from the former by replacing all occurrences of (n, Bpi E) and (n', v, E')
by (n, 'pi E U 'p1 E').
Consider a Si = (ni, E1) E 'p W. If ni 54 n then there exists exactly one
structure in Bpi W, call it C'(S1), that satisfies
E(E-1(Si)) = S1 .
VA SO
Si)
=
{i(c(Si)) if not S, n,
b S if n of S1 = n.
Extend 0' to a total map by letting it glide outside 'p W. To prove that 0' is
a realisation we prove that for all Si E 'p W and for all strzd , if Si strid exists
then (O' S1)strid exists and (O' Si)strid = /'(Si strid ).
Again this is clear when n of Si 54 n and n of (Si strid) 54 n. The remaining
cases are:
Case 1: n of Si = n and n of (Si strid) 54 n.
Here Si strid = (n, Bpi E U 'p1 E')strid by the coherence of 'p W.
If strid E Dom E we have
,'(Si surd) = O'(cpi E strid )
_ 01 E-1(Vi E strid) as n of ('pi E strid) 54n
= 01 Bpi E strid as n strnames((pi E strid )
= 0 E strid by (11.48)
CHAPTER 11. UNIFICATION OF STRUCTURES 138
= ( S)strid as 0 is a realisation
= (,' Sl)strid by the definition of 0'.
Otherwise strid E Dom E' and we get
,b'(S1 strid) _ (/ S')strid as above
(0 S)strid since 0 unifies S and S'
("' Si)strzd
as desired.
Case 2: n of S1 n and n of (Sl strid) = n. Since S1 strid exists and
n of S1 z/ n, (e-1 Sl)strid must exist. Now a is a realisation map (see the proof
of theorem 11.5) so (e(e-1 Sl))strid exists and
(01(E-1 Si))strid = 7p S
we have In, n'} fl Inv co1 = 0. Therefore, n of (co1 w) 0 In, n'}. Thus by the
definition of ', 0'(W' w) _ 0'(e(co1 w)) = 01(co1 w) _ Ow by (11.48). This
shows (11.46).
CHAPTER 11. UNIFICATION OF STRUCTURES 139
Conversely assume that S and S' have no M-unifier. If S E strs E' or S' E
strs E then Unify fails. But if S strs E' and S' 0 E' there cannot be any M-
unifier for E and E' (if (1 were one, c o (p1 would be an M-unifier for S and S',
where c is as in the algorithm). Therefore by the inner induction, Unify(M, E, E')
fails so that also Unify(M, S, S') fails.
Continuing the case analysis in the inner inductive step, we now turn to
environments. So assume that not both of E and E' are the empty map. There
are two possibilities:
DomEflDomE' = 0 Trivial
01W=(01001)IW (11.49)
an M-unifier for El and E'1 so by (11.49) 01 is an M-unifier for (p1 E and (p1 E.
Now ifpl=IDwehave (p1El=E1and(p1Ei=E'1 and(p1W=Wandwe
simply apply the inner induction to conclude that (p1 = Unify(M, (p1 E1i (p1 Ei)
succeeds and that there exists an M-realisation 0' such that
observing that Unzfy succeeds with cp = (02 0 (p1 and thus 0 J. W = (V)' o (p) 1 W.
On the other hand, if (p1 is not ID, we use (11.6) of theorem 11.5 to infer
I cc1 W1 < JW I. Then we use the outer induction to infer the same conclusions.
Conversely, assume that E and E' have no M-unifier. Then
We now see that our initial theorem, theorem 11.4, follows from the sound-
ness and completeness theorems (theorem 11.5 and theorem 11.7). Assume
that IS, S'} is coherent and that M-strs{S, S'} is substructure closed. Then
W = strs{S, S'} is simple with respect to M. Either there exists an M-unifier
for S and S' or there does not. In the former case, P = Unify(M, S, S') succeeds
(by the completeness theorem), (P M-unifier (by the soundness theorem)
is an
which in fact is locally principal (by the completeness theorem). In the latter
case, Unify(M, S, S') fails by the completeness theorem.
Still under the assumption that each function symbol has a fixed arity, a
principal M-unifier for rep(ti) and rep(t2) gives a maximal unifier for tl and t2.
Therefore, the structure unification algorithm is also a decision procedure for the
existence of term unifiers, and when it succeeds, it produces an M-unifier from
which a maximal term unifier can be derived.2
Apart from the generality that lies in having o be a lattice, these definitions give
a richer variety of objects than our structures. Firstly, 0 need not be finite, so
in particular terms can be cyclic. Secondly, one has the ability to distinguish
between for example
and
(The first of these has three coreference classes, the second only two). In the
modules semantics based on coherence sharing is the same as structure identity,
so it is the latter interpretation we want. Any structure S = (n, E) can be drawn
as a tree or, equivalently, it can be regarded as a pair S = (0, 0), where 0 is
a finite term domain and 0 a map from addresses in 0 (i.e., nodes) to symbols
(i.e., structure names). We then turn a "structure" S = (0, 0) into a well-formed
term rep(S) = (0, 0, ic) by taking , _ Kma", where
Vu, v E Al
U KI"ax v if S(u) = S(v). (11.53)
alone a lattice. Instead, we shall take the flat lattice obtained by adding a gratest
element, T, and a smallest element, 1, to the unordered set of structure names.
Then we can think of a structure as a pair S = (0, 0), where Rng onIT, I} = 0.
Let us say that a realisation map W is name preserving if n of S = n of (cP S)
for all S. Then
Observation 11.8 There exists a name preserving realisation map, gyp, with
cP S1 = S2 if and only of rep(Si) }- rep (S2) -
Proof. Assume 'P S1 = S2, where 'p is a name preserving realisation. Clearly
Al C L. Since 'P is a map from structures to structures, we have ic'' C rc28?
and since 'P is name preserving we have ?1(w) = 02(w) showing (11.56).
Conversely, if rep(Si) }- rep(S2) then O1 C A2 so for all w E O1 we can
define
Y'(S1(w)) = S2(w)
Since C tc2 a" and these are maximal, we have that this equation actually
rcm
defines a map on Sl and its substructures. Extend this to a total map, also called
0, letting 0 glide outside S1. By definition 0 is a realisation. Moreover, rep(Si)
does not contain T and rep(S2) does not contain 1, so by (11.56), 0 preserves
names.
Unfortunately, name preserving realisations are not terribly interesting in the
modules semantics. Indeed, if we are not allowed to change the name of a given
structure it is because the structure is "constant" (Section 8.4) and so we should
not be allowed to add more components either.
This is the crucial difference between the two approaches. In Ait-Kaci's
approach, the adding of components is independent from the symbol ordering.
In our approach, the two are linked in that widening is allowed for structures
with bound names only. (Names not in M can be represented by T so that they
can be instantiated to either T or to an ordinary structure name). For instance
in Ait-Kaci's approach one can unify
a
and
CHAPTER 11. UNIFICATION OF STRUCTURES 144
to obtain a
and 0m
A
Ib
must fail.
Alt-Kaci has an elegant proof that if E is a lattice then the well-formed terms
over E form a lattice with the ordering -<. The construction of the greatest lower
bound corresponds to unification and is construed as a closure operation on the
coreference relations. This operation is very similar to the algorithm Unify up
to the difference described above.
Chapter 12
Principal Signatures
In this chapter we shall prove that if a signature expression has a signature then
it has a principal signature, as defined in definition 8.7. We do so by giving
an algorithm, a so-called signature checker, which either fails or succeeds and
succeeds with a principal signature when any legal signature exists.
The algorithm is called SC, which can be read "signature checker" or "specifi-
cation checker" depending on the phrase class, and uses the unification algorithm
defined in Chapter 11. Before disclosing the fascinating inner workings of SC, let
us summarize its properties.
In what follows, U ranges over finite subsets of StrName. Intuitively, U means
the set of "used" names.
Similarly, if
(go, E', U') = SC(B, spec, U)
succeeds then W is an M-realisation and
WBI-spec =E'.
'Because of the global constraints (definition 9.12), this says rather a lot about co(B) and
S.
145
CHAPTER 12. PRINCIPAL SIGNATURES 146
Intuitively, U contains all names "used" in B and U' is the set of new names
used in the call i.e., u fl U' = 0.
Recall from Section 9.2 that W B, the application of w to B, is defined by
Here E may contain variable structures that are affected by unification that
the level of signature declarations, B will be
takes place during the call of SC. At
strongly robust, so that W E = E, but if we are inside a specification or signature
expression then E may contain variable structures.
Moreover, SC has the property that it chooses new names in such a way that
E = Clos , B S.
(Recall from definition 9.14 that Clos ,B S means (N)S, where
N = strnames S \ strnames(M, F, G, W E).) Note that theorem 12.2 implies that
E is well-formed. (That E is coherent, in fact that {B, E} is coherent, follows
from theorem 12.1).
As for completeness, still assuming B = (M, F, G, E),
.' B I- szgexp = E.
Then (gyp, S, U') = SC(B, sigexp, U) succeeds and there exists an
Proof. The proof uses theorem 12.1, theorem 12.2 and theorem 12.3 all of which
we shall soon have the opportunity to prove. Moreover, we use corollary 10.6.
Assume B F- sigexp = E. Then by the global constraints (definition 9.12), B
is robust. Let U = strnames B and let zb = ID. Thus 0 B F- sigexp = E, so by
theorem 12.3,
(O, S, U') = SC(B, sigexp, U)
-
succeeds and there exists an
(O' o
M-realisation, 0', such that whenever
by use of the generalization rule without violating the global constraints. Let
E' be such that C1osW BS -L V. Then 0'(c' B) = B and E' > E. Thus it will
suffice to prove that
B F- sigexp = V. (12.3)
This we wish to prove by applying corollary 10.6 on (12.2). Thus we must prove
that M-strs E' is substructure closed and that {B, E'} is coherent. But since
every structure free in C1osWB S occurs free in O B, every structure free in E'
occurs free in b'(P B) = B. Therefore M-strs E' is substructure closed and
{B, E'} is coherent. Thus the desired (12.3) follows from (12.2). 1
The reader will probably already have noticed the similarity with the sound-
ness and completeness results that hold for the purely applicative type discipline
(see Part I, Section 2.4).
CHAPTER 12. PRINCIPAL SIGNATURES 148
( ) : (ID, {}, 0)
(specs spec2) :
SC(B, sigexp, U) =
let (M, F, G, E) = B in
case sigexp of
(sigid) .
In the algorithm ModL phrases are enclosed in angle brackets to avoid con-
fusion of reserved words. The case
because the generalisation and instantiation rules can be used to widen structures
that are not constants. To capture this, SC calls a function Fresh, which has the
following property:
no n1 nk-1 nk
0 1*
strid strid k
and U' = {no,. .. , nk}, u n U' = 0 and all the n, are distinct.
In the case sigexp = (sigid) the bound names are replaced by fresh names.
This is similar to taking a fresh generic instance in the type checker for the
applicative type discipline (Part I).
12.2 Soundness of SC
For brevity we shall use the following
succeeds, then
cP is an M-realisation and (12.4)
Observation 12.9 Theorem 12.6 implies theorem 12.1 and theorem 12.2 as fol-
lows. Assume that B is robust and that strnames B C U. Let W = strs B. Then
W covers B and MUstrnames W C U. Assume that (W, S, U') = SC(B, sigexp, U)
succeeds. Then, by theorem 12.6, cP in an M-realisation and W B F sigexp = (0) S
CHAPTER 12. PRINCIPAL SIGNATURES 152
Observation 12.10 To ease the proof of (12.6), we shall now show that if we
can prove (12.4), (12.7), (12.8), (12.10) and that W' is coherent then it follows
that W' covers 'P B.
Firstly, that 'P B is robust is seen as follows. We have
The first of these is trivial, the second easy (use the instantiation rule once) so
let us go straight to the third one, sharing.
By the definition of SC we must have longstrid 1 = strid 1.1ongstrid i and also
strid 1 E DomE. Also, (R1, U1) = Fresh (Iongstrid U). Now let
W1 = W U strs R1.
is in strnames((P1 R1)
(P1 is an M-realisation
Cpl W1 is simple with respect to M
M-strs('p1 W1) = M-strs W1.
Next, let
W2 = 01 W1 U strs R2.
Given that 01 W1 is simple with respect to M it is easy to check that W2 is
simple with respect to M and that R2 and (Pl E strid 2 are members of W2. Thus
using theorem 11.5 and its corollary again, we get
co2R2 = E strid2)
(P2(cp1
Inv 02 C strnames{R2, `p1 E strid 2}
W2 does not change the name of any structure whose name
is in strnames((P2 R2)
`p2 is an M-realisation
`p2 W2 is simple with respect to M
M-strs((p2 W2) = M-strs W2.
CHAPTER 12. PRINCIPAL SIGNATURES 154
Hence, letting
W3 = cp2 W2,
W3 is simple with respect to M and given the fact that cpl and (p2 are unifiers it is
easy to see that (`P2 P1 E)longstrid 1 and (W2 P1 E)longstrid 2 both are members
of W3.
Therefore, applying the theorem and corollary a final time,
(p3 is an M-realisation
= U2 U strnames E
Inv Bpi U
= U2 U U1 U strnames E
C U' U strnames{E, G}.
Proof of (12.9). Since 01 does not change the name of any structure whose
name is in strnames(O1 R1) and since Inv 01 C strnames{R1, E strid 1}, we have
that W1 does not change the name of any structure whose name is in 01 E.
01 does not change the name of any structure whose name is in R2 and since
Inv cp2 C strnames{R2, 01 E strid 2}, we have that 01 does not change the name
of any structure whose name occurs is 02 01 E. Since Inv 03 C strnames 02 W1 E,
we have that 01 does not change the name of any structure whose name is in
03 02 o1 E i.e., in o E.
Next, since 02 does not change the name of any structure whose name is
in strnames(02 R2) and Inv 02 C strnames{R2, Bpi E strid 2} we have that 02
does not change the name of any structure whose name is in 02 01 E. Since
Inv 03 C strnames{02 01 E} we have that 02 does not change the name of any
structure whose name occurs in 03 02 01 E i.e., o E.
Finally, since 03 does not change the name of any structure whose name
occurs in 03((02 01 E)longstrzd 1) and
we have that 03 does not change the name of any structure the name of which
is in O E.
Since nither 01 nor 02 nor 03 change the name of any structure whose name
is in O E we have that O has that property too. This proves (12.9).
Finally u n U' = U n (U1 U U2) by the properties of Fresh, show-
ing (12.10).
we have
'P1 is an M-realisation (12.13)
strnames E1 C strnames{G, E} U U1
Inv 'P1 U (12.17)
SP1 does not change the name of any structure whose
(12.18)
name is in cot E or in E1
U n U1 = 0. (12.19)
We now wish to use the induction hypothesis once again with W1 for W and
'P1B ± E1 for B and U U U1 for U. Given that W1 covers 01 B and contains all
structures in E1 we have that W1 covers 'P1 B ± El, if just '1 B ± E1 is robust.
But 'P1 B ± E1 is admissible by (12.14), and strnames F C M and strnames G C
M since 'p B is robust, and M-strs(E ± E1) is substructure closed by (12.14).
Thus '1 B ± E1 is robust, so W1 covers Cpl B ± E.
Before we can apply the induction we must also check that
where
W2 = strs{W2(W1), E2}.
Now SC succeeds with
(P,E',U') _ (W2o1p1,1p2E1±E2jUlUU2).
W'CW2. (12.27)
p2ca1B = (M,F,G,co2co1E)
sigexp = sig spec end Easy inductive step using one application of rule 8.12.
12.3 Completeness of SC
We shall prove the following strengthened version of the completeness result.
then (ip, S, U') = SC(B, sigexp, U) succeeds and there exists an M-realisation,
01, and a signature, E1, such that
From observation 12.8 we know that strs E C strs((P W). Therefore, if there
exists a c01 as described above then there exists one that in addition satisfies
Supp 01 C strs(P W).
Moreover, to prove (12.34) without having to mention renamings explicitly,
notice the following. Let E = (N)S and Eo = (No) So be well-formed signatures,
let be a realisation such that No fl
co Reg(P I strs E) = 0 and (P(S) = So. Then
there exists a signature E1 such that
Proof. [of theorem 12.12] The proof uses the soundness and completeness results
about Unify (theorem 11.5 and theorem 11.7), the soundness of SC (theorem 12.6)
and observation 12.8.
The two parts of the statement (regarding success and failure, respectively)
are proved separately. The first part is proved by induction on the depth of
inference of 0o B F- sigexp = Eo and 0o B F- spec = Eo. There is one case for
each inference rule.
The case for empty specifications is trivial -
take 01 = 0o. In the case for
structure specifications one takes the 01 that is supplied by induction. Let us
therefore go straight to the first non-trivial case.
Sequential Specification, rule 8.10 Consider a proof ending
01 El = El .
Now we wish to use induction again, this time on the second premise of (12.36).
To see that this basis is of the required kind, we compute
0o B ± Ei = 01(gP1 B) ± E1 01
by (12.37) and (12.38)
= 01(`P1 B E1)f
_ 01 B1,
where
B1 = cot B ± E1.
Thus, by (12.36) we have 01 B1 I- spec2 = E2 in strictly fewer steps.
Let W1 = strs{W1(W), E1}. As we saw in the proof of theorem 12.6, W1
covers B1 and M U strnames W1 C U U U1. Thus by induction ((P2, E2, U2) _
SC(B1i spec2, U U U1) succeeds and there exists an M-realisation 02 with
J. W1 = (020c02) 1 W1 (12.39)
and
E.
/2 E2 =E2' (12.40)
CHAPTER 12. PRINCIPAL SIGNATURES 161
Thus SC succeeds with (sp, E', U') = (°2 0 Cpl, cp2 E1 ± E2, Ul U U2)- Now
001 W== (020W) 1W since for each w E W,
bo w = 01(w1 w) by (12.37)
= ?2(p2(W1 w)) by (12.39)
= 7fi2l`p w).
as desired. Moreover,
We now wish to use the completeness result about Unify (theorem 11.7) a first
time. To this end let
W1 = W U strs R1.
W1 is simple with respect to M and it contains R1 and E(strid 1). Moreover,
(?o(E strzd 1)) longstrzd 1 exists by (12.41). Since strs R1 fl w = 0 there exists
an M-realisation, 01, such that 0 1 W = 01 1 W and 01(R1) _ 01(E strid 1).
Thus by theorem 11.7, W1 = Unify(M, R1, E strid 1) succeeds and there exists an
M-realisation, '2, such that
Next, strzd 2 E DomE by (12.41) so SCdoes not fail that test. Let (R2, U2) =
Fresh(longstrid 2, UUU1). We now wish to apply the completeness result for Unify
a second time.
To this end, let W2 = W1 W1 U strs R2. It follows from theorem 11.5 that W2
is simple with respect to M. Now R2 and Cpl E strzd 2 are in W2 and they have
an M-unifier. More precisely,
CHAPTER 12. PRINCIPAL SIGNATURES 162
there exists an M-realisation, 03 with 03 strs((p1 W1) J. _ 021 strs(W1 W1) which
unifies (p1 E strid 2 and R2. Thus by theorem 11.7,
We now want to apply the completeness result for Unify a third time. To this
end, let
W3= (P2 W2.
Thus SC returns ((p, E', U')= ((P3 0 (P2 0 (P1, {}, Ul U U2). We have z/io 1 W=
(05 0 (p) . W since for all w E W,
5o(w) _ 01(w)
= b2 (P1 w by (12.42)
= 53(p1w
= 04 (P2 (P1 W by (12.43)
= 55 (P3W2 p1 w by (12.44)
CHAPTER 12. PRINCIPAL SIGNATURES 163
=5cpw.
Finally, 05 E'== 05{} _ {} = Eo as desired.
Basic Signature Expression, rule 8.12 Consider a proof ending
,bo B I- spec Eo
(12.45)
0o B f- sig spec end = (0) (n, Eo)
By induction (c01i E1, U1) = SC(B, spec, U) succeeds and there exists an M-
realisation, V1, such that
''oIW=(11°p1)IW (12.46)
and
01 El = Eo. (12.47)
Thus SC succeeds with ('p, S, U') _ ('P1, (nl, E1), Ul U {n,}), where n1
U U U1. The desired conclusions follow from (12.46) and (12.47) provided n1
really is bound in Closww(n1iE1). But that follows from theorem 12.6 which
ensures that strnames('Pi W) C U U U1.
Signature Identifier, rule 8.13 Consider a proof of the form
('o B) sigid = Eo
Eo.
00 B f- rigid
we must show that no Reg(&1 . strs E). This is seen as follows. By observa-
tion 12.8 we have strs E C strs(W B). Thus
Rng(z&1 , strsE) C strs('t&1(cPB))
= strs(OoB) by (12.48)
so Reg(z&1 . strs E) C strnames(oo B). Since no strnames('o B) we have
no 0 Reg(O . strs E).
The Instantiation Rule, rule 8.15 Use induction once, take the 01 provided by
induction and use the transitivity of >.
This concludes the first half of the proof (regarding the success of SC). The
second part is shown by structural induction on sigexp and spec. We show the
two non-trivial cases:
CHAPTER 12. PRINCIPAL SIGNATURES 165
Sequential Specification, spec = specs spec2 Assume SC(B, spec, U) does not
succeed. Then, by induction, if the first call of SC does not succeed it stops
with fail (and we are done); so assume it succeeds. Then, as we saw above,
f
W1 = strs('p1 W)Ustrs(E1) covers B1 = 'P1 B E1 and MUstrnames W1 C UUU1
and the second call of SC cannot have succeeded so by induction it stopped with
fail.
Having proved theorem 12.12, we see that it really does imply theorem 12.3:
Assume B robust and strnames B C U and 0 is an M-realisation and E a sig-
nature such that 0 B F szgexp = E. Let W = strs B. Then W covers B and
MUstrnames W C U, so by theorem 12.12 ('p, S, U') = SC(B, sigexp, U) succeeds
and there exists an M-realisation, 0', and a signature E1 such that 0 1 W =
(0' o W, Closw W S 0') E1, and E1 > E. Thus (O' o 'p) E = 0 E. Moreover,
'p) I
(and this is the only interesting point in this argument) C1osWB S = Clos , S
by observation 12.8. Thus, if Closw B S E', then Closw W S + E' and since
also Closww S ; E1 we must have E' = E1. Thus E' - E1 by lemma 9.17 so
E' > E1 >E as desired.
Chapter 13
Conclusion
We first summarize what has been done and then comment on the role of oper-
ational semantics in language design.
13.1 Summary
We have investigated three type disciplines that accomodate different, and yet
similar kinds of polymorphism.
The first was Milner's polymorphic type discipline. We stated its consistency
with a dynamic operational semantics by defining a relation between values and
types. In particular, the definition of what it is for a closure to have a type is
similar to the definition of what it is for a function in a domain to have that type.
We then proved the soundness by structural induction.
The second is a new type discipline for polymorphic references. It is less
powerful but simpler than Damas' system and I believe the new system is pow-
erful enough to be of practical use. It is easy to extend the distinction between
expansive and non-expansive expressions to a larger language. Besides the type
inference system itself, the technical novelty is the definition of the relation be-
tween values and types as the maximal fixpoint of a monotonic operator.
The third is a type discipline for program modules. We saw how one set of
inference rules gives rise to two different semantics, one based on coherence and
one based on consistency. The former was investigated in detail. A signature
checker was presented and proved sound and complete with respect to the se-
mantics. The signature checker uses a generalization of the ordinary first order
term unification algorithm.
Milner's polymorphic type discipline strongly influenced the two others. The
166
CHAPTER 13. CONCLUSION 167
ML [20].
But how were the semantic issues isolated? Some came as a result of just
trying to write down the rules. But there is a long way from writing down
a set of rules to understanding how they interact and how they depend upon
assumptions about well-formedness constraints on the semantic objects. These
things were often understood only as a result of trying to prove some theorems
about the skeletal language.
We did not first define a semantics and then prove theorems about it. The
definition of the semantics and the properties of it developed side by side influ-
encing each other. The process was akin to that of developing a program and
proving it correct at the same time. Thus the proof activity is at the very heart
of operational semantics and deserves special attention, not least because finding
and proving theorems is a complex intellectual activity, costly in time and en-
ergy. What are the complications that arise if we try to scale up the work from a
skeletal language to a realistic programming language? To what extend can we
envisage the use of computers to assist the proof finding?
The proofs I have done regarding ModL are fairly long, I think, and I want to
base my answer to the above two questions on the experience of doing these proofs
by hand. In retrospect, it seems that there were two factors that complicated
the work.
The first factor is that although we use relatively standard mathematical
reasoning, we often find that we are not really interested in reasoning about
natural numbers, polynomials, or other objects that we are already familiar with
from mathematics. On the contrary, we have to define our own semantic objects,
such as structures, signatures, realisations. As these objects are new in our
experience we have to do a lot of basic reasoning. The technology of substitutions
is a refined one that has taken time to mature. When we generalize to realisations,
we have once again to think about renaming, free and bound names and so on,
even though the definition of realisation maps itself is simple.
The second factor is that the constuctions we want to prove theorems about
are bigger than normal in mathematics. A semantics with 15 inference rules is
a very small semantics compared with a real language semantics but it feels big
once you start a case analysis with 15 cases. I have not experienced that most of
the cases are trivial, indeed the norm has been that many cases require good ideas
and that it takes many failed attempts before one finds an induction hypothesis
that survives all 15 cases.
CHAPTER 13. CONCLUSION 1-71
The two factors are active at the same time so that the proof activity involves
high-level considerations (will this induction hypothesis work?) and, at the same
time, low-level considerations (what do I need to know about realisations to
rewrite Win i-i n,} S to {n' i-i n} Win n'} S?). The basic concepts are not
given from the outset but emerge as a result of looking for theorems. When one
is stuck in a proof, at least while the theory is still young, it is sometimes hard to
decide whether to try to change the theorem or the basic definitions that underlie
it.
Both factors contribute to giving long proofs, indeed the proofs I have done
are long more because of these two factors than because I'm trying to prove
something very surprising.
To return to the original questions, the larger the language, the more new
semantics objects we have to define and get used to. There will be more con-
nections to understand at the basic theoretical level. The larger the language,
the more cases to consider and the more times we have to start all over again.
Different individuals can cope with different levels of complexity, of course, but
will not everybody feel that at some point they will start forgetting dependencies,
getting the same good ideas many times, changing indecisively from alternative
to alternative?
That machines should be able to take over the proof finding at the point
where we have to give up seems absurd considering the things we can successfully
program machines to do. A much more sensible goal is to use the machine to
help us organize our proof finding.
A handwritten proof is a sequence of sentences. Some of these serve to explain
the main ideas of the proof; some are used to introduce new notation and to bind
variables. Others are judgements. A sequence of judgements will normally have
to speak for itself. We do not consistently refer to a set of inference rules and
lemmas to chain together the individual judgements. After all, we do not want
to be more pedantic than we have to in order to feel confident that what we write
is correct. For each judgement there is an implicit unproved lemma, namely that
this judgement follows from the previous judgements. Whenever we choose to
be explicit about how one judgement is obtained from its predecessors, there is
the possibility of letting the machine "perform" the inference as a computation
so that we don't have to worry about this proof step, but only the rule applied,
if the proof is to be done again later on.
CHAPTER 13. CONCLUSION 172
Writing a program using just a screen editor or pen and paper is like pro-
gramming in an untyped language. One has complete freedom but little control
of the inferences one makes. The more explicit one makes the structure of a
proof, the more work one has to set up the proof, but the pay-off is that one (or
a machine) can perform a kind of type checking of the proof. If, for instance you
have to check 5 things before you apply an induction hypothesis, you should not
get away with forgetting to check one of them. Indeed, the paradigm in much
current work on formalizing logics is that proof checking is type checking (see for
instance the Edinburgh Logical Framework, [17]). A tool that allows you to be
explicit when you want to and does not force you to be explicit when you don't
want to could be of tremendous help in the proof finding process.
Incidently, the problem of polymorphic references seems very suitable for
machine assisted proof. It has deceived people again and again. Everybody I
know who has tried to solve the problem share the experience that firstly, it is
hard to say what the problem really is and secondly, that when something seems
to work, it is hard to give a good explanation of why it works. With the proof
method I have presented I think there has been sufficient progress that it would
be a realistic task to try to prove (or disprove) the consistency theorem with the
assistance of a machine. Firstly, it would be wonderful to have a strict control of
proofs, and secondly, it would be interesting to find out whether the work would
result in new knowledge about the problem itself.
thing that works for coherence works for consistency without modifications. For
instance, coherence is important for the unification algorithm, I have presented.
When relaxing coherence to consistency, special care has to be taken in the uni-
fication algorithm to avoid the creation of cyclic structures. One cannot unify
the (sub)structures (n, {}) and (m, {}), say, if somewhere else there is a structure
(n, {A H (m, {})}).
The initial constaint that functors cannot take functors as arguments nor
produce functors as result was introduced simply because it was felt that one
should not try to do too many difficult things at the same time. Now that we
understand the semantics of the first order functors, it does not seem frightening
at all to start considering higher order functors. We have already had to introduce
functor signatures and functor instances as semantic objects even before there is
any program notation for writing down and binding functor signatures.
Appendix A
Robustness Proofs
This appendix contains the proofs of the robustness results stated in Chapter 10.
Lemma 10.1 If E is admissible and E > S' and E --' E1 then E1 > V S'.
S.
(0o Ip) S = Si (A.1)
By the coherence of 5, for every structure, T, that occurs bound in E1, there
is a unique structure, let us call it V-1 T, bound in E, such that
(V50 Ip)(I-1 T) = T.
Since E > 5' there exists a realisation W with Supp W C boundstrs E and
(PS=5'.
For any substructure T of S1 let us define
f(P(-1 T)), if n of T E Nl
`P'(T) l T, otherwise
(A.2)
and extend it to a total map by letting it glide on all structures that do not occur
in S1. To prove E1 > 0 5' it will suffice to prove
This proves (A.3). Next, we prove (A.4) by a (much simpler) case analysis:
APPENDIX A. ROBUSTNESS PROOFS 176
Lemma 10.2 If E E1 and E' Ei and E >_ E' and E is admissible then
E1 > Ei.
by corollary 9.16. Write E' on the form (N')S'. Then since V-24 Ei we have
E 'pI°,} E1.
(A.9)
E1 S.
> (co p') S
l
(A.10)
Lemma 10.4 For all functor signatures (D 1, and functor instances 13, 14,
(D 2, if
401 is admissible and 401 > 13 and 01--->'02 and 13 `a
14 then '02 > I4.
-4
-
W1 W2
`V 1 V V 02
13 I4
Write
'D 1 = (N1) (S1, (NJ') S') 'D 2 = (N2)(S2, (N2)S2)
13 = (S3, (N3) S3) 14 = (S4, (N4)S4).
By the assumptions all of these are well-formed.
Let 'pl = (p . strs(Nj)Sl and let cpi = cp 1 strs(Ni U Ni) S'1. Since D1---> D2
there exists a bijection
p:N1UNi--N2UN2
such that
pi :N1-N2=p.JN,
and
Pi:N' N2=p.JN1
are bijections and
and
(N2 U N2) n Reg pi = 0 and (Pi 1p) S' = S'.. (A.13)
As in the proof of lemma 10.1 for any structureT bound in (N2)S2 there is a
unique structure, call it cp-1 T, bound in (N1)Sl such that
179
and
Supp 01 C boundstrs(Ni)Si. (A.16)
Let 11 be 01 J. strs(Nf)S'. By (A.15) there exists a bijection p13 : Nl -> N3
such that
N3 fl Reg V) 1 = 0 and (1 IPi3) Sl = S3 . (A.17)
By the final assumption, 13 I44 we have
We can now define the realisation that instantiaties 41)2 to 14. For every
S = (n, E) E Str, we define
S)), if S E boundstrs(N2)S2
/2(S) = S, if S E strs(N2)S2 (A.20)
(n, b2 E), otherwise.
As in the proof of lemma 10.1 it is proved that 02 is a realisation with
Supp b2 C boundstrs(N2)S2 and '2 S2 = S4. To prove 41)2 > I4 we are therefore
left with proving
N4 fl Reg b = 0 (A.21)
and
(02 IP2) S2 = S4' (A.22)
N4-Str = 0 as desired.
SEstrs(Nf)S' andnofSEN1 Then (ip' pi) S is free in (N2) S2' and n of
1
= (P(01 S) by (A.20).
S4 - W3 IP3)S3
IP3)(,/'l
(W3 IP13) Sl
is well-formed
4'2(W1 1P1) S as (W1 Ipl) S is free in (N2)S2
'(01 S) by the definition of 02
(3 IP3) //,,
( 2 I (c1 1p) E)
((p2 o p)n, (4'2 Ip2)(W1
p2)(P(n),
E) 1p)
Theorem 10.5 Let B = M, F, G, E and B' = M', F', G', E' be bases with
B w B'.
If
B I- spec El (10.1)
M'-strs(W E1) is substructure closed (10.2)
{B',coE,} is coherent (10.3)
then
B' H spec 'p El .
Similarly, if
B f- sigexp E and E E' (10.4)
M'-strs E' is substructure closed (10.5)
{B', E'} is coherent (10.6)
then
B' sigexp
f V.
Proof. By induction on the depth of inference of (10.1) and (10.4). One case
for each inference rule.
Empty specification, rule 8.8 Trivial.
B H sigexp = (0) S
B I- structure strzd : szgexp = {strid -4 S}
So El = {strid --f S}. Assume (10.2) and (10.3). Now M'-strs(cp Ei)
M'-strs(cp S) = M'-strs E', for E' = (0) (W S). Therefore we have (10.4)-(10.5),
so by induction we have B' F- sigexp =, (0)(coS). Thus by rule 8.9 we have
B' I- structure strid : sigexp = WE, as desired.
APPENDIX A. ROBUSTNESS PROOFS 183
B b B' (A.29)
But (A.29) is obvious; and (A.30) follows from (A.26) and the definition of gyp';
and (A.31) follows from (A.27) and the properties of z.
Thus by induction
B' I- specs W' E1. (A.32)
Next, (A.34) follows from (A.26) and (A.28). Also, (A.35) follows from (A.27)
and the definition of cp'. Hence by induction on the second premise of (A.25),
by rule (8.10). To check that this conclusion is admissible (c.f. definition 9.12)
we must check that
f
{B', co'(E1 E2)} is admissible (A.37)
The well-formedness of {B', W'(E1 f E2)} comes from the robustness of B';
the coherence from (A.27) and the definition of gyp'. Thus (A.37) holds.
Next, (A.38) and the first half of (A.39) follow from the robustness of B', and
the second half of (A.39) follows from (A.26) and (A.28). From (A.36) and (A.28)
we get
B' I- specs spec2 W(E1 f E2)
as required.
n of B(longstrid 1) = n of B(longstrzd 2)
(A.40)
B I- sharing longstrid 1 = longstrid 2 {}
Since B is coherent the premise implies that B(longstrid 1) equals B(longstrid 2).
Thus we have
B'(longstrid 1) = E' longstrid 1
(gyp E)longstrzd 1
_ co(E longstrid 1) as cP is a realisation
W(E longstrid 2) by (A.40)
(co E)longstrid 2
B'(longstrid 2).
In particular, n of B'(longstrid 1) = n of B'(longstrid 2), so by rule (8.11) we
have
B' I- sharing longstrid 1 = longstrid 2 {}
which is the desired conclusion . The conclusion is admissible.
APPENDIX A. ROBUSTNESS PROOFS 185
BI- spec=El
(A41)
B F- sig spec end = (0) (n, E1) .
Thus E (0) (n, E1). Assume E E'. Then E' must be (0) W(n, E1). Thus
the assumptions (10.5) and (10.6) read
where we choose n' disjoint from strnames{B' W E1} in order to make sure that
(A.47) is an admissible conclusion.
Then by the generalization rule, rule 8.14, we have
Since E ---> E', E' has the form (N') S' where there is a bijection
p: N1U{n,}--+ N'
such that Reg 'Po f1N' = 0 and ('Po p) S1 = S1, where 'Po = 0 I strs E. The
bijection p can be partitioned into two bijections R1 N1 --p Nl and pi : {n,}
:
BI Hszgexp=(Ni)Si
BI Hsigexp=(NiU{n})S'. (A.51)
PV= R1U{n1-+n,}
which is a bijection
p,,:N1U{n1}-4N,'U{n}.
Define a map Str-*Strby
1(nv, `P E), if n = nl
(n, E) _ 'p(n, E), if (n, E) E strs{B, (Ni U {n1}) Si}
(n, '% E), otherwise.
Because cp is a realisation and (Ni) Sl and (Ni U {n1}) Sl are well-formed and
nl strnames B, 0 is a realisation. We intend to use induction on 0. Clearly we
have B b B', and we also have
Because of the way we chose n,,, we
that E1 Ei, where E' = (N,') In' n,,} S'
get that M'-strs Ei is substructure closed
and that {B', Ei} is coherent using (A.49) and (A.50).
Thus by induction we have
which is an admissible conclusion. Since n, 0 strs B', and this is why we did the
renaming, we can use the generalization rule to conclude
so in particular
B I- sigexp El > E
El
(A.54)
BI- sigexp=E
Assume E - E' and
Using induction on these and the first premise of (A.54) we get B' I- sigexp =
Ei and since Ei > E' we use the instantiation rule to get the desired conclusion
B' I- sigexp = E'. The conclusion is admissible. 0
APPENDIX A. ROBUSTNESS PROOFS 189
E2 is coherent (A.59)
B f- dec =E n strnames(E) U (M of B)
B f- struct dec end = (n, E)
By induction E is coherent and M-strs E C strs B. Since n strnames E we
have that S is coherent. Since n M we have M-strs S = M-strs E C strs B as
desired.
Long structure identifier, rule 8.6
B(longstrid) = S
B f- longstrid = S
Trivial.
Functor application, rule 9.2
{B, S} is coherent.
Let 4D = (N0)(So, (No)S') be B(funzd). Since 4D > (S, (N') S') there exist a
realisation 0 with Supp 0 C boundstrs(No)So, 0 So = S and (No)SS -4(N')S'.
Now 0 is the identity on all structures free in (No U No)SS. All structures in
No-strs(NN)S5 occur in So since 4D is admissible. It then follows
from (No)SS -4(N')S' that
C M-strs{B, S} by (A.61)
C strs B since M-strs S C strs B.
APPENDIX A. ROBUSTNESS PROOFS 191
BF
dec= E
B F dec = (strnames E, {}, {}, E)
Trivial inductive case.
Signature declaration, rule 8.17
Since E is admissible, B' = (strnames E, {}, {szgid H E}, {}) is strictly robust.
By lemma 10.9 we have strs E C strs B. Thus M-strs B' C strs B.
Functor declaration, rule 8.18
B1 = B ®{strid H S}.
where now Ml = M of B1 = (M of B) U N.
Now let us show that (D = (N)(S, (N')S') is admissible. We already know
that (N)S is admissible and that S' is coherent. It remains to be shown that
Thus is admissible.
We have strs C strs B by (A.62) and the above argument that strs(N U
N')S' C strs B. Thus B' is strictly robust, and M-strs B' = strs P C strs B as
required.
BHprogl=:. B1 B±B1Hprog2=:. B2
B I- prog1 prog2 = B1 ± B2
By induction
B1 is strictly robust (A.67)
Thus by induction,
B2 is strictly robust (A.69)
Theorem 10.12 If B F- strexp = S and B b B', then for all S' E Str,
BI- = {}
Here B' F- = E' if E' _ {} if ClosB{} ClosB, E'.
B F- strexp = S
B F- structure strid = strexp = {strid H S}
Here
-
3 S' E' = {strid H S'} and ClosB S
Now N1nN2=N1nN2=0, so
al Ua2:N1UN2--*NjUN2
is abijection.
Let N = strnames(E1 ± E2) \ M and N' = strnames(E' ± E2) \ M'. Clearly,
NCN1UN2and N'CNNUN2but in general N=NlUN2and N'=NNUN2
need not hold.
We wish to prove
We have
(cP° l al U a2) E1 = (cP° la1) E1 as N2-strs E1 = 0
= (cPf lal) E1 by theorem 10.8
= E'1 by (A.72).
Moreover, by theorem 10.8, for every structure S2 in E2 either S2 is free in
B1 or n Of S2 E N2. In the former case,
(02 la2) S2
which with the above equation, (cp° l a1 U a2) El = Ei, gives (A.76).
Now let a = (a1 U a2) . N. Let us show that the co-domain of a is N'.
APPENDIX A. ROBUSTNESS PROOFS 196
Conversely, assume
i.e., all names that are new in E1 or in E2, and whose co-domain does not intersect
M'UNi2
Let W° = W I strs B and let us define
Now
E112 = (`Pi2 ja12)(E1 ± E2) by (A.77)
APPENDIX A. ROBUSTNESS PROOFS 197
B' 1- dec1 =- E.
Ei (A.81)
B I- dec =: E n strnames(E) U (M of B)
B I- struct dec end =: (n, E)
Assume B I- dec E and n strnames E UM. Then
if
there exists n', E', such that S' = (n', E') and B' F-
if
ClosB(n, E) -- ClosB' S' .
B(longstrid) = S
B I- longstrid S
Let E = E of B. Then
B' I- longstrid = S'
if
(E of B') longstrid = S'
if
(co E)longstrid = S'
if
co(E longstrid) = S' (given that E longstrid exists)
if
coy=S'
if
ClosB S -' ClosB' S'
as B and B' strictly robust implies ClosB S = (0) S and ClosB' S' = (0) S'.
APPENDIX A. ROBUSTNESS PROOFS 199
Using lemma 10.4 on (A.84), (A.85) and B(funid) > (So, (N)S) gives
Since we also have B'(funad) > (So, (N')S') we must have (N")S" = (N')S'
by lemma 9.18. Thus by (A.84),
We wish to prove
(N1)S -°'(N,)S', (A.87)
where Nl = strnames S\M and Ni = strnames S' \M'. Since NnM = N'nM' =
0, we have N C Nl and N' C Ni but the equalities need not hold as (N)S
may contain free structures that are in So but not free in B. More precisely,
since F(funzd) is well-formed and coherent and F(funzd) > (So, (N)S), every
APPENDIX A. ROBUSTNESS PROOFS 200
ao:No -*No,
'
So = (Wo Jao) So. Then (No) So --(No) S. Thus by induction B' I- strexp S.
Let W° = W I strs B and let W1 = W° Then W1 So = S' and
lao.
(N)S F(N')S' for N' = a1(N1). Thus (So, (N)S) + (So, (N')S').
Since also B(funid) > B'(funid) and B(funid) > (So, (N)S) we have
B'(funid) > (So, (N')S') by lemma 10.4. Also N'f1M' c N11 f1M' = 0. Therefore,
by the functor application rule we have the desired B' I- funid(strexp) = S'.
Bibliography
[1] P. Aczel, An Introduction to Inductive Definitions, in J. Barwise (ed.) Hand-
book of Mathematical Logic, North-Holland Publishing Company, 1977
[5] H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-
Holland, Amsterdam 1981.
[6] R. Burstall and B. Lampson, A kernel language for abstract data types
and module, in Symposium on Semantics of Data Types, Sophia Antipolis,
Springer, Lecture Notes in Computer Science 173, 1984, 1-50.
[14] L. Damas and R. Milner, Principal type schemes for functional programs, in
Proceedings of the 9th ACM Symposium on the Principles of Programming
Languages, pp. 207-212, 1982
[18] R. Harper, David MacQueen and R Milner, Standard ML, Laboratory for
Foundations of Computer Science, Department of Computer Science, Uni-
versity of Edinburgh, ECS-LFCS-86-2, 1986
[19] R. Harper, R. Milner and M. Tofte, A type discipline for program modules,
Proc. TAPSOFT '87, Springer, Lecture Notes in Computer Science 250,
Berlin - Heidelberg - New York, 1987, 308-319.
BIBLIOGRAPHY 203
[20] R. Harper, R. Milner and M. Tofte, The semantics of Standard ML, Ver-
sion 1, Laboratory for Foundations of Computer Science, Department of
Computer Science, University of Edinburgh, ECS-LFCS-87-36, 1987
[21] R Harper and M. Tofte. The Static Semantics of Standard ML, DRAFT.
Unpublished. 1 November, 1985.
[26] J. McCarthy et al. LISP 1.5 Programmer's Manual, MIT Press, Cambridge,
Mass. 1965
[35] J.C. Reynolds, Towards a Theory of Type Structure, Proc. Colloque sur
la Programmation, Lecture Notes in Computer Science 19, Springer, New
York, 1974, pp. 408-425.
[38] S. Ronchi Della Rocca and B. Venneri, Principal type schemes for an ex-
tended type theory, Theoretical Computer Science 28, North-Holland (1984)
151-169.
[41] Reference Manual for the Ada Programming Language, (Proposed Standard
Document), United States Department of Defence, July 1980
[42] M. Wand, Complete Type Inference for Simple Objects, Symposium on Logic
in Computer Science, Ithaca, New York, Proceedings, 1987, 37-44.