Typing References by Effect Inference

Andrew K. Wright^{∗} Department of Computer Science Rice University Houston, TX 77251-1892 wright@cs.rice.edu

European Symposium on Programming Rennes France, February 1992 Springer-Verlag Lecture Notes in Computer Science

Abstract

Hindley/Milner-style polymorphism is a simple, natural, and flexible type discipline for functional languages, but incorporating imperative extensions is difficult. We present a new technique for typing references in the presence of polymorphism by inferring a concise summary of each expression’s allocation behavior—a type effect. A simple technique for proving soundness with respect to a reduction semantics demonstrates that the type system prevents type errors. By establishing that the system corresponds to an alternate system better suited to implementation, we obtain an algorithm to perform type and effect inference.

1 Polymorphism and References

Hindley/Milner-style polymorphism [8, 12] is a simple, natural, and flexible type discipline for functional languages, but incorporating imperative extensions is difficult. While a number of systems for typing reference cells exist [3, 10, 16, 17, 18], we have devised a more direct approach based on inferring a concise summary of each expression’s allocation behavior. Our system has several desirable characteristics: the curried version of a function may be used wherever the uncurried version applies; all expressions typable in the functional sublanguage are typable; the system has a direct inference rule formulation; and it can be implemented efficiently. In this paper, we discuss the typing of Standard ML’s reference cells by our method, give a formal description of a type system for references, and show how it may be implemented. We begin with an illustration of the difficulties involved in typing references in the presence of polymorphism, and outline our solution.

∗This research was supported in part by the United States Department of Defense under a National Defense Science and Engineering Graduate Fellowship, and by NSF grant CCR 89–17022.

1.1 Hindley/Milner Polymorphism

Hindley/Milner-style type systems express polymorphism with let-expressions. In functional languages, understanding such expressions as abbreviations offers a simple explanation of polymorphism. Semantically, the expression:

let x = e_{1} in e_{2}

has the same meaning as e_{2}[x/e_{1}], the capture-avoiding substitution of e_{1} for free x in e_{2} (assuming that e_{1} does not diverge). However, in typing the substituted expression e_{2}[x/e_{1}], each occurrence of the bound expression e_{1} may have a different type. For example, if e_{1} is λz.z, one occurrence could be assigned int → int, while another occurrence is assigned bool → bool. Hence to type a let-expression we associate with x the set of types of e_{1}. Each occurrence of x in the body e_{2} may have any type in this set. In the expression:

let id = λz.z in id 1; id true

id is associated with the infinite set of types {τ → τ | τ ∈ Type}.

Type schemes represent the sets of types that are associated with identifiers bound by let-expressions. A type scheme ∀α_{1} … α_{n}. τ consists of a body (τ), which is a type that may contain type variables (α_{i}), and a set of bound variables (α_{1} … α_{n}). The set of types described by a type scheme consists of those types that may be obtained by substituting types for the bound variables in the body of the type scheme. The type scheme ∀α. α → α describes the set of all function types whose input and output types are the same, i.e., {τ → τ | τ ∈ Type}.

To determine the type scheme for x in the expression let x = e_{1} in e_{2}, we first find a most general type for e_{1} by using type variables wherever possible. For example, a most general type for compose = λf.λg.λz. f (g z) is:

(β → γ) → (α → β) → α → γ.

The type scheme for x is obtained by binding or generalizing type variables in the type of e_{1} (that are not used in typing expressions outside the let-expression in question [13: p. 40]). In the expression:

let compose = λf.λg.λz. f (g z) in …

α, β, and γ are generalized to yield type scheme ∀αβγ. (β → γ) → (α → β) → α → γ for compose.

1.2 References

The operators ref, !, and := provide reference cells as first-class values. When applied to a value, the ref operator creates a reference cell containing that value; applying ! to a reference cell extracts the contents of the cell; and := changes the contents of a cell.

To type reference cells, we introduce the type τ ref for reference cells containing values of type τ. Since the ref operator takes a value of any type and returns a cell containing that value, one might naïvely expect ref to have type scheme ∀α. α → α ref , ! to have type scheme ∀α. α ref → α, and := to have type scheme ∀α. α ref → α → α (:= returns the value assigned). However, this naïve typing for references is unsound, as the following expression illustrates:

let x = ref (λz.z) in x := (λn. n + 1); (! x) true

The most general type for ref (λz.z) is (α → α) ref , and generalizing α yields type scheme ∀α. ((α → α) ref ) for x. This type scheme can be instantiated to (int → int)ref to type the assignment, and to (bool → bool) ref to type the dereference, but when evaluated, this expression causes a type error by attempting to add 1 to true.

Reference cells invalidate the explanation of let-expressions as abbreviations, due to the sharing implied by references: the expression let x = e_{1} in e_{2} no longer has the same meaning as e_{2}[x/e_{1}]. Just as references change the semantics of let-expressions, they also necessitate a change in how let-expressions are typed.

1.3 The Problem is Generalization

The solution our system and all existing systems use is to require that reference cells have only one type. This is achieved by restricting generalization at let-expressions. In the previous example, if α is not generalized, then it is free in the resulting type scheme ∀. ((α → α) ref ). A free type variable may later be replaced with a specific type; in the above example, typing the assignment replaces α with int. The subsequent dereference can no longer be typed, as x now has type scheme ∀. ((int → int) ref ).

The type variables that must not be generalized are those that appear in the types of reference cells allocated by the bound expression [18]. However, this set cannot be precisely determined, since the set of cells allocated by an expression cannot be statically determined. Hence any static type system that attempts to integrate reference cells in this way must use a conservative approximation. Our system uses a more direct method than existing systems to approximate the set of type variables that appear in the types of allocated reference cells.

1.4 Controlling Generalization with Effects

The essential idea behind our system is to associate with every expression a conservative approximation to the set of reference cells that the expression allocates, the expression’s allocation effect.^{1} Since our type system needs only the type variables in the types of these reference cells, we infer for each expression a type effect—the set of type variables that appear in the expression’s allocation effect. In typing a let-expression, the type effect of the bound expression provides the information we need to determine which type variables must not be generalized.

