Type and Behaviour Reconstruction for Higher-Order Concurrent Programs

Torben Amtoft, Flemming Nielson, Hanne Riis Nielson DAIMI, Aarhus University Ny Munkegade, DK-8000 Århus C, Denmark

                {tamtoft,fn,hrn}@daimi.aau.dk

Abstract: In this paper we develop a sound and complete type and behaviour inference algorithm for a fragment of CML (Standard ML with primitives for concurrency). Behaviours resemble terms of a process algebra and yield a concise presentation of the communications taking place during execution; types are mostly as usual except that function types and “delayed communication types” are labelled by behaviours expressing the communications that will eventually take place. The development of the present paper improves a previously published algorithm in not only achieving a sound algorithm for type inference but also one that is complete, due to an alternative strategy for generalising over types and behaviours. Although we show how to solve special kinds of constraints the problem of a general solution procedure for the constraints generated remains; this is related to an open problem concerning whether all programs typable in Standard ML (with concurrency primitives) are also typable in our system.

1 Introduction

It is well-known that testing can only demonstrate the presence of bugs, never their absence. This has motivated a vast amount of software related activities on guaranteeing statically (that is, at compile-time rather than run-time) that the software behaves in certain ways; a prime example is the formal (and usually manual) verification of software. In this line of activities various notions of type systems have been put forward because these allow static checks of certain kinds of bugs: while at run-time there may still be a need to check for division by zero there will never be a need to check for the addition of booleans and files. As programming languages evolve in terms of features, like module systems and the integration of different programming paradigms, the research on “type systems” is constantly pressed for new problems to be treated.

Our research has been motivated by the integration of the functional and concurrent programming paradigms. Example programming languages are CML [Rep91] that extends Standard ML with primitives for concurrency, Facile [PGM90] that follows a similar approach but more directly contains syntax for expressing CCS-like process composition, and LCS [BS94]. The overall communication structure of such programs may not be immediately clear and hence one would like to find compact ways of recording the communications taking place during execution. One such representation is behaviours, a kind of process algebra expressions.

In [NN93] and [NN94a] inference systems are developed that extend the usual notion of types with a formal way of linking behaviours to the syntax of programs. Applications of such information are demonstrated in [NN94a] and [NN94c].

The question remains: how to implement the inference system, i.e. how to reconstruct the types and behaviours? It seems suitable to use a modified version of algorithm W [Mil78]. This algorithm works by unification, but since our behaviours constitute a non-free algebra (due to the laws imposed on them) this approach is not immediately feasible in our framework. Instead we employ the technique of algebraic reconstruction [JG91, TJ92a]; that is the algorithm unifies the free part of the type structure and generates constraints to cater for the non-free parts.

This idea is carried out in [NN94b], where a reconstruction algorithm is presented which is sound but not complete. The algorithm returns two kind of constraints: C-constraints and S-constraints. The C-constraints represent the “monomorphic” aspects of the analysis whereas the S-constraints are needed to cope with polymorphism: they express that instances of polymorphic variables should remain instances even after applying a solution substitution. Using S-constraints is not a standard tool when analysing polymorphic languages; they seem to be needed because the C-constraints apparently lack a “principal solution property” (a phenomenon well-known in unification theory). Finding \underline{a} solution to C-constraints is feasible as shown in [NN94b]. It is harder to solve S-constraints and in fact they can be seen as a special case of semiunification; the relationship between type inference for polymorphic languages and semiunification is discussed in [Hen93].

The purpose of the present paper is to present a sound and complete reconstruction algorithm. This algorithm also returns S-constraints together with the C-constraints, albeit in a different version than [NN94b]. However, the problem of finding an algorithm for solving these constraints remains.

Overview of paper

In Section 2 we introduce the basic concepts; apart from the treatment of type schemes and from the introduction of S-constraints and from the notion of “downwards closure” they are pretty standard. In Section 3 we present our version of the inference system from [NN94a]. In Section 4 the reconstruction algorithm W is presented. In Section 5 the algorithm is shown to be sound. In Section 6 we motivate our non-standard notion of type schemes, leading to a slightly different (but equivalent) inference system. This inference system allows us to prove the completeness of W in Section 7. In Section 8 we discuss our choice of generalisation strategy for W and compare it to the one used in [NN94b]. Then in Section 9 we show how to solve the constraints generated for some special cases; this solution in effect loses all polymorphism. Section 10 concludes.

2 Preliminaries

CML expressions. Expressions e are built from identifiers x, constants c, applications e_{1} e_{2}, monomorphic abstractions λx.e_{0}, polymorphic abstractions let x=e_{1} in e_{0}, conditionals if e_{0} e_{1} e_{2} and recursive constructs rec f(x) ⇒ e_{0}.

This is much like ML, the concurrent aspects being taken care of by the constants c. Some of these will be listed in Section 3 together with their types. We refer to [NN94a] for a more thorough motivation.

Free and bound variables. We shall employ two kinds of variables, and use γ to range over either kind: behaviour variables β and type variables α. We write fv( ) for the free variables and bv( ) for the bound variables – the definition of these sets is mostly obvious. It is convenient also to define var( ) = fv( )∪bv( ) and to use F to range over sets of free variables.

Substitutions. These are total functions that for each β produces a behaviour b and for each α produces a type t. We use g to range over types and behaviours collectively; similarly the letters ϕ, ψ and θ range over substitutions. The result of applying a substitution ϕ to some entity g is denoted g[ϕ]. The substitution which works by first applying ϕ_{1} and then applying ϕ_{2} is denoted ϕ_{1}; ϕ_{2}. The substitution which maps γ into g and leaves all other variables unchanged is denoted [γ ↦ g]. If γ[ϕ_{1}] = γ[ϕ_{2}] for all γ ∈ F we write ϕ_{1} =^{F} ϕ_{2}. The following standard conventions apply for a substitution ϕ: the domain dom(ϕ) = {γ | γ[ϕ] ≠ γ}; the range ran(ϕ) = {γ | ∃γ′ ∈ dom(ϕ) : γ ∈ fv(γ′[ϕ])}; and fv(ϕ) = dom(ϕ) ∪ ran(ϕ).

Behaviours. Behaviours b are built using the syntax

b ::= β | ϵ | !t | ?t | t CHAN | FORK b | RECβ.b | b_{1}; b_{2} | b_{1} + b_{2}

that is they can be one of the following: a behaviour variable β; the empty behaviour ϵ (no communications take place); an output action !t (a value of type t is sent); an input action ?t (a value of type t is received); a channel action t CHAN (a channel able to transmit values of type t is created); a fork action FORK b (a process with behaviour b is created); a recursive behaviour RECβ.b (where b can “call” itself recursively via β); a sequential composition b_{1}; b_{2} (first b_{1} is performed and then b_{2}); a non-deterministic choice b_{1} + b_{2} (either b_{1} or b_{2} are performed).

For a behaviour b we define bv(b) = ∅ whereas fv(b) is defined such that fv(RECβ.b′) = fv(b′) \ {β}. In other words, the β in RECβ.b′ is considered a “nameless dummy”, i.e. we have some sort of implicit deBruijn-notation. Accordingly we do not distinguish between behaviours which are equivalent modulo alpha-conversion, so RECβ.b is considered identical to RECβ′.b[β ↦ β′] if β′ does not occur in b (in [NN94b, Table 3] this was listed as axiom R2). Thus it makes sense to define (RECβ.b)[ψ] = RECβ.b[ψ] where β ∉ var(ψ).

Just as in [NN94a, Table 3] we impose a preorder ⊒ on behaviours. The intuition behind b_{1}⊒b_{2} is that any action performed by b_{2} can be performed by b_{1} as well (but not necessarily vice-versa). This preorder is listed in Fig. 1, where b_{1}≡b_{2} denotes that b_{1}⊒b_{2} and b_{2}⊒b_{1}.

P1 b⊒b  S1 b_{1}; (b_{2}; b_{3})≡(b_{1}; b_{2}); b_{3}
P2 b_{1}⊒b_{2} ∧ b_{2}⊒b_{3} ⇒ b_{1}⊒b_{3}  S2 (b_{1} + b_{2}); b_{3}≡(b_{1}; b_{3}) + (b_{2}; b_{3})
C1 b_{1}⊒b_{2} ∧ b_{3}⊒b_{4} ⇒ b_{1}; b_{3}⊒b_{2}; b_{4}  E1 b≡ϵ; b
C2 b_{1}⊒b_{2} ∧ b_{3}⊒b_{4} ⇒ b_{1} + b_{3}⊒b_{2} + b_{4} E2 b; ϵ≡b
C3 b_{1}⊒b_{2} ⇒ FORK b_{1}⊒FORK b_{2}  J1 b_{1} + b_{2}⊒b_{1} ∧ b_{1} + b_{2}⊒b_{2}
C4 b_{1}⊒b_{2} ⇒ RECβ.b_{1}⊒RECβ.b_{2}  J2 b⊒b + b
R1 RECβ.b≡b[β ↦ RECβ.b]

Figure 1: The preorder ⊒ on behaviours with equivalence ≡.

Fact 2.1 If b_{1}⊒b_{2} then fv(b_{1}) ⊇ fv(b_{2}), and for any ψ we also have b_{1}[ψ]⊒b_{2}[ψ].

Types. Types t can be either a type variable α, a base type like Int or Bool or Unit, a function type t_{1} →^{b} t_{2} (given a value of type t_{1} a computation is initiated that behaves as indicated by b and that returns a value of type t_{2}), a list type t list, a communication type t com b (if such a communication possibility if activated it behaves as indicated by b and returns a value of type t), or a channel type t chan (a channel able to transmit values of type t).

For all types t we have bv(t) = ∅; so as is the case for behaviours there is no difference between writing fv(t) (fv(b)) and writing var(t) (var(b)).

Type schemes. These are denoted by ts and are of form ∀\overline{F} .t where F are the free variables: to be more precise we have fv(ts) = F and bv(ts) = fv(t) \ F. If F ⊆ fv(t) we say that ts is a kernel type scheme; if this is not necessarily the case we say that ts is an enriched type scheme. For every ts we define a kernel type scheme κ(ts) by ∀\overline{F′}.t where F′ = F ∩ fv(t).

Remark: These definitions are highly non-standard. Although there is a natural bijection between “standard” type schemes (of form ∀γ⃗.t where γ⃗ is the list of bound variables) and kernel type schemes we shall have to deal with enriched type schemes, as will be explained in Section 6.

Further notice that the names of the bound variables do matter; they are not just nameless dummies (as they are recorded in S-constraints): so ∀\overline{∅}.α →ϵ α is not interchangeable with ∀\overline{∅}.α′ →ϵ α′.

Substitutions on type schemes. Given a type scheme ts = ∀\overline{F} .t and a substitution ψ, we define ts[ψ] = ∀\overline{F′}.(t[ψ]) where F′ = var(F [ψ]). With this definition we have

fv(ts[ψ]) = var(fv(ts)[ψ])

but it does not necessarily hold that bv(ts[ψ]) = var(bv(ts)[ψ]); the latter situation arises when β_{1}[ψ] = β_{2}[ψ] where β_{1} ∈ fv(ts) and β_{2} ∈ bv(ts).

Relations on type schemes. We say that t′ is an instance of ∀\overline{F} .t, written ∀\overline{F} .t ≻ t′, iff there exists ψ with dom(ψ) ∩ F = ∅ such that t′ = t[ψ].

Let ts = ∀\overline{F} .t and ts′ = ∀\overline{F′}.t′ be type schemes. We then say that ts is more general than ts′, written ts ⪰ ts′, iff t = t′ and F ⊆ F′. Notice that this is a more “syntactic” (and more restrictive) definition than is standard in the literature; we have chosen the current definition to simplify some proofs later.

Fact 2.2 Suppose ts ⪰ ts′ and that ts′ ≻ t′. Then also ts ≻ t′.

Substitution relations. Stating that ∀\overline{F} .t ≻ t′ amounts to specifying what the bound variables of t (i.e. those not in F) are instantiated to. This motivates the introduction of substitution relations, of form ∀\overline{F} .g⃗ ≻ g⃗′ where one can think of g⃗ as the bound variables. Such a relation will hold iff there exists ψ with dom(ψ) ∩ F = ∅ such that g⃗′ = g⃗[ψ]. Notice that with fv(g⃗′′) = F the relation will hold iff ∀\overline{∅}.(g⃗g⃗′′) ≻ (g⃗′g⃗′′); hence substitution relations can be represented as semi-unification problems (at the cost of losing some structure). We shall refrain from doing so, however, since semi-unification is undecidable in general and it is unclear if our problem is a general semi-unification problem.

