Unification and Polymorphism in Region Inference

Mads Tofte, Department of Computer Science, University of Copenhagen
Lars Birkedal, School of Computer Science, Carnegie Mellon University

Dedicated to Robin Milner on the occasion of his 60th birthday.
Abstract

Region Inference is a technique for inferring lifetimes of values in strict, higher-order programming
languages such as Standard ML. The purpose of this paper is to show how ideas
from Milner's polymorphic type discipline can serve as a basis for region inference, even in the
presence of a limited form of polymorphic recursion.
1 Introduction

Most programming languages provide some facility for dynamic allocation and de-allocation of
memory cells. The reason for this is that the number of cells which the program wishes to allocate
and use at some point during the computation often is much larger than the number of cells which
have to exist at any one point of the computation.
The stack discipline which originated with Algol 60[15] is a particularly elegant discipline for
dynamic memory management. Restricted versions of the original stack discipline are used in
many languages in current use, e.g., C and Pascal. In the stack discipline, every point of memory
allocation is matched by a point of de-allocation, and these points are easy to identify from the
program text. The evident connection between allocation and de-allocation makes it possible for
programmers to reason about the lifetimes of storage cells. However, the stack discipline imposes
rather severe restrictions on the programming language. For example, functions are not allowed
to return lists or functions as results.
To overcome these limitations, many programming languages assume an additional memory
area, the heap, which holds values whose final size or lifetime is not known when allocation of
memory to hold the value takes place. In some languages, for example C, it is the responsibility
of the programmer to allocate blocks of memory and to free them once they are no longer needed.
While it is easy to allocate memory, it is in general extremely hard to know when it is safe
to de-allocate memory. Intuitively, a memory cell can be reclaimed (it is "garbage"), if and
only if its contents is not needed by the remainder of the computation. This is an undecidable
property. To make matters worse, de-allocating memory too early can cause the program to crash,
while de-allocating memory too late can cause "space leaks", i.e., programs that hold on to much
more memory than is necessary. Moreover, unlike what is the case for the stack discipline, the
programming language does not help the programmer in reasoning about lifetimes of storage cells.
The term "garbage collection" is traditionally used for a range of heap memory management
techniques, including reference counting, copying collection and generational collection (see [25]
for an excellent overview).

1

Common to all of these techniques is that there is a strict separation
between the program which allocates memory, called the mutator, and the part of the runtime system,
called the garbage collector, which manages recycling of memory. For some garbage collection
schemes, it is hard for users to know when garbage collection takes place and how long it will take.
Garbage collection was first used with Lisp; it is used both in implementations of functional and
object oriented languages.

1

This use of language is arguably misleading: the stack discipline also collects garbage and it does so very
efficiently, by popping the stack.

Garbage collection techniques have developed very significantly over the past decade and the
time spent by garbage collection is often modest (say less than 5% of the total running time).
However, the strict separation between allocation and de-allocation means that there is no language
support for reasoning about the lifetimes of storage cells, and thus it is in general very difficult for
programmers to reason about how much memory their programs will use.
Region-based memory management[23, 1, 2] is yet a form of automatic management of dynamic
allocation. Conceptually, the store consists of a stack of regions. A region can be thought of as
a heap which can grow dynamically depending on how many values it needs to hold. Regions are
allocated and de-allocated in a stack-like manner, i.e., a region is not de-allocated unless it is the
topmost region on the region stack. All values are put into regions, including for example lists and
function closures. The only mechanism for freeing memory is to pop the region stack, which is a
constant time operation, for a suitable choice of concrete representation of regions.
Rather than forcing the programmer to introduce and eliminate regions, we have taken the
approach to use an existing language, Standard ML[11], as the source language. The region scheme,
including the algorithms presented in this paper, are implemented in the ML Kit with Regions
[21] which compiles Standard ML Core Language programs to C and HP PA-RISC code. The ML
Kit subjects source programs to a particular static analysis, region inference. The analysis decides
where regions should be allocated and de-allocated. Region inference also decides, for each valueproducing
expression in the program, into which region the value will be put. Region inference
handles recursive datatypes and higher-order functions. Moreover, region inference preserves a
close connection between program structure and lifetimes of values, making it possible for humans
to reason about lifetimes and making it easy for profiling tools to report actual memory usage
in terms of regions which can be related to the program text. Finally, the memory management
directives which region inference inserts during compilation each use only constant time and space
at runtime. Thus programs can be run as they are written, without hidden extra costs of unbounded
size (in contrast to what is the case for other existing ML implementations).
Some programs are ill-suited for region inference. An example of such a program is an interpreter
for S, K and I combinators. Here the region inference will not be able to distinguish lifetimes
of different terms and memory usage will be linear in running time. However, even programs which
were originally thought to require garbage collection (for instance Knuth-Bendix completion) have
been made to run in much less space using regions than using traditional garbage collection; the
region scheme is not magic, but it can often be used to obtain programs that have time and memory
performance that is better than those reported for systems that use traditional garbage collection
techniques. This is as one might expect, at a superficial level at least, for while most garbage collection
techniques are general techniques which treat all programs equally, region inference specialises
memory management to the particular program that is being compiled.
The relevance of region inference to this Festschrift is that Milner's work on type inference
and type checking[10] has provided many of the technical insights which underlie region inference.
(Other origins of region inference are listed in Section 3.) In particular, the idea of using unification
in type checking and the notions of polymorphic type schemes and generic instance are heavily
exploited in work on regions. As it happens, region inference is not restricted to languages that
use ML-style type polymorphism. But as we describe below, there are close connections between
region- and effect polymorphism and the ability to extend the stack discipline to cover language
constructs found in SML, specifically recursive datatypes and higher-order functions.
The rest of this paper is organised as follows. We first introduce the region-annotated types that
underlie region inference, illustrating the basic ideas by means of a well-known program: the towers
of Hanoi. We then introduce a technical notion, consistency, which is required for the statement
and proof of a key lemma. Informally speaking, this lemma (Lemma 6) says that Robinson's
result[17] concerning most general unifiers of terms generalises to the case where terms are types
which are annotated with regions and effects, provided the annotation is done consistently. We
define operations corresponding to Milner's notions of generic instance and generalisation in the
setting of region-annotated types and introduce a particular class of type schemes which is general
enough to allow a limited form of polymorphic recursion in regions and yet restricted enough that
one can prove that region inference always terminates.

fun hanoi(n,from ,to,other ,acc) =
if n=0 then (from ,to)::acc

else hanoi (n-1, from , other , to, (from , to) :: hanoi (n-1, other , to, from , acc))

val solution = hanoi (20,"a","b","c",nil)
Figure 1: The Towers of Hanoi (source program).
2 Region-annotated programs

In this section we introduce the three kinds of region annotations which region inference inserts
into source programs. Readers who are familiar with region inference may want to proceed directly
to Section 3.
The Towers of Hanoi is the name of a game which involves one monk, three vertical pegs (A,
B and C) an n discs of different sizes. The discs have holes in them, so that the monk can stack
them on top of each other on the pegs. Initially, there are n discs on A, stacked in decreasing size
(with the smallest disc at the top) while B and C contain no discs. The problem for the monk
is to move the discs around between the pegs, one at the time, in such a way that at the end, C
contains all the discs and A and B contain no discs. The moves have to be such that no disc is
ever placed on top of a smaller disc.
The Standard ML program in Figure 1 solves the problem. hanoi (n; from ; to; other ; acc) moves

n + 1 discs from the from peg to the to peg, using also the other peg, if necessary. Moves are
accumulated onto the list acc.

Region inference translates this source program into the program shown in Figure 2. Every
value-producing expression has been decorated with an annotation of the form "at ae", where ae is
a region variable. The annotation indicates the region into which the value should be put. In line
18, for example, the constant 1 is put into region ae 26 .
The construct "letregion ae in e end" binds ae within e. At runtime, first a region is allocated
and bound to ae; then e is evaluated, perhaps using the region for storing and fetching values; finally,
upon reaching "end", the region is de-allocated. In line 18, for example, ae 26 is only needed for the
computation of n \Gamma 1. Regions can also contain tuples (see ae 18 and ae 24 , for example) and closures
(not illustrated by the example).
Notice that the region inference algorithm has given hanoi six additional formal region parameters:
 ae 6 ; : : : ; ae 11 . These are enclosed in square brackets to distinguish them from parameters which
the programmer writes. Correspondingly, the references to hanoi (lines 10, 17 and 32) each have
six actual region parameters. The region parameters give the regions of the argument and result of
the function. Result regions indicate where the function should put the result value, if it creates
one. For example, ae 9 is the region where the pairs which represent moves are put and ae 7 holds the
spine of the list of moves. ae 6 is the region where the argument quintuple to hanoi is stored (we
treat all tuples as boxed).
Notice that the three calls to hanoi have different actual region arguments. We refer to this
feature as region polymorphism, a term that will be justified once we have introduced regionannotated
types and type schemes. Note that even within the body of hanoi , the actual region
arguments to hanoi differ from the formal region parameters. We refer to this feature of the system
as region-polymorphic recursion; it is essential for obtaining good results.
By examining the region annotations one can determine that the maximal memory requirement
for the computation will be c + c 1 \Theta n + c 2 \Theta (2

n+1

\Gamma 1) words, where n is the first argument to

hanoi (here 20), c is a (small) constant, c 1 is the number of words it takes to represent the fixed
size regions in lines 9 and 15 and c 2 is the number of words it takes to represent one move in the
accumulating parameter. Here the third term clearly dominates. Indeed, for the ML Kit, c 2 is 4
(4 words = 16 bytes) and when running the program under the ML Kit one finds the expected
maximal memory usage of approximately c 2 words \Theta 4bytes=word \Theta 2

21

= 32 Mb. The run takes
1.85 seconds of user time on an HP 9000s700 (C100). The corresponding numbers for the same

1 fun hanoi at ae 5 [ae 6 ,ae 7 ,ae 8 ,ae 9 ,ae 10 ,ae 11 ](var 6 ) =

2 let val n = #0 var 6 ; val from = #1 var 6 ;
3 val to = #2 var 6 ; val other = #3 var 6 ;
4 val acc = #4 var 6

5 in letregion ae 13

6 in (case letregion ae 14 in (n = (0 at ae 14 ))at ae 13 end (*ae 14 *)

7 of true =? let val v 170 = ((from , to) at ae 9 , acc) at ae 8 in :: at ae 7 v 170 end

8 --- false =?

9 letregion ae 16 , ae 18 , ae 19 (* for region tuple, quintuple and n-1, respectively*)

10 in hanoi [ae 18 ,ae 7 ,ae 8 ,ae 9 ,ae 10 ,ae 19 ] at ae 16

11 (letregion ae 20 in (n-1at ae 20 ) at ae 19 end (*ae 20 *),

12 from , other , to,

13 let val v 171 =

14 ((from , to) at ae 9 ,
15 letregion ae 22 , ae 24 , ae 25

16 (* for region tuple, quintuple and n-1, respectively *)

17 in hanoi [ae 24 ,ae 7 ,ae 8 ,ae 9 ,ae 10 ,ae 25 ] at ae 22

18 (letregion ae 26 in (n-1at ae 26 ) at ae 25 end (*ae 26 *),

19 other , to, from , acc

20 ) at ae 24

21 end (*ae 22 , ae 24 , ae 25 *)

22 ) at ae 8

23 in :: at ae 7 v 171

24 end

25 ) at ae 18

26 end (*ae 16 , ae 18 , ae 19 *)

27 ) (*case*)

28 end (*ae 13 *)

29 end ;
30 val solution =

31 letregion ae 27 , ae 29 , ae 30

32 in hanoi [ae 29 ,ae 1 ,ae 2 ,ae 3 ,ae 4 ,ae 30 ] at ae 27

33 (20 at ae 30 , "a" at ae 4 , "b" at ae 4 , "c" at ae 4 , nil at ae 1 ) at ae 29

34 end (*ae 27 , ae 29 , ae 30 *)
Figure 2: The region-annotated version of hanoi .
program running under Standard ML of New Jersey, version 93, on the same machine are 75 Mb
and 28.36 seconds, respectively. This difference in running times is particularly noteworthy when
one considers that the ML Kit boxes all tuples, including the tuples of region variables that are
passed to region-polymorphic functions; that is what regions ae 16 , ae 22 and ae 27 are used for.
3 Related Work

The basic ideas of the region inference scheme are described in [23]. An extended version, including
a proof that the region inference rules are sound, may be found in [24]. Other analysis which have
been combined with region inference are described in [1, 2].
The emphasis of this paper is on using unification to constrain region variables and arrow
effects. (Arrow effects decorate function arrows in the region type system with information of how
the function uses regions.) In the case of arrow effects, the difficulty is that the unification is of
sets rather than terms. Similar forms of unification have been studied in record typing[16] and in
type systems for polymorphic references[9].

The region inference algorithm that is currently used in the ML Kit is described and proved
correct in [20]. It is a syntax-directed algorithm, similar to Milner's algorithm W , and it relies on
the results about unification proved in the present paper.
A different approach to region inference is to use constraints. Constraints have been used in
previous work on ML type inference[5], subtyping [12, 4] and effect systems[19, 18, 14, 13]. We are
currently exploring using constraints for region inference. The relative merits of the two approaches
to region inference (syntax-directed region inference versus constraint generation and constraint
solving) are not clear at the time of writing. In both cases, however, termination of the algorithms
depends crucially on the limitations on polymorphic recursion which we introduce in the present
paper.
4 Region Inference Rules

In order to give an overview of the inference problem we are addressing, this section contains the
inference rules which guide our region inference algorithms. (Presenting a full algorithm would require
more space than is available.) Concepts and notation which will be defined in the subsequent
sections of the paper are marked by forward references.
For the purpose of stating invariants about the region algorithms, it is useful to keep careful
track of the sets of region and effect variables that are used by the algorithm. Thus we introduce
(in Section 6) a notion of a basis, B = (Q; \Phi) where Q is a set of region variables and \Phi is a set of

arrow effects. Arrow effects decorate function arrows in derivations. An arrow effect takes the form

ffl:', where ffl is an effect variable and ' is an effect. Amongst the invariants which are essential for
obtaining the result about principal unifiers (Section 8), is that whenever ffl 1 :' 1 and ffl 2 :' 2 are both
members of \Phi and ffl 1 = ffl 2 then ' 1 = ' 2 . The invariants about sets of region variables and arrow
effects that turn out to be important are collected in the definition of consistent bases (Section 6).
Section 6 also defines the disjoint union of bases (B ] B

0

) found in the rules.
The inference rules allow one to infer statements of the form B; TE ` e : ��; ', read: in basis B

and type environment TE, e has type with place �� and effect '. Effects and types with places are
defined in Section 5. Given a consistent basis B, only some types with places make sense. This is
captured by a definition (in Section 5) of what it means for a type with place �� to be consistent
in a basis, B, written B ` ��.

A type environment, TE, is a finite map from program variables to pairs of the form (oe; ae),

where oe is a region-annotated type scheme (Section 9) and ae is a region variable.
The expressions that appear in the rules are called "target expressions", since they are output
from region inference. The terms contain enough type, region and effect information that
the entire proof of the conclusion B; TE ` e : ��; ' is fully determined by B, TE and e. Some
of this information is not necessary at runtime. Therefore, in examples we often abbreviate

letregion B in e end to letregion ae 1 ; : : : ; ae k in e end, where fae 1 ; : : : ; ae k g = Q of B (Section
6). Similarly, we often abbreviate

letrec f : (oe; ae 0 )(x) = e 1 in e 2 end
to letrec f [ae 1 ; : : : ; ae k ] at ae 0 (x) = e 1 in e 2 end, where ae 1 , : : :, ae k are the bound region variables
of oe.

In target expressions, every binding occurrence of a variable is decorated by a region type
scheme (Section 9). Within the scope of the binding, each non-binding occurrence of the variable
is annotated by its own instantiation list (Section 11) which defines an instance of the type
scheme particular to that occurrence. Given a consistent basis B, only some instantiation lists
are meaningful; Section 11 defines what it means for an instantiation list il to be consistent in a
basis, B, written B ` il . In examples (and at runtime) we omit the first and third component of
instantiation list triples, so that x il becomes simply x[ae 1 ; : : : ; ae k ], where ( ; [ae 1 ; : : : ; ae k ]; ) = il .
Given a consistent basis B, only some region-annotated type schemes make sense: Section 10
defines what it means for a region-annotated type scheme oe to be consistent in a basis, B, written

B ` oe. Poitwise extension gives a relation B ` TE.

In the following, we write B ` (TE; il ; ��) as a shorthand for B ` TE, B ` il and B ` ��. It
turns out that B; TE ` e : ��; ' implies that B is consistent and B ` (TE; ��; '). In rule (6) we use
the function Observe defined by Observe(B; ' 1 ) = ' 1 " fv(B).

In the rules, S denotes a substitution, as defined in Section 7.

B ` (TE; il ; ��) TE(x) = (oe; ae) �� = (��; ae)
oe = 8ff 1 \Delta \Delta \Delta ff n ffl 1 \Delta \Delta \Delta ffl m :�� 0 il = ([�� 1 ; : : : ; �� n ]; [ ]; [ffl

0

1 :'

0

1 ; : : : ; ffl

0

m :'

0

m ])

S = (fff 1 7! �� 1 ; : : : ; ff n 7! �� n g; fg; fffl 1 7! ffl

0

1 :'

0

1 ; : : : ; ffl m 7! ffl

0

m :'

0

m g)

�� = S(�� 0 )

B; TE ` x il : ��; ;

(1)
B ` (TE; il ; ��) TE(x) = (oe; ae) �� = (��; ae

0

)

oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� 0 il = ([�� 1 ; : : : ; �� n ]; [ae

0

1 ; : : : ; ae

0

k ]; [ffl

0

1 :'

0

1 ; : : : ; ffl

0

m :'

0

m ])

S = (fff 1 7! �� 1 ; : : : ; ff n 7! �� n g; fae 1 7! ae

0

1 ; : : : ; ae k 7! ae

0

k g; fffl 1 7! ffl

0

1 :'

0

1 ; : : : ; ffl m 7! ffl

0

m :'

0

m g)

�� = S(�� 0 )

B; TE ` x il at ae

0

: �� : fae; ae

0

g

(2)
B ` TE B; TE + fx 7! �� x g ` e 1 : �� 1 ; ' 1 ' 0 ' ' 1 (faeg; fffl:' 0 g) ` B
B; TE ` x : �� x :e 1 : (�� x
ffl:' 0

\Gamma\Gamma\Gamma\Gamma! �� 1 ; ae); faeg

(3)
B; TE ` e 1 : (��

0 ffl 0 :'0

\Gamma\Gamma\Gamma\Gamma! ��; ae 0 ); ' 1 B; TE ` e 2 : ��

0

; ' 2

B; TE ` e 1 e 2 : ��; ' 1 [ ' 2 [ fffl 0 ; ae 0 g [ ' 0

(4)
B ` (TE; ' 1 ) oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� 0  oe = 8ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� 0

B 1 = bound(oe) B ] B 1 exists �� 0 = �� x
ffl 0 :'0

\Gamma\Gamma\Gamma\Gamma! �� 1 btv(oe) " ftv(TE) = ;

B ] B 1 ; TE + ff 7! (oe; ae 0 )g ` x : �� x :e 1 : (�� 0 ; ae 0 ); ' 1

B; TE + ff 7! (oe; ae 0 )g ` e 2 : ��; ' 2

B; TE ` letrec f : (oe; ae 0 )(x)= e 1 in e 2 end : ��; ' 1 [ ' 2

(5)
B ] B 1 exists B ] B 1 ; TE ` e 1 : �� : ' 1 B ` (TE; ��) ' = Observe(B; ' 1 )

B; TE ` letregion B 1 in e 1 : �� : ' 1 end : �� : '

(6)
5 Types and Effects

In this section we first motivate the region-annotated types and type schemes that are used in
region inference and then define them formally.

5.1 Region Variables and Effects

The region scheme annotates every type constructor with a region variable. Also, type schemes
can universally quantify region variables and (as in Milner's type discipline) type variables. The
type scheme of hanoi of Figure 2 is approximately the following:

8ae 6 ae 7 ae 8 ae 9 ae 10 ae 11 :

\Gamma

(int; ae 11 )  (ff; ae 10 )  (ff; ae 10 )  (ff; ae 10 )  (((ff; ae 10 )  (ff; ae 10 ); ae 9 )list hae 8 i ; ae 7 );

ae 6

\Delta ffl

\Gamma!(((ff; ae 10 )  (ff; ae 10 ); ae 9 )list hae 8 i ; ae 7 )
where ffl = fae 6 ; ae 7 ; ae 8 ; ae 9 ; ae 11 g

Here ff is paired with ae 10 , list with ae 7 and the tuple constructor (     ) is paired with

ae 6 . The datatype constructor list has an additional, so-called auxiliary region variable, here ae 8 .
This is the region where the pairs to which cons (::) is applied are put. The set ffl which appears
on the function arrow is an effect ; it contains all the regions which the evaluation of the function
body might access. hanoi reads from region ae 6 (when it extracts the components of its argument
quintuple), it reads n from region ae 11 and it puts values into regions ae 7 , ae 8 and ae 9 . The effect
reveals that hanoi does not access ae 10 at all.
In [23] there is a distinction between put and get effects; for example, the above effect would be
written fget(ae 6 ); put(ae 7 ); put(ae 8 ); put(ae 9 ); get(ae 11 )g. This distinction is useful for other analyses
and optimisations which can be combined with region inference[2]; however, for the purpose of this
paper, the distinction between put and get is not important and is therefore omitted.
5.2 Effect Variables and Arrow Effects

In the type scheme for hanoi we use ffl and "where" as meta-notation to make the type scheme easier
to read. A crucial next step, invented in work on effect inference[18], is to make effect variables
part of the language of types, on a par with type variables and region variables. Moreover, we
represent "where ffl = fae 6 ; ae 7 ; ae 8 ; ae 9 ; ae 11 g" by a formal object "ffl:fae 6 ; ae 7 ; ae 8 ; ae 9 ; ae 11 g" which is called
an arrow effect, because arrow effects appear on function arrows. Using an effect variable and an
arrow effect, the type scheme for hanoi becomes:

oe h = 8ffae 6 ae 7 ae 8 ae 9 ae 10 ae 11 ffl 12 :

\Gamma

(int; ae 11 )  (ff; ae 10 )  (ff; ae 10 )  (ff; ae 10 )
(((ff; ae 10 )  (ff; ae 10 ); ae 9 )list hae 8 i ; ae 7 ); ae 6

\Delta

ffl 12 :fae 6 ;ae 7 ;ae 8 ;ae 9 ;ae 11 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(((ff; ae 10 )  (ff; ae 10 ); ae 9 )list hae 8 i ; ae 7 )
As we shall see in Section 11 instantiation of type schemes allows universally quantified effects to
increase; so one can equally think of ffl:' as meaning "ffl, where ffl ' "'. Note that the scope of the
effect variable is now given by 8, which can bind type, region and effect variables. Capture-avoiding
renaming of bound variables is permitted in the usual way.
In a first-order programming language, one could do region inference without effect variables.
But for a higher-order language, effect variables are essential for representing the effects of (unknown)
functions. To illustrate this, assume we continue our example program with the declarations:


fun app f x = f(x)

fun run n = app hanoi (n, "a", "b", "c", nil)

The function app has the type scheme

oe app = 8ff 1 ff 2 ae 1 ae 2 ae 3 ffl 1 ffl 2 ffl 3 :

\Gamma

(ff 1 ; ae 1 )

ffl 1 :;

\Gamma\Gamma\Gamma!(ff 2 ; ae 2 ); ae 3

\Delta ffl 2 :fae 4 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!

\Gamma

(ff 1 ; ae 1 )

ffl 3 :fae 3 ;ffl 1 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(ff 2 ; ae 2 ); ae 4

\Delta

The arrow effect ffl 3 :fae 3 ; ffl 1 g is justified as follows: ae 3 has to be in the effect since the evaluation
of f(x) involves accessing ae 3 , the region holding the function f . Also, the effect of the expression

f(x) has to be at least the effect of the function f , irrespective of what actual arguments we pass
in for f ; this is represented by letting ffl 1 be in the arrow effect. In other words, app has an "effect
dependent" type: the effect of app f depends on the effect of f .
To see how this dependency comes into use, consider the application app hanoi in the declaration
of run. Let ff

0

, ae

0

6 ; ae

0

7 , ae

0

8 , ae

0

9 , ae

0

10 , ae

0

11 and ffl

0

12 be fresh variables. We can give the occurrence of

hanoi in the declaration of run the following instance of oe h :

�� h =

\Gamma

(int; ae

0

11 )  (ff

0

; ae

0

10 )  (ff

0

; ae

0

10 )  (ff

0

; ae

0

10 )  (((ff

0

; ae

0

10 )  (ff

0

; ae

0

10 ); ae

0

9 )list hae

0

8 i ; ae

0

7 ); ae

0

6

\Delta

ffl

0

12 :fae

0

6 ;ae

0

7 ;ae

0

8 ;ae

0

9 ;ae

0

11 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(((ff

0

; ae

0

10 )  (ff

0

; ae

0

10 ); ae

0

9 )list hae

0

8 i ; ae

0

7 )
Similarly, the following type is an instance of oe app :

�� 0 = (�� h ; ae 100 )

ffl 101 :'

0

\Gamma\Gamma\Gamma\Gamma\Gamma!(�� h ; ae 102 )

where ae 100 , ffl 101 and ae 102 are fresh ('

0

will be determined shortly). Here we have instantiated the arrow
effect ffl 1 :; of oe app to the arrow effect ffl

0

12 :fae

0

6 ; ae

0

7 ; ae

0

8 ; ae

0

9 ; ae

0

11 g of �� h . But when we then instantiate
the arrow effect ffl 3 :fae 3 ; ffl 1 g from oe app , the dependency of ffl 3 upon ffl 1 implies that the effect to which

ffl 3 is instantiated must contain all that ffl

0

12 stands for, i.e., the effect fae

0

6 ; ae

0

7 ; ae

0

8 ; ae

0

9 ; ae

0

11 g. In fact, the
definition of generic instance presented in Section 11 will take '

0

to be fae 100 ; ffl

0

12 ; ae

0

6 ; ae

0

7 ; ae

0

8 ; ae

0

9 ; ae

0

11 g,

where the presence of ffl

0

12 keeps track of the fact that the result of evaluating app hanoi , when applied
to (n, "a", "b", "c", nil), will call hanoi .
To sum up, effect variables are useful for tracking function applications in functional languages.
Moreover, using effect polymorphism to represent function dependencies has two advantages:
1. The effect dependencies of app can be determined from its declaration alone, without looking
at how the function is subsequently used;
2. In the scope of the declaration of app, if there are two applications, app g and app h, say,
then the arrow effects of g and h need not be the same;
Both advantages are inherited from Milner-style polymorphism.
5.3 Definitions

We assume a denumerably infinite set TyVar of type variables. We use ff to range over type
variables. Next, ML types, ��

ML

, and ML type schemes, oe

ML

, are given by the grammar:

��

ML

::= int j ff j ��

ML

! ��

ML

ML type

oe

ML

::= ��

ML

j 8ff:oe

ML

ML type scheme
For the purpose of region inference, we assume two additional denumerably infinite sets:

ae 2 RegVar region variables

ffl 2 EffVar effect variables
TyVar, RegVar and EffVar are assumed to be pairwise disjoint. An atomic effect is a region variable
or an effect variable; an effect is a finite set of atomic effects:

j 2 AtEff = RegVar [ EffVar atomic effect

' or fj 1 ; : : : ; j k g 2 Effect = Fin(AtEff) effect

ffl:' 2 ArrEff = EffVar \Theta Effect arrow effect
Annotated types are given by:

�� ::= int j ff j ��

ffl:'

\Gamma\Gamma\Gamma! �� annotated type

�� ::= (��; ae) annotated type with place
The set of annotated types is denoted Type and the set of annotated types with places is denoted
TypeWithPlace; "annotated type" is abbreviated to "type" when confusion with "ML type" is
unlikely. In a function type ��

ffl:'

\Gamma\Gamma\Gamma! ��

0

the object ffl:' is called an arrow effect. Formally, an arrow
effect is a pair of an effect variable and an effect; we refer to ffl and ' as the handle and the latent
effect, respectively.
Equality of types is defined by term equality, as usual, but up to set equality of latent effects.
For example, the arrow effects ffl:fae; ae

0

g and ffl:fae

0

; aeg are equal.
We refer to the above semantic objects (i.e., type variables, region variables, effect variables,
atomic effects, effects, arrow effects, types and types with places) collectively as basic semantic
objects and use o to range over these. Erasure of region and effect information from annotated
types yields ML types; it is defined recursively by:

ML(ff) = ff; ML(int) = int; ML(��; ae) = ML(��)
ML(��

ffl:'

\Gamma\Gamma\Gamma! ��

0

) = ML(��) ! ML(��

0

)

Let �� or �� be a type or a type with place. The arrow effects of �� (or ��), written arreff (��) (or

arreff (��)) is the set of arrow effects defined by

arreff (ff) = ;; arreff (int) = ;; arreff (��; ae) = arreff (��)

arreff (��

ffl:'

\Gamma\Gamma\Gamma! ��

0

) = fffl:'g [ arreff (��) [ arreff (��

0

)
The set of type variables, effect variables and region variables that occur free in a semantic object A

will be denoted ftv(A), fev (A) and frv(A), respectively. For basic semantic objects, these functions
are defined by:

ftv(int) = ; ftv(ff) = fffg ftv(��

ffl:'

\Gamma\Gamma\Gamma! ��

0

) = ftv(��) [ ftv(��

0

) ftv(��; ae) = ftv(��)
frv (ae) = faeg frv(��; ae) = faeg [ frv(��) frv (int) = frv (ff) = ;

frv(��

ffl:'

\Gamma\Gamma\Gamma! ��

0

) = frv (��) [ frv(ffl:') [ frv (��

0

) frv(ffl:') = ' " RegVar

fev (ae) = ; fev (��; ae) = fev (��) fev(int) = fev (ff) = ;

fev (��

ffl:'

\Gamma\Gamma\Gamma! ��

0

) = fev (��) [ fev (ffl:') [ fev (��

0

) fev (ffl:') = ffflg [ (' " EffVar)
We denote the set of free variables of A (of either kind) by fv(A), i.e., fv (A) = frv (A) [ ftv(A) [

fev (A).
A finite map is a function whose domain is finite. When A and B are sets, the set of finite
maps from A to B is denoted A

fin

! B. The domain and range of a finite map, f , are denoted
Dom(f) and Rng(f ), respectively; the restriction of f to a set, A, is written f # A. A finite map
is often written explicitly in the form fa 1 7! b 1 ; : : : ; a k 7! b k g, k  0; in particular, the empty
map is fg. For every f : A

fin

! B and g : B ! C the finite map g ffl f : A

fin

! C is defined by
Dom(g ffl f) = Dom(f) and (g ffl f)(x) = g(f(x)).
6 Consistent Bases

To obtain eager recycling of memory, regions should be kept distinct, unless they are forced to be
equal. Although not all the concepts have been formally introduced yet, the reader might want to
take a sneak preview of the region inference rules in Section 4. These rules specify which region
annotations are permitted in a skeletal language. The region inference algorithm (not presented)
will keep regions distinct, unless they are required by the rules to be equal. The only rule which
forces regions to be equal is rule (4) which concerns function application. Since types are decorated
with regions (and arrow effects) the two occurrences of ��

0

in the premises of the rule demands that
function and argument agree not just on types but also on regions and effects. In order to satisfy
the premises of the inference rule, the region inference algorithm needs to be able to unify types
which contain region and effect information.
Hindley[6] and Milner[10] discovered that Robinson's unification algorithm can be used for
unifying types. We assume that type inference has already been carried out by the time region
inference is performed. Thus the problem we are faced with is to unify region-annotated types which
have the same underlying ML types but which may have different region and effect annotations.
This problem would be very simple, were it not for the fact that types can contain effects, which
are sets. It is not the case that if a set unification problem has a solution (a substitution which
when applied to the two sets makes them equal) then it has a most general solution.
However, the use of arrow effects suggests an alternative to using set unification. Assume we
are given two arrow effects ffl 1 :' 1 and ffl 2 :' 2 which we want to "unify". (For simplicity, assume

fffl 1 ; ffl 2 g " (' 1 [ ' 2 ) = ;.) We now simply select one of the effect variables, say ffl 1 , and let it stand
for ' 1 [ ' 2 :

ffl 1 :' 1 ffl 2 :' 2

Before unification
After unification

@
@
@
@
@ @R
\Gamma
\Gamma
\Gamma
\Gamma
\Gamma \Gamma\Psi

S S
ffl 1 :(' 1 [ ' 2 )
In the picture, S is a substitution. (Substitutions will be defined in Section 7.)
Another way of thinking of ffl 1 :' 1 and ffl 2 :' 2 is as two constraints ffl 1 ' ' 1 and ffl 2 ' ' 2 [18];
then the "unification" of the two arrow effect corresponds to replacing ffl 2 by ffl 1 everywhere and
replacing the two constraints by a single constraint ffl 1 ' (' 1 [ ' 2 ).
Although the region inference rules (1) -- (6) can be expressed using constraints rather than
arrow effects along the lines of [18], constraint sets complicate the definitions of type schemes,
generic instance, generalisation and the Observe operation given later in this paper. The best
approach seems to be to use arrow effects for presenting the region inference system and then
either also use arrow effects in the algorithms (as we do in this paper) or relate the region rules
presented in this paper to a separate inference system which uses constraints that are solved
separately. We are currently also exploring the latter possibility.
It is convenient to be able to see what effect a given effect variable in a given type denotes
without reference to a constraint set. Therefore, within the scope of a binding occurrence of an
effect variable ffl, we want ffl to be the handle of one and only one effect. There are other natural
well-formedness conditions which we expect to hold. For example, in a type scheme of the form

8ffl 1 ffl 2 :((�� 1

ffl 1 :'1

\Gamma\Gamma\Gamma\Gamma! �� 2 ); ae 1 )

ffl 2 :'2

\Gamma\Gamma\Gamma\Gamma! �� 3

if we have ffl 1 2 ' 2 then we should also have ' 1 ` ' 2 . These invariants are formalised by the notion
of effect consistency defined below. As we shall see later, types which are decorated with arrow
effects taken from an effect consistent set have most general unifiers, in a sense which will be made
precise below.

Definition 1 A set \Phi of arrow effects is effect consistent, written ` \Phi, if
1. \Phi is functional: for all (ffl 1 :' 1 ) 2 \Phi and (ffl 2 :' 2 ) 2 \Phi if ffl 1 = ffl 2 then ' 1 = ' 2 ;
2. \Phi is closed: for all (ffl:') 2 \Phi and ffl

0

2 ' there exists '

0

such that (ffl

0

:'

0

) 2 \Phi;

3. \Phi is transitive: for all (ffl 1 :' 1 ) 2 \Phi and (ffl 2 :' 2 ) 2 \Phi if ffl 2 2 ' 1 then ' 2 ` ' 1 ; ut

For any functional \Phi, the effect map of \Phi, written  \Phi, is the partial map from effect variables
to effects defined by  \Phi(ffl) = ', if ffl:' 2 \Phi. We define frv (\Phi) = [ffrv(ffl:') j ffl:' 2 \Phig and

fev (\Phi) = [ffev(ffl:') j ffl:' 2 \Phig.
A basis is a pair B = (Q; \Phi), where Q is a set of region variables and \Phi is a set of arrow effects.
The set of bases is called Basis. We say that B is consistent, written ` B, if Q ' frv (\Phi) and ` \Phi.
We define frv(B) = Q [ frv (\Phi) and fev(B) = fev (\Phi). Notice that if B = (Q; \Phi) is consistent then

frv(B) = Q since Q ' frv (\Phi). Moreover, if B = (Q; \Phi) is consistent then fev (B) = Dom(

\Phi), since
\Phi is closed. The domain of a consistent basis B = (Q; \Phi), written Dom(B), is the set Q [ fev (\Phi).
A basis B = (Q; \Phi) is finite if Q and \Phi are both finite sets. When B is a basis we write Q of B

and \Phi of B for the first and second component of B, respectively.

Example 5.1 The basis B 1 = (fae 1 g; fffl 1 :;; ffl 1 :fae 1 gg) is not consistent: ffl 1 cannot both denote
the empty effect and the effect fae 1 g. Formally, B 1 is not functional. However, B 2 =
(fae 1 g; fffl 1 :;; ffl 2 :fae 1 gg) is consistent. ut

Example 5.2 The basis B 3 = (fae 1 ; ae 2 g; fffl 1 :fae 1 g; ffl 2 :fffl 1 ; ae 2 gg) is not consistent: the effect which

ffl 2 denotes has ffl 1 as a member but is not a superset of the set which ffl 1 denotes. Formally: B 3 is
not transitive. However, B 4 = (fae 1 ; ae 2 g; fffl 1 :fae 1 g; ffl 2 :fffl 1 ; ae 1 ; ae 2 gg is consistent. ut

Let o range over basic semantic objects and let B = (Q; \Phi) be a basis. We say that o is

consistent in B, if the sentence B ` o can be inferred from the following rules:

` B ae 2 Q of B
B ` ae

` B ffl:' 2 \Phi of B
B ` ffl:'

` B j 2 fv(B)

B ` j

` B
B ` int

` B
B ` ff
B ` �� B ` ae
B ` (��; ae)
B ` �� 1 B ` ffl:' B ` �� 2

B ` �� 1

ffl:'

\Gamma\Gamma\Gamma! �� 2

ffl = 2 fev (\Phi) [ ' ` (Q; \Phi [ fffl:'g)

(Q; \Phi) ` '

All these rules, except the last one, should be straightforward: they simply state that a semantic
object is consistent in a basis B = (Q; \Phi) only if (a) the basis is consistent by itself and (b) all the
region and effect variables appearing in o are free in B and (c) if an arrow effect ffl:' occurs in o then

' is uniquely determined by the equation ' =

\Phi(ffl). The last inference rule says that ' is consistent
in B if, imagining that we pick a fresh effect variable ffl

0

, the extended basis B [ (;; ffl

0

:') would
become consistent. Alternatively, this rule can be expressed as the conjunction of (a) B = (Q; \Phi)
is consistent, (b) ' ` fv(B) and (c) for all ffl 2 ' one has

\Phi(ffl) ` '.
Example 5.3 Let �� = (int; ae 1 ). The types ��

ffl 1 :;

\Gamma\Gamma\Gamma! �� and ��

ffl 1 :fae 1 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma! �� cannot be consistent
in the same basis. However, ��

ffl 1 :;

\Gamma\Gamma\Gamma! �� and ��

ffl 2 :fae 1 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma! �� are both consistent in the basis B 2 from
Example 5.1. ut

Example 5.4 Consider the basis B 4 from Example 5.2. The effect fae 1 g is consistent in B 4 ; so
is fffl 1 ; ae 1 ; ae 2 g, but not fffl 2 ; ae 1 g. ut

As usual, we often write "B ` o" to mean "there exists a proof tree with conclusion B ` o." It
is easy to see that B ` o implies that B is consistent and that fv(o) ` Dom(B).
Let B 1 = (Q 1 ; \Phi 1 ) and B 2 = (Q 2 ; \Phi 2 ) be bases. We define the union of B 1 and B 2 , written

B 1 [B 2 to be (Q 1 [ Q 2 ; \Phi 1 [ \Phi 2 ). We define the disjoint union of B 1 and B 2 , written B 1 ]B 2 , to
be B 1 [B 2 provided B 1 [B 2 is consistent and Dom(B 1 ) " Dom(B 1 ) = ;, and undefined otherwise.
Note that B 1 ]B 2 can be defined even in cases where B 1 and B 2 are not consistent by themselves.
Typically, this concept is used for expressing disjointness of bound variables, for example in rule (5),
where B is consistent and B ] B 1 is consistent, but B 1 not necessarily is consistent, since it can
contain occurrences of region and effect variables that are in Dom(B).

7 Substitution

Suppose for example that we want to unify the two types �� 1 = (int; ae 1 )

ffl 1 :fae 1 ;ae 2 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(int; ae 2 ) and

�� 2 = (int; ae 3 )

ffl 2 :;

\Gamma\Gamma\Gamma!(int; ae 3 ). These two types could arise during region inference, for example as
the type of the then branch and the else branch, respectively, of the conditional:

if true then (fn x =? x+1) else (fn y =? y)
From the region variables that decorate int in �� 1 and �� 2 we see that a unifier for �� 1 and �� 2 has
to map ae 1 , ae 2 and ae 3 to the same region variable, say ae 1 . But a unifier for �� 1 and �� 2 must also
map the arrow effects in �� 1 and �� 2 to the same arrow effect, for example ffl 1 :fae 1 g. But how can a
substitution map ffl 2 :; to ffl 1 :fae 1 g? Certainly it cannot, if substitutions simply map effect variables
to effect variables. Letting substitutions map effect variables to effects and defining S(ffl:') to be

S(ffl):S(') is not an option either for S(ffl) would not be an effect variable and S(ffl):S(') therefore

not an arrow effect. The solution is to let substitutions map effect variables to arrow effects.
For example, we allow S

e

0 = fffl 1 7! ffl 1 :fae 1 g; ffl 2 7! ffl 1 :fae 1 gg as a substitution. The definition of
substitution given below is such that S

e

0 (ffl 1 :fae 1 g) = ffl 1 :fae 1 g = S

e

0 (ffl 2 :;), i.e, that S

e

0 is a unifier for

ffl 1 :fae 1 g and ffl 2 :;.

Formally, a type substitution is a map from type variables to types; a region substitution is a
map from region variables to region variables; an effect substitution is a map from effect variables to
arrow effects. We we use S

t

, S

r

and S

e

to range over type, region and effect substitutions, respectively.
A substitution is a triple (S

t

; S

r

; S

e

); we use S to range over substitutions. Substitution
on basic semantic objects is defined as follows. Let S = (S

t

; S

r

; S

e

); then

Effects
S(') = fS r (ae) j ae 2 'g [
fj j 9ffl; ffl

0

; '

0

: ffl 2 '  ffl

0

:'

0

= S e (ffl)  j 2 fffl

0

g [ '

0

g

Arrow Effects
S(ffl:') = ffl

0

:('

0

[ S(')); where ffl

0

:'

0

= S e (ffl)

Types and Region Variables

S(int) = int S(ff) = S t (ff) S(ae) = S r (ae)

S(��; ae) = (S(��); S(ae))
S(��

ffl:'

\Gamma\Gamma\Gamma! ��

0

) = S(��)

S(ffl:')

\Gamma\Gamma\Gamma\Gamma\Gamma! S(��

0

)
We write S 2 ffi S 1 for the composition of S 2 and S 1 : (S 2 ffi S 1 )(x) = S 2 (S 1 (x)). The identity

substitution Id = (Id

t

; Id

r

; Id

e

), defined by Id

r

(ae) for all ae 2 RegVar, Id

t

(ff) = ff for all ff 2 TyVar,
and Id

e

(ffl) = ffl:; for all ffl 2 EffVar.
The support of a type substitution S

t

, written Supp(S

t

), is the set fff 2 TyVar j S

t

(ff) 6= ffg.

Similarly for region substitutions. The support of an effect substitution S

e

, written Supp(S

e

), is
the set fffl 2 EffVar j S

e

(ffl) 6= ffl:;g. The support of a substitution S, written Supp(S), is the
union of the supports of its three components. The yield of S, written Yield (S), is fv (Rng(S

t

#

(Supp(S

t

))) [ Rng(S

r

# (Supp(S

r

))) [ Rng(S

e

# (Supp(S

e

)))). The set of variables involved in S,

written Inv(S), is defined to be Supp(S) [ Yield (S).
A finite substitution is a triple S = (S

t

; S

r

; S

e

) where S

t

, S

r

and S

e

are finite maps of the
appropriate types. When S

0

is a substitution and S = (S

t

; S

r

; S

e

) is a finite substitution, we write

S

0

ffl S to mean the finite substitution (S

0

ffl S

t

; S

0

ffl S

r

; S

0

ffl S

e

). The composition S

0

ffl S is useful
when S instantiates the bound variables of a type scheme and S

0

is a substitution applied to the
whole type scheme (see the proof of Lemma 7 for an example).
Every finite substitution can be extended a (total) substitution on basic semantic objects and
we shall often tacitly assume that this extension has taken place before the substitution is applied.
Application of a substitution S to a basis B = (Q; \Phi) yields the basis S(B) = (fS(ae) j ae 2

Qg; fS(ffl:') j ffl:' 2 \Phig).
7.1 Contraction

It turns out, that unification always can be expressed as the composition of substitutions of a
particularly simple kind, namely the so-called elementary contractions:

Definition 2 Let B = (Q; \Phi) be a consistent basis. A substitution S is an elementary contraction
of B if
1. S = Id; or

2. S = (fg; fae 1 7! ae 2 g; fg), for some ae 1 ; ae 2 2 Q; or
3. S = (fg; fg; fffl 1 7! ffl 2 :;g), where fffl 1 ; ffl 2 g ` Dom(  \Phi) and  \Phi(ffl 1 ) =  \Phi(ffl 2 ); or
4. S = (fg; fg; fffl 7! ffl:'g), for some ffl and ' with ffl 2 Dom(  \Phi) and B ` ' and ' '  \Phi(ffl); ut

In terms of constraints, the third item allows us to collapse two constraints ffl 1 ' ' and ffl 2 ' '

into a single constraint ffl 2 ' '

0

(where '

0

is ' with any occurrence of ffl 1 replaced by ffl 2 ). Similarly,
the fourth item corresponds to strengthening a constraint ffl ' ' 1 to ffl ' ' 1 [ '

0

, provided ' [ '

0

is consistent in B. (In particular, one cannot introduce region and effect variables which are not
already in Dom(B).)
Elementary contractions are idempotent. If S is an elementary contraction of a consistent basis

B, then S(B) is consistent.
Let B be a consistent basis. We say that a substitution S is a contraction of B if it can be
written as a composition S = Sn ffi : : : ffi S 1 , n  1, such that S 1 is an elementary contraction of B

and for all i with 1 ! i  n, S i is an elementary contraction of (S i\Gamma1 ffi : : : ffi S 1 )(B).
We say that B 1 is less than or equal to B 2 , written B 1  B 2 , if there exists a contraction S

of B 2 such that B 1 = S(B 2 ). Note that if S is an elementary contraction of B and S(B) 6= B

then there exists no contraction S

0

of S(B) such that S

0

(S(B)) = B. Thus  is a partial order on
consistent bases. We write B 1 ! B 2 to mean B 1  B 2 and B 1 6= B 2 .

Lemma 3 Let B 0 be a finite, consistent basis. There exists no infinite descending chain:

B 0 ? B 1 ? B 2 ? \Delta \Delta \Delta

A proof of the above lemma may be found in [20]. The lemma plays a crucial role in the proof
that the region inference algorithm terminates. The region inference algorithm iterates over the
program, contracting the basis and modifying the program annotations in the process. Things are
arranged so that if the program has been traversed without making the basis smaller, then the
annotated program is well-typed according to the region inference rules. Lemma 3 ensures that
this will eventually happen.

Lemma 4 Let o be a basic semantic object and let S be a contraction of a basis B. If B ` o then

S(B) ` S(o).

In particular, if B is consistent and S is a contraction then S(B) is consistent.

Proof By induction on the number of elementary contractions out of which S is constructed, with
an inner induction on the depth of B ` o. ut
8 Unification

8.1 Unification of Arrow Effects

Let B = (Q; \Phi) be a consistent basis and assume ffl 1 :' 1 2 \Phi and ffl 2 :' 2 2 \Phi. A substitution S is a

unifier for ffl 1 :' 1 and ffl 2 :' 2 in B if S(B) is consistent and S(ffl 1 :' 1 ) = S(ffl 2 :' 2 ). A substitution S



is a most general unifier for ffl 1 :' 1 and ffl 2 :' 2 in B, if S



is a unifier for ffl 1 :' 1 and ffl 2 :' 2 in B and
for every unifier S for ffl 1 :' 1 and ffl 2 :' 2 in B there exists a substitution S

0

such that
1. S(ae) = S

0

(S



(ae)), for all ae 2 Q;

2. S(ffl:') = S

0

(S



(ffl:')), for all ffl:' 2 \Phi;
The following algorithm takes two arrow effects as arguments and returns an effect substitution
which is a most general unifier for the two arrow effects:

unifyArrEff (ffl 1 :' 1 ; ffl 2 :' 2 ) =
let

S

e

1 = if ' 2 ` ' 1 then Id

e

else fffl 1 7! ffl 1 :(' 1 [ ' 2 )g

S

e

2 = if ' 1 ` ' 2 then Id

e

else fffl 2 7! ffl 2 :(' 1 [ ' 2 )g

S

e

3 = if ffl 1 = ffl 2 then Id

e

else fffl 2 7! ffl 1 :;g

in

S

e

3 ffi S

e

2 ffi S

e

1

end
Lemma 5 Let B = (Q; \Phi) be a consistent basis and let ffl 1 :' 1 2 \Phi and ffl 2 :' 2 2 \Phi. Then S

e

=

unifyArrEff (ffl 1 :' 1 ; ffl 2 :' 2 ) succeeds and
1. S

e

is a most general unifier for ffl 1 :' 1 and ffl 2 :' 2 in B;

2. S

e

is a contraction of B;

3. S

e

(B) = B implies S

e

= Id

e

;

Proof Let (Q; \Phi) = B. Since B ` ' 1 [ ' 2 and ' 1 [ ' 2 ' ' 1 =

\Phi(ffl 1 ), we have that S

e

1 is an
elementary contraction, even if ' 2 6` ' 1 . Thus S

e

1 (B) is consistent. Next, S

e

2 is an elementary
contraction of S

e

1 (B), since either S

e

2 = Id

e

or S

e

1 (B) ` ' 1 [ ' 2 and ' 1 [ ' 2 ' d S

e

1 (\Phi)(ffl 2 ) =

' 2 . Thus S

e

2 (S

e

1 (B)) is consistent. Next, S

e

2 (S

e

1 (ffl 1 :' 1 )) = S

e

2 (ffl 1 :(' 1 [ ' 2 )) = ffl 1 :(' 1 [ ' 2 ) and

S

e

2 (S

e

1 (ffl 2 :' 2 )) = S

e

2 (ffl 2 :' 2 ) = ffl 2 :(' 1 [ ' 2 ). Thus S

e

3 is an elementary contraction of S

e

2 (S

e

1 (B)),
even if ffl 1 6= ffl 2 . Thus S

e

is a contraction of B.

The following calculation shows that S

e

unifies ffl 1 :' 1 and ffl 2 :' 2 : S

e

(ffl 1 :' 1 ) = S

e

3 (S

e

2 (S

e

1 (ffl 1 :' 1 ))) =

S

e

3 (S

e

2 (ffl 1 :(' 1 [ ' 2 ))) = S

e

3 (ffl 1 :(' 1 [ ' 2 )) = S

e

3 (ffl 2 :(' 1 [ ' 2 )) = S

e

3 (S

e

2 (ffl 2 :' 2 )) = S

e

3 (S

e

2 (S

e

1 (ffl 2 :' 2 ))).
Since S

e

is a contraction of B we have that S

e

(B) is consistent, so S

e

really is a unifier for ffl 1 :' 1

and ffl 2 :' 2 in B.

Finally, we show that S

e

is a most general unifier. Let S be any unifier for ffl 1 :' 1 and ffl 2 :' 2 in

B. Let ffl

0

:'

0

= S(ffl 1 :' 1 ) = S(ffl 2 :' 2 ) and let S

0

= fffl

0

7! ffl

0

:'

0

g ffi S. We now show that this S

0

has
the desired properties. Certainly, S(ae) = S

0

(S

e

(ae)), for all ae 2 Q, since S

e

is an effect substitution.
Next, take an arbitrary ffl:' 2 \Phi. We proceed by case analysis:
ffl 6= ffl 1  ffl 6= ffl 2  ffl 1 62 '  ffl 2 62 ' Here S

0

(S

e

(ffl:')) = S

0

(ffl:') = fffl

0

7! ffl

0

:'

0

g(S(ffl:')) = S(ffl:')

since S(ffl:') and ffl

0

:'

0

both are members of S(\Phi), which, by assumption, is effect consistent.
ffl 6= ffl 1  ffl 6= ffl 2  (ffl 1 2 '  ffl 2 2 ') Let ffl

00

:'

00

= S(ffl). We first prove

S(') = S

0

(S

e

(')) (7)
We have S(') = S(' [' 1 [' 2 ) since fffl 1 ; ffl 2 g " ' 6= ; and therefore, by consistency, fffl 1 g [' 1 ` '

or fffl 2 g [ ' 2 ` ', so that S(fffl 1 g [ ' 1 ) = S(fffl 2 g [ ' 2 ) ` S('). Moreover, we have S(fffl 2 7!

ffl 1 :;g(' [ ' 1 [ ' 2 )) ` S(' [ ' 1 [ ' 2 ), even if ffl 1 62 '; for in that case we must have ffl 2 2 '

(by case assumption) and therefore fv(S(ffl 1 )) ` fffl

0

g [ '

0

` S('). We do not necessarily have

S(fffl 2 7! ffl 1 :;g(' [ ' 1 [ ' 2 )) = S(' [ ' 1 [ ' 2 ).

2

But '

0

[ S(fffl 2 7! ffl 1 :;g(' [ ' 1 [ ' 2 )) =

S(' [ ' 1 [ ' 2 ), since S(ffl 1 :' 1 ) = S(ffl 2 :' 2 ) = ffl

0

:'

0

. Thus S(') = S(' [ ' 1 [ ' 2 ) = '

0

[ S(fffl 2 7!

ffl 1 :;g(' [ ' 1 [ ' 2 )) = S

0

(S

e

(')), proving (7). Now the following computation gives the desired
result: S

0

(S

e

(ffl:')) = S

0

(ffl:S

e

(')) = fffl

0

7! ffl

0

:'

0

g(S(ffl:S

e

('))) = fffl

0

7! ffl

0

:'

0

g(ffl

00

:('

00

[S(S

e

(')))) =

ffl

00

:('

00

[ '

0

[ S(S

e

('))) = ffl

00

:('

00

[ S

0

(S

e

('))) = ffl

00

:('

00

[ S(')) = S(ffl:').
ffl = ffl 1 Since B is consistent we have ffl:' = ffl 1 :' 1 , so S

0

(S

e

(ffl:')) = fffl

0

7! ffl

0

:'

0

g(S(S

e

(ffl 1 :' 1 ))) =

2

Example: Consider ffl 1 :' 1 = ffl 1 :fffl 2 g, ffl 2 :' 2 = ffl 2 :;; let S(ffl 1 ) = ffl

0

:; and S(ffl 2 ) = ffl

0

:fffl

0

; aeg. Then S(ffl 1 :fffl 2 g) =

S(ffl 2 :;) = ffl

0

:fffl

0

; aeg, S

e

(ffl 1 ) = S

e

(ffl 2 ) = ffl 1 :fffl 1 g but S(fffl 1 g) = fffl

0

g ae fffl

0

; aeg = S(fffl 1 ; ffl 2 g).

fffl

0

7! ffl

0

:'

0

g(S(ffl 1 :fffl 2 7! ffl 1 :;g(' 1 [ ' 2 ))) = ffl

0

:'

0

= S(ffl 1 :' 1 ) = S(ffl:').
ffl = ffl 2 Since B is consistent we have ffl:' = ffl 2 :' 2 , so S

0

(S

e

(ffl:')) = fffl

0

7! ffl

0

:'

0

g(S(S

e

(ffl 2 :' 2 ))) =

fffl

0

7! ffl

0

:'

0

g(S(ffl 1 :fffl 2 7! ffl 1 :;g(' 1 [ ' 2 ))) = ffl

0

:'

0

= S(ffl 2 :' 2 ) = S(ffl:'). ut
8.2 Unification of Types

We now extend the above results about unification to cover annotated types. Let B = (Q; \Phi) be
a consistent basis and let �� 1 and �� 2 be types satisfying B ` �� 1 and B ` �� 2 . A substitution S is a

unifier of �� 1 and �� 2 in B if S takes the form (fg; S

r

; S

e

), S(B) is consistent and S(�� 1 ) = S(�� 2 ).
Note that a unifier is not allowed to have type variables in its support (we do not attempt to do ML
type inference and region inference simultaneously.) A substitution S



is a most general unifier of

�� 1 and �� 2 in B, if S



is a unifier of �� 1 and �� 2 in B and for every unifier S of �� 1 and �� 2 in B there
exists a substitution S

0

such that:
1. S(ae) = S

0

(S



(ae)), for all ae 2 Q;

2. S(ffl:') = S

0

(S



(ffl:')), for all ffl:' 2 \Phi;
Notice that the condition in item (1) is "for all ae 2 Q", not just "for all ae 2 frv (�� 1 ; �� 2 )"; similarly,
note that the condition in item (2) is "for all ffl:' 2 \Phi", not just "for all ffl:' 2 arreff (�� 1 )[arreff (�� 2 )".
This stronger property of principal unifiers will be used several times in what follows. One can
prove that if S



is a most general unifier for �� 1 and �� 2 in B then Inv(S



) ` fv(�� 1 ; �� 2 ).
The algorithm below computes most general unifiers in consistent bases:
unifyRho(ae 1 ; ae 2 ) =
if ae 1 = ae 2 then Id
else (fg; fae 2 7! ae 1 g; fg)
unifyMu((�� 1 ; ae 1 ); (�� 2 ; ae 2 )) =
let

S 1 = unifyTy(�� 1 ; �� 2 )

S 2 = unifyRho(S 1 ae 1 ; S 1 ae 2 )
in

S 2 ffi S 1

end

unifyTy(�� 1 ; �� 2 ) = case (�� 1 ; �� 2 ) of
(int; int)) Id

j (ff; fi) ) if ff = fi then Id else FAIL

j (�� 1

ffl 1 :'1

\Gamma\Gamma\Gamma\Gamma! �� 2 ; ��

0

1

ffl

0

1 :'

0

1

\Gamma\Gamma\Gamma\Gamma! ��

0

2 ) )

let

S 1 = unifyMu(�� 1 ; ��

0

1 )

S 2 = unifyArrEff (S 1 (ffl 1 :' 1 ); S 1 (ffl

0

1 :'

0

1 ))

S 3 = unifyMu(S 2 (S 1 (�� 2 )); S 2 (S 1 (��

0

2 )))
in

S 3 ffi S 2 ffi S 1

end

j ( ; ) ) FAIL
Lemma 6 Let B be a consistent basis and assume B ` �� 1 and B ` �� 2 and ML(�� 1 ) = ML(�� 2 ).

Then S



= unifyTy(�� 1 ; �� 2 ) succeeds and
1. S



is a most general unifier of �� 1 and �� 2 in B;

2. S



is a contraction of B;

3. S



(B) = B implies S



= Id;

Similarly for types with places (��) and region variables.

Proof By induction on the structure of ML(�� 1 ). We show only the case �� 1 = �� 1

ffl 1 :'1

\Gamma\Gamma\Gamma\Gamma! �� 2 , in
which case ML(�� 1 ) = ML(�� 2 ) gives that �� 2 must take the form ��

0

1

ffl

0

1 :'

0

1

\Gamma\Gamma\Gamma\Gamma! ��

0

2 . We have B ` �� 1 ,

B ` ��

0

1 and ML(�� 1 ) = ML(��

0

1 ). Thus by induction

S 1 is a most general unifier for �� 1 and ��

0

1 in B (8)

S 1 is a contraction of B (9)

S 1 (B) = B implies S 1 = Id (10)
By (9) and Lemma 4 we have S 1 (B) ` S 1 (�� 1 ) and S 1 (B) ` S 1 (�� 2 ). Therefore, by Lemma 5,

S 2 = unifyArrEff (S 1 (ffl 1 :' 1 ); S 1 (ffl

0

1 :'

0

1 )) succeeds and

S 2 is a most general unifier for S 1 (ffl 1 :' 1 ) and S 1 (ffl

0

1 :'

0

1 ) in S 1 (B) (11)

S 2 is a contraction of S 1 (B) (12)

S 2 (S 1 (B)) = S 1 (B) implies S 2 = Id (13)
By Lemma 4 on (12) we get S 2 (S 1 (B)) ` S 2 (S 1 (�� 1 )) and S 2 (S 1 (B)) ` S 2 (S 1 (�� 2 )). Also, ML(S 2 (S 1 �� 2 )) =

ML(�� 2 ) = ML(��

0

2 ) = ML(S 2 (S 1 ��

0

2 )), since S 1 and S 2 are contractions. By induction, S 3 =

unifyMu(S 2 (S 1 (�� 2 )); S 2 (S 1 (��

0

2 ))) succeeds and

S 3 is a most general unifier for S 2 (S 1 (�� 2 )) and S 2 (S 1 (��

0

2 )) in S 2 (S 1 (B)) (14)

S 3 is a contraction of S 2 (S 1 (B)) (15)

S 3 (S 2 (S 1 (B))) = S 2 (S 1 (B)) implies S 3 = Id (16)
Thus unifyTy(�� 1 ; �� 2 ) succeeds with result S



= S 3 ffi S 2 ffi S 1 . From (8), (11) and (14) we get that

S



is a unifier for �� 1 and �� 2 in B. From (9), (12) and (15) we get that S



is a contraction of B.

From (9), (12) and (15) together with (10), (13) and (16) we get that S



(B) = B implies S



= Id.
It remains to prove that S



is a most general unifier for �� 1 and �� 2 in B. Let S be any unifier for �� 1

and �� 2 in B and let (Q; \Phi) = B. Now S is a unifier for �� 1 and ��

0

1 in B. Thus, by (8), there exists
an S

0

1 such that

8ae 2 Q:S(ae) = S

0

1 (S 1 (ae))  8ffl:' 2 \Phi:S(ffl:') = S

0

1 (S 1 (ffl:')) (17)
Thus, since S is a unifier for ffl 1 :' 1 and ffl

0

1 :'

0

1 , S

0

1 is a unifier for S 1 (ffl 1 :' 1 ) and S 1 (ffl

0

1 :'

0

1 ) in S 1 (B).
Thus, by (11), there exists a S

0

2 such that

8ae 2 S 1 (Q):S

0

1 (ae) = S

0

2 (S 2 (ae))  8ffl:' 2 S 1 (\Phi):S

0

1 (ffl:') = S

0

2 (S 2 (ffl:')) (18)
Since S is a unifier for �� 2 and ��

0

2 in B and (17) and (18) we have that S

0

2 is a unifier for S 2 (S 1 (�� 2 ))
and S 2 (S 1 (��

0

2 )) in S 2 (S 1 (B)). Thus, by (14), there exists an S

0

3 such that

8ae 2 S 2 (S 1 (Q)):S

0

2 (ae) = S

0

3 (S 3 (ae))  8ffl:' 2 S 2 (S 1 (\Phi)):S

0

2 (ffl:') = S

0

3 (S 3 (ffl:')) (19)
By (17), (18) and (19) we get the desired

8ae 2 Q:S(ae) = S

0

3 (S



(ae))  8ffl:' 2 \Phi:S(ffl:') = S

0

3 (S



(ffl:')) (20)

ut

It turns out that the premises of lemma 6 are always met in the region inference algorithm we use
(this is proved in [20]). Therefore, unification never fails. Informally, the fact that the premise

ML(�� 1 ) = ML(�� 2 ) is satisfied is not surprising, for
1. region inference takes place after type inference; and
2. roughly, region inference simply re-typechecks the program using annotated versions of the
types that were determined by type inference, so if two region-annotated types are unified,
they will have the same underlying ML type.

Example 7.1 The two types

�� 1 = (int; ae 1 )

ffl 2 :fae 1 ;ae 3 ;ae 4 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(int; ae 4 )
and

�� 2 = (int; ae 5 )

ffl 6 :fae 5 ;ae 7 ;ae 8 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(int; ae 8 )
are consistent in the basis B = (fae 1 ; ae 3 ; ae 4 ; ae 5 ; ae 7 ; ae 8 g; fffl 2 :fae 1 ; ae 3 ; ae 4 g; ffl 6 :fae 5 ; ae 7 ; ae 8 gg. The result
of unifyTy(�� 1 ; �� 2 ) is the substitution S = (S

t

; S

r

; S

e

), where S

t

= Id, S

r

= fae 5 7! ae 1 ; ae 8 7! ae 4 g

and S

e

= fffl 6 7! ffl 2 :fae 1 ; ae 3 ; ae 4 ; ae 7 g; ffl 2 7! ffl 2 :fae 1 ; ae 3 ; ae 4 ; ae 7 gg. By Lemma 6, S is a contraction of B

and S is a most general unifier for �� 1 and �� 2 in B. ut
In Example 7.1, notice that S does not map ae 3 and ae 7 to the same region variable: region
and effect variables which occur in effects only in the types that are unified (i.e., they do not
occur paired with a type constructor or as the handle of an arrow effect) are not affected by the
unification algorithm. This distinction between different occurrences is important, also for the
termination of region inference, so we define it formally. For basic semantic objects o, we define
sets pfrv (o) and pfev (o) as follows:

pfev (int)=; pfrv (int)=;

pfev (ff)=; pfrv (ff)=;

pfev (��

ffl:'

\Gamma\Gamma\Gamma! ��

0

)=pfev (��) [ pfev (��

0

) [ ffflg pfrv (��

ffl:'

\Gamma\Gamma\Gamma! ��

0

)=pfrv (��) [ pfrv (��

0

)

pfev (��; ae)=pfev (��) pfrv (��; ae)=pfrv (��) [ faeg

The set pfev (o) is called the set of primary (free) effect variables of o; the set pfrv (o) is called
the set of primary (free) region variables of o. We say that an effect variable ffl is a secondary effect
variable in �� if ffl 2 fev(��) n pfev (�� ); similarly, we say that a region variable ae is secondary in �� if

ae 2 frv (��) n pfrv (�� ).
Given types �� 1 and �� 2 with ML(�� 1 ) = ML(�� 2 ), unifyTy(�� 1 ; �� 2 ) returns a substitution which has
only region and effect variables which are primary in �� 1 or �� 2 in its support. (In Example 7.1, ae 7

and ae 3 are secondary variables; all the other variables are primary.) This is as one would expect.
For in order to obtain good separation of lifetimes, unification should only identify two region
variables when they must denote the same region. Secondary occurrences of region variables
do not force identification of regions. For example, amongst the less general unifiers for the
two arrow effects ffl:fae 1 ; ae 2 g and ffl

0

:fae 3 ; ae 4 g we have S = (fffl 7! ffl

0

:;g; fae 1 7! ae 3 ; ae 2 7! ae 4 g) and

S

0

= (fffl 7! ffl

0

:;g; fae 1 7! ae 4 ; ae 2 7! ae 3 g). These unifiers lead to smaller effects than the most general
unifier, but they also lead to unnecessary identifications of regions and are therefore undesirable.
9 Type Schemes

Type schemes resemble the type schemes of Damas and Milner[3] but with additional quantification
over region variables and effect variables:

oe ::= 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� (n  0, k  0 and m  0)
Here �� is the body of oe, written body(oe). The bound variables of oe, written bv(oe) is the set

fff 1 ; : : : ; ff n g [ fae 1 ; : : : ; ae k g [ fffl 1 ; : : : ; ffl mg; we define the set of bound type variables of oe, written

btv(oe), to be the set fff 1 ; : : : ; ff n g. The free variables of oe, written fv(oe), is the set fv (��) n bv(oe).

The bound variables of a type scheme must be distinct. The arity of oe is the triple (n; k; m).

The erase function, ML, of Section 5 is extended to type schemes by

ML(8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� ) = 8ff 1 \Delta \Delta \Delta ff n : ML(��)

We sometimes regard a type �� as the trivial type scheme 8:�� . Type schemes that arise from
each other by renaming of bound variables are considered equal.

A type ��

0

is an instance of oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� , written oe  ��

0

, if there exists a
substitution S such that Supp(S) ` bv (oe) and S(��) = ��

0

. When we want to make a particular S

explicit, we say that ��

0

is an instance of oe via S, written oe  ��

0

via S. Furthermore, we say that
a type scheme oe

0

= 8ff

0

1 \Delta \Delta \Delta ff

0

n

0 ae

0

1 \Delta \Delta \Delta ae

0

k

0 ffl

0

1 \Delta \Delta \Delta ffl

0

m

0 :��

0

is an instance of oe (via S), written oe  oe

0

(via

S), if oe  ��

0

and bv(oe

0

) " fv(oe) = ;. As in Milner's type system one has:

Lemma 7 Let oe and oe

0

be type schemes. Then oe  oe

0

iff for every �� , oe

0

 �� implies oe  �� .

Proof Assume that for every �� , oe

0

 �� implies oe  �� . By renaming the bound variables of

oe

0

, if necessary, achieve that bv(oe

0

) " fv(oe) = ;. Then oe

0

 body(oe

0

) and thus, by assumption,

oe  body(oe

0

), showing oe  oe

0

. Conversely, assume oe  oe

0

via S. Without loss of generality, we
can assume that S is finite and that Dom(S) = bv(oe). Assume oe

0

 �� via S

0

. We then have

oe  �� via S

0

ffl S. To prove this, it suffices to prove
(S

0

ffi S)�� 0 = (S

0

ffl S)�� 0 (21)
where �� 0 = body(oe), for by assumption we have (S

0

ffi S)�� 0 = �� . We prove (21) by induction on the
structure of �� 0 . We show only the case ffl:' 2 arreff (�� 0 ). Note that (S

0

ffl S)(') = (S

0

ffi S)('), since

bv(oe

0

) " fv(oe) = ;. Now there are two cases. First, assume ffl 2 Dom(S). Let ffl

0

:'

0

= S(ffl) and let

ffl

00

:'

00

= S

0

(ffl

0

). Thus (S

0

ffl S)(ffl:') = ffl

00

:('

00

[S

0

('

0

) [ (S

0

ffl S)(')) = ffl

00

:('

00

[S

0

('

0

) [ (S

0

ffi S)(')) =
(S

0

ffi S)(ffl:'), as desired. Second, assume ffl = 2 Dom(S). Then (S

0

ffl S)(ffl:') = ffl:((S

0

ffl S)(')) =

ffl:((S

0

ffi S)(')) = (S

0

ffi S)(ffl:'), since ffl 2 fv (oe) and bv(oe

0

) " fv (oe) = ;. ut

As a consequence,  is a transitive relation on type schemes. We say that oe and oe

0

are

equivalent, written oe j oe

0

, if oe  oe

0

and oe

0

 oe. This relation is larger than just renaming of
bound variables. For example, letting �� 0 = (int; ae 0 ) we have

8fflae:�� 0

ffl:faeg

\Gamma\Gamma\Gamma\Gamma! �� 0 j 8fflaeae

0

:�� 0

ffl:fae;ae

0

g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma! �� 0 (22)
Thus  induces a partial order on equivalence classes of type schemes. This partial order is
non-well-founded (just like the corresponding partial order on ML type schemes).
There are certain type schemes we want to reject as ill-formed, because they are in fundamental
conflict with the idea of basing region inference on unification of consistent types.

Definition 8 A type scheme oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� is said to be well-formed if, for
every arrow effect ffl:' occurring on a function arrow in �� if ffl = 2 bv(oe) then fv(') " bv(oe) = ;.

Otherwise, oe is said to be ill-formed.
In other words, well-formedness requires that if the handle of an arrow effect in �� is free then the
entire arrow effect is free.
We shall later impose a restriction which bans ill-formed type schemes. That this is to be
expected is illustrated by the following example.

Example 8.1 Consider the type scheme oe = 8ae:(int; ae)

ffl:faeg

\Gamma\Gamma\Gamma\Gamma!(int; ae) which is ill-formed. The
problem with oe is that if it is instantiated twice, via different substitutions, say S 1 = fae 7! ae 1 g and

S 2 = fae 7! ae 2 g, then the two resulting types (int; ae 1 )

ffl:fae 1 g

\Gamma\Gamma\Gamma\Gamma\Gamma!(int; ae 1 ) and (int; ae 2 )

ffl:fae 2 g

\Gamma\Gamma\Gamma\Gamma\Gamma!(int; ae 2 )
are not consistent in any basis: ffl cannot both "denote" the set fae 1 g and the set fae 2 g. If, however,

ffl had been quantified as well, the type schemes would have been well-formed and one could pick
fresh effect variables each time the type scheme were instantiated. ut

10 Polymorphic Recursion

In practice, much of the ability of the region inference to reclaim memory comes from rule (5).
The crucial point is that within e 1 , the type environment associates f with the region type scheme
 oe, so that free occurrences of f in e 1 potentially can be given types different from �� 0 . We refer
to this feature as region-polymorphic recursion. (An example of region-polymorphic recursion at
work was presented in Section 2.)
Notice that rule (5) does not allow polymorphic recursion in types: the type scheme for f in e 1

is only  oe, not oe. Thus the region rules are faithful to the treatment of recursive functions in ML
as far as type polymorphism is concerned[10]. The reason for this limitation is that type inference
for (type-) polymorphic recursion is equivalent to semi-unification[5, 8], which is undecidable[7].
However, it can be proved that every well-typed source expression can be region-annotated
in accordance with the region inference rules[24]. Moreover, in the absence of region-polymorphic
recursion, Milner's notion of principal type schemes extends to region inference[22]. In the presence
of polymorphic recursion, however, it is not known whether (in some sense) it is possible to infer
a principal region type scheme for every ML-typable expression. There seems to be a tension
between, on the one hand, the desire for obtaining region type schemes that are as general as
possible and on the other hand the desire to know that region inference always terminates.
We have chosen to resolve this (alleged) tension in the favour of termination: the algorithm
described in [20] always finds a region annotation which is legal according to the region inference
rules, although in doing so, it may fail to give every recursive function in the program a region
type scheme which is the most general one permitted by the region inference rules.
The algorithm in [20] handles polymorphic recursion using a two-phase approach. The first
phase, called spreading, generates a (possibly large) basis by choosing fresh region and effect
variables wherever a region or effect annotation is required in the target program. The second
phase, called fixed point resolution, collapses region variables (and effect variables) by unifying
region-annotated types. Unification of region-annotated types produces contractions of the basis
(see Section 8), and a cornerstone of the termination proof is that no finite basis can be contracted
indefinitely (Lemma 3). Thus a crucial idea in the algorithm is to separate the generation of fresh
variables from the region inference proper. The same idea is used for ensuring termination in our
constraint-based approach mentioned in Section 3.
But is it possible to know how many region and effect variables one needs for doing region inference
for a given program without actually doing the region inference? This is where the distinction
between secondary and primary region (and effect) variables in types becomes important. Given
an ML type ��

ML

, let us consider the set of region annotated types �� for which ML(��) = ��

ML

. For
every such �� , the number of region and effect variables that appear in primary positions in �� is
bounded by the size of �� : one at most needs one effect variable for each function arrow in ��

ML

and
one region variable for each occurrence of a type constructor or a type variable in ��

ML

. However,
it is not clear how many secondary region and effect variables one might wish to have on function
arrows that appear in ��

ML

. But in that case, how many bound region and effect variables does it
take at most to make a region-annotated type scheme  oe of the form found in rule (5)? Since there
is no obvious bound on the number of secondary region and effect variables in �� 0 , and since there
is in general nothing that prevents secondary region and effect variables from being universally
quantified in  oe, there is no obvious bound on how many bound region and effect variables one will
need for  oe.

Why does one need a bound on the arity of  oe? Because each free occurrence of f within e 1

and e 2 potentially gives rise to generation of k fresh region variables and m fresh effect variables,
where ( ; k; m) is the arity of  oe. Without a bound on k and m, how can we generate all the fresh
region and effect variables we need in the initial phase?
To avoid an ever-expanding number of quantified secondary region and effect variables in regionannotated
type schemes, our algorithm never produces type schemes which have quantified region
or effect variables which occur in secondary positions of the body of the type scheme only (see
Section 12). Formally, we define:

Definition 9 A type scheme oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� is said to have structural quantification
 if fae 1 ; : : : ; ae k g ` pfrv (��), fffl 1 ; : : : ; ffl m g ` pfev (��) and fff 1 ; : : : ; ff n g ` ftv(��).

The operation by which we form type schemes (see Section 12.2) only produces type schemes
which have structural quantification.

Example 9.1 The following expression has a type which contains a secondary region variable:

z : (ff; ae 0 ):let x = 1 at ae 1

in (y : (int; ae 2 ):(x + y) at ae 3 ) at ae 4 :

(ff; ae 0 )

ffl 1 :fae 1 ;ae 4 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!((int; ae 2 )

ffl 2 :fae 1 ;ae 2 ;ae 3 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(int; ae 3 ); ae 4 )

--- --z 

��0

Here ae 1 is a secondary region variable in �� 0 ; it represents the region of a temporary value which
is not necessarily in the same region as the argument or result of either of the two functions but
which is captured in the function value (closure) of the function y \Delta \Delta \Delta. If the above function is
used in a declaration of a region-polymorphic function

letrec f(z) = let x = 1 \Delta \Delta \Delta

then one might want to give f the type scheme oe = 8ae 0 ae 1 ae 2 ae 3 ae 4 ffl 1 ffl 1 :�� 0 but this type scheme has
non-structural quantification. Instead, the RegEffClos algorithm (Section 12.2) will construct the
less general type scheme oe = 8ae 0 ae 2 ae 3 ae 4 ffl 1 ffl 1 :�� 0 . ut

We are now ready to extend the definition of consistency to cover type schemes. Let oe =

8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� be a type scheme with structural quantification. The bound basis of

oe, written bound(oe), is the basis (fae 1 ; : : : ; ae k g; fffl:' 2 arreff (��) j ffl 2 bv(oe)g).

Definition 10 Type scheme oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� is consistent in basis B, written

B ` oe, if B is consistent, oe has structural quantification and, letting B

0

= bound(oe), the basis

B ] B

0

exists and is consistent and B ] B

0

` �� .

Notice that if B ` oe and oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� then, since oe has structural quantification,
we have Dom( c \Phi oe ) = fffl 1 ; : : : ; ffl mg, where \Phi oe = \Phi of bound(oe).

Lemma 11 If B ` oe then oe is well-formed.
Proof Assume B ` oe, where oe = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� . Let B

0

= (Q

0

; \Phi

0

) = bound(oe). By

B ` oe we have that the basis B ]B

0

exists, is consistent and B ]B

0

` �� . Take ffl:' 2 arreff (��) and
assume ffl = 2 fffl 1 ; : : : ; ffl m g. Now B ] B

0

` �� implies ffl:' 2 \Phi of (B ] B

0

). Since B ] B

0

is consistent
and ffl = 2 bv(oe) we have ffl:' 2 B. But then, since B itself is consistent we have fv(ffl:') ` fv(B) and
thus fv (ffl:') " (Q

0

; Dom(  \Phi

0

)) = ;. ut

The definition of consistency does not depend on any particular choice of bound variables in oe,

except that the bound variables must be chosen disjoint from B.

We emphasise that consistency of type schemes is introduced for algorithmic reasons only.
Soundness of the region inference rules has been proved without assuming consistency[23, 24].
Also, we have not found the restriction to consistent type schemes (and the loss in polymorphism
it entails) to be serious in practice.

Definition 12 A type environment TE is consistent in B = (Q; \Phi), written B ` TE, if for all

x 2 Dom(TE), letting (oe; ae) = TE(x), one has B ` oe and ae 2 Q.

This definition is used in the inference rules in Section 4.

11 Instantiation of Type Schemes

An instantiation list is a triple of the form
([�� 1 ; : : : ; �� n ]; [ae 1 ; : : : ; ae k ]; [ffl 1 :' 1 ; : : : ; ffl m :' m ]) n  0; k  0; m  0
The triple (n; k; m) is called the arity of the instantiation list. We use il to range over instantiation
lists. Instantiation lists annotate program variables, see rules (1) and (2). We say that il is

consistent in basis B, written B ` il , if B ` �� i , for all i = 1::n, B ` ae i , for all i = 1::k, and

B ` ffl i :' i , for all i = 1::m.
Let oe be a type scheme 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� and let

il = ([�� 1 ; : : : ; �� n ]; [ae

0

1 ; : : : ; ae

0

k ]; [ffl

0

1 :'

0

1 ; : : : ; ffl

0

m :'

0

m ])
be an instantiation list with the same arity as oe. Let S = (fff 1 7! �� 1 ; : : : ; ff n 7! �� n g; fae 1 7!

ae

0

1 ; : : : ; ae k 7! ae

0

k g; fffl 1 7! ffl

0

1 :'

0

1 ; : : : ; ffl m 7! ffl

0

m :'

0

m g). Then we refer to the type ��

0

= S(��) as the

instance of oe given by il ; we write oe  ��

0

via il to mean that ��

0

is the instance of oe given by il .
Consider the situation where B is a basis, oe a type scheme, il an instantiation list of the same
arity as oe and assume B ` oe and B ` il . Surprisingly, perhaps, it is not necessarily the case that
the instance of oe via il is consistent in B. The reason is that the instantiation may produce arrow
effects which are strictly larger than the arrow effects found in B.
Example 10.1 Consider B = (fae 0 g; fffl 0 :;g), oe = 8fflae:(int; ae 0 )

ffl:faeg

\Gamma\Gamma\Gamma\Gamma!(int; ae) and S = (fae 7!

ae 0 g; fffl 7! ffl 0 :;g). The instance of oe via S is the type ��

0

= (int; ae 0 )

ffl 0 :fae 0 g

\Gamma\Gamma\Gamma\Gamma\Gamma\Gamma!(int; ae 0 ), which is not
consistent in B, since the arrow effect ffl 0 :; has "grown" to become ffl 0 :fae 0 g.Another way to explain
this "growth" is as follows. Since ffl and ae are quantified in oe, the arrow effect ffl:faeg can be thought
of a quantified constraint: 8ffl; ae:

\Gamma

ffl ' faeg ) (int; ae 0 )

ffl

\Gamma!(int; ae)

\Delta

. Thus instantiating ffl and ae to

ffl 0 and ae 0 , respectively, results in the constraint ffl 0 ' fae 0 g. We represent this "growth" of the set
which ffl 0 denotes by application of the contraction fffl 0 7! ffl 0 :fae 0 gg to B. ut
In general, the operation of instantiating oe using il in B returns not just a type, ��

0

, but also a
contraction, which can be applied to B to obtain a basis in which ��

0

is consistent.
The instantiation algorithm is defined by the mutually recursive function declarations shown
below. All the functions return an effect substitution, which is a contraction of the basis; the main
function is inst(oe; il ) which returns both an effect substitution and a type, the latter being the
instance of oe via il .
instArrEff (S

e

; ffl:') =
if ffl = 2 Dom(S

e

) then Id

e

else let ffl 1 :' 1 = S

e

(ffl)
in if S

e

(') ` ' 1 then Id

e

else fffl 1 7! ffl 1 :(' 1 [ S

e

('))g
end

instTy(S

e

; ��) = case �� of

ff ) Id

e

j int ) Id

e

j �� 1

ffl:'

\Gamma\Gamma\Gamma! �� 2 )

let S

e

1 = instMu(S

e

; �� 1 )

S

e

2 = instMu(S

e

1 ffl S

e

; S

e

1 (�� 2 ))

S

e

3 = instArrEff (S

e

2 ffl (S

e

1 ffl S

e

);
(S

e

2 ffi S

e

1 )(ffl:'))
in S

e

3 ffi S

e

2 ffi S

e

1 end

instMu(S

e

; (��; ae)) = instTy(S

e

; ��)

inst(oe; il ) =
let 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :�� = oe

([�� 1 ; \Delta \Delta \Delta ; �� n ]; [ae

0

1 ; \Delta \Delta \Delta ; ae

0

k ]; [ffl

0

1 :'

0

1 ; \Delta \Delta \Delta ; ffl

0

m :'

0

m ]) = il

(FAIL if oe and il have different arity)

S = (S

t

; S

r

; S

e

), where

S

t

= fff 1 7! �� 1 ; : : : ; ff n 7! �� n g

S

r

= fae 1 7! ae

0

1 ; : : : ; ae k 7! ae

0

k g

S

e

= fffl 1 7! ffl

0

1 :'

0

1 ; : : : ; ffl m 7! ffl

0

m :'

0

m g

S

e

1 = instTy(S

e

; S

r

(S

t

(��)))
in (S

e

1 ; S

e

1 (S

e

(S

r

(S

t

��)))) end

Lemma 13 Let S

e

be a finite effect substitution. Assume ` B, B ] B

0

exists, B ] B

0

` �� ,

B ` Rng(S

e

) and Dom(S

e

) = Dom( c \Phi

0

), where \Phi

0

= \Phi of B

0

. Then S

e

1 = instTy(S

e

; ��) succeeds
and
1. S

e

1 is a contraction of B;

2. S

e

1 (B) ` (S

e

1 ffl S

e

)(S

e

1 (��));

3. S

e

1 (B) = B implies S

e

1 = Id

e

.
Similarly with instMu and �� for instTy and �� , and with instArrEff and ffl:' for instTy and �� .

Proof Write B in the form (Q; \Phi) and write B

0

in the form (Q

0

; \Phi

0

). We first prove the result for

instArrEff and ffl:' in place of instTy and �� . As in the definition of instArrEff , make the following
case analysis.
ffl = 2 Dom(S

e

) Here S

e

1 = Id

e

, which is a contraction of B. Moreover, since B ] B

0

exists
and B ] B

0

` ffl:' and ffl = 2 Dom(S

e

) and Dom(S

e

) = Dom(  \Phi

0

) we have B ` ffl:'. Thus (S

e

1 ffl

S

e

)(S

e

1 (ffl:')) = S

e

(ffl:') = ffl:'. (In short, if the instantiation substitution S

e

does not have ffl in its
domain then it has no variable in ' in its domain.) Thus (2) and (3) hold.
ffl 2 Dom(S

e

)  S

e

(') ` ' 1 Here S

e

1 = Id

e

, which is a contraction of B. Moreover, (S

e

1 ffl

S

e

)(S

e

1 (ffl:')) = S

e

(ffl:') = ffl 1 :(' 1 [ S

e

(')) = ffl 1 :' 1 . Since ffl 1 :' 1 2 Rng(S

e

) and B ` Rng(S

e

)
we thus have (2) as desired. Also (3) holds.
ffl 2 Dom(S

e

)  S

e

(') 6` ' 1 Here S

e

1 = fffl 1 7! ffl 1 :(' 1 [ S

e

('))g. Since B ` ffl:' and B ` Rng(S

e

)
we have B ` S

e

('). Thus S

e

1 is a contraction of B and since S

e

(') 6` ' 1 we have S

e

1 (B) ! B.

Thus (3) holds trivially. As for (2), we have
(S

e

1 ffl S

e

)(S

e

1 (ffl:'))
= S

e

1 (S

e

(ffl:')) since Inv(S

e

1 ) " Dom(S

e

) = ;

= S

e

1 (ffl 1 :(' 1 [ S

e

(')))
= ffl 1 :(' 1 [ S

e

(')) by the definition of S

e

1
Now ffl 1 :' 1 2 \Phi so S

e

1 (ffl 1 :' 1 ) 2 S

e

1 (\Phi). Moreover, S

e

1 (ffl 1 :' 1 ) = ffl 1 :(' 1 [ S

e

(') [ S

e

1 (' 1 )) = ffl 1 :(' 1 [

S

e

(')). Thus S

e

1 B ` (S

e

1 ffl S

e

)(S

e

1 (ffl:')) as required.
We now proceed to the cases for instTy and instMu , which are done simultaneously, by structural
induction on �� and ��. The only interesting case is the following:

�� j �� 1

ffl:'

\Gamma\Gamma\Gamma! �� 2 Since B ]B

0

` �� we have B ]B

0

` �� 1 , B ]B

0

` �� 2 and B ]B

0

` ffl:'. Following
the definition of instTy(S

e

; ��) we have by induction that S

e

1 = instMu(S

e

; �� 1 ) succeeds and

S

e

1 is a contraction on B (23)

S

e

1 (B) ` (S

e

1 ffl S

e

)(S

e

1 �� 1 ) (24)

S

e

1 (B) = B implies S

e

1 = Id

e

(25)
By Lemma 4 on (23) and B ] B

0

` �� 2 we get S

e

1 (B ] B

0

) ` S

e

1 (�� 2 ). Moreover, S

e

1 (B) ] S

e

1 (B

0

)
exists and is equal to S

e

1 (B ] B

0

). Moreover, Dom(S

e

1 ffl S

e

) = Dom(S

e

) = Dom( c \Phi

0

1 ) and S

e

1 (B) `

Rng(S

e

1 fflS

e

), where \Phi

0

1 = \Phiof S

e

1 (B

0

). Thus by induction we have that S

e

2 = instMu(S

e

1 fflS

e

; S

e

1 (�� 2 ))
succeeds and that

S

e

2 is a contraction on S

e

1 (B) (26)

S

e

21 (B) ` (S

e

21 ffl S

e

)(S

e

21 �� 2 ) (27)

S

e

21 (B) = S

e

1 (B) implies S

e

2 = Id

e

(28)
where S

e

21 is defined to be S

e

2 ffi S

e

1 . (Here we use the general fact that for all substitutions S 1 ,

S 2 and S 3 , if S 1 is finite then S 3 ffl (S 2 ffl S 1 ) = (S 3 ffi S 2 ) ffl S 1 .) By (26) and (23) we get that

S

e

21 (B) is consistent and that S

e

21 (B) ] S

e

21 (B

0

) exists and equals S

e

21 (B ] B

0

). By Lemma 4 on

B ] B

0

` ffl:' and B ` Rng(S

e

) we have S

e

21 (B) ] S

e

21 (B

0

) ` S

e

21 (ffl:') and S

e

21 (B) ` Rng(S

e

21 ffl S

e

).
Also Dom(S

e

21 ffl S

e

) = Dom(S

e

) = Dom( c \Phi

0

2 ), where \Phi

0

2 = \Phi of S

e

21 (B

0

). Thus by the first part of
the lemma we have that S

e

3 = instArrEff (S

e

21 ffl S

e

; S

e

21 (ffl:')) succeeds and that

S

e

3 is a contraction of S

e

21 (B) (29)

S

e

321 (B) ` (S

e

321 ffl S

e

)(S

e

321 (ffl:')) (30)

S

e

321 (B) = S

e

21 (B) implies S

e

3 = Id

e

(31)
where S

e

321 = S

e

3 ffi S

e

21 . Thus instTy(S

e

; ��) succeeds with result S

e

321 . By (23), (26) and (29) we
get that S 321 is a contraction of B, as required. Next, from (24) we get S

e

321 (B) ` (S

e

3 ffi S

e

2 )((S

e

1 ffl

S

e

)(S

e

1 �� 1 )), i.e., since Inv(S

e

321 ) " Dom(S

e

) = ;,

S

e

321 (B) ` (S

e

321 ffl S

e

)(S

e

321 (�� 1 )) (32)
Similarly, from (27) we get

S

e

321 (B) ` (S

e

321 ffl S

e

)(S

e

321 (�� 2 )) (33)
By (30), (32) and (33) we get the desired S

e

321 (B) ` (S

e

321 ffl S

e

)(S

e

321 (�� )). Finally, assume S

e

321 (B) =

B. Then S

e

321 (B) = S

e

21 (B) = S

e

1 (B) = B, so S

e

321 = Id

e

, by (25), (28) and (31). ut

Theorem 14 Assume B ` oe and B ` il (by which we mean that B ` e for each list element e of
il ). Also assume that oe and il have the same arity. Then (S

e

1 ; ��

0

) = inst(oe; il ) succeeds and
1. S

e

1 is a contraction of B;

2. S

e

1 (oe)  ��

0

via S

e

1 (il ) and S

e

1 (B) ` ��

0

;
3. S

e

1 (B) = B implies S

e

1 = Id

e

;

Proof Let B

0

= (Q

0

; \Phi

0

) = bound(oe) and let �� be as in the definition of inst . Since B ` oe we have

` B and B ] B

0

` �� . Since B ` il we have that B ] (;; S

r

(\Phi

0

)) exists and that B ] (;; S

r

(\Phi

0

)) `

S

r

(S

t

�� ), using the declarations in the definition of inst . Also, Dom(S

e

) = Dom( d S

r

(\Phi

0

)) and

B ] (;; S

r

(\Phi

0

)) ` Rng(S

e

). Thus by Lemma 13 we have that S

e

1 = inst(S

e

; S

r

(S

t

(��))) succeeds
and that

S

e

1 is a contraction of B (34)

S

e

1 (B) ` (S

e

1 ffl S

e

)(S

e

1 (S

r

(S

t

(��)))) (35)

S

e

1 (B) = B implies S

e

1 = Id

e

(36)
Thus inst(oe; il ) succeeds with result (S

e

1 ; ��

0

) = (S

e

1 ; S

e

1 (S

e

(S

r

(S

t

(��))))). Moreover, (34) and (36)
are two of the desired results. Also, by (34) and the fact that B ] B

0

exists, we have Inv(S

e

1 ) "

Dom(S

e

) = ;. Thus (S

e

1 fflS

e

)(S

e

1 (S

r

(S

t

(��)))) = S

e

1 (S

e

(S

r

(S

t

(��)))) = (S

e

1 fflS

t

; S

e

1 fflS

r

; S

e

1 fflS

e

)(S

e

1 �� ).
Furthermore, by (34) we have that S

e

(oe) = 8ff 1 \Delta \Delta \Delta ff n ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :S

e

(�� ), without any renaming
of bound variables being necessary. Thus S

e

1 (oe)  ��

0

via S

e

1 (il ) and S

e

1 (B) ` ��

0

follow
from (35). ut
12 Generalisation of Region and Effect Variables

In this section, we describe how to form type schemes from types. In order to ensure that the
produced type schemes are consistent, an operation called Below is used.

12.1 The Below Operation

Let B = (Q; \Phi) be a consistent basis and let B 0 = (Q 0 ; \Phi 0 ) be a basis with B 0 ` B --- by which we
mean Q 0 ` Q and \Phi 0 ` \Phi. Clearly, \Phi 0 is functional and transitive, but it need not be closed. Also,
we do not necessarily have Q 0 ' frv (\Phi 0 ). Thus B 0 is not necessarily consistent. However, there
is a smallest basis (with respect to `), denoted Below (B; B 0 ), which is consistent and satisfies

B ' Below (B; B 0 ) ' B 0 . It is defined thus: let \Phi 1 be the smallest closed subset of \Phi satisfying
\Phi 1 ' \Phi 0 . (This exists since B is consistent and B 0 ` B.) Further, let Q 1 be Q 0 [ frv (\Phi 1 ). Then

Below (B; B 0 ) is defined to be (Q 1 ; \Phi 1 ).
12.2 The RegEffClos operation

Damas and Milner[3] define a closure operation, let us write it Clos

TE

(�� ), which forms a type
scheme from a type �� and a type environment TE. We now define the corresponding operation for
forming region-annotated type schemes. Let �� be a type and let ' 1 be an effect. Further, let B 0

and B be bases with B ' B 0 and B ` �� . (The basis B 0 contains region and effect variables that
must not be quantified, for example because they occur free in the type environment.)
1 RegEffClos(B; B 0 ; ')(��) =
2 let
3 (Q; \Phi) = B and (Q 0 ; \Phi 0 ) = B 0

4 Q

0

0 = Q 0 [ frv(') [ frv(��) n pfrv (��)
5 \Phi

0

0 = \Phi 0 [ fffl:'

0

2 \Phi j ffl 2 (' [ (fev (��) n pfev (��)))g
6 B 1 as (Q 1 ; \Phi 1 ) = Below (B; (Q

0

0 ; \Phi

0

0 ))
7 fffl 1 :' 1 ; : : : ; ffl m :' m g = \Phi n \Phi 1

8 fae 1 ; : : : ; ae k g = Q n Q 1

9 oe = 8ae 1 \Delta \Delta \Delta ae k ffl 1 \Delta \Delta \Delta ffl m :��

10 in
11 (B 1 ; oe)

12 end
Here Q

0

0 and \Phi

0

0 contain the region and effect variables that must not be generalised. In addition
to the variables in B 0 , Q

0

0 and \Phi

0

0 include all region and effect variables in ' and secondary region
and effect variables in �� (see lines 4 and 5). In lines 7 and 8 we determine the set of region and
effect variables that are generalised. The generalisation takes place in line 9.
For every type �� and basis B with B ` �� , we write Below (B; (B 0 ; ��)) as a shorthand for

Below (B; (B 0 [ (frv (��); arreff (��)))).

Lemma 15 Let B ` �� , B ` ', let B 0 be a basis and assume B 0 ` B and B = Below (B; (B 0 ; ��)).

Then (B 1 ; oe) = RegEffClos(B; B 0 ; ')(��) succeeds and B 1 ` oe and B 1 ` ' and B ' B 1 ' B 0 .

Proof The call (B 1 ; oe) = RegEffClos(B; B 0 ; ')(��) clearly succeeds and B ' B 1 ' B 0 follows
from the definition of Below . From B = Below (B; (B 0 ; ��)) and the definition of Q

0

0 and \Phi

0

0 we get

fae 1 ; : : : ; ae k g ` pfrv (��) and fffl 1 ; : : : ; ffl mg ` pfev (�� ). Let B

0

= (QnQ 1 ; \Phi n \Phi 1 ). Then B

0

= bound(oe).

Also, B 1 ] B

0

exists and is equal to B, which is consistent. Also B ` �� . Thus we have B 1 ` oe,

according to Definition 10. Also, B 1 ` ' holds by the definition of Q

0

0 and \Phi

0

0 . ut

An example of the use of RegEffClos was provided in Example 10.1.
13 Conclusion

A comparison between the type inference rules of Milner's polymorphic type discipline[3] and the
region inference rules in Section 4 leads to the conclusion that upon something simple, something
complicated will inevitably be erected. In our experience, however, Milner's type discipline carries

even fairly heavy load well and we think that it is fascinating that it can be used for reasoning not
just about the soundness of programs but also for reasoning about memory management.
References

[1] A. Aiken, M. Fahndrich, and R. Levien. Better static memory management: Improving regionbased
analysis of higher-order languages. In Proc. of the ACM SIGPLAN '95 Conference on
Programming Languages and Implementation (PLDI), pages 174--185, La Jolla, CA, June
1995. ACM Press.
[2] L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to von Neumann machines
via region representation inference. In Proceedings of the 23rd ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, pages 171--183. ACM Press, January
1996. (accepted).
[3] L. Damas and R. Milner. Principal type schemes for functional programs. In Proc. 9th Annual
ACM Symp. on Principles of Programming Languages, pages 207--212, Jan. 1982.
[4] Y. Fuh and P. Mishra. Type inference with subtypes. Theoretical Computer Science (TCS),

73:155--175, 1990.
[5] F. Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming
Languages and Systems, 15(2):253, April 1993.
[6] R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math.
Soc., 146:29--60, Dec. 1969.
[7] A. Kfoury, J. Tiuryn, and P. Urzyczyn. The undecidability of the semi-unification problem.

Information and Computation, pages 83--101, 1993.
[8] A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type reconstruction in the presence of polymorphic
recursion. ACM Transactions on Programming Languages and Systems, 15(2):290--311, April
1993.
[9] X. Leroy. Typage polymorphe d'un langage algorithmique. PhD thesis, University Paris VII,
1992. English version: Polymorphic Typing of an Algorithmic Language, INRIA Research
Report no. 1778, October 1992.
[10] R. Milner. A theory of type polymorphism in programming. J. Computer and System Sciences,

17:348--375, 1978.
[11] R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised).

MIT Press, 1997.
[12] J. Mitchell. Coercion and type inference. In Proc. 11th ACM Symp. on Principles of Programming
Languages (POPL), 1984.
[13] F. Nielson, H. R. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: the algorithm.
Technical Report LOMAPS-DAIMI-16, Department of Computer Science, University
of Aarhus (DAIMI), April 1996.
[14] H. R. Nielson and F. Nielson. Higher-order concurrent programs with finite communication
topology. In Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 84--97. ACM Press, January 1994.
[15] Peter Naur (ed.). Revised report on the algorithmic language Algol 60. Comm. ACM, 1:1--17,
1963.

[16] D. R'emy. Typechecking records and variants in a natural extension of ML. In Proc. 16th
Annual ACM Symp. on Principles of Programming Languages, pages 77--88. ACM, Jan. 1989.
[17] J. Robinson. A machine-oriented logic based on the resolution principle. J. Assoc. Comput.
Mach., 12(1):23--41, 1965.
[18] J.-P. Talpin and P. Jouvelot. Polymorphic type, region and effect inference. Journal of
Functional Programming, 2(3), 1992.
[19] J.-P. Talpin and P. Jouvelot. The type and effect discipline. In Proceedings of the seventh
IEEE Conference on Logic in Computer Science, pages 162--173, June 1992. Also, (extended
version) technical report EMP/CRI/A-206, Ecole des Mines de Paris, April 1992.
[20] M. Tofte and L. Birkedal. A region inference algorithm. (Submitted for publication; available
at http://www.diku.dk/users/tofte/publ/toplassubm.a4.ps.Z ), November 1996.
[21] M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, P. Sestoft, and P. Bertelsen.
Programming with regions in the ML Kit. Technical Report DIKU-TR-97/12, Department
of Computer Science, University of Copenhagen, 1997. (http://www.diku.dk/researchgroups
/topps/activities/topps/kit2).
[22] M. Tofte and J.-P. Talpin. Data region inference for polymorphic functional languages (technical
summary). Technical Report EMP/CRI/A-229, Ecole des Mines de Paris, 1992.
[23] M. Tofte and J.-P. Talpin. Implementing the call-by-value lambda-calculus using a stack of
regions. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 188--201. ACM Press, January 1994.
[24] M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation,

132(2):109--176, 1997.
[25] P. R. Wilson. Uniprocessor garbage collection techniques. In Y. Bekkers and J. Cohen,
editors, Memory Management, Proceedings, International Workshop IWMM92, pages 1--42.
Springer-Verlag, September 1992.