The type effect of an application (e_{1} e_{2}) is a combination of the effects of evaluating the function and argument subexpressions e_{1} and e_{2}, and of the effect caused by applying the function to which e_{1} evaluates. Hence, we record the type effect that the function causes when applied above the arrow in the type of a function. For example, the function:

λx. (ref 1; ref true; ref x; false) allocates cells of type int, bool, and α when applied (where x has type α). The type effect of the set {int, bool, α} is α, since α is the only type variable in the set, hence the type of the above function is α →^{α} bool. The λ-expression itself has the empty type effect, written ∅, because its evaluation to a closure allocates no cells.

1We borrow the term effect from FX [11]. Jouvelot and Gifford [9] describe a system that infers types and effects for expressions. While this system records effect information with function types in a manner similar to ours, the information is not used to control generalization of let-expressions.

To handle higher-order functions, we introduce effect variables, denoted ς. Effect variables are analogous to type variables; for example, the function:

apply = λf.λx.f x

has type (α →^{ς} β) →^{∅} α →^{ς} β for any types α and β and type effect ς. Application of apply to a single argument yields a result of type α →^{ς} β, causing no effect. The type effect ς occurs only when apply is given a second argument, as indicated by the empty type effect on its outermost function constructor. As another example, the function:

compose = λf.λg.λx. f (g x)

has type (α →^{ς_{1}} β) →^{∅} (γ →^{ς_{2}} α) →^{∅} γ ⟶^{ς_{1}ς_{2}} β. When applied to three arguments, it causes the combined effects of both f and g.

As in the functional case, the type scheme for x in the expression let x = e_{1} in e_{2} is determined by generalizing variables in the type of the bound expression e_{1}. To prevent generalizing variables that appear in the types of cells allocated by e_{1}, we simply restrict generalization to those variables not in the effect of e_{1}. For example, in the expression:

let x = ref (λy.y) in x := (λn. n + 1); (! x) true

the bound expression ref (λy.y) has type (α →^{∅} α) ref and effect {α}. Since α appears in the effect, it cannot be generalized, and the expression is not typable.

As a further example, consider the following imperative version of map [10]:

let imap = λf.λx. let a = ref x and b = ref nil
in while not (null !a) do

b := (f (hd !a)) :: !b; a := tl !a

reverse !b

in …

If f has type α →^{ς} β and x has type α list (τ list is the type of lists containing elements of type τ), then the body of the function allocates reference cells of type α list ref and β list ref . While α and β must not be generalized by the inner let in the type schemes for a and b, they can be generalized by the outer let in the type scheme for

imap: ∀αβς_{1}ς_{2}ς_{3}. (α →^{ς_{1}} β) →^{ς_{2}} α list ⟶^{ς_{1}ς_{3}αβ} β list.

1.5 Outline

In the next section, we present the syntax and semantics of a simple language with references. Section 3 defines our type system for this language in detail, and sketches a proof of soundness. In Section 4 we obtain a corresponding type inference algorithm by reformulating the system in a manner better suited to implementation. We conclude with a comparison to other systems for typing references in the presence of polymorphism.

2 A Polymorphic Language with References

We study our type system in the context of a simple language with references. It is easy to extend this language and its type system to a realistic language including pattern matching, exceptions, and modules, such as Standard ML [13, 14].

2.1 Abstract Syntax

Our language has expressions, Exp, and values, Val, of the form:

(Exp)  e ::= v | e_{1} e_{2} | let x = e_{1} in e_{2}
(Val)  v ::= x | c | λx.e | setref v

x ∈ Id c, ref,!, setref ∈ Const

The set Id is a countably infinite set of identifiers (whenever we refer to variables, we mean entities of the type system, not identifiers). The set of constants, Const, consists of data, of primitive operations, and of the distinguished constants ref, !, and setref.

Juxtaposition denotes application and is left associative; λ constructs call-by-value procedural abstractions. Semantically a let-expression behaves like ((λx.e_{2}) e_{1}); however, the type system allows x to be polymorphic. The constants ref, !, and setref provide the usual operations on references. We use the curried binary assignment operator setref rather than the customary infix := to simplify the language. The application of setref to one value is a value—it may be thought of as a capability to assign to a cell. Therefore, the application of setref to a value is included in the syntactic class of values.

Free and bound identifiers are defined as usual. Following Barendregt [1], we assume that bound identifiers are always distinct from free identifiers in distinct metavariables ranging over expressions, and we identify expressions that differ by only a consistent renaming of the bound identifiers.

2.2 Semantics

Rather than using (a variant of) structural operational semantics [13, 14] to give a formal semantics for our language, we define the semantics with a term rewriting system, using the technique of reduction semantics [5, 6, 7]. This formulation allows a compact and elegant presentation of the semantics and a simple proof of type soundness [19].

Evaluation proceeds as a sequence of rewriting steps, or reductions, from one intermediate state of evaluation to another. Each state has a syntactic representation:

(State)  s ::= ρθ.e
(Store)  θ ::= { ⟨x, v⟩ }^{∗}

The sequence θ represents the contents of the store. The first component of a pair ⟨x, v⟩ is a location name; the second component is the value stored there. The phrase ρ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩.e binds x_{1}, …, x_{n} in v_{1}, …, v_{n}, e; hence, ρ-phrases permit recursive bindings. While θ is syntactically a sequence of pairs, we treat θ as a finite function, i.e., we disregard the order of pairs and require that the first components be unique.

(δ)  ρθ.E[c c′] ⟼ ρθ.E[δ(c, c′)] if δ(c, c′) is defined
(β_{v})  ρθ.E[(λx.e) v] ⟼ ρθ.E[e[x/v]]
(let_{v})  ρθ.E[let x = v in e] ⟼ ρθ.E[e[x/v]]
(ref )  ρθ.E[ref v] ⟼ ρθ⟨x, v⟩.E[x]
(!)  ρθ⟨x, v⟩.E[! x] ⟼ ρθ⟨x, v⟩.E[v]
(setref )  ρθ⟨x, v′⟩.E[setref x v] ⟼ ρθ⟨x, v⟩.E[v]

E ::= [] | E e | v E | let x = E in e

Figure 1: The reduction relation ⟼

As with expressions, we identify states that differ by a consistent renaming of bound identifiers.

Figure 1 specifies the reduction relation ⟼: State × State. The notation e[x/v] means the capture-avoiding substitution of v for free x in e. The partial function δ : Const × Const ⇀ Const interprets the application of constants other than ref, !, and setref; the type system places some additional constraints on δ to achieve soundness. The renaming conventions ensure that the identifiers bound by ρ-phrases in the ref, !, and setref reductions are renamed appropriately to avoid capture, as in β_{v}.

The definition of the reduction relation relies on evaluation contexts, E. An evaluation context is an expression with one subexpression replaced by a hole, denoted []. An expression may be placed in the hole of an evaluation context, yielding an expression; we write E[e]. The definition of evaluation contexts forces evaluation to proceed from left to right. As a result, the relation ⟼ is a function.

The evaluation function eval maps programs to answers:

eval(e) = a if and only if ρ.e → ⟼ a

where → ⟼ is the transitive and reflexive closure of the reduction relation ⟼. Programs are simply closed expressions; answers (a) are states of the form ρθ.v.

The evaluation function is partial and may be undefined for two reasons: evaluation may diverge, or it may become stuck. An expression diverges, written e ⇑, if it has an infinite reduction sequence, i.e., if e ⟼ e′ for some e′, and for all e′ such that e → ⟼ e′, there exists e′′ such that e′ ⟼ e′′. Evaluation is stuck if it reaches a state that is not an answer, but from which no further reduction is possible. Stuck states represent the application of a primitive function to an argument for which it is not defined, or the application of a non-function; examples are ρ.(succ true) and ρ.(1 2). When a program reaches a stuck state, it is said to have caused a type error. The intent of a static type system is to filter out programs that may cause type errors.

3 Typing References

The following subsections present a type system for our language. The system requires a syntactic description of types and type inference rules for assigning types to programs. A type soundness theorem establishes that the system filters out all type errors.

3.1 Types and Effects

The sets of types, effects, and type schemes are defined inductively as follows:

(Type)  τ ::= ι | α | τ →^{Δ} τ | τ ref
(Effect)  Δ ::= ν^{∗}
(TypeScheme)  σ ::= ∀ν^{∗}. τ
(Var)  ν ::= α | ς

α ∈ TypeVar ς ∈ EffectVar ι ∈ TypeConst

The set TypeConst is a finite set of ground types, like int and bool. The sets TypeVar and EffectVar are countably infinite and disjoint. An effect is syntactically a sequence of type and effect variables, but we treat effects as finite sets, identifying effects that have the same elements. We write ∅ for the empty effect. We also identify ∀.τ with τ; hence, the set of types is a proper subset of the set of type schemes.

A type scheme ∀ν_{1} … ν_{n}. τ binds ν_{1} through ν_{n} in τ, giving rise to free and bound variables for types and type schemes; F V (σ) is the set of free variables of σ. A type scheme ∀ν_{1} … ν_{n}.τ denotes the set of types that may be obtained by substituting for its bound variables:

{τ′ | τ′ = μτ for some substitution μ with domain {ν_{1}, …, ν_{n}}}.

Substitutions are finite maps from type variables to types and effect variables to effects; juxtaposition denotes application. Substitutions are applied to types as usual, but the application of a substitution μ to an effect Δ yields the set of variables appearing in the pointwise application of μ to each member of Δ:

μΔ = ⋃_{ν∈Δ} F V (μν).

For example, with μ = {α ↦ (β →^{γ} β)} and Δ = ας,

μΔ = F V (μα) ∪ F V (μς) = F V (β →^{γ} β) ∪ F V (ς) = βγς.

So far, our definitions admit several different type schemes that denote the same set of types. As usual, we identify type schemes that differ by only a consistent renaming of bound variables. However, this does not identify all type schemes that denote the same set of types; witness ∀ας. (α →^{ς} α) →^{ς} α and ∀βς_{1}ς_{2}. (β ⟶^{ς_{1}ς_{2}} β) ⟶^{ς_{1}ς_{2}} β. To identify these type schemes, we extend the renaming process to allow the consistent replacement of an effect variable by one or more effect variables. Under this extended process of renaming, all type schemes that denote the same set of types are equivalent.

3.2 Type and Effect Assignment

The type system in Figure 2 is a deductive proof system that assigns a type and an effect to an expression. A type judgement Γ ⊢ e : τ, Δ states that expression e has type τ and effect Δ in type environment Γ. A type environment is a finite map from identifiers to type schemes; type environments give types to the free identifiers of an

TypeOf (ref) = ∀ας. α ⟶^{ας} α ref
TypeOf (!) = ∀ας. α ref →^{ς} α
TypeOf (setref) = ∀ας_{1}ς_{2}. α ref →^{ς_{1}} α →^{ς_{2}} α

Γ ⊢ x : τ, ∅ if τ ∈ Γ(x) (id)

Γ ⊢ c : τ, ∅ if τ ∈ TypeOf (c)

(const)

\frac{Γ[x/τ_{1}] ⊢ e : τ_{2}, Δ}{Γ ⊢ λx.e : τ_{1} →^{Δ} τ_{2}, ∅} (abs)

\frac{Γ ⊢ e_{1} : τ_{1} →^{Δ_{3}} τ_{2}, Δ_{1} Γ ⊢ e_{2} : τ_{1}, Δ_{2}}{Γ ⊢ e_{1} e_{2} : τ_{2}, Δ_{1} ∪ Δ_{2} ∪ Δ_{3}} (app)

\frac{Γ ⊢ e_{1} : τ_{1}, Δ_{1} Γ[x/Close(τ_{1}, Γ, Δ_{1})] ⊢ e_{2} : τ_{2}, Δ_{2}}{Γ ⊢ let x = e_{1} in e_{2} : τ_{2}, Δ_{1} ∪ Δ_{2}} (let)

\frac{Γ ⊢ e : τ, Δ_{1} Δ_{1} ⊆ Δ_{2}}{Γ ⊢ e : τ, Δ_{2}} (sub)

Close(τ, Γ, Δ) = ∀ν_{1} … ν_{n}. τ where {ν_{1}, …, ν_{n}} = F V (τ) \ (F V (Γ) ∪ F V (Δ))

Figure 2: Type and effect assignment

expression. The notation Γ[x/σ] means the functional extension or update of Γ at x to σ. An expression e is well-typed if there exists a derivation that assigns a type τ and an effect Δ to e in the empty environment; we write ⊢ e : τ, Δ.

The rules for typing variables and constants depend on a notion of generalization. A type scheme σ = ∀ν_{1} … ν_{n}. τ′ generalizes a type τ, written τ ∈ σ, if there exists a substitution μ with domain {ν_{1}, …, ν_{n}} such that μτ′ = τ, i.e., if τ is in the set of types denoted by σ. Alternatively, we say that τ is an instance of σ. For example,

int →^{∅} int ∈ ∀ας. α →^{ς} α
(β →^{γ} β) ⟶^{βγ} (β →^{γ} β) ref ∈ ∀ας. α ⟶^{ας} α ref

In the last example, note that when the substitution {α ↦ (β →^{γ} β); ς ↦ ∅} is applied to the effect ας on the function arrow, the result is the “flattened” effect βγ.

As rule (id) indicates, an identifier may have any type that is an instance of its type scheme in the type environment. As an identifier has a binding in the type environment only if it is bound by a surrounding let- or λ-expression, well-typed programs are closed. An identifier has the empty effect since its evaluation allocates no reference cells.

Rule (const) uses the function TypeOf : Const → TypeScheme to assign type schemes to constants. For type soundness to make sense for an unspecified set of constants, we impose a typability condition on the interpretation of constants:

τ′ →^{Δ} τ ∈ TypeOf (c_{1}) and τ′ ∈ TypeOf (c_{2})

implies δ(c_{1}, c_{2}) is defined and τ ∈ TypeOf (δ(c_{1}, c_{2})).

(δ-typability)

This condition requires δ to be defined for all constants of functional type and arguments of matching type, and restricts the range of values that it may produce.^{2}

The type of an abstraction λx.e is determined from the type and effect of its body, as (abs) indicates. Assuming that the argument x has type τ_{1}, if the body e has type τ_{2} and effect Δ, then the abstraction is a function of type τ_{1} →^{Δ} τ_{2}. Since the evaluation of an abstraction itself creates no reference cells, the effect of an abstraction is empty.

To determine the type of an application, the argument’s type is required to match the function’s type as usual. The effect of an application is the union of the effects of its subexpressions and of the effect the function causes.

The type of a let-expression is determined from the type of the body, in a type environment extended with a generalization of the most general type of the bound expression. The function Close generalizes free type and effect variables of the bound expression’s type that are not also free in the type environment or in the bound expression’s effect (the function F V is extended pointwise to type environments).

The subsumption rule (sub) allows any expression to be treated as having more effects than it actually does. By applying subsumption to the body of an abstraction, the abstraction may be treated as causing more effects when applied than it actually does; for example, λx.x may be typed as α →^{Δ} α for any effect Δ. Hence the type scheme for a function includes an effect variable in its type. For example, the type scheme for the identity function λx.x is ∀ας. α →^{ς} α; likewise, the type scheme for ref is ∀ας. α ⟶^{ας} α ref . Without subsumption, a value of type int →^{∅} int and a value of type int →^{int} int could not both be passed as arguments to the same (non-polymorphic) function, because the function and argument types would have to match exactly.

3.3 Type Soundness

To prove that this type system is sound, we use our extension of subject reduction to imperative languages [19]. By expressing the semantics of the language as a term rewriting system, we can use the type system to check that each intermediate state of evaluation is well-typed, and thus show that evaluation preserves typing. Since no stuck state is typable, it follows that evaluation cannot reach a stuck state and cause a type error. The soundness theorem states that all well-typed programs either diverge or produce an answer of the expected type.

Theorem 3.1 (Type Soundness) If ⊢ s : τ, Δ then s ⇑ or s → ⟼ a and ⊢ a : τ, Δ.

Proof Sketch. In order to show that evaluation preserves typing, it must be possible to type all intermediate states of evaluation. Therefore, we augment the type system with a typing rule for states:

\frac{∅[x_{1}/τ_{1} ref ] … [x_{n}/τ_{n} ref ] ⊢ e : τ, Δ ∅[x_{1}/τ_{1} ref ] … [x_{n}/τ_{n} ref ] ⊢ v_{i} : τ_{i}, ∅ 1 ≤ i ≤ n}{⊢ ρ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩.e : τ, Δ} (state)

2This condition precludes partial constant functions that are not defined on all values of their input type, such as ÷ : int × int → int. Such functions may be extended to total functions by raising exceptions. Typing exceptions requires similar restrictions on polymorphism as typing references; type soundness for exceptions is treated in [19].

In the augmented system, reductions preserve the type and effect of a state:

if ⊢ s_{1} : τ, Δ and s_{1} ⟼ s_{2} then ⊢ s_{2} : τ, Δ.

This lemma (subject reduction) is proved by case analysis according to the reduction. Stuck states have the form:

ρθ.E[c v] where δ(c, v) is undefined and c ≠ ref,!, setref; ρθ.E[! v] where v ∉ Id; ρθ.E[setref v_{1} v_{2}] where v_{1} ∉ Id; or ρθ⟨x, v_{1}⟩.E[x v_{2}].

By examining each case in the definition of stuck states, we can show that no stuck state is typable.

Finally, we know that either s ⇑, s → ⟼ a, or s → ⟼ s′ and s′ is stuck. Since ⊢ s : τ, Δ, type and effect preservation implies ⊢ a : τ, Δ and ⊢ s′ : τ, Δ. Suppose s → ⟼ s′ and s′ is stuck. Since stuck states are untypable, ⊢ s′ : τ, Δ is a contradiction, therefore this case cannot occur. Hence either s ⇑ or s → ⟼ a and ⊢ a : τ, Δ.

4 Implementing the Type System

The type system of the preceding section may be used to verify that a typing is valid, but we would like an algorithm that infers a typing if one exists. The algorithms for functional languages rely on ordinary unification to achieve efficient implementation. However, our function types include effect sets, hence unifying two function types apparently requires unifying two sets. Fortunately, we can obtain an indirect reformulation of the type system that has a corresponding algorithm using ordinary unification.

Subsumption is the key to avoiding set unification. To type the application (e_{1} e_{2}) where e_{1} and e_{2} have types:

e_{1} : (τ →^{Δ_{1}} τ′) → τ′′ and e_{2} : τ →^{Δ_{2}} τ′

we must unify τ →^{Δ_{1}} τ′ and τ →^{Δ_{2}} τ′. But subsumption permits embedded effects to be unbounded, hence we can retype e_{1} and e_{2} as:

e_{1} : (τ ⟶^{Δ_{1}∪Δ_{2}} τ′) → τ′′ and e_{2} : τ ⟶^{Δ_{1}∪Δ_{2}} τ′.

The function and argument types now match appropriately.

To permit the use of ordinary unification, we replace the effect sets on function arrows with labels and record the effect information separately in a constraint. The constraint is simply a list of label–effect pairs; the effect information corresponding to a given label is determined by pairs in the constraint with that label. To unite two effects embedded in types, we simply unify their labels in both the types and the constraint. Effect variables provide a convenient source of labels.

In the following subsections we present the indirect system, sketch a proof of its correspondence to the direct system, and give the type inference algorithm.

4.1 The Indirect System

In the indirect system, functions are labeled with only a single effect variable. Constraints record the effect information separately:

(Type)  τ ::= ι | α | τ →^{ς} τ | τ ref
(Constraint)  κ ::= { ⟨ς, ν⟩ }^{∗}
(TypeScheme)  σ ::= ∀ν^{∗}. τ with κ

A constraint is treated as a set of pairs of an effect variable and either a type variable or an effect variable. The effect information associated with an effect variable ς under constraint κ is the least set E of type and effect variables such that ς ∈ E, and if ς′ ∈ E and ⟨ς′, ν⟩ ∈ κ then ν ∈ E. For example, the effect information corresponding to ς_{1} in the constraint ⟨ς_{1}, α_{1}⟩⟨ς_{1}, α_{2}⟩⟨ς_{1}, ς_{2}⟩⟨ς_{2}, α_{3}⟩⟨ς_{3}, α_{4}⟩ is {α_{1}, α_{2}, α_{3}, ς_{1}, ς_{2}}.

Generalization for the indirect system is defined as:

(τ, κ) ∈ ∀ν_{1} … ν_{n}. τ′ with κ′

iff Dom(S) = {ν_{1}, …, ν_{n}} and Sτ′ = τ and Sκ′ ⊆ κ

where S is a substitution from type variables to types and from effect variables to effect variables. Application of substitutions to types is defined as usual; substitution on constraints is defined as follows:

Sκ = ⋃_{⟨ς,ν⟩∈κ}{⟨Sς, ν′⟩ | ν′ occurs in Sν}.

The indirect system derives judgements of the form Γ ▷ e : τ, ς, κ, meaning that expression e has type τ and effect ς in type environment Γ under constraint κ. Figure 3 presents the typing rules for the indirect formulation; Figure 4 defines the function IF V to compute free type and effect variables for the indirect formulation.

4.2 Correspondence of the Direct and Indirect Systems

To prove that an expression has a type in the indirect system if and only if it has a type in the direct system, we must account for two differences between the direct and indirect systems. First, the indirect system represents effect information by constraints. Second, the indirect system does not have an explicit subsumption rule, but instead folds subsumption into the other rules. We prove each direction separately by constructing translations from a type derivation in one system into a derivation in the other system.

For the translation from the indirect system to the direct system, Figure 5 defines the translation D from indirect types to direct types. The two systems must agree on the types of constants, hence we require that all constants be of closed type, and that:

TypeOf (c) = D[[IndTypeOf (c)]]κ for all κ.

If e has a derivation in the indirect system, then e has a corresponding derivation in the direct system.

IndTypeOf (ref) = ∀ας. α →^{ς} α ref with ⟨ς, α⟩
IndTypeOf (!) = ∀ας. α ref →^{ς} α with ∅
IndTypeOf (setref) = ∀ας_{1}ς_{2}. α ref →^{ς_{1}} α →^{ς_{2}} α with ∅

Γ ▷ x : τ, ς, κ if (τ, κ) ∈ Γ(x) (id)

Γ ▷ c : τ, ς, κ if (τ, κ) ∈ IndTypeOf (c)

(const)

\frac{Γ[x/τ_{1}] ▷ e : τ_{2}, ς, κ}{Γ ▷ λx.e : τ_{1} →^{ς} τ_{2}, ς′, κ} (abs)

\frac{Γ ▷ e_{1} : τ_{1} →^{ς′} τ_{2}, ς, κ Γ ▷ e_{2} : τ_{1}, ς, κ}{Γ ▷ e_{1} e_{2} : τ_{2}, ς, κ ∪ \{⟨ς, ς′⟩\}} (app)

\frac{Γ ▷ e_{1} : τ_{1}, ς, κ_{1} (σ, κ_{2}) = Close(τ_{1}, Γ, ς, κ_{1}) Γ[x/σ] ▷ e_{2} : τ_{2}, ς, κ_{2}}{Γ ▷ let x = e_{1} in e_{2} : τ_{2}, ς, κ_{2}} (let)

Close(τ, Γ, ς, κ) = (∀α_{1} … α_{m}ς_{1} … ς_{n}. τ with κ′, κ \ κ′)
where {α_{1}, …, α_{m}, ς_{1}, …, ς_{n}} = IF V (τ, κ) \ (IF V (Γ, κ) ∪ IF V (ς, κ))
κ′ = {⟨ς, ν⟩ | ⟨ς, ν⟩ ∈ κ, ς ∈ {ς_{1}, …, ς_{n}}}

Figure 3: Indirect type assignment

IF V (ι, κ) = ∅
IF V (α, κ) = {α}
IF V (τ ref , κ) = IF V (τ, κ)
IF V (τ_{1} →^{ς} τ_{2}, κ) = IF V (τ_{1}, κ) ∪ IF V (τ_{2}, κ) ∪ IF V (ς, κ)
IF V (ς, κ) = {ς} ∪ ⋃_{⟨ς,ν⟩∈κ} IF V (ν, {⟨ς′, ν′⟩ | ⟨ς′, ν′⟩ ∈ κ, ς′ ≠ ς})
IF V (∀ν_{1} … ν_{n}. τ with κ′, κ) = IF V (τ, κ′ ∪ κ) \ {ν_{1}, …, ν_{n}}
IF V (Γ, κ) = ⋃_{x∈Dom(Γ)} IF V (Γ(x), κ).

Figure 4: Free variables for the indirect system

Theorem 4.1 (Indirect to Direct) If Γ ▷ e : τ, ς, κ then D[[Γ]]κ ⊢ e : D[[τ]]κ, D[[ς]]κ.

The proof of this theorem proceeds by induction on the derivation of Γ ▷ e : τ, ς, κ. For this induction, it is critical that the translation D preserve free type and effect variables:

\begin{aligned}IF V (τ, κ) & = & F V (D[[τ]]κ); & IF V (σ, κ) & = & F V (D[[σ]]κ); \\ IF V (ς, κ) & = & F V (D[[ς]]κ); & IF V (Γ, κ) & = & F V (D[[Γ]]κ). \end{aligned}

For the translation from the direct system to the indirect system, Figure 6 defines the translation I from direct types to indirect types. The function F is any one-to-one function from effects to effect variables such that its range is fresh (no element appears in any derivation). Σ represents sets of effect variables. Let ⊑ be the relation between constraints such that κ_{1} ⊑ κ_{2} iff:

Dom(κ_{1}) ⊆ Dom(κ_{2}) and IF V (ς, κ_{1}) = IF V (ς, κ_{2}) for all ς ∈ Dom(κ_{1}).

D[[ι]]κ = ι
D[[α]]κ = α
D[[τ ref ]]κ = (D[[τ]]κ) ref
D[[τ_{1} →^{ς} τ_{2}]]κ = let Δ = D[[ς]]κ, τ′_{1} = D[[τ_{1}]]κ, τ′_{2} = D[[τ_{2}]]κ in τ′_{1} →^{Δ} τ′_{2}
D[[ς]]κ = IF V (ς, κ)
D[[∀ν_{1} … ν_{n}. τ with κ′]]κ = ∀ν_{1} … ν_{n}. D[[τ]](κ ∪ κ′)  (ν_{1}, …, ν_{n} ∉ κ)
D[[Γ]]κ = {x ↦ D[[Γ(x)]]κ | x ∈ Dom(Γ)}

Figure 5: Translation from indirect types to direct types

I[[ι]] = (ι, ∅, ∅)
I[[α]] = (α, ∅, ∅)
I[[τ ref ]] = let (τ′, κ, Σ) = I[[τ]] in (τ′ ref , κ, Σ)
I[[τ_{1} →^{Δ} τ_{2}]] = let (τ′_{1}, κ_{1}, Σ_{1}) = I[[τ_{1}]], (τ′_{2}, κ_{2}, Σ_{2}) = I[[τ_{2}]], (ς, κ_{3}) = I[[Δ]]

in (τ′_{1} →^{ς} τ′_{2}, κ_{1} ∪ κ_{2} ∪ κ_{3}, Σ_{1} ∪ Σ_{2} ∪ {ς})

I[[Δ]] = let ς = F(Δ) in (ς, {⟨ς, ν⟩ | ν ∈ Δ} ∪ {⟨ς, ς⟩})
I[[∀ν_{1} … ν_{n}. τ]] = let (τ′, κ, Σ) = I[[τ]], κ′ = {⟨ς_{i}, τ_{i}⟩ ∈ κ | ς_{i} ∈ {ν_{1}, …, ν_{n}} ∪ Σ}

in (∀ν_{1} … ν_{n}Σ. τ′ with κ′, κ \ κ′)

I[[Γ]] = let (σ_{i}, κ_{i}) = I[[Γ(x_{i})]] for x_{i} ∈ Dom(Γ)

in ({x_{i} ↦ σ_{i}}, ⋃_{i} κ_{i})

Figure 6: Translation from direct types to indirect types

If e has a derivation in the direct system, then e has a derivation in the indirect system.

Theorem 4.2 (Direct to Indirect) If Γ ⊢ e : τ, Δ and (\overline{τ}, κ_{τ} , Σ) = I[[τ]] and (\overline{ς}, κ_{Δ}) = I[[Δ]] and (\overline{Γ}, κ_{Γ}) = I[[Γ]] then \overline{Γ} ▷ e : \overline{τ}, \overline{ς}, κ where κ_{Γ}, κ_{τ} , κ_{Δ} ⊑ κ.

Again, the proof relies on the translation I preserving free type and effect variables:

if I[[τ]] = (\overline{τ}, κ, Σ) then IF V (\overline{τ}, κ) = F V (τ) ∪ Σ;
if I[[Δ]] = (\overline{ς}, κ) then IF V (\overline{ς}, κ) = F V (Δ) ∪ \{\overline{ς}\};
if I[[σ]] = (\overline{σ}, κ) then IF V (\overline{σ}, κ) = F V (σ);
if I[[Γ]] = (\overline{Γ}, κ) then IF V (\overline{Γ}, κ) = F V (Γ).

4.3 Algorithm

Obtaining an algorithm from the indirect system is straightforward [10]. Given an expression, a type environment, and a constraint, algorithm W in Figure 7 computes a type, a substitution to be applied to the type environment, an effect variable, and a new constraint. The function unify performs ordinary unification, returning a substitution that unifies its arguments; I is the identity substitution. Soundness and completeness theorems may be demonstrated to establish the correspondence of the algorithm to the indirect system as usual [2, 17].

W (x, Γ, κ) = if x ∉ Dom(Γ) then fail (expression is not closed)

let ς, α′_{1}, …, α′_{m}, ς′_{1}, …, ς′_{n} be fresh ∀α_{1} … α_{m}ς_{1} … ς_{n}. τ with κ′ = Γ(x) S = {α_{i} ↦ α′_{i}, ς_{j} ↦ ς′_{j}}

in (Sτ, I, ς, κ ∪ Sκ′)

W (c, Γ, κ) = let ς, α′_{1}, …, α′_{m}, ς′_{1}, …, ς′_{n} be fresh ∀α_{1} … α_{m}ς_{1} … ς_{n}. τ with κ′ = IndTypeOf (c) S = {α_{i} ↦ α′_{i}, ς_{j} ↦ ς′_{j}}

in (Sτ, I, ς, κ ∪ Sκ′)

W (λx.e, Γ, κ) = let α, ς be fresh

(τ, S, ς′, κ′) = W (e, Γ[x/α], κ)

in (Sα →^{ς} τ, S, ς, κ′)

W ((e_{1} e_{2}), Γ, κ) = let α, ς be fresh

(τ_{1}, S_{1}, ς_{1}, κ_{1}) = W (e_{1}, Γ, κ)
(τ_{2}, S_{2}, ς_{2}, κ_{2}) = W (e_{2}, S_{1}Γ, κ_{1})
S_{3} = unify(S_{2}τ_{1}, τ_{2} →^{ς} α) (may fail)
S_{4} = unify(S_{3}S_{2}ς_{1}, S_{3}ς_{2}) (will not fail)

in (S_{4}S_{3}α, S_{4} ∘ S_{3} ∘ S_{2} ∘ S_{1}, S_{4}S_{3}ς_{2}, S_{4}S_{3}(κ_{2} ∪ {⟨ς, ς_{2}⟩}))

W (let x = e_{1} in e_{2}, Γ, κ) = let (τ_{1}, S_{1}, ς_{1}, κ_{1}) = W (e_{1}, Γ, κ)) (σ, κ_{2}) = Close(τ_{1}, S_{1}Γ, ς_{1}, κ_{1}) (τ_{2}, S_{2}, ς_{2}, κ_{3}) = W (e_{2}, (S_{1}Γ)[x/σ], κ_{2}) S_{3} = unify(S_{2}ς_{1}, ς_{2}) (will not fail)

in (S_{3}τ_{2}, S_{3} ∘ S_{2} ∘ S_{1}, S_{3}ς_{2}, S_{3}κ_{3})

Figure 7: Type Inference Algorithm

Our algorithm is similar to Milner’s algorithm W [12] for a functional language. In our algorithm, the case for applications contains an additional invocation of unify, but this second invocation always unifies two effect variables, and is very cheap. The main difference is that our algorithm must maintain a set of constraints that grows linearly with the number of applications and that must be searched in typing a let-expression. The practical performance of our algorithm depends on the efficiency of constraint handling; the techniques for manipulating constraints discussed by Leroy and Weis [10] should be applicable to our algorithm.

5 Comparison with Other Systems

There are several other systems for typing references in the presence of polymorphism; O’Toole [15] presents detailed comparisons between four of them. Ideally, we would like a simple, intuitive system that is at least as powerful as any of the others, but unfortunately, there are no systems that meet this goal. While we believe our system is relatively simple and natural, it is incomparable to the other systems: there are expressions typable in one system but not the other, and vice versa. Hence comparisons between systems must be pragmatic.

Tofte [18] A system proposed by Tofte and adopted for Standard ML [13, 14] has two kinds of type variables: imperative variables and applicative variables. Types are classified accordingly: imperative types may only contain imperative type variables; applicative types may contain either. The ref operator may only be applied to values of imperative type. In typing the expression let x = e_{1} in e_{2}, imperative variables in the type of e_{1} can be generalized only if e_{1} is non-expansive, that is, if e_{1} has a certain syntactic shape which guarantees that its evaluation does not allocate any references (in Standard ML, e_{1} must be a variable, constant, or λ-expression). We may think of ref as contaminating all type variables in the type of its argument. Generalizing contaminated (imperative) type variables may result in generalizing the type of a value in a reference cell; hence, generalization of contaminated types must be restricted. For example, the expression λx. ! (ref x) has type α^{∗} → α^{∗}, where the superscript ^{∗} indicates that α^{∗} is an imperative type variable. However, α^{∗} can be generalized in the expression:

let i = λx. ! (ref x) in …

as λx. ! (ref x) is non-expansive, and hence does not allocate any references.

A drawback to this system is that partial applications of imperative functions cannot be polymorphic. For example, the function imap (from Section 1.4) has type scheme:

∀α^{∗}β^{∗}. (α^{∗} → β^{∗}) → α^{∗} list → β^{∗} list.

When only partially applied, as in:

let i = imap (λx.x) in …

i cannot be used polymorphically. The expression imap (λx.x) has type α^{∗} list → α^{∗} list and is expansive, hence α^{∗} cannot be generalized. However, in the expression:

let i = λz. imap (λx.x) z in …

α^{∗} can be generalized since the bound expression is non-expansive.

MacQueen [16] A system proposed by MacQueen and implemented by Standard ML of New Jersey attempts to address the curried application problem described above by recognizing how many arguments a function must be applied to before it creates any references. In this system, imap has type scheme (α^{2} → β^{2}) → α^{2} list → β^{2} list. The result of the application imap (λx.x) has type α^{1} list → β^{1} list and can be used polymorphically. The superscript indicates the number of times the function must be applied before a cell is allocated whose type involves that type variable; applications decrease the superscript. Variables with superscript 0 may not be generalized.

Although the system addresses common uses of currying, such as the partial application of imap above, there are cases in which it fails. The system assigns a polymorphic type to f in only the second of the following two expressions:

let f = map ref in …

let f = λz. map ref z in …

The system is unable to recognize that map ref does not allocate any references until it is further applied, since the type scheme for the non-imperative function map : ∀αβ. (α → β) → α list → β list does not indicate that the functional argument to map is invoked only after a second argument is provided. Furthermore, the only formal description of the system is the New Jersey compiler’s source code; no inference rule formulation exists. The system is believed to be strictly stronger than Tofte’s system, i.e., any expression typable by Tofte’s system is typable by MacQueen’s system [18].

In contrast to the above two systems, our system handles partial applications properly. For example, our system assigns a polymorphic type to f in both of the following expressions:

let f = imap λx.x in … let f = map ref in …

Our system recognizes when allocations occur with greater precision by recording type effects above function type arrows.

Damas [3] Damas proposed one of the earliest systems for typing references. This system appears to lie between Tofte’s and MacQueen’s systems in power [18], and although the system has little advantage over Tofte’s system, it did inspire our work. The system infers information similar to type effects, but records information on only the outermost arrow of a function type; hence, the determination of when allocation occurs is fairly imprecise. Damas was apparently aware of this problem, as he states that “the inclusion [of effects among function types], which would be the natural thing to do … would preclude the extension of the type assignment algorithm … to this extended type inference system” [3: p. 90]. Our insight was to include effects in function types and use the constraint manipulation ideas of Leroy and Weis’s system to construct an inference system with a corresponding algorithm.