Environments. An environment E is a list of the form [[x_{1} : ts_{1}] … [x_{n} : ts_{n}]] (the x_{i}’s not necessarily distinct). We shall often write a type t_{i} in place of an ts_{i}: this is a short hand for ∀\overline{F_{i}}.t_{i} where F_{i} = fv(t_{i}).

We say that E(x) = s if s = s_{i} for an i satisfying that x = x_{i} and that x ≠ x_{j} for all j > i (in other words we look up in E by searching from the right). The result of updating E with [x : s], to be written E ⊕ [x : s], is the environment [[x_{1} : s_{1}] … [x_{n} : s_{n}][x : s]].

We shall feel free to use the relations and predicates on type schemes also on environments; as an example we say that E is a kernel environments if s_{i} is a kernel type scheme for all i ∈ {1 … n}.

Constraints. There are two kinds of constraints c:

• C-constraints (for \underline{c}ontainment), of form b_{1} ˙⊒b_{2}. This constraint is satisfied iff b_{1}⊒b_{2}. The result c[ψ] of applying a substitution ψ to this constraint is b_{1}[ψ] ˙⊒b_{2}[ψ];

• S-constraints (for \underline{s}ubstitutions), of form ∀\overline{F} .g⃗_{1} ˙≻ g⃗_{2}. This constraint is satisfied iff the substitution relation ∀\overline{F} .g⃗_{1} ≻ g⃗_{2} holds. The result c[ψ] of applying a substitution ψ to this constraint is ∀\overline{F′}.g⃗_{1}[ψ] ˙≻ g⃗_{2}[ψ] where F′ = var(F [ψ]).

If c[ψ] is satisfied we say that ψ satisfies c and write ψ ⊧ c. Notice that if ψ ⊧ c then also ψ; ϕ ⊧ c if c is a C-constraint (by Fact 2.1), but not necessarily if c is an S-constraint – this fact is a major obstacle for solving constraints “sequentially” as we shall see in Section 9. Further notice that ψ; ϕ ⊧ c holds iff ϕ ⊧ c[ψ].

The capital letter C ranges over lists of constraints and we say that ψ ⊧ C iff ψ ⊧ c holds for all elements c of C. The concatenation of C_{1} and C_{2} is written as C_{1}⊕C_{2}. The reason for choosing lists rather than sets is that this extra structure makes it possible to formulate some properties of the constraints generated by the reconstruction algorithm – due to space limits this line will not be pursued further in the present paper.

Principal solutions to C-constraints. With the ordering on behaviours axiomatised in Fig. 1 there seems to be no notion of “principal solutions” to Cconstraints. For an example of this, consider the constraint β⊒β; !Int; !Int. The substitution ψ_{1} which maps β into RECβ.(β; !Int; !Int) as well as the substitution ψ_{2} which maps β into RECβ.(β; !Int) will satisfy this constraint; but using the axiomatisation in Fig. 1 it seems hard to find a sense in which ψ_{1} and ψ_{2} are comparable.

A remedy, inspired by [CC91] where a similar observation is made concerning recursive types, might be to consider RECβ.b equivalent to its infinite unfolding (cf. rule R1 in Fig. 1 which states that RECβ.b is equivalent to its finite unfoldings). It is not yet clear whether such a change in the axiomatisation will be sufficient to gain some notion of principality.

Downwards closure. Given a set of variables F and a list of constraints C we define the downwards closure of F with respect to C, written F^{C}, as the smallest set F′ such that F ⊆ F′ and such that whenever β ˙⊒b ∈ C and β ∈ F′ then also fv(b) ⊆ F′. It is easy to see that F^{C} can be computed constructively.

A brief motivation: think of the variables in F as the “non-polymorphic” ones; i.e. those the reconstruction algorithm is not allowed to “make copies of”. Then if β ˙⊒b ∈ C with β ∈ F also the variables in b should be non-polymorphic. We shall elaborate on this in Section 8; more formally we have the following result which is a consequence of Fact 2.1:

Fact 2.3 If ψ ⊧ C then fv(F [ψ]) = fv(F^{C}[ψ]).

3 The type and behaviour inference system

In Fig. 2 we list (part of) the inference system for which we are going to present a reconstruction algorithm. A judgement is of the form E ⊢ e : t & b and says that in (kernel) environment E one can infer that expression e has type t and behaviour b.

For constants a function CTypeOf() is employed, assigning an extended type scheme to each constant. An extended type scheme ts is of form ∀\overline{∅}.(t, C) (so fv(ts) = ∅). Consistent with previous definitions we say that t′ is an instance of ∀\overline{∅}.(t, C), written ∀\overline{∅}.(t, C) ≻ t′, iff there exists ψ such that t′ = t[ψ] and such that ψ ⊧ C. The value of CTypeOf() on some constants is tabulated below (adopted from [NN94b, Table 4]).

CTypeOf(+)  = ∀\overline{∅}.(Int →^{β_{1}} Int →^{β_{2}} Int, [β_{1}⊒ϵ, β_{2}⊒ϵ])
CTypeOf(sync)  = ∀\overline{∅}.((α com β_{1}) →^{β_{2}} α, [β_{2}⊒β_{1}])
CTypeOf(send)  = ∀\overline{∅}.(α chan × α →^{β_{1}} α com β_{2}, [β_{1}⊒ϵ, β_{2}⊒!α])
CTypeOf(receive) = ∀\overline{∅}.(α chan →^{β_{1}} α com β_{2}, [β_{1}⊒ϵ, β_{2}⊒?α])
CTypeOf(channel) = ∀\overline{∅}.(Unit →^{β} α chan, [β⊒α CHAN])
CTypeOf(fork)  = ∀\overline{∅}.((Unit →^{β_{1}} α) →^{β_{2}} Unit, β_{2}⊒FORK β_{1})

The inference system is much as in [NN94a], but there are the following differences: (i) we use the non-standard notation for type schemes that was introduced in Section 2; (ii) we have removed regions from behaviours; (iii) we

E ⊢ x : t & b  if E(x) ≻ t and b⊒ϵ
E ⊢ c : t & b  if CTypeOf(c) ≻ t and b⊒ϵ
\frac{E ⊢ e_{1} : t_{1} & b_{1}, E ⊢ e_{2} : t_{2} & b_{2}}{E ⊢ e_{1} e_{2} : t & b}  if t_{1} = t_{2} →^{b_{0}} t and b⊒b_{1}; b_{2}; b_{0}

\frac{E ⊕ [x : t_{1}] ⊢ e_{0} : t_{0} & b_{0}}{E ⊢ λx.e_{0} : t & b}  if t = t_{1} →^{b_{0}} t_{0} and b⊒ϵ

\frac{E ⊢ e_{1} : t_{1} & b_{1}, E ⊕ [x : ∀\overline{F} .t_{1}] ⊢ e_{0} : t & b_{0}}{E ⊢ let x=e_{1} in e_{0} : t & b} if b⊒b_{1}; b_{0}

where F = (fv(E) ∪ fv(b_{1})) ∩ fv(t_{1})

Figure 2: Selected parts of the type and behaviour inference system.

avoid coding the constraints present in the definition of CTypeOf() into the types (as in TypeOf of [NN94a]).

Example 3.1 Consider the following CML-program map2, a version of the well-known map function where a process is forked for each tail while the forking process itself works on the head. A rather informal notation is employed; for instance we write e_{1}; e_{2} as an abbreviation for (λd.e_{2}) e_{1}.

rec mp2(f) ⇒ λxs.if xs = [] then []

else let ch = channel ()

in fork (λd.(sync (send ⟨ch,mp2 f (tail xs)⟩))); cons (f (head xs)) (sync (receive ch))

We expect to have ∅ ⊢ map2 : ((α_{1} →^{β_{1}} α_{2}) →ϵ (α_{1} list →^{β_{2}} α_{2} list)) & ϵ where β_{2} = RECβ.(ϵ + ((α_{2} list) CHAN; FORK (β; !(α_{2} list)); β_{1}; ?(α_{2} list))).

We now list some properties of the inference system (the latter due to Fact 2.2):

Fact 3.2 Suppose E ⊢ e : t & b and b′⊒b. Then also E ⊢ e : t & b′.

Fact 3.3 Let E and E′ be kernel environments with E′ ⪰ E. Suppose that E ⊢ e : t & b. Then also E′ ⊢ e : t & b.

4 A reconstruction algorithm

Our goal is to produce an algorithm which works in the spirit of the well-known algorithm W [Mil78]. Hence we have to perform unification over types; but in order to unify t_{1} →^{b} t_{2} with t′_{1} →^{b′} t′_{2} we have to unify b and b′, and if for example b = b_{1}; b_{2} and b′ = b′_{1}; b′_{2} this cannot always be done “compositionally” by first unifying b_{1} with b′_{1} and then unifying b_{2} with b′_{2} – for then we will lose the possibility that say b_{1} = b′_{2} = ϵ and b′_{1} = b_{2} = !Int.

The remedy (as done in [TJ92a] and [NN94b] but not in [JG91] where no unification is performed) is to introduce the notion of simplicity: a type is simple if all the behaviours it contains are behaviour variables (so t_{1} →^{b} t_{2} is simple iff t_{1} and t_{2} are both simple and b = β for some β); a behaviour is simple if all the types it contains are simple (so e.g. !t is simple iff t is simple) and if it does not contain sub-behaviours of form RECβ.b; a C-constraint is simple if it is of form β ˙⊒b with b simple; an S-constraint is simple if it is of form ∀\overline{F} .(t⃗β⃗) ˙≻ (t⃗′β⃗′), with t and t′ simple types^{1}; a substitution is simple if it maps type variables into simple types and maps behaviour variables into behaviour variables (rather than simple behaviours).

Fact 4.1 Let t be a simple type; let b be a simple behaviour; let C be a list of simple constraints; and let ϕ and ϕ′ be simple substitutions. Then t[ϕ] is a simple type; b[ϕ] is a simple behaviour; C[ϕ] is a list of simple constraints; and ϕ; ϕ′ is a simple substitution.

We can now define a procedure UNIFY which takes two simple types t_{1} and t_{2} and returns the most general unifier if one unifier exists – otherwise UNIFY fails. Some of the more interesting clauses of UNIFY are listed below:

UNIFY(α, t) = θ  iff  θ = [α ↦ t] and (t = α or α ∉ fv(t))

UNIFY(t_{1} com β_{1}, t_{2} com β_{2}) = θ iff UNIFY(t_{1}, t_{2}) = θ′ and β′_{1} = β_{1}[θ′] and β′_{2} = β_{2}[θ′]

and θ = θ′; [β′_{1} ↦ β′_{2}]

Lemma 4.2 Let t_{1} and t_{2} be simple types. First suppose that UNIFY(t_{1}, t_{2}) = θ. Then θ is simple and t_{1}[θ] = t_{2}[θ].

Conversely assume that t_{1}[ϕ] = t_{2}[ϕ]. Then UNIFY(t_{1}, t_{2}) succeeds with result θ; and there exists ϕ′ such that ϕ = θ; ϕ′.

We are now ready to define the reconstruction algorithm W, as is done in Figure 3. The algorithm fails if and only if a call to UNIFY fails.

The most interesting cases are the ones for identifiers and for polymorphic abstractions:

An identifier x is looked up in the environment and fresh copies γ⃗′ of the bound variables γ⃗ of their type schemes are generated. Moreover, it is recorded (via an S-constraint) that a solution should map γ⃗′ to an instance of what γ⃗ is mapped into in such a way that it does not interfere with the free variables.

For a polymorphic abstraction let x=e_{1} in e_{0} the algorithm first finds the type t_{1} and behaviour b_{1} of e_{1}; then e_{0} is analysed in an environment where x is bound to a type scheme with type part t_{1}. The free variables of the type scheme (i.e. the non-polymorphic ones) are built from those which are free in the environment together with those which are free in b_{1}. This corresponds

1In fact it holds that t will be of form α⃗ for all simple S-constraints produced by W.

W (x, E) = (t, ϵ, C, id) W (e_{1} e_{2}, E) = (t, b, C, θ)

iff E(x) = ∀\overline{F_{x}}.t_{x} iff W (e_{1}, E) = (t_{1}, b_{1}, C_{1}, θ_{1}) and γ⃗ = fv(t_{x}) \ F_{x} and W (e_{2}, E[θ_{1}]) = (t_{2}, b_{2}, C_{2}, θ_{2}) and γ⃗′ are fresh copies of γ⃗ and α and β_{0} are fresh and t = t_{x}[γ⃗ ↦ γ⃗′] and UNIFY(t_{1}[θ_{2}], t_{2} →^{β_{0}} α) = θ_{0} and C = [∀\overline{F_{x}}.γ⃗ ˙≻ γ⃗′] and t = α[θ_{0}]

and b = b_{1}[θ_{2}; θ_{0}]; b_{2}[θ_{0}]; β_{0}[θ_{0}]

W (c, E) = (t, ϵ, C, id) and C = C_{1}[θ_{2}; θ_{0}]⊕C_{2}[θ_{0}]

iff CTypeOf(c) = ∀\overline{∅}.(t_{c}, C_{c}) and θ = θ_{1}; θ_{2}; θ_{0} and γ⃗ = fv(t_{c}) ∪ fv(C_{c}) and γ⃗′ are fresh copies of γ⃗ W (let x=e_{1} in e_{0}, E) = (t, b, C, θ) and t = t_{c}[γ⃗ ↦ γ⃗′] iff W (e_{1}, E) = (t_{1}, b_{1}, C_{1}, θ_{1}) and C = C_{c}[γ⃗ ↦ γ⃗′] and W (e_{0}, E[θ_{1}] ⊕ [x : ∀\overline{N Q}.t_{1}])

= (t_{0}, b_{0}, C_{0}, θ_{0})

W (λx.e_{0}, E) = (t, ϵ, C, θ) and t = t_{0}

iff α_{1} and β_{0} are fresh and b = b_{1}[θ_{0}]; b_{0} and W (e_{0}, E ⊕ [x : α_{1}]) and C = C_{1}[θ_{0}]⊕C_{0}

= (t_{0}, b_{0}, C_{0}, θ_{0}) and θ = θ_{1}; θ_{0} and t = α_{1}[θ_{0}] →^{β_{0}} t_{0} where N Q = (fv(E[θ_{1}]) ∪ fv(b_{1}))^{C_{1}} and C = C_{0}⊕[β_{0} ˙⊒b_{0}] and θ = θ_{0}

Figure 3: Selected clauses of Algorithm W.

to the inference system in Fig. 2, but notice the following differences: (a) in contrast to the inference system the algorithm does not intersect with fv(t_{1}) and thus an enriched type scheme is generated; (b) the algorithm takes the downwards closure with respect to the constraints C_{1}. We shall elaborate upon the former point in Section 6 and upon the latter point in Section 8.

Fact 4.3 Suppose that W (e, E) = (t, b, C, θ) where the types in E are simple. Then t is a simple type, b is a simple behaviour, C is a list of simple constraints, and θ is a simple substitution.

5 Soundness of algorithm W

We are now going to prove that the algorithm is sound; this means that a solution to the constraints gives rise to a valid inference in the inference system of Figure 2.

Theorem 5.1 Suppose that W (e, ∅) = (t, b, C, θ) and suppose that ψ is such that ψ ⊧ C and t′ = t[ψ] and b′⊒b[ψ]. Then it holds that ∅ ⊢ e : t′ & b′.

This theorem follows easily from Fact 3.2 and the following proposition that allows a proof by induction:

Proposition 5.2 Suppose that W (e, E) = (t, b, C, θ). Then for all ψ such that ψ ⊧ C we have κ(E[θ][ψ]) ⊢ e : t[ψ] & b[ψ]. (Recall that W deals with enriched environments whereas the inference system of Figure 2 deals with kernel environments.)

Proof: We perform induction on e; to conserve space we use the same terminology as in the definition of the relevant clause for W. There are seven cases; here we shall list the two most interesting ones only.

The case W (x, E): Let F′ = var(F_{x}[ψ]) and let F′_{x} = F′ ∩ fv(t_{x}[ψ]). Our aim is to show that κ(E[ψ])(x) ≻ t[ψ], which amounts to

∀\overline{F′_{x}}.(t_{x}[ψ]) ≻ t_{x}[γ⃗ ↦ γ⃗′][ψ].  (1)

Since ψ ⊧ C we have ∀\overline{F′}.γ⃗[ψ] ≻ γ⃗′[ψ]; so there exists a ϕ′ with dom(ϕ′)∩F′ = ∅ such that ψ; ϕ′ =^{γ⃗} [γ⃗ ↦ γ⃗′]; ψ. This implies, since var(t_{x}) ⊆ γ⃗ ∪ F_{x}, that we

even have ψ; ϕ′ {var(t_{x}) \atop =} [γ⃗ ↦ γ⃗′]; ψ. But this shows that (1) holds, with ϕ′ as the “instance substitution”.

The case W (let x=e_{1} in e_{0}, E): First a remark: the only property of N Q we shall exploit is the following which is a consequence of Fact 2.3 (the condition may seem superfluous but is added to make (2) and (5) dual):

ψ ⊧ C_{1} implies var(N Q[ψ]) ⊇ var(fv(E[θ_{1}])[ψ]) ∪ var(b_{1}[ψ]).  (2)

First observe that θ_{0}; ψ ⊧ C_{1}; so we can apply the induction hypothesis on the call W (e_{1}, E) and the substitution θ_{0}; ψ to get

κ(E[θ][ψ]) ⊢ e_{1} : t_{1}[θ_{0}; ψ] & b_{1}[θ_{0}; ψ].

Since ψ ⊧ C_{0} we can apply the induction hypothesis on the call W (e_{0}, E[θ_{1}] ⊕ [x : …]) and the substitution ψ to get

κ(E[θ][ψ]) ⊕ [x : ∀\overline{F′}.(t_{1}[θ_{0}; ψ])] ⊢ e_{0} : t_{0}[ψ] & b_{0}[ψ]

where F′ = fv(N Q[θ_{0}; ψ]) ∩ fv(t_{1}[θ_{0}; ψ]).

Let F′′ = (fv(κ(E[θ][ψ])) ∪ fv(b_{1}[θ_{0}; ψ])) ∩ fv(t_{1}[θ_{0}; ψ]). Applying (2) on the substitution θ_{0}; ψ tells us that F′′ ⊆ F′ so by Fact 3.3 we infer that

κ(E[θ][ψ]) ⊕ [x : ∀\overline{F′′}.t_{1}[θ_{0}; ψ]] ⊢ e_{0} : t_{0}[ψ] & b_{0}[ψ].

This shows that we have the desired judgment

κ(E[θ][ψ]) ⊢ let x=e_{1} in e_{0} : t_{0}[ψ] & b[ψ].

6 The need for enriched type schemes

Enriched type schemes in algorithm W. The reconstruction algorithm from [NN94b] carries constraints around, together with type schemes in kernel form. Our algorithm carries no constraints in the environment, but in order to preserve soundness the type schemes have to be enriched. This is informally illustrated by the following example.

Let e = let x=e_{1} in e_{0} and suppose that W (e_{1}, E) = (t_{1}, b_{1}, C_{1}, θ_{1}) where t_{1} = Unit →^{β} Unit and where C_{1} contains the constraint β ˙⊒!α, where α ∈ fv(E). The intuitive interpretation of this is that when analysing e_{0}, β is a polymorphic variable with a non-polymorphic subpart α. Thus β cannot be instantiated freely; hence the need to carry α around in the environment (via the type scheme ∀\overline{\{α\}}.t_{1}).

Enriched type schemes in the completeness proof. It turns out to be hard to give a direct proof of the completeness of W with respect to the inference system of Fig. 2, due to the fact that for inferences in this system it does not necessarily hold that “bound variables are unique” (space limits prevent us from giving a more precise definition and/or an example of this phenomenon). We shall alleviate this by presenting an alternative (but equivalent) inference system having the aforementioned property:

An enriched inference system. Inferences are of form E ⊢_{2} e : t & b, where E is an enriched environment. The system is as in Fig. 2, except that the rule for polymorphic abstraction is as follows:

\frac{{E ⊢_{2} e_{1} : t_{1} & b_{1} \atop E ⊕ [x : ∀\overline{F} .t_{1}] ⊢_{2} e_{0} : t & b_{0}}}{E ⊢_{2} let x=e_{1} in e_{0} : t & b} if F = fv(E) ∪ fv(b_{1}) and b⊒b_{1}; b_{0}. (3)

The two inference systems are equivalent in the following sense:

Theorem 6.1 ∅ ⊢ e : t & b holds iff ∅ ⊢_{2} e : t & b holds.

This is a consequence of the following two propositions:

Proposition 6.2 Suppose E ⊢_{2} e : t & b. Then also κ(E) ⊢ e : t & b.

Proposition 6.3 Suppose E ⊢ e : t & b and that κ(E′) = E. Then also E′ ⊢_{2} e : t & b.

7 Completeness of algorithm W

We are now in a position to prove that algorithm W is complete: if there exists a valid inference then the algorithm will produce a set of constraints that can be satisfied.

Theorem 7.1 Suppose ∅ ⊢ e : t′ & b′. Then W (e, ∅) = (t, b, C, θ) and there exists a ψ such that ψ ⊧ C and t′ = t[ψ] and b′⊒b[ψ].

Notice the symmetry with Theorem 5.1. The theorem follows easily from Theorem 6.1 and the following proposition that admits a proof by induction:

Proposition 7.2 Suppose E′ ⊢_{2} e : t′ & b′ and E[ϕ] ⪰ E′. Then W (e, E) =

(t, b, C, θ) and there exists a ψ such that θ; ψ {var(E) \atop =} ϕ and ψ ⊧ C and t[ψ] = t′ and b′⊒b[ψ].

Proof: Induction on the derivation tree for E′ ⊢_{2} e : t′ & b′; to conserve space we use the same terminology as in the definition of the relevant clause for W and we write e.g. ψ =^{E} ϕ instead of ψ =^{F} ϕ where F = var(E). There are seven cases; here we shall list the two most interesting ones only.

The case e = x: Suppose E′ ⊢_{2} x : t′ & b′ holds because E′(x) = ∀\overline{F′_{x}}.t′_{x}, because t′ = t′_{x}[ϕ′] with dom(ϕ′) ∩ F′_{x} = ∅, and because b′⊒ϵ.

Since E[ϕ] ⪰ E′ it holds that t_{x}[ϕ] = t′_{x} (thanks to our syntactic definition of ⪰ ) and that var(F_{x}[ϕ]) ⊆ F′_{x}. From this we infer that

dom(ϕ′) ∩ var(F_{x}[ϕ]) = ∅.  (4)

Now define ψ as follows: it maps γ⃗′ into γ⃗[ϕ; ϕ′]; and otherwise it behaves like ϕ. This ensures that θ; ψ =^{E} ϕ; and it is trivial that b′⊒b[ψ].

For our remaining claims, observe that due to (4) we have

[γ⃗ ↦ γ⃗′]; ψ =^{γ⃗∪F_{x}} ψ; ϕ′ with dom(ϕ′) ∩ fv(F_{x}[ψ]) = ∅

showing that ∀\overline{F_{x}[ψ]}.γ⃗[ψ] ≻ γ⃗′[ψ] implying ψ ⊧ C; and that (since var(t_{x}) ⊆ F_{x} ∪ γ⃗) t[ψ] = t_{x}[[γ⃗ ↦ γ⃗′]; ψ] = t_{x}[ψ; ϕ′] = t_{x}[ϕ; ϕ′] = t′_{x}[ϕ′] = t′.

The case e = let x=e_{1} in e_{0}: First a remark: the only property of N Q we shall exploit is the following:

ψ ⊧ C_{1} implies var(N Q[ψ]) ⊆ var(fv(E[θ_{1}])[ψ]) ∪ var(b_{1}[ψ]).  (5)

Notice the duality between (2) and (5); and notice that the conjunction of these two is a consequence of Fact 2.3.

Some terminology: we define V_{1} = var(t_{1}, b_{1}, C_{1}, θ_{1}) and V_{0} = var(t_{0}, b_{0}, C_{0}, θ_{0}) and V_{e} = var(E[θ_{1}]) ∪ N Q ∪ fv(t_{1}); and say that a variable is “internal” if it occurs in V_{1} but not in V_{e}. We can assume that no internal variable occurs in V_{0}.

Suppose E′ ⊢_{2} let x=e_{1} in e_{0} : t′ & b′ because of E′ ⊢_{2} e_{1} : t′_{1} & b′_{1} and of F′ = fv(E′) ∪ fv(b′_{1}) and of E′ ⊕ [x : ∀\overline{F′}.t′_{1}] ⊢_{2} e_{0} : t′ & b′_{0} and because of b′⊒b′_{1}; b′_{0}. By induction we see that W (e_{1}, E) succeeds and that there exists ψ_{1} such that θ_{1}; ψ_{1} =^{E} ϕ, such that ψ_{1} ⊧ C_{1}, such that t_{1}[ψ_{1}] = t′_{1}, and such that b′_{1}⊒b_{1}[ψ_{1}]. It holds that

var(N Q[ψ_{1}]) ⊆ F′

for by (5) we have var(N Q[ψ_{1}]) ⊆ var(fv(E[θ_{1}])[ψ_{1}])∪var(b_{1}[ψ_{1}]), by assumption we have var(fv(E[θ_{1}])[ψ_{1}]) = fv(E[θ_{1}][ψ_{1}]) = fv(E[ϕ]) ⊆ fv(E′), and by Fact 2.1 we have fv(b_{1}[ψ_{1}]) ⊆ fv(b′_{1}).^{2} Using the above observation it is straightforward to verify that

2It is not possible to replace this subset inclusion by set equality. This is the motivation for making E[ϕ] ⪰ E′ (and not E[ϕ] = E′) be part of the induction hypothesis.

(E[θ_{1}] ⊕ [x : ∀\overline{N Q}.t_{1}])[ψ_{1}] ⪰ E′ ⊕ [x : ∀\overline{F′}.t′_{1}]

so by induction we see that W (e_{0}, ) succeeds and that there exists ψ_{0} such that θ_{0}; ψ_{0} =^{V_{e}} ψ_{1}, such that ψ_{0} ⊧ C_{0}, such that t_{0}[ψ_{0}] = t′ and such that b′_{0}⊒b_{0}[ψ_{0}].

Now define ψ to behave as ψ_{0} except that is behaves as ψ_{1} on internal variables. We have the following relations:

ψ =^{V_{0}} ψ_{0} and θ_{0}; ψ =^{V_{1}∪V_{e}} ψ_{1}  (6)

where the second part follows from the following reasoning: if γ is internal then γ[θ_{0}; ψ] = γ[ψ] = γ[ψ_{1}]; and if γ is not internal (and hence belongs to V_{e}) then γ[θ_{0}] does not contain any internal variables so γ[θ_{0}; ψ] = γ[θ_{0}; ψ_{0}] = γ[ψ_{1}].

Using (6) enables us to infer the desired properties of ψ: (i) if γ ∈ var(E) then γ[θ; ψ] = γ[θ_{1}][θ_{0}; ψ] = γ[θ_{1}][ψ_{1}] = γ[ϕ]; (ii) ψ ⊧ C holds because ψ ⊧ C_{1}[θ_{0}] (which follows from ψ_{1} ⊧ C_{1}) and because C_{0}[ψ] = C_{0}[ψ_{0}]; (iii) t[ψ] = t_{0}[ψ_{0}] = t′; (iv) we infer that b′⊒b′_{1}; b′_{0}⊒b_{1}[ψ_{1}]; b_{0}[ψ_{0}] = b_{1}[θ_{0}][ψ]; b_{0}[ψ] = b[ψ].

8 Choice of generalisation strategy

In this section we shall discuss alternative ways of defining the entity N Q occurring in Figure 3 (the clause for polymorphic abstractions). Recall that N Q satisfies the following property:

β ˙⊒b ∈ C_{1} and β ∈ N Q implies fv(b) ⊆ N Q

stating that if a variable is not polymorphic then neither of its “subparts” can be polymorphic. We now consider two variations on this theme.

8.1 An algorithm not taking the downwards closure

First define a version of W, to be called W^{n} for \underline{n}o closure, where simply N Q = fv(E[θ_{1}]) ∪ fv(b_{1}). It is trivial that (2) and (5) still hold and hence W^{n} will be sound as well as complete. On the other hand, failures are reported at a later stage as witnessed by the expression e = let ch=channel () in e_{1} where in e_{1} an integer as well as a boolean is transmitted over the newly generated channel ch. W^{n} applied to e will terminate successfully and return constraints including the following

[β ˙⊒α CHAN, ∀\overline{\{β\}}.α ˙≻ Bool, ∀\overline{\{β\}}.α ˙≻ Int]

which are easily seen to be unsolvable; whereas W applied to e will fail immediately (since α is considered a non-polymorphic variable and hence is not copied, causing UNIFY to fail). So it seems that W should be preferred to W^{n} on the basis that failures should be reported as early as possible.

Note that e above can be typed if ch is assigned the type scheme ∀\overline{∅}.α chan but cannot be typed if ch is assigned the type scheme ∀\overline{\{α\}}.α chan. The former case will arise if α chan is handled as α list; whereas the latter case will arise if α chan is handled by the techniques for α ref developed in [TJ92b] and [BD93].

8.2 An algorithm taking the upwards closure

Next define a version of W, to be called W^{ud} for \underline{u}pwards and \underline{d}ownwards closure, where N Q is defined in such a way that

β ˙⊒b ∈ C_{1} and (fv(b) ∪ {β}) ∩ N Q ≠ ∅ implies (fv(b) ∪ {β}) ⊆ N Q

which in effect states that in order for a variable to be polymorphic, all of its “subparts” should be polymorphic as well. As we shall see this approach to separating polymorphic and non-polymorphic variables is too strong. On the positive side (2) still holds so W^{ud} is sound. On the negative side (5) does not hold; in fact completeness fails because we have found a well-typed expression upon which W^{ud} does not succeed.

The algorithm presented in [NN94b] essentially works similar to W^{ud}.

9 Solving the constraints

In this section we discuss how to solve the constraints generated by Algorithm W. As stated in Fact 4.3, the C-constraints are of form β ˙⊒b and the S-constraints are of form ∀\overline{F} .t⃗β⃗ ˙≻ t⃗′β⃗′ (where actually, among other things, t⃗ is of form α⃗ and where α⃗ as well as β⃗ are disjoint variables). The right hand sides of the C-constraints may be quite lengthy, for instance they will often involve sub-behaviours of form ϵ; ϵ; …, but we have implemented an algorithm that applies the behaviour equivalences from Fig. 1 so as to decrease the size of behaviours significantly (in most cases).

Solving constraints sequentially. Given a set of constraints C, a natural way to search for a substitution ψ that satisfies C is to proceed sequentially:

• if C is empty, let ψ = id;

• otherwise, let C be the disjoint union of C′ and C′′. Suppose we can find ψ′ which solves C′. Next suppose we (recursively) can find ψ′′ which solves C′′[ψ′]. Then return ψ = ψ′; ψ′′.

It is easy to see that ψ ⊧ C provided C′[ψ′] is such that for all ϕ we have ϕ ⊧ C′[ψ′]. This will be the case if C′[ψ] only contains C-constraints (due to Fact 2.1) and S-constraints of form ∀\overline{F} .g⃗ ˙≻ g⃗, the latter kind to be denoted S-equalities. So we arrive at the following (informally specified) condition:

S-constraints are not solved unless they become S-equalities.  (7)

Moreover, we have the following (also informally specified) condition:

applying ψ′ to C′′ should preserve any “nice structure” that C′′ has. (8)

Some constraints we know how to solve. If C is a list of constraints, such that all S-constraints in C are of form ∀\overline{F} .(α⃗, β⃗) ˙≻ (α⃗′, β⃗′), we can apply the scheme for sequential solution outlined in the preceding section (we shall not deal with other kinds of S-constraints even though some of those might have simple solutions as well).

First we convert the S-constraints into S-equalities, cf. (7). This is done by identifying all type and behaviour variables occurring in “corresponding positions” (thus going from a polymorphic world into a monomorphic world).

Next we have to solve the C-constraints sequentially; and the invariant to be preserved during this process (cf. (8)) is that they should be of form β ˙⊒b (where b is no longer assured to be a simple behaviour, as it may contain recursion). It is easy to see that this invariant will be maintained provided we can solve a constraint set of the form {β ˙⊒b_{1}, …, β ˙⊒b_{n}} by means of a substitution whose domain is {β}. But this can easily be achieved, due to rule R1 in Figure 1: just map β into RECβ.b_{1} + … + b_{n} (if β does not occur in the b_{i}’s, we can omit the recursion). This is also the way that C-constraints are solved in [NN94b].

10 Conclusion

In this paper we have adapted the traditional algorithm W to our type and behaviour system. The algorithm has been implemented and has provided quite illuminating analyses of example CML programs.

One difference from the traditional formulation of W is that we generate so-called C-constraints that then have to be solved. This is a consequence of our behaviours being a non-free algebra and is an phenomenon found also in [JG91].

Another and major difference from the traditional formulation, as well as that of [JG91], is that we generate so-called S-constraints that also have to be solved. This phenomenon is needed because our C-constraints would seem not to have principal solutions (as was discussed in Section 2). This in not the case for the traditional “free” unification of Standard ML, but it is a phenomenon well-known in unification theory [Sie89]. As a consequence we have to ensure that the different solutions to the C-constraints (concerning the polymorphic definition and its instantiations) are comparable and this is the purpose of the S-constraints. At present it is an open problem how hard it is to solve Sconstraints in the presence of C-constraints and whether it is as hard as general semi-unification (which is undecidable). This problem is closely related to the question of whether all expressions typeable in (C)ML are also typable in our system. More precisely consider an expression e that is typeable in Standard ML when types α chan are handled by the techniques for α ref developed in [TJ92b]; the (open) question then is whether this expression is always typeable in our system. If this should ever fail it means that the causality espressed in the behaviours constitute an unwarranted restriction upon the language.

Future work will show how to overcome these problems. One avenue of research is to extend our axiomatization of ⊒ such that principal solutions exist; perhaps by identifying recursive behaviours with their infinite unfolding just as done in [CC91] for recursive types. Another avenue is to accept that there definitely will be applications of “effect systems” in theories that are known not to have principal solutions; in this case we may try to reduce our problems by incorporating a more general rule for subtyping into the inference system.

Acknowledgements This research has been supported by the DART and LOMAPS projects.

References

[BD93] Dominique Bolignano and Mourad Debabi. A coherent type system for a concurrent, functional and imperative programming language. In AMAST ’93, 1993.

[BS94] Bernard Berthomieu and Thierry Le Sergent. Programming with behaviours in an ML framework: the syntax and semantics of LCS. In ESOP ’94, volume 788 of LNCS, pages 89–104. Springer-Verlag, 1994.

[CC91] Felice Cardone and Mario Coppo. Type inference with recursive types: Syntax and semantics. Information and Computation, 92:48–80, 1991.

[Hen93] Fritz Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253–289, April 1993.

[JG91] Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In ACM Symposium on Principles of Programming Languages, pages 303–310. ACM Press, 1991.

[Mil78] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

[NN93] Flemming Nielson and Hanne Riis Nielson. From CML to process algebras. In CONCUR ’93, volume 715 of LNCS. Springer-Verlag, 1993. An expanded version appears as DAIMI technical report no. PB-433.

[NN94a] Hanne Riis Nielson and Flemming Nielson. Higher-order concurrent programs with finite communication topology. In ACM Symposium on Principles of Programming Languages. ACM Press, January 1994.

[NN94b] Flemming Nielson and Hanne Riis Nielson. Constraints for polymorphic behaviours of concurrent ML. In Constraints in Computational Logics (CCL ’94), volume 845 of LNCS. Springer-Verlag, September 1994.

[NN94c] Hanne Riis Nielson and Flemming Nielson. Static and dynamic processor allocation for higher-order concurrent languages. Technical Report PB-483, DAIMI, University of Aarhus, Denmark, 1994. Also see this volume.

[PGM90] Sanjiva Prasad, Alessandro Giacalone, and Prateek Mishra. Operational and algebraic semantics for Facile: A symmetric integration of concurrent and functional programming. In ICALP 90, 1990.

[Rep91] John H. Reppy. CML: A higher-order concurrent language. In SIGPLAN’91 Conference on Programming Language Design and Implementation, June 1991.

[Sie89] Jörg H. Siekmann. Unification theory. J. Symbolic Computation, 7:207–274, 1989.

[TJ92a] Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programing, 2(3):245–271, 1992.

[TJ92b] Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. In IEEE Symposium on Logic in Computer Science, pages 162–173, 1992. Also see Information and Computation 111 2, 1994.