upwards closed do regions C, AF-e : a&b 1 Introduction Polymorphic Subtyping for Effect Analysis: The Algorithm

The Algorithm

Flemming Nielson & Hanne Riis Nielson & Torben Amtoft Computer Science Department, Aarhus University, Denmark

e - m a i l : {fnielson, hrnielson, t amt of t }@daimi. aau .dk

A b s t r a c t . We study an annotated type and effect system that inte- grates let-polymorphism, effects, and subtyping into an annotated type and effect system for a fragment of Concurrent ML. First we define a type inference algorithm and then construct procedures for constraint normalisation and simplification. Next these algorithms are proved syn- tactically sound with respect to the annotated type and effect system.

1 Introduction

In a recent paper [11] we developed an a n n o t a t e d type and effect system for a fragment of Concurrent ML [12]. Judgements are of form

C, AF-e : a & b

with e an expression, b a " b e h a v i o u r ' , r7 a type or a type scheme (to incor- porate ML-style l e t - p o l y m o r p h i s m ) , C a set of constraints among types and behaviours, and A an environment. Behaviours record channel allocations and thereby the set of "dangerous variables", cf. [19] (where these are called "imper- ative" variables) and [21]. A subtyping relation is defined using a subeffecting relation on behaviours, with the usual contravariant ordering for function space but there is no inclusion between base types.

In our approach types are a n n o t a t e d with behaviour information (for example the function type tl __.b t2). Compared with the literature we do not a t t e m p t to collect information a b o u t the regions in which communications take place [17, 20]; neither do we enable polymorphic recursion in the type annotations as in [4~ 20]; on the other hand we do allow behaviours to contain a n n o t a t e d types.

. In [11] it was demonstrated t h a t one must be very careful when deciding the set of variables over which to generalise in the inference rule for l e t : not only should this set be disjoint from the set of variables occurring in the behaviour (as is standard in effect systems, e.g. [17]) but it should also be upwards closed with respect to a constraint set. T h e semantic soundness of the generalisation rule (and of the overall system) was proved in [1] and relied heavily on the upwards closure.

T h e goal of this paper is to produce a type reconstruction algorithm in the spirit of Milner's algorithm W [7]: given an expression e and an environment A, the recursively defined function ]4; will produce a substitution S, a t y p e t,

and a behaviour b. The definition in [7] employs unification: if el has been given type to --+ tl and e2 has been given type t2 then in order to type el e2 one must unify to and t2. Unification works by decomposition: in order to unify tl --* t2 and t~ --* t~ one recursively unifies tl with t~ and t2 with t~. Decomposition is valid because types constitute a "free algebra": two types are equal if and only if they have the same top-level constructor and also their subcomponents are equal. However, this will not be the case for behaviours, and therefore YV of [7]

cannot immediately be generalised to work on annotated types.

We thus have to rethink the unification algorithm. As the behaviours of this paper satisfy certain associativity and commutativity properties one might adapt results from unification theory [13] to get a unification algorithm producing a set of unifiers from which all other unifiers can be derived; but as we shall aim at a theory which facilitates extension to more complex behaviours (such as those presented in [10]) where it seems unlikely t h a t we can use results from unification theory, we shall refrain from such attempts and instead follow [6] and generate behaviour constraints: t h a t is, in the process of uniting tl __,b t2 and t~ __.b' t~

we generate constraints relating b and b'.

In order to incorporate subtyping we also need to generate type constraints as in [3, 15] (in these papers there m a y also be inclusions between base types such as • C r e a l ) . The presence of type constraints as well as behaviour con- straints is a consequence of our overall design: types and behaviours should be inferred simultaneously "from scratch", as is done by the algorithm YV presented in Sect. 3. This should be compared with the approach in [18] where an effect sys- tem with subtyping but without polymorphism is presented; as the "underlying"

types are given in advance it is sufficient to generate behaviour constraints.

The constraints generated by }IV have to be massaged so as to satisfy certain invariants ("atomicity" and "simplicity") and for this we devise the algorithm

~- (Sect. 4), inspired by [3]. Still the algorithm will produce a rather unwieldy number of constraints; to reduce this number dramatically we m a y apply an algorithm ~ (defined in Sect. 5) which adapts the techniques of [2, 15]. The resulting algorithm YV (which uses Jr and Tr has been implemented, and in Sect. 6 we shall see t h a t the output produced by our prototype is quite readable and informative.

S o u n d n e s s . In Sect. 7 we shall prove t h a t ~iV is (syntactically) sound, t h a t is if ~V(A, e) = (S, t, b, C) then C, S A F- e : t & b; the completeness of ~V is still an open question and we do not attempt to estimate the complexity of the algorithm.

As the main distinguishing feature of our inference system (as mentioned above), essential for semantic soundness, was the choice of generalisation rule;

so the distinguishing feature of our algorithm, essential for syntactic soundness (and which still leaves hope for completeness), is the choice of generalisation rule.

This involves (much as in [21]) taking downwards closure of a set of variables with respect to a constraint set.

In Sect. 8 we shall see t h a t the constraints generated by 14] can always be solved provided recursive behaviour systems are admitted. Alternatively recur-

sive behaviour systems can be disallowed thus rejecting programs t h a t implement recursion in an indirect way through communication; this is quite analogous to the way the absence of recursive types in the simply typed A-calculi forbids defin- ing the Y combinator and instead requires recursion to be an explicit primitive in the language.

2 I n f e r e n c e S y s t e m

In this section we briefly recapitulate the inference system [11]. Expressions and constants are given by

e ::= e I x I f n x ~ e I el e2 I l e t x = el i n e2 ] r e c f x ~ e l i f e t h e n e i e l s e e 2 e : : = () I t r u e l f a l s e l n l + l , I = l - - -

I p a i r I f s t l s n d l n i l I cons I h d l t l t i s n i l I send I receive I sync I ch~'nel I fork

where there are four kinds of constants: sequential constructors like true and p a i r , sequential base functions like + and f s t , the non-sequential constructors s e n d and r e c e i v e for creating delayed output and input communications, and the non-sequential base functions sync (for synchronising a delayed communi- cation), c h a n n e l (for allocating a new communication channel) and f o r k (for spawning a new process).

Types and behaviours are given by

t ::---- c~ l unit Iint I bool I tl x t2 I t list I tl __>b t2 I t chan I t corn b

b ::= {t CHAN} I /~ I 0 I 51 U52

where a type tl 4 5 t2 denotes a function which given a value of type tl computes a value of type t2 with "side effect" b; where a type t chart denotes a channel allowing values of type t to be transmitted; and where a type t corn b denotes a delayed communication t h a t when synchronised will give rise to side effect b and result in a type t. A behaviour can (apart from the presence of behaviour variables) be viewed as a set of "atomic" behaviours which each record the creation of a channel.

Type schemes t s are of form V(6/~: C). t with C a set of constraints, where a constraint is either of form tl C_ t2 or of form bl C b2. The type schemes of selected constants are given in Figure 1.

The ordering among types and behaviours is depicted in Figure 2; in par- ticular notice t h a t the ordering is contravariant in the argument position of a function type and t h a t in order for t chart C t' chan and {t CHAN} _C_C {t'

CHAN}

to hold we must demand t h a t t -= t', i.e. t C t' and t' C t, since t occurs covariantly when used in r e c e i v e and contravariantly when used in send.

The inference system is defined in Figure 3. The rules for abstraction and application are as usual in effect systems: the latent behaviour of the b o d y of

c TypeOf(C)

+ int • int _.0 int

p a i r V(ala2 : 0). G1 ._..>0 G2 -'+~ G1 X Ol 2 f s t V(OLIOL2 : 0). a l X O~ 2 --->~ Ot 1 s n d V(GIG2 : 0). g l X G2 __+0 Or2