Leroy & Weis [10] Leroy and Weis propose a closure typing system based on the observation that it is only necessary to prohibit generalization of type variables appearing in the types of cells reachable after the bound expression has been evaluated (i.e., cells that would not be reclaimed by a garbage collection at this point). As cells may be reachable through the free identifiers of closures, the system records the types of the free identifiers of a function in the function’s type. This system has the advantage that it can assign a fully polymorphic type to some functions that make purely local use of a reference cell, such as imap: the system is able to recognize when effects can be masked. However, it fails to type some purely functional expressions that are typable in the functional sublanguage, such as the following:

λz. let id = λx. ((if true then z else λy.(x; y)); x) in id 1; id true

The problem is that by introducing the types of free variables into function types, additional type variables may be introduced into the type environment. In the above example, the if-expression forces z and λy.(x; y) to have the same type. Suppose that x has type α and y has type β. Since x is free in λy.(x; y), this expression has type β →^{α} β, hence z has type β →^{α} β. As α appears in the type of z, α is free in the type environment of the let-expression, and cannot be generalized. In the ordinary Hindley/Milner system, λy.(x; y) and z have type β → β, and α is not free in the type environment. All of the other systems, including ours, will assign types to such functional expressions.

Talpin & Jouvelot [17] Talpin and Jouvelot present an ambitious system that infers types, effects, and regions for expressions in a manner similar to our indirect system.^{3} A reference cell containing a value of type τ has type ref_{ρ}τ; two reference cells share the same region ρ if they may alias. Regions provide finer grained information about allocation behavior than our type effects, and the information about potential aliasing is used to mask local effects. The system includes subsumption on effects, and infers not only allocation effects but also read and write effects that may be useful for compiler optimizations. We conjecture that Talpin and Jouvelot’s system is strictly more powerful than our system.

5.1 Effect Masking

A shortcoming of our system is its inability to recognize when a reference is only used locally and to mask the allocation. When local effects are masked, the function imap has the same type as its functional counterpart map. However, just as precisely determining when allocations occur is impossible, so too is precise effect masking. The following expression is rejected by both Leroy and Weis’s system and Talpin and Jouvelot’s system,^{4} although these systems incorporate effect masking:

λz. let id = λx. ((if true then z else λy. (\underline{\underline{ref x}}; y)); x)

in id 1; id true

This example is also rejected by our system, but Tofte’s, Damas’s, and MacQueen’s systems accept it.

Abstractly, adding effect masking to our system is easy:

\frac{Γ ⊢ e : τ, Δ_{1} Δ_{2} is maskable in e}{Γ ⊢ e : τ, Δ_{1} \ Δ_{2}}

(mask)

Selecting criteria to determine which effects are maskable is more difficult. Data flow analysis and compile time garbage collection techniques [4] might be used to discover references that are not reachable after the bound expression has been evaluated. Even the simplest local flow analysis algorithms would address examples such as the one above.

Effect masking raises the issue of just how far to push static type systems for references. The more powerful the type system is, the more complex its description becomes. If flow analysis is used to mask effects, then a precise description of the flow analysis algorithm is an essential part of the description of the type system. Without a precise description of the type system, the set of well-typed programs is unspecified, and the programmer is left at the mercy of the implementor.

Acknowledgements

I am indebted to Jean-Pierre Talpin and Pierre Jouvelot for many helpful discussions on direct and indirect formulations of effect inference, and to Matthias Felleisen for comments on drafts of this paper.

3It should be possible to reformulate this system in a direct fashion.

4Talpin and Jouvelot now have a refined system that can type this example [personal communication, November ’91].

References

[1] Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics, revised ed., vol. 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1984.

[2] Damas, L., and Milner, R. Principal type schemes for functional programs. Proceedings of the 9th Annual Symposium on Principles of Programming Languages (January 1982), 207–212.

[3] Damas, L. M. M. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1985.

[4] Deutsch, A. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. Proceedings of the 17th Annual Symposium on Principles of Programming Languages (January 1990), 157–168.

[5] Felleisen, M., and Friedman, D. P. A syntactic theory of sequential state. Theoretical Computer Science 69, 3 (1989), 243–287. Preliminary version in: Proceedings of the 14th Annual Symposium on Principles of Programming Languages, 1987, 314-325.

[6] Felleisen, M., Friedman, D. P., Kohlbecker, E. E., and Duba, B. A syntactic theory of sequential control. Theoretical Computer Science 52, 3 (1987), 205–237. Preliminary version in: Proceedings of the Symposium on Logic in Computer Science, 1986, 131–141.

[7] Felleisen, M., and Hieb, R. The revised report on the syntactic theories of sequential control and state. Tech. Rep. TR-100, Rice University, June 1989. To appear in: Theoretical Computer Science.

[8] Hindley, R. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146 (December 1969), 29–60.

[9] Jouvelot, P., and Gifford, D. K. Algebraic reconstruction of types and effects. Proceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991), 303–310.

[10] Leroy, X., and Weis, P. Polymorphic type inference and assignment. Proceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991), 291–302.

[11] Lucassen, J. M., and Gifford, D. K. Polymorphic effect systems. Proceedings of the 15th Annual Symposium on Principles of Programming Languages (January 1988), 47–57.

[12] Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17 (1978), 348–375.

[13] Milner, R., and Tofte, M. Commentary on Standard ML. MIT Press, Cambridge, Massachusetts, 1991.

[14] Milner, R., Tofte, M., and Harper, R. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990.

[15] O’Toole Jr., J. W. Type abstraction rules for references: A comparison of four which have achieved notoriety. Unpublished, 1990.

[16] Standard ML of New Jersey release notes (version 0.75). AT&T Bell Laboratories, November 1991.

[17] Talpin, J.-P., and Jouvelot, P. The type and effect discipline. Tech. Rep. EMP-CRI A/206, Ecole des Mines de Paris, July 1991.

[18] Tofte, M. Type inference for polymorphic references. Information and Computation 89, 1 (November 1990), 1–34.

[19] Wright, A. K., and Felleisen, M. A syntactic approach to type soundness. Tech. Rep. 91-160, Rice University, April 1991. To appear in: Information and Computation.