send V(G: 0). (a c h ~ ) • ~ - ~ (~ corn 0)

~ e e ~ i ~ v ( ~ : 0). (~ c h ~ ) __,0 (~ corn 0) sync V(a/3 : 0). (a ^corn p) --># o~

e h ~ n ~ 1 v ( ~ z : {{~ C~AN} ___ Z}). unit ~ (~ c h ~ )

f o r k V(a/g : 0). ( u n i t --+# a ) --+0 u n i t Fig. 1. Type schemes for selected constants.

a function abstraction is placed on the arrow of the function type, and once the function is applied the latent behaviour is added to the effect of evaluating the function and its argument, reflecting t h a t the language is call-by-value. T h e rule for recursion makes use of function abstraction to concisely represent the

"fixed point requirement" of typing recursive functions; note t h a t we do not a d m i t p o l y m o r p h i c recursion. T h e rule (sub) makes use of the s u b t y p i n g and subeffecting relation defined in Fig. 2. T h e rule (ins) allows one to instantiate a t y p e scheme and employs the notion of solvability: we say t h a t the t y p e scheme Y(~/3: Co). to is

solvable

from C by So if

Dom(So) c_

{~/~} and if

CFSoCo,

where we write C [- C ' to m e a n t h a t I C F gl _C g2 for all gl C g2 in C ' .

T h e generalisation rule (gen) employs the notion of

well-formedness

where we need several auxiliary concepts: the judgement C F V1 +-- "72 holds if there exists (gl _Cg2) in C such t h a t 3'~ e

FV(g~)

for i = 1, 2; the relation ---* is the inverse of

~ ; the relation ~ is the

union

of +-- a n d 4 ; and as usual ~ * (respectively 4 "

and ~ * ) denotes the reflexive and transitive closure of these relations. We then define

upwards closure, downwards closure,

and

up-downwards closure:

x c T = {'YI 3 - / ~ X : C [ - - / ~ * -~}

X e l = {~ ] 3~' ~ X : C F ~' --+* -y}

x c I = {~1 3~' ~ X : C F - / ~ * -~}

and are then ready to define well-formedness for constraints and for t y p e schemes:

1 We use g~ to range over t or b as appropriate and V to range over a and f~ as appropriate and a to range over t and

ts as

appropriate.

O r d e r i n g o n b e h a v i o u r s

(&xiom) C f- bl C b2 (refl) C f- b C b

CI-bl Cb2 Ct-b2Cb3 (trans) C ~ bl C b3

CF-t ~ t'

(CHAN) C~-{t CHAN}C {t' CHAN}

(~) C~-~Cb

(u) Ceb~C_(bl ob2)

C I - b l C b C F b 2 C b (lub) Cl-(bl Ub2) Cb

if (blCb2) E C

for i = 1,2

O r d e r i n g o n t y p e s

(&xiom) CFtlC_t2 i f ( t l C t 2 ) e C (refl) C~tC_t

C I - t l Ct2 C~-t2Ct3 (tr~ns) C F- tl C t3

CI-t'~ Ctl CFt2 Ct'2 CI-bCb'

(-~)

c ~ (tl __,b t~) c (t'~ __,b, t'~)

C~t~ c_t'~ CFt2 c_t'2

(•

c ~ ( t ~ x

t~)c_(t;

x

t~)

Ct-tC_t'

(zi~t)

c F (t l i s t ) c (t' list) CF-t = t' (chem)

C e (t c h ~ ) C (t' c h ~ ) C I - t C t ' CI--bC_b' (corn) CF-(t corn b) C (t' comb')

Fig. 2. Subtyping and subeffecting.

D e f i n i t i o n 1. A constraint set is well-formed if all constraints are of form t C_ a or b C f l .

A t y p e scheme V(~/3: Co). to is well-formed if Co is well-formed and if all constraints in Co contain at least one variable a m o n g {~/~} and if it is upwards closed: t h a t is {ff/~}c~ T = {c~/~}.

A t y p e t is trivially well-formed. []

Requiring a t y p e scheme to be well-formed (in p a r t i c u l a r upwards closed) is a crucial feature in the a p p r o a c h of [11], t h e s e m a n t i c soundness of which was established in [1].

(con) C, A ~- c : TypeOf(c) a 0

(id) C , A ~ - x : A(x)&O

C , A [ x : t l ] F - e : t 2 a b (abs) C, A F - f n x ~ e : ( t ~ b t 2 ) & r

C1,AF-el : (t2--+b t l ) & b l C2,A~-e2 : tz&bz (app) (C~ U Cz), A }- e~ ez : tl & (b~ U bz U b)

C1,A~-el : t s l & b l C2,A[x:tsl]~-e2 : t~ab2 (let) ( C 1 U C 2 ) , A ~ - l e t x = e l i n e 2 : t2&(blt_Jb2) (rec) C , A [ f : t ] ~ - f n x = ~ e : t a b

C , A } - r e c f x ~ e : t a b

Co,A~-eo : bool&bo C1,A~-ez : t a b ~ C2,Al-e2 : t a b 2 (if) ( C o U C 1 U C 2 ) , A ~ - i f e o t h e n e l e l s e ez : t & ( b o t 3 b l U b z )

C, AF-e : t a b

(~ub) C,--,-A-Vi : t' a b' if C~-t C_ t' and C}-b C b'

(ins) C, A I - e : V(d/~: Co). togcb ifV(~/~: Co). to is solvable from C by So C,A~-e : Sotogzb

C U C o , A F - e : tomb if V(~/~:Co).to is both well-formed, (gen) C, A F- e : V(d/~: Co). to & b solvable from C, and satisfies (~/~} N

FV(C, A, b) =

Fig. 3. The type inference system.

As expected (and proved in [11]) we have the following results, crucial for showing soundness of our inference algorithm, saying t h a t we can apply a sub- stitution or strengthen the constraint set, and still get a valid judgement:

L e m m a 2 . Substitution L e m m a For all substitutions S:

(a) If C ~- C ' then S C F S Cq

(b) If C, A F e : a & b then S C, S A F e : S a & S b (and has the same shape).

L e m m a 3 . E n t a i l m e n t L e m m a

For all sets C ' of constraints satisfying C ~ f- C:

(a) If C F Co then C ' ~- Co.

(b) If C, A F e : a & b then C ' , A F e : a & b (and has the same shape).

3 T h e I n f e r e n c e A l g o r i t h m

In designing an inference algorithm W for the type inference system we are (cf. the Introduction) motivated by the overall approach of [15, 3]. One ingre- dient (called W') of this will be to perform a syntax-directed traversal of the expression in order to determine its type and behaviour; this will involve con- structing a constraint set for expressing the required relationship between the type and behaviour variables. The second ingredient (called 9 ~) will be to per- form a decomposition of the constraint set into one t h a t is well-formed. The third ingredient (called 7~) amounts to reducing the constraint set; this is optional and a somewhat open ended endeavour.

3.1 Well-formedness, Simplicity and A t o m i c i t y

In Definition 1 we introduced the notion of well-formedness for constraint sets and type schemes; for use by the algorithm we shall in addition introduce the notions of s i m p l i c i t y and atomicity.

Simplicity. As we do not know how to solve general behaviour constraints (for example we have no techniques available for decomposing constraints of form ~1 _C f12 U ~3) we shall wish to maintain the invariant t h a t all (behaviour) constraints which arise in the algorithm must be well-formed. In order to achieve this we must follow [16] and [21] and demand t h a t all types in question are (what [9] calls) simple, t h a t is all behaviour annotations are variables (as is the case for int - ~ int).

D e f i n i t i o n 4 . A type is simple if all its behaviour annotations are behaviour variables; a constraint set is simple if all type constraints are of form (tl C t2) with tl and t2 simple and if all behaviour constraints are of form (b C ~); a type scheme is simple if the constraint set and the type both are; an environment is simple if all its type schemes are; finally a substitution is simple if it maps behaviour variables to behaviour variables and type variables to simple types.

T h a t is, with st ranging over simple types we have st :: . . . . [ st1 --*~ st2 [ st1 x st2 [ . . . st corn

F a c t 5. Let t be a simple type, C be a simple constraint set, ts be a simple type scheme, and S, S ~ be simple substitutions. Then S t is a simple type, S C is a simple constraint set, S ts is a simple type scheme, and S ~ S is a simple substitution.

T h e r e is a discrepancy between the inference system and the algorithm in the sense t h a t non-simple types are allowed in the former, in order to increase ex- pressibility, but disallowed in the latter. In [21] a "direct" as well as an "indirect"

inference system is presented; the "indirect" is geared towards an algorithm and requires simplicity and employs constraints. A perhaps more uniform approach is given in [20] where arrows are annotated with pairs of form e.r with e an effect variable and with r a set of region or effect variables; one can think of this as an arrow annotated by e together with the constraint r C e.

A t o m i c i t y . As in [8, 3, 15] we shall want the type constraints to match and shall decompose them into atomic constraints; in our setting these will not contain base types as we have no ordering among those.

D e f i n i t i o n 6 . A constraint set is atomic if all type constraints are of form a l c a2 and if all behaviour constraints are of form {t CHAN} C ~ or /3 t C j3.

F a c t 7. An atomic constraint set is also well-formed and simple.

Requiring a well-formed set of behaviour constraints to be atomic is unproblem- atic because a constraint (0 C fl) can always be thrown away and a constraint (bl U b2 C_ fl) can always be split to (bl _C j3) and (b2 C_/3). Requiring atomicity of type constraints is responsible for transforming constraints like ( i n t _ a) and (tl X t2 ~ O~) by forcing a to be replaced by a type expression t h a t "matches"

the left hand side, and for disallowing constraints like (tl x t2 c_ t] __~b t~). This feature is responsible for making the algorithm a "conservative extension" of the way algorithm W for Standard ML would operate if effects were not taken into account: in particular our algorithm will fail, rather than produce an unsolvable constraint set, if the underlying type constraints of the effect-free system cannot be solved. (We shall make this point more precise at the end of Section 7.) 3.2 A l g o r i t h m

Our key algorithm W is described by W(A, e) = (S, t, b, C)

and we shall aim at defining it such t h a t C, S A t-e : t & b holds (soundness) and such that we might hope for some notion of principality (completeness);

here completeness might be taken to mean that if also C I, Stt A ~- e : t t & b r then

there exists S' such t h a t C' F- S' C and C t k S ~ t C_ t' and C r t- S' b C_ b' and S' S equals S ~' on A. It is an open question whether such a principal typing exists and, if this is the case, whether our algorithm actually computes this principal typing.

We shall enforce t h r o u g h o u t t h a t if A is simple then all of S, t and C are simple and t h a t C is atomic. Algorithm 142 is defined by the clause

W ( A , e) = let ($1, tl, bl, C1) = W ' ( A , e) let ($2, C2) = ~ ( C 1 )

let (C3, t3, 53) = n ( C 2 , $2 tl, $2 51, $2 $1 A) in ($2 $1, t3, b3, C3)

where the definitions of W ' and W are mutually recursive; algorithm W ' is responsible for the syntax-directed traversal of the argument expression e. In general, W ' will fail to produce an atomic constraint set C, even when the environment A is well-formed and simple; it will be the case, however, t h a t all of $1, t l , and C1 are simple. This then motivates the need for a transformation

~" (Section 4) t h a t maps a simple constraint set into an atomic (hence also well-formed and simple) constraint set; since this involves splitting variables we shall need to produce a simple substitution as well. T h e final transformation 7~ merely a t t e m p t s to get a smaller constraint set by removing variables t h a t are not strictly needed. Its operation is not essential for the soundness of our algorithm and thus one might define it by T~(C, t, b, A) = (C, t, b); in Section 5 we shall consider a more powerful version of T~.

Example 1. To make the intentions a bit clearer suppose W ' ( A , e) = (S1, tl, bl, C1) so t h a t C1, $1 A }- e : tt & bl is a typing of e. If

C1 {0/1 • 0/2~0/3, int___0/4, {0/5 CHAN} U 0 ~ } then ($2, C2) = Jr(Ct) should give

c2 = {a, c a3t, a2 c a32, {as tHAN} C_ ~}

$2 ---- [0/3 ~'+ 0/31 X 0/32, 0/4 }--+ i n t ]

Here we expand 0/3 to 0/31 x 0/32 so t h a t the resulting constraint a t x 0/2 C_

0/3t x 0/32 can be "decomposed" into 0/1 C 0/31 and 0/2 C 0132 t h a t are b o t h atomic.

Furthermore we have expanded 0/4 to i n t as it follows from Figure 2 t h a t 0 ~- i n t C t necessitates t h a t t equals i n t . Finally we have decomposed the con- straint upon /J into two and then removed the trivial 0 C_/3 constraint. T h e intention is t h a t also C2, $2 St A ~- e : $2 tl & $2 bl is a typing of e; additionally the constraint set is atomic (unlike what is the case for C1); and we have not lost any principality when going from the former typing to the latter. []

3.3 A l g o r i t h m ~ 2 I

Algorithm W ' is defined by the clauses in Figure 4 and calls W in a number of places. Actually it could call itself recursively(rather than calling l/V, in all but

one place2: the call to Fl? immediately prior to the use of

GEN

to generalise the type of the l e t - b o u n d identifier to a type scheme. T h e algorithm follows the overall approach of [15, 5] except t h a t as in [3] there are no explicit unification steps; these all take place as part of the ~" transformation. T h e only novel ingre- dient of our approach shows up in the clause for l e t as we shall explain shortly.

Concentrating on "the overall picture" we thus have clauses for identifiers and constants; b o t h make use of the auxiliary function

INST

defined by

INST(V(~fi:

C). t) = let ~ ' # be fresh let R = [~/~-* o ~ ] in (Id, R t, 0, R C)

INST(t)

= (Id, t, O, O)

in order to produce a fresh instance of the relevant type or type scheme (as determined from T y p e O f or from A); in order to ensure t h a t this instance is simple (as will be needed if it is determined from TypeOf) we also need the funktion

Mk, simple

which replaces all occurrences of 0 in a t y p e by fresh behaviour variables, for instance we have

Mk-simple(int __.o

int -~r int) = i n t --~fl~ i n t ___,f12 i n t with ~1 and ~2 fresh. As all behaviour annotations in Fig. 1 are either 0 or variables, and as the former kind of a n n o t a t i o n occurs only in top-level positive position (that is, not on the left hand side of a function arrow or inside some channel type), the following property holds:

F a c t 8. Let c be a constant, and let

INST(TypeOf(c)) = (S, t, b, C).

T h e n C is a simple constraint set,

Mk-simple(t)

is a simple type and

0 ~- t C Mk-simple(t).

T h e clause for function abstraction is rather straightforward; note the use of a fresh behaviour variable in order to ensure t h a t only simple types are produced;

we then add a constraint to record the "meaning" of the behaviour variable.

Also the clause for application is rather straightforward; note t h a t instead of a unification step we record the desired connection between the operator and operand types by means of a constraint. T h e clauses for recursion and conditional follow the same p a t t e r n as the clauses for abstraction and application.

T h e only novelty in the clause for l e t is the function

GEN

used for general- isation:

GEN(A, b)(C,

t) = let { ~ }

= (fV(t) 05) \ (FV(A, b) c~)

let Co = C ] {,v,~_~.,

- r

in V ( ~ : Co). t

where C I { ~ } = {(gl _Cg2)

C C ] FV(gl,g2) N

{ ~ } # 0}. T h e definition of Co thus establishes the part of the well-formedness condition t h a t requires each constraint to involve at least one bound variable.

2 Interestingly, this is exactly the place where the algorithm of [15] makes use of con- straint simplification in the

"close"

function; however, our prototype implementation suggests that the choice embodied in the definition of W gives faster performance.

W ' ( A , c) = if c E Dom(TypeOf)

then let (S, t, b, C) = I N S ~ T y p e O f ( c) ) in (S, Mk-simple(t), b, C)

else failco~s t

W ' ( A , x) = if x E Dora(A) then INST(A(x)) else ]ailide~t W'(A, f n x =:k co)

let a be fresh

let (So, to, bo, Co) = W ( A [ x : a], eo) let fl be fresh

in (So, So a - - ~ to, ~, Co U {bo C fl}) I,V'(A, et e2) =

let (Sl,tx,bx,C1) = W ( A , e ~ ) let ($2, t2, b2, C2) = YV(S~ A, e2) let a , fl be fresh

in ( S2 SI , a, S2 bl U b2 U l3 ,

$2 6 1 U 6 2 U{$2$1 Ct2 ....~B o~}) W ' ( A , l e t x -- el i n e2) =

let (S~,tI,b~,C~) -- I/V(A,e~) let tsl -- GEN(S1 A, bl)(Cl,tt)

let (S2,t2,b2,C2) = W((S~ A)[x: tst],e2) in (S2Sl,t2,S2bl Ub2,S2C1 UC2) W'(A, rec f x ~ eo) =

let a l , j3, a2 be fresh

let (so,to, bo,Co) = YV(A[f : a l --*# a2][x : a~],eo) in (So, So ( a l --*~ a2), 0, Co U {bo C_ So fl, to C_ So a~})

W'(A,

i f eo t h e n el e l s e e2) let (So, to, bo, Co) let (SI,$1,bl, Cz) let ($2, t2, b2, C2) let a be fresh

= PV(A, eo)

= W(So A, el)

=

W(S1 So A, e2)

in ( 82 B1So, a, B2 St bo U S2 bl U b2,

$2SICOUS2C1 U C 2 U { S 2 S l t o C b o o l , $ 2 $ 1 C a , t 2 C a } ) Fig. 4. Syntax-directed constraint generation.

The exclusion of the set

FV(A,

b) c l (rather t h a n just

FV(A, b))

is necessary in order to ensure {d/~} v~ -- {~f~} which (cf. the remarks concerning Def. 1) is essential for semantic soundness; the computation of "Indirect Free Variables"

of [21] is very similar to our notion of downwards closure. Finally we have chosen

FV(t) cI

as the "universe" in which to perform the set difference; this universe must be large enough t h a t we m a y still hope for syntactic completeness and all of

FV(t), FV(t) C~

(similar to what is in fact taken in [21]) and

FV(t) cT

are apparently too small for this (except for the latter t h e y are not even upwards closed).

F a c t 9. Let

a = GEN(A, b)(C,

t); if C is well-formed then so is a.

Proof.

The only non-trivial task is to show t h a t {d~}CoT ~ { ( ~ } where {~/~}

is as in the defining clause for

GEN.

So assume Co [-~'1 ~-- 72 (and hence also C~-71 e- 72) with 71 6 {~f~}; we must show t h a t 72 6 {dfl~. Now 71 E

FV(t) CI

and ~'1 ~

FV(A, b) c~,

hence we infer 72 6

FV(t) cI

and ~/2 •

FV(A, b) c~

which

amounts to the desired result. []

R e m a r k . Note t h a t

FV(t) cI

is a subset of

FV(t, C)

and t h a t it m a y well be a proper subset; when this is the case it avoids to generalise over "purely internal"

variables t h a t are inconsequential for the overall type. If one were to regard l e t x -- el i n e2 as equivalent to

e2[el/x]

(which is sensible only if el has an empty behaviour) this corresponds to forcing all "purely internal" variables in corresponding copies of el to be equal. This is helpful for reducing the size of

constraint sets and type schemes. []

4 A l g o r i t h m .%"

We are now going to define the algorithm ~ which "forces type constraints to match" by transforming them into atomic constraints; the algorithm closely resembles [3, procedure MATCH].

The algorithm m a y be described as a non-deterministic rewriting process.

It operates over triples of the form ( S, C, ~ ) where S is a substitution, C is a constraint set, and ~ is an equivalence relation among the finite set of type variables in C; we shall write E q c for the identity relation over type variables in C. We then define ~" by

~-(C) = let (S', C', ~ ' ) be given by (Id, C, Eqc) ~* (S', C', ~ ' ) / in if C ' is atomic

then (S', C') else

failforcing

The rewriting relation is defined by the axioms of Figure 6 and will be explained below; it makes use of an auxiliary rewriting relation, defined in Figure 5, which operates over constraint sets.

The axioms of Figure 5 are rather straightforward. For behaviours the axiom (O) simply throws away constraints of the form 0 C_ b and the axiom (U) simply

(~)

(u) (x)

CU{O C b}~C

CU{b~ U b2 C IJ} ~ C U {b~ C_ b, ta C_ b}

c u { h x t2 c t3 x t d ~ c u {t~ c_ t3, t2 g t4}

( l i s t ) CU{f4 l i s t C t2 l i s t } ~ C U {h C_ t2}

( o , ~ ) co{tl

r C t= r U {t~ C_ t=, t2 C h}

CU{h corn bl C_t2 corn b 2 } ~ C U {tlCt2,bl C_b~}

CU{tl __~6~ h C ta ~b~ t4}

~ C U {t3 ~ h , b l C_b2,tz _Ct4}

~ C

(int) cu{int_C i.t} /

(bool) Cb{bool =_ boo~}

( ~ i t ) c u { = i t c ~ i t }

^]

Fig. 5. Decomposition of constraints.

C ~ C '

(ac) (s. c.~)---.(s, c,, ~7

(mr) (S, CO{t C ~}, ~)---~(RS, R e U {Rt C_ R~}, ~') provided 3d(a, t, % R, ,,/)

(=~)

(s, c6{~ =_ t}, ~)--~(R s, R c u {a~ =_ Re},

~')

provided ^M(a, t, ^~, R, ^{J )}

Fig. 6. Rewriting rules for 5r: forcing well-formedness.

decomposes constraints of ^the form bl U b2 C b to ^the simpler constraints bl C b and b2 _C_ b. (A small notational point: in Figure 5 and in Figure 6 we write C(AC' for C U C ' in case C N C ' = 0.) For types the axioms (x), ( l i s t ) , (chart), (corn), and (--*) essentially run the inference system of Figure 2 in a backwards way and generate new constraints h C_ t2 and t2 C_ tl whenever we had tl ~ t2 in Figure 2. Axioms ( i n t ) , (bool) and ( u n i t ) are simple instances of reflexivity.

F a c t 10. The rewriting relation -~ is confluent and if C1--~C2 then C2 P C1.

Proof.

Confluence follows since each rewriting operates on a single element only, and for each element there is only one possible rewriting. []

We now t u r n to Figure 6. T h e axiom (dc) decomposes the constraint set but does not modify the substitution nor the equivalence relation among type variables. T h e axioms (mr) and (ml) force left and right hand sides of type constraints to match and produces a new substitution as a result; additionally it m a y modify the equivalence relation among type variables. T h e details require the predicate Jr4 (which performs an "occur check"), to be defined shortly. Before presenting the formal definition we consider an example.

Example 2.

Consider the constraint tl C c~0 where tl = ( a l l • a12) com ~1- Forc- ing the left and right hand sides to match means finding a substitution R such t h a t

at1

and Rc~0 have the same shape. A natural way to achieve this is by creating new type variables a21 and o~22 and a new behaviour variable ~2 and by defining

R ---= [c~ 0 e---> (~21 X Ot22 ) COIn f12]"

T h e n

at1

-- tl = (c~11 x c~12) corn fll and Rc~o = (c~21 x c~22) corn f12 and these types intuitively have the same shape. Returning to Figure 6 we would thus expect 2~4(~0, tl, ~ , R, ~).

If instead we had considered the constraint (a x c~) corn fl C ~ then the above procedure would not lead to a matching constraint. We would get

R = [~ ~ ( ~ ' x ~ " ) corn

#']

and the constraint R ((~ x ~) corn fl) C_C_ R a t h e n is

(((o/x 0/9 co,,, #') x ( ( o / x o/') ~om #')) r #' c_ (o~' x o/') ~om

#'

which does not match. Indeed it would seem t h a t matching could go on forever without ever producing a matching result. To detect this situation we have an

"occur check": when Ad(a, t, ~, R, ~') holds no variable in

Dora(R)

must occur in t. This condition fails when t = (c~ x o~) coin j3.

However, there are more subtle ways in which termination m a y fail. Consider the constraint set

{~I corn #i c ~ 0 , a 0 c ~i}

where only the first constraint does not match. A t t e m p t i n g a m a t c h we get R1 = [o~0 ~-+ o~2 ^{c o m} ~2]

and note t h a t the "occur check" succeeds. T h e resulting constraint set is {OZl ^corn/~1 C_ 0~2 ^corn

~2,

^{OZ2 corn ~2 C} Ozl}

which m a y be reduced to

{al c_ ~2, #I c_ #2, a2 corn ~2 c_ al}.

T h e type part is isomorphic to the initial constraints, so this process m a y con- tinue forever: we perform a second match and produce a second substitution R2, etc.

To detect this situation we follow [3] in making use of the equivalence relation and extend it with a l "- a2 after the first match t h a t produced R1; the intuition is t h a t a l and a2 eventually must be bound to types having the same shape. W h e n performing the second match we then require R2 not only to expand a l but also all a ' satisfying a ' ~ a l ; this means t h a t

R2

must expand also a2.

Consequently the "extended occur check"

Dora(R2) N FV(a2

corn f12) = 0 fails.

[]

R e m a r k . Matching bears certain similarities to unification and can actually be defined in terms of unification. In [8] matching is performed by first doing unification and then the resulting substitution is transformed such t h a t it "maps into fresh variables". In [14, Fig. 3.7] it is first checked whether it is possible to unify a certain set of equations, derived from the constraint set; if this is the case then the algorithm behaves similar to the one presented here except t h a t

the equivalence relation is no longer needed. []

To formalise the development of the example we need to be more precise a b o u t the shape of a type and when two types match.

D e f i n i t i o n 11. A shape

sh

is a t y p e with holes in it for all type variables and for all behaviours; it m a y be formally defined by:

sh ::= [] l

u n i t l i n t l b o o l l s h l

x sh2 I shl --~[l sh2 I sh l i s t

I sh I corn

[]

We write

sh[t,

b] for the type obtained by replacing all type holes with the relevant t y p e in the list t' and replacing all behaviour holes with the relevant behaviour in the list b ; we assume t h r o u g h o u t t h a t the lengths of the lists equal the number of holes and shall dispense with a formal definition. For each type t there clearly exists unique

sh, ~

and b such t h a t t =

sh[~,

b], and t is simple if and only if M1 elements of b are variables.

Example3.

If

sh

= ([] x []) corn [] then

sh[~,b]

= (tl x t2) com bl if and only if

= tit2

and b = bl. []

T h e axioms (mr) and (ml) force a type t to match a t y p e variable a and employ the predicate .AA defined in Figure 7. This predicate m a y also be consid- ered a partial function with its first three parameters being input and the last two being output; the "call" A~(a, t, ~, R, ~ ' ) produces the substitution R and modifies the equivalence relation N (over the free type variables of a constraint set C r) to another equivalence relation ,-Y (over the free type variables of the constraint set R C'). In axioms (mr) and (ml) the newly produced substitution R is composed with the previously produced substitution. Also note t h a t the

"extended occur check" in Figure 7 ensures t h a t

R t = t.

Using Fact 5 it is straightforward to establish:

A,t(a, t, ~, R, ~') holds

if {c~1,-", c~n} N F V ( t ) = 0

and R = [c~1 ~-~ s h [ ~ l , ~ l ] , . . . , o~,~ ~ s h [ ~ , , ~ , ] ]

and . - / i s the least equivalence relation containing the pairs {(~', ~")

In'

~ c~"A {~',a"} f] {~i,.-. ,~.} = ~} U

{ ( ~ 0 ~ , a ~ ) I ~ 0 = ~ O l - - . a 0 ~ , ~ = ~ . . . a~,~, 1 < i < n, 1 < j < m } where { ~ 1 , ' " , ~ } = {~'la' ~ ~}

and sh[~o,~o] = t with C~o having length m

and 6 1 , ' " , ~ n are vectors of fresh variables of length m

and ~ 1 , ' " , fin are vectors of fresh variables of the same length as ~0

Fig. 7. Forced matching for simple types.

F a c t 12. Suppose (S, C, ~ ) , (S', C', ~ ' ) . T h e n there exists simple R such t h a t S ' = R S and such t h a t R C ~ * C ' . Moreover, if S and C are simple then also S' and C ' are simple.

R e m a r k : t y p e c y c l e s b e c o m e b e h a v i o u r c y c l e s . To understand why ~ does not report failure in m o r e cases t h a n a "classical type checker", the following example is helpful. Consider the constraint set

C = {int -~{~ CHAN} int C_ a}

which will not cause a classical type checker to fail since a is simply unified with i n t --~ i n t . Now let us see how ~- behaves on this constraint, encoded as a set of s i m p l e constraints:

{ i n t --~/~ i n t C ~, {c~ CHAN} C ~}.

Here case (mr) in Figure 6 is enabled, and consequentially a substitution which maps ~ into i n t --*~' i n t (with/3' new) is applied to the constraints. T h e re- sulting constraint set is

{ i n t - - ~ i n t c_ i n t --*~' i n t , { ( i n z - ~ ' i n t ) CHAN}

C ~}

and after first applying case (dc) for (-*) and then applying case (dc) for ( i n t ) we end up with the constraint set

C' = {flC~', {(int -~/~' int)

CHAN} C_~}

which cannot be rewritten further. T h e set C' is atomic so Algorithm J: succeeds

on C. []

4 . 1 T e r m i n a t i o n a n d S o u n d n e s s o f :T"

Having completed the definition of .Ad, , and ~ we can state:

L e n m a a 13. 9~(C) always terminates (possibly with failure). If ~-(C) = (S', C') then

- if C is simple then S' is simple and C ' is atomic;

- C ' is determined from S' C in the sense t h a t S' C--~*C'~.

Proof. We first address termination and for this purpose we (much as in [3]) define an ordering on triples (S, C, ~ ) as follows: (S', C', ~') is less t h a n ( S, C, ~ ) if either the number of equivalence classes in FV(C') wrt. ,-J is less than the number of equivalence classes in FV(C) wrt. ,~ or these numbers are equal but C ' is less t h a n C according to the following definition:

for all i > 0 let s~ be the number of constraints in C containing i symbols and let s~ be the number of constraints in C ~ containing i symbols; then C '

I I

is less t h a n C if there exists a n such t h a t s n < sn and such t h a t s~ -- si for all i > n.

This relation on constraint sets is clearly transitive and it is easy to see t h a t it is also well-founded, hence the (lexicographically defined) ordering on triples is well-founded. Thus it suffices to show t h a t if (S, C, N)---+(S', C', ~') then i S', C', ~ ' ) is less t h a n (S, C, ,-). If the rule (dc) has been applied then C ' is less t h a n C (as n in the above definition we can use the number of symbols in the constraint being decomposed) and ~'=~. If the rule (mr) or (ml) has been applied then the number of equivalence classes wrt. ~ will decrease as can be seen from the definition of A4 in Fig. 7: the equivalence class containing ~ is removed (as this class equals Dora(R) and C' = R C) and no new classes are added (as all type variables in Ran(R) are put into some existing equivalence class).

We have thus proved termination; it is easy to see t h a t the other claims will follow provided we can show t h a t if

(Id, C, E q c ) '*(Sn, C ~ , ~ n )

then Sn C ~ * C n and if C is simple then Sn and Cn are simple. We do this by induction on the length of the derivation, where the base case as well as the part concerning simplicity (where we use Fact 12) is trivial. For the inductive step, suppose t h a t

(Id, C, EQc)

'*(Sn, Cn, "~n) )(Sn+l, Cn+l,

' ~ n ~ - l )

where the induction hypothesis ensures t h a t Sn C~*Cn. By Fact 12 there exists R such t h a t Sn+l = R S n and such t h a t RCn~*Cn+I. As it is easy to see t h a t the relation ~ is closed under substitution it holds t h a t R S~ C-~*R C~, hence

the claim. []

L e m m a 14. ~ is sound

If bY(G) = (S', C') then C ' }- S' C.

Proof. By L e m m a 13 we have S' C--~*C ', which yields the claim due to Fact 10.

R e m a r k . By Fact 10 we know t h a t ~ is confluent but this does not directly carry over to ~ or 5r: the constraint c~l C c~2 m a y yield ([~l H C~o], {c~0 C a2}) as well as ([~2 ~-* so], {c~1 C C~o}). However, L e m m a 13 told us t h a t 9c(C) = (S', C') ensures t h a t C ' is determined from S' C, and we conjecture t h a t S' is determined (up to some notion of renaming) from C.

5 A l g o r i t h m 7~

The purpose of algorithm 7~ is to reduce the size of a constraint set which is already atomic. The techniques used are basically those of [15] and [2], adapted to our framework.

The transformation T~ m a y be described as a non-deterministic rewriting process, operating over triples of form (C, t, b), and with respect to a fixed envi- ronment A. We then define Ts by:

T~(C, t, b, A) = let (C', t', b') be given by

AF-(C,t,b)----**(C',t',b')/ ,

in (C', t', b')

The rewriting relation is defined by the axioms of Figure 8 and will be explained below (recall t h a t U means disjoint union). To understand the axioms, it is helpful to view the constraints as a directed graph where the nodes are type or behaviour variables or of form {t CHAN}, and the arrows cannot have a node of form {t CHAN} as the source. To this end we define:

D e f i n i t i o n 15. We write C F V ~ * ~' if there is a path from 7' to 7: t h a t is there exists 70"" " % (n > 0) such t h a t 70 = 7 and 7n = 7' and (7~ C 7~+1) E C for all i E { 0 . . . n - 1}.

Notice t h a t C ~- 7 ~ * 7 holds also if 7 ~

FV(C).

From reflexivity and transitivity of C we have:

F a c t 16. If C}-7 ~ * 7' then also C ~ - 7 C 7 r.

We have a substitution result similar to L e m m a 2:

F a c t 17. Let S be a substitution mapping variables into variables, and suppose C F f f ~ * V'. Then also

S C F S 7 r $7'.

We say t h a t C is cyclic if there exists V1,72 E

FV(C)

with 71 ~ 72 such t h a t C F T 1 ~ * 72 and C~-72 ~ * 71.

We now explain the rules: (redund) removes constraints which are redun- dant due to the ordering C being reflexive and transitive; applying this rule repeatedly is called "transitive reduction" in [15] and is essential for a compact representation of the constraints.

The remaining rules all replace some variable 7 by another variable 7'. How- ever, it is not the case t h a t all substitutions t h a t solve C can be written on the form S' [7 ~-* ~/] and therefore we might lose completeness if the substitution

(redund) A t- (CU{~/' C 7}, t, b)---*(C, t, b) provided C F-V I ~=* 7

(cycle)

At-(C,t,b) ,(SC, St, Sb)

where S -- [~, ~-* ~/] with -), ~ ~/

provided C ~-V r ~ / a n d C t - ~ r ~, and provided V ~

FV(A)

(shrink) A t- (CO[-),' C_ "r}, t, b)---~ (S C, S t, S b) where S = IV ~-~ ~'] with ~/~ V' provided ~ r

FV(RHS(C), A)

and

provided t, b, and each element in

LHS(C)

is monotonic in V (boost) A~ (CO{v c V'},t, b)---.(S C, St, Sb)

where S = [q~ ~-* ~/] with - / ~ V ~ provided V ~ FV(A) and

provided $, b and each element in

LHS(C)

is anti-monotonic in ~/

Fig. 8. Eliminating constraints.

IV ~-~ 3'~] was to be returned (in the style of ~-) and subsequently applied to A.

In order to maintain soundness we must therefore d e m a n d t h a t 3" ~

FV(A).

T h e rule (cycle) collapses cycles in the graph; due to the remark above a cycle which involves

two

elements of

FV(A)

cannot be eliminated. (In [14] it holds t h a t 0 ~-tl -- t2 implies tl = t2 so if V and V ~ belong to the same cycle in C then all substitutions t h a t solve C can be written on the form S ~ IV ~-~ V~], hence cycle elimination can be part of the analogue of ~'.)

T h e rule (shrink) expresses t h a t a variable 3' can be replaced by its

"im-

mediate predecessor" 7 ~, and due to the ability to perform transitive reduction this can be strengthened to the requirement t h a t 3"~ is the "only predecessor"

of % which can be formalised as the side condition 3' ~

FV(RHS(C))

where

RHS(C) =

{3" [ 3g : (gC_3") C C}. We can allow 3" to belong to t and b and

LHS(C),

where

LHS(C) = {g [ B3" : (g C_

3") e C}, as long as we do not

"lose instances", t h a t is we must have t h a t S t _c t, S b c b, and S g C_ g for each

g E LHS(C).

This will be the case provided t and b and each element of

LHS(C)

are

monotonic

in % where for example t -- a l __~1 a2 ___~f~l a l (recall t h a t is right-associative) is monotonic in 3' for

all

3' ~ { a l , a2}. A more formal treat- ment of the concept of monotonicity will be given shortly, for now notice t h a t if

3" ~ FV(g)

or if g = 3' then g is monotonic in 3".

T h e rule (boost) expresses t h a t a variable V can be replaced by its "immediate successor" 3"~, and due to the ability to perform transitive reduction this can be strengthened to the requirement t h a t 3"~ must be the "only successor" of V. In addition we must d e m a n d t h a t we do not "lose instances", t h a t is we must have

t h a t

StC_t, SbC_b,

and

S g C g

for each

g E LttS(C).

This will be the case provided t and 3 b and each element of

LHS(C)

are

anti-monotonic

in V, where for example t = s t _~1 c~2 --*~ ~ t is anti-monotonic in 7 for

all

7 ~ {c~1, ill}.

Notice t h a t if each element of

LHS(C)

is anti-monotonic i n V then 7 ~ in fact is the only successor of V.

Example 4.

Let C and t be given by

C = {O/1 C O~2} and t = s t ~ a2. (1)

As t is monotonic in a2, it is possible to apply (shrink) and get

C ~ = 0 a n d t ' ~ a l - - ~ a l . (2)

T h e soundness and completeness of this transformation m a y informally be ar- gued as follows: ( t ) "denotes" the set of types

{tl __,b t2 I 0 F t l C_t2} and b is a behaviour

but this is also the set of types denoted by (2), due to the presence of subtyping.

Notice t h a t since t is anti-monotonic in a l , it is also possible to apply (boost) from (1) and arrive at

C ~ = 0 a n d t p ~ a 2 - - * ~ a2

which modulo renaming is equal to (2).

Example 5.

Let C and t be given by C = {a2_Cal} a n d t = a l --*~ a2.

T h e n neither (shrink) nor (boost) is applicable, as t is not monotonic in a l nor anti-monotonic in a2.

Monotonicity

D e f i n i t i o n 18. Given a constraint set C. We say t h a t a substitution S is increas- ing (respectively decreasing) wrt. C if for all V we have C ~- 3` C_ S 3' (respectively

C~ S~C_~).

We say t h a t a substitution S increases (respectively decreases) g wrt. C whenever C ~- g C_ S g (respectively C ~- S g C g).

We want to define the concepts of monotonicity and anti-monotonicity such t h a t the following result holds:

Actually, the condition that b is anti-monotonic in 3, amounts to 7 ~

FV(b).

Similarly with the requirement on

LHS(C) (as C

is atomic).

L e m m a 19. Suppose t h a t g is monotonic in M17 E

Dom(S);

then if S is increas- ing (respectively decreasing) wrt. C then S increases (respectively decreases) g wrt. C.

Suppose t h a t g is a n t i - m o n o t o n i c in all 7 E

Dom(S);

t h e n if S is increasing (respectively decreasing) wrt. C t h e n S decreases (respectively increases) g wrt.

C.

To this end we m a k e t h e following recursive definition of sets

NA(g)

and

NM(g)

(for "Not Anti-monotonic" and "Not Monotonic"):

NA(7) = {7} a n d

NM(7)

= 0;

N A ( u n i t ) = N A ( i n t ) = N A ( b o o l ) =

NA(O)

= 0;

N M ( u n i t ) = N M ( i n t ) = N M ( b o o l ) =

NM(O)

= 0;

NA(tl _~b

t2) = N M ( t l ) U

NA(b) U NA(t2);

NM(tl

__,b $2) = N A ( Q ) U

NM(b)

U NM(t2);

NA(tl

x t2) =

NA(tl) U

NA(t2) and

NM(Q

x t2) = N M ( t l ) O NM(t2);

NA(t

l i s t ) =

NA(t)

a n d

NM(t

l i s t )

= NM(t);

NA(t

chem) =

NM(t

chart) =

FV(t);

NA(t

corn b) =

NA(*) U NA(b)

and

NM(t

corn b) =

NM(t) U Nm(b);

NA({t

CHAN})

= NM({t

CHAN}) = f V ( t ) ;

NA(bl

U 52) =

NA(bl) U NA(b2)

and

NM(bl U 52) = NM(bl) U NM(b2).

We are now ready to define the concept "is monotonic

in".

D e f i n i t i o n 2 0 . We say t h a t g is monotonic in 7 if 7 ~

NM(g);

a n d we say t h a t g is a n t i - m o n o t o n i c in 7 if 7 ~

NA(g).

F a c t 21. For all types a n d behaviours g, it holds t h a t

NM(g) UNA(g) = FV(g).

(So if g is m o n o t o n i c as well as a n t i - m o n o t o n i c in 7, t h e n 7 r

FV(g).)

I t does not necessarily hold t h a t

NM(g)

a n d

NA(g)

are disjoint (we have e.g.

a C NM(a

chart) M

NA(a

chart)). Now we can prove L e m m a 19:

Proof.

Induction on g, where there are two typical cases:

g is a v a r i a b l e : T h e claims follow from the fact t h a t if g is a n t i - m o n o t o n i c in all 7 E

Dora(S),

t h e n

g ~ Dora(S).

g is a f u n c t i o n t y p e tl ._r t 2 . " First consider the sub-case where g is m o n o t o n i c in all 7 E

Dom(S)

and where S is increasing wrt. C. T h e n 7 E

Dora(S)

gives

7 r NM(tl _~b

t2), a n d we infer t h a t 7 ~

NA(tl), 7 ~ NM(b),

and 7 ~

NM(t2),

so t h a t tl is a n t i - m o n o t o n i c in 7 whereas t2 a n d b are monotonic in 7- We can thus a p p l y the induction hypothesis to infer t h a t S decreases t l wrt. C and t h a t S increases t2 as well as b wit. C. B u t then it is straightforward t h a t S increases g w r t . C.

T h e other sub-cases are similar. []

5.1 T e r m i n a t i o n a n d S o u n d n e s s o f 7~

L e m m a 22. The algorithm ~ always terminates successfully. If T~(C, t, b, A) = (C ~, t/, b t) where C is atomic and t is simple then also C f is atomic and t ~ is simple.

Proof. Termination is ensured since each rewriting step either decreases the num- ber of constraints, or (as is the case for (cycle)) decreases the number of variables without increasing the number of constraints. Each rewriting step trivially pre-

serves atomicity and simplicity. []

Turning to soundness, we first prove an auxiliary result about the rewriting relation:

L e m m a 2 3 . Suppose A F ( C , t , b ) ~(C',t',bt). Then there exists S such that C~ F S C, t / = S t , b ~ = S b, and A = S A .

Proof. For (redund) we can use S = Id and the claim follows from Fact 16. For (cycle) the claim is trivial; and for (shrink) and (boost) the claim follows from the fact that with (V1 _C V2) the "discarded" constraint it holds that (S 9'1 C S 72)

is an instance of reflexivity. []

Using Lemma 2 and Lemma 3 we then get:

C o r o l l a r y 24. Suppose A }- (C, t, b)--~(C', t', b').

If C, A } - e : t & b t h e n C ~ , A } - e : t~ & b I.

By repeated application of this corollary we get the desired result:

L e m m a 25. Suppose that 7~(C, t, b, A) = (C', t', b').

If C, A l- e : t & b then C~, A F e : tt & b/.

5.2 R e s u l t s c o n c e r n i n g C o n f l u e n c e a n d D e t e r m i n i s m No new paths are introduced in the graph by applying ~:

L e m m a 26. Suppose A F (C', t', b') *(C', t ' , b") and let "h, V2 e F V ( C ' ) . Then C ~ F71 ~ * V2 holds iff C'~-71 ~ * V2 holds.

Proof. See Appendix A.

O b s e r v a t i o n 27. Suppose A F- (C, t, b) > (C t, t ~, b t) where the rule (cycle) is not applicable from the configuration (C, t, b). Then the rule (cycle) is not applicable from the configuration (C ~, t ~, b ~) either.

This suggests that an implementation could begin by collapsing all cycles once and for all, without having to worry about cycles again. On the other hand, it is not possible to perform transitive reduction in a separate phase as (redund) may become enabled after applying (shrink) or (boost): as an example consider the situation where C contains the constraints

'70 C_'7, '7 C_'71,

"70 C_ "7', '7' C_ '71

and (redund) is not applicable. By applying (shrink) with the substitution ['7 ~-~ '70]

we end up with the constraints 70 C-'h, "70 C_'7', "7' C_ 71

of which the former can be eliminated by (redund).

Concerning confluency, one would like to show a "diamond property" but this cannot be done in the presence of cycles in the constraint set (especiMly if these contain multiple elements of

FV(A)):

as an example consider the constraints

70 C-7, '70 C_'7', 7C_7', 'Tt C_ 7

with 7, 7' E FV(A); here we can apply (redund) to eliminate either the first or the second constraint but then we are stuck as (cycle) is not applicable and therefore we cannot complete the diamond. As another example, consider the case where we have a cycle containing 70, 71 and 72 with '70, '71 E FV(A). Then we can apply (cycle) to map '72 into either '7o or 71 but then we are stuck and the graphs will be different (due to the arrows to or from '72) unless we devise some notion of graph equivalence.

On the other hand, we have the following result:

Proposition 28. Suppose t h a t A}- (C, t, b)--~(C1, tl, bl) and g~- (C, t, b)---~(C2, t2, b2)

l ' l l

where C is

acyclic

as well as atomic. Then there exists (C~, tl, bl) and (C2, t2, b~), which are equal up to renaming, such t h a t

A F ( C I , t l , bl) .<1(C~, ' . - tl, bl) and ' A F (C2, t2, b 2 ) ><1 (C~, t~, b~)

(here ,<1 denotes t h a t either , or = holds).

Proof.

See Appendix A.

5.3 E x t e n s i o n s o f "R.

In addition to the rewritings presented in Figure 8 one might introduce several other rules, some of which are listed in Figure 9.

The rule Club-exists) allows us to dispense with constraints which state t h a t some behaviours have an upper bound, as long as this upper bound does not occur elsewhere. Notice t h a t a similar rule for types would be invalid, since two types do not necessarily possess an upper bound.

The rules (shrink-chan) and (shrink-empty) extend (shrink) in t h a t they replace a variable fl by its "immediate predecessor" b' even if b' is not a variable:

(lub-exists)

(shrink-than)

(shrink-empty)

Ab-(C(A{bI C_B}(A...LA(b, C~},t,b) ,(C,t,b)

provided fl ~

FV(C,t,b,A) and ~ q~ FV(bl,... ,bn)

A 5 (CU{{t' CHAN} C__ ~}, ~, b)---*(S C, S t, S b) where S = [fl ~-+ {t' CHAN}]

provided f l r

FV(RHS(C), A, t')

and

provided t, b, and each element in

LHS(C)

is monotonic in ~3 and provided that S t is simple

A~-(C,t,b)---~(C',St, Sb)

with C' = {(gl

Cg2) E SC [ gl • 0}

where S = [fl ~-* $] with ~ C

FV(C, t, b)

provided ~ r FV( RHS(C), A) and

provided t, b, and each element in

LHS(C)

is monotonic in fl and provided that S t is simple

Fig. 9. Additional simplifications.

for (shrink-chan) b' is a behaviour {t' CHAN} (where an "occur check" has to be performed), and for (shrink-empty) it is ~ (which is a "trivial predecessor").

For the rules (shrink-chan) and (shrink-empty), we must preserve the sim- plicity of the type and we have explicit clauses for ensuring this; we also must preserve atomicity of the constraint set and therefore rule (shrink-empty) dis- cards all constraints with 0 on the left hand side.

T e r m i n a t i o n a n d s o u n d n e s s

Adding the rules in Figure 9 preserves termination and soundness, as it is easy to see t h a t Lemma 22 and L e m m a 23 still hold: for (shrink-chan) we employ the side condition fl r FV(t'); for (shrink-empty) we employ t h a t ~ is the least behaviour; for (lub-exists) we use S = [fi ~-* bl U . - - U bn] and then employ t h a t U is an upper bound operator, together with the side condition ~ r

FV(bl,..., bn).

Notice, however, t h a t it would no longer hold in general t h a t the substitution S used in L e m m a 23 is simple; so if we were to extend T~ with the rules in Figure 9 we would lose the property t h a t the inference tree "constructed by" the inference algorithm is "simple".

6 E x p e r i m e n t a l R e s u l t s In [11] we considered the program

f n f = > l e t i d = f n y = >

( i f ^{t r u e}

t h e n f

e l s e f n x =>

( s y n c ( s e n d ( c h a n n e l ( ) ,

y));

x));

Y in id id

which demonstrated the power of our inference system relative to some other approaches. Analysing this program with ~ as described in Figure 8, our proto- type implementation produces 4 type constraints and 7 behaviour constraints.

T h e resulting simple type is

((0/44 ~ 0/45) ~ (0/54 ~ 0/5~))

the resulting behaviour is O and the resulting type constraints are 0/44 C 0/45, 0/54 C 0~49 , 0/58 C 0/54, 0/54 C 0/59

and the resulting behaviour constraints are

~20 C ~23, {0/7 CHAN} C__ ~23,

~2o c_ ~25, {(0/5s ~ 0/59) CHA~} C &5,

~20 (Z fl27, {0/49 CHAN} C ~27,

&1 c_ ~33.

R e m a r k . Analysing the program above with a version of Tr which uses only (redund) and (cycle) b u t not (shrink) or (boost), our implementation produces 71 type constraints and 88 behaviour constraints. This shows t h a t it is essential to use a non-trivial version of ~ in order to get readable output. Alternatively, (shrink) and (boost) could be applied only in the top-level call to 142; then the implementation produces a result isomorphic to the one above (4 type constraints and 7 behaviour constraints), but is much slower (due to the need to carry around

a large set of constraints). []

A d d i t i o n a l s i m p l i f i c a t i o n s . This is not quite as informative as we might wish, which suggests t h a t 7s should be extended with the r u l e s i n Figure 9: by applying (lub-exists) repeatedly we can eliminate 6 of the behaviour constraints such t h a t the remaining type and behaviour constraints are

0/44 C__ 0/45, 0/54 C__ 0/49, 0/58 C__ 0/54, 0/54 C__ 0/59, ~31 ~ f~33

and this makes it possible to shrink ;333, a49, and a59 and to boost 0/5s such t h a t we end up with one constraint only:

((0/44 ~o 0/4~) ~ (0/54 ~ 0/54))

where 0/44 ~ 0/45

This is small enough to be manageable and is actually more precise t h a n the type

(~ _ ~ ~)_~0 (~, _~0 ~,)

(and no constraints) t h a t is perhaps closer to what the programmer might have expected.

7 Syntactic Soundness of Algorithm

A main technical property of algorithm W is t h a t it always terminates:

L e m m a 2 9 . W(A, e) and

W'(A, e)

always terminate (possibly with failure). If A is simple t h e n the following holds:

- if W(A, e) = (S, t, b, C) then t and S are simple and C is atomic;

- if

W'(A, e) = (S, t, b, C)

then t and S as well as C are simple;

- all subcalls to W and W ' are made with a simple environment.

Proof.

This result is proved by structural induction in e where for constants we employ Fact 8; to lift the results from W ' to W we employ L e m m a 13 and

L e m m a 22; and throughout we employ Fact 5. []

As a final preparation for establishing soundness of algorithm W we establish a result about our formula for generalisation.

L e m m a 30. Let C be well-formed; then C, A }-e : t & b holds if and only if

C, AF-e : GEN(A,b)(C,t)&=b.

Proof.

See Appendix A.

T h e o r e m 31. If W(A, e) = (S, t, b, C) with A simple then C, S A F- e : t & b.

Proof.

The result is shown by induction in e with a similar result for yyt. See Appendix A for the details.

Note t h a t if the expression e only mentions identifiers in the domain of A (as when e is closed), and t h a t if e only mentions constants for which TypeOf is defined, then the only possible form for failure is due to ~-. We m a y hope (as a weak completeness property) t h a t then also ML typing would have failed.

On the other hand, suppose t h a t W succeeds on some program e; t h a t is we have (with [] the empty environment)

rv([],e)

= ( S , t , b , C )

which by Theorem 31 and L e m m a 29 implies t h a t C, [] }- e : t ~ b with C atomic.

We then have: