A Type System for a Lambda Calculus with Assignments

Kung Chen  Martin Odersky
Dept. of Computer Science  Dept. of Informatics
Yale University  Universität Karlsruhe
New Haven, CT 06520, USA  76128 Karlsruhe, Germany
chenk@cs.yale.edu  odersky@ira.uka.de

Appeared in Proc. Symp. on Theoretical Aspects of Computer Software, pp.347-364, Springer LNCS 789, 1994

Abstract. We present a Hindley/Milner-style polymorphic type system for λ_{var}, an extension of the call-by-name λ-calculus with mutable variables and assignments. To match λ_{var}’s explicit distinction between functional and imperative worlds, the type universe is stratified into two layers: one for applicative expressions and one for imperative state transformers. In inferring types for λ_{var}-terms, the type system performs a simple effect analysis to statically verify the safety of coercing a state transformer to a pure value. We prove the soundness of the type system with respect to λ_{var}’s untyped reduction semantics so that any welltyped program will evaluate to an answer, provided the evaluation terminates. We also discuss some practical aspects of the type system and present a type checker based on the well-known W algorithm.

1 Introduction

We study a type system for λ_{var}, an imperative extension of λ-calculus. Unlike other such extensions [Rey88, WF93, SRI91], which are explicitly and monomorphically typed, we have studied the theory of λ_{var} initially in an untyped setting [ORH93]. In this paper, we present a polymorphic type system in the Hindley/Milner style for λ_{var}. We prove that the type system is sound with respect to the original, untyped semantics. We also show that the type system admits a straightforward algorithm for type reconstruction. Polymorphic type systems for functional/imperative language combinations usually treat the types of mutable variables specially: unlike the types of immutable variables they can be instantiated only once [Dam85, Tof90]. This is necessary in order to avoid the situation where assignments and read-accesses on a mutable variable occur at different types. The distinction is generally reflected in the use of two type variable alphabets — one containing those variables that can be generalized in a type scheme, the other containing weak type variables that cannot be generalized.

Languages such as ML, in which every expression can have side effects, make finding the types of mutable variables non-trivial. Several type systems with various degrees of accuracy and complexity have been proposed for ML [Dam85, Tof90, LW91, Wri92, HMV93]. Some of the recent proposals have many things in common with effect-systems [TJ93].

In λ_{var}, we face a different situation. Side effects can be caused only by terms that occur in a state transformer and the results of those terms are always λ-bound (because they are defined in a monadic bind operation [Wad92]). The evaluation of a let-bound value, on the other hand, never involves side effects. This makes the purely functional Hindley/Milner system, which generalizes only the types of let-bound variables, a good match for λ_{var}. As a consequence, typing the letconstruct is considerably simpler in λ_{var} than in imperative versions of ML. Like Mairson [Mai93] for functional ML, we can conceptually type a program with let’s by expanding all let’s and typing the resulting program in a monomorphic type system.

λ_{var}’s approach to let-typing is very close to some of the recent proposals for simplifying the typing of references in ML, even though it was developed independently. Leroy [Ler93] proposes to introduce two kinds of let, one monomorphic with call-by-value semantics, the other polymorphic with call-by-name semantics. Monomorphic let′s correspond to the monadic bind operations of λ_{var}, while the polymorphic versions correspond to λ_{var}’s let construct (which is callby-name). Wright [Wri93] proposes an even stronger restriction that admits just values in the definitions of polymorphic let-bound variables. Wright shows that his restriction invalidates a surprisingly small amount of existing ML program code.

On the other hand, the type system for λ_{var} has to solve a problem not present in either functional languages or ML: It has to guarantee statically that a state transformer enclosed in a pure construct is referentially transparent. We present here a simple method to verify this fact. Firstly, to match λ_{var}’s explicit distinction between functional and imperative worlds, the type universe is stratified into two layers: one for applicative expressions and one for imperative state transformers. Secondly, in inferring types for λ_{var}-terms, the type system performs a simple effect analysis based on type stratification to statically verify the safety of coercing a state transformer to a pure value.

We prove that the resulting type system is sound with respect to the untyped reduction semantics of λ_{var}. Similar to the approach of [WF92], this is shown by a syntactic method, based on a subject reduction theorem and a characterization of the types of irreducible terms. We also discuss some practical aspects of the type system and present a type reconstruction algorithm based on the wellknown algorithm W [Mil78].

The rest of this paper is organized as follows. Section 2 gives an overview of the original, untyped version of λ_{var}. Section 3 introduces a Hindley/Milnerstyle type system for this language. Section 4 states and proves the semantic soundness of the type system. Section 5 discusses type reconstruction. Section 6 concludes.

2 Preliminaries

In this section, we briefly review the syntax and semantics of λ_{var}. We refer the reader to [ORH93] for examples and a more detailed description.

2.1 Term Syntax of λ_{var}

The syntax of λ_{var} is given in Figure 1. On the first line are productions for primitive function symbols f, data constructors c^{n}, identifiers x, function abstractions x.M^{1}, function applications M_{1} M_{2} and a let construct. The second line adds constructs for modelling state transformers. A state transformer is a function that maps an initial state to some result value and a final state. States are composed of mutable variables (or: tags) v which are bound in terms var v.M. Tags (denoted by the letters u, v, w) are different from immutable variables (denoted here by x, y, z), but are like them subject to α-renaming. Primitive operations on tags v are assignments M =: v and reads v?. These operations can be combined in a monadic style into larger state transformers using the “bind” expression M_{1} ▷ x.M_{2}. We take (▷) to be right-associative and often employ the following abbreviation:

N ; M =^{def} N ▷ x.M (x ∉ fv M).

M ::= f | c^{n} | x | x.M | M_{1} M_{2} | let y = N in M
| v | var v.M | M? | M_{1} =: M_{2} | M_{1} ▷ x.M_{2}
| return M | pure M

Fig. 1. Syntax of λ_{var}.

1 Note the absence of a leading λ; this is done to make terms and reduction rules simpler to read.

The productions on the last line mediate between values and state transformers. return M is the state transformer that yields M without modifying the state. pure M reduces to the final result of state transformer M, provided M has no global side effects.

β (x.M) N  → [N/x] M
δ f V  → δ(f, V)  (δ(f, V) defined)
let let y = N in M  → [N/y] M
▷▷ (M_{1} ▷ x.M_{2}) ▷ y.M_{3}  → M_{1} ▷ x.(M_{2} ▷ y.M_{3})
r▷ (return N) ▷ x.M  → (x.M) N
v▷ (var v.M) ▷ x.N  → var v.(M ▷ x.N)
=:▷ (M_{1} =: M_{2}) ▷ x.M_{3}  → M_{1} =: M_{2} ; (x.M_{3}) ()  (x ∈ fv M_{3})
f N =: v ; v? ▷ x . M  → N =: v ; (x.M) N
b_{1} N =: v ; w? ▷ x . M  → w? ▷ x . N =: v ; M  (v ≠ w)
b_{2} var v . w? ▷ x . M  → w? ▷ x . var v . M  (v ≠ w)
⊥ var v . v? ▷ x . M  → var v . v? ▷ x . M
p_{c} pure (S[return c^{n} M_{1} ... M_{k}]) →

c^{n} (pure (S[return M_{1}])) ... (pure (S[return M_{k}])) (k ≤ n)

p_{λ} pure (S[return x.M])  → x . pure (S[return M])
p_{f} pure (S[return f])  → f

Fig. 2. Reduction rules for λ_{var}.

The type system for λ-var turns state transformers into a Kleisli monad with (▷) as the bind operator and with return as unit. Untyped λ-var on the other hand, satisfies only two of the three laws of a Kleisli monad (▷ is associative and return is a left-unit).

2.2 Operational Semantics of λ_{var}

The reduction rules given in Figure 2 define an operational semantics for λ_{var}.

We use bv M (fv M) to denote the bound (free) variables and tags in a term M. A term is closed if fv M = ∅. We use M ≡ N for syntactic equality of terms (modulo α-renaming) and reserve M = N for convertibility. We assume everywhere the “hygiene” convention of Barendregt [Bar84] that bound and free variables and tags in a term are distinct.

A value V is a λ-abstraction, a primitive function, or a (possibly applied) constructor. An observable value (or answer) A is an element of some nonempty subset of the basic constants. A context C is a term with a hole [ ] in it. A prefix P is a context of one of the forms

P ::= [ ] | var v.P | M ▷ x.P .

A pre-state prefix R is a “normalized” prefix

R ::= [ ] | var v.R | M =: v ; R ,

and a state prefix S is a pre-state prefix that satisfies in addition the requirement that wr S ⊆ bv S. The set of variables written in S, wr S, is defined as follows:

\begin{aligned}wr [ ] & = & ∅ \\ wr (var v.S) & = & wr S \\ wr (M =: v ; S) & = & \{v\} ∪ wr S. \end{aligned}

Rules (β), (δ), and (let) are the standard rules for reducing terms in an applied λ-calculus. Rules (▷▷) and (r▷) represent two of the three laws of a Kleisli monad. Rule (v▷) extends the scope of a tag over a (▷) to the right. Rule ( =:▷ ) passes (), the result value of an assignment, to the term that follows the assignment. Rules (f), (b_{1}) and (b_{2}) deal with assignments. The fusion rule (f) reduces a pair of an assignment and a dereference with the same tag. The bubble rules (b_{1}) and (b_{2}) allow variable-readers to “bubble” to the left past assignments and introductions involving other tags. Rule (⊥) is not present in [ORH93]; it is added here to force the evaluation of a term with uninitialized variables to diverge. This is necessary, since we do not attempt to detect unititialized variables statically.

The final three rules implement “effect masking”, by which local state manipulation can be isolated for use in a purely functional context. The context condition for state prefixes S that assigned variables must be locally bound ensures that evaluation of the argument to pure neither affects nor observes global storage.

In [ORH93] it was shown that this notion of reduction generates a confluent equational theory which admits a standard reduction order, derived using the evaluation contexts E:

E ::= [ ] | E M | f E | pure E | pure S[return E]
| var v.E | E? | M =: E | E ▷ x.M | M =: v ▷ x.E

Such a left-to-right reduction, denoted by ⟼, defines a deterministic evaluator, eval_{var}, for λ_{var} in the standard manner.

3 The Type System for λ_{var}

3.1 Types

Let \underline{α} and α range over two disjoint denumerable sets of type variables. The syntax of λ_{var} types is as follows:

Applicative types τ ::= \underline{α} | () | τ → τ | κ^{n} τ_{1} … τ_{n}
Command types θ ::= α | τ | θ → θ | κ^{n} θ_{1} … θ_{n} | Cmd θ | V ar θ

The type system is stratified into two layers. The applicative layer τ contains the types of state-independent terms. These applicative types include applicative type variables \underline{α}, the unit type () and are closed under the function space and algebraic data type constructions. The command layer θ extends the applicative layer to type state transformers. The type V ar θ is used to type store tags, while Cmd θ types state transformers with type θ. The command layer includes type variables α, all applicative types and is closed under the type constructors →, κ^{n}, V ar and Cmd.

Note that applicative type variables \underline{α} serve a different purpose than either imperative type variables [Tof90] or weak type variables [AM87] used in Standard ML. They are used to type polymorphic pure terms, not to solve the problem with polymorphic references.

If an overloading system like Haskell’s is available in the underlying programming language the stratification into applicative and command types can be expressed using type classes. A type τ(\underline{α}) with an applicative type variable \underline{α} would be expressed

Applicative α ⇒ τ(\underline{α}).

The resulting type system would be a direct extension of an ML-style system with overloading, with additional inference rules for the imperative constructs.

3.2 Typing Rules

Rules for inferring types for λ_{var}-terms are given in Figure 3. A type judgement Γ ⊢ M : θ states that term M has type τ in type environment Γ. A type environment is a finite set of type assumptions of the forms x: θ and v: V ar θ, with no variable (tag) occurring twice. We write dom(Γ) for the set of variables and tags occur in Γ, and Γ (a) for the unique θ with a : θ in Γ, if it exists. Assuming a ∉ dom(Γ), we write Γ.a:θ for Γ ∪ {a : θ}.

Basically, each rule corresponds to one syntactic construct in the term language. Primitive functions and data constructors are collectively called constants c. Rule (const) uses the function T ypeOf : Const ↦ Set of applicative types to assign types to constants. We assume that the types associated with a constant are the

(const)  Γ ⊢ c : τ τ ∈ T ypeOf(c)
(var)  Γ ⊢ x : θ x : θ ∈ Γ
(tag)  Γ ⊢ v : V ar θ  v : V ar θ ∈ Γ
(abs)  \frac{Γ.x : θ′ ⊢ M : θ}{Γ ⊢ x.M : θ′ → θ}

(app)  \frac{Γ ⊢ M : θ′ → θ  Γ ⊢ N : θ′}{Γ ⊢ M N : θ}

(let)  \frac{Γ ⊢ N : θ′ Γ ⊢ [N/y] M : θ}{Γ ⊢ let y = N in M : θ}

(reader)  \frac{Γ ⊢ M : V ar θ}{Γ ⊢ M? : Cmd θ}

(assign)  \frac{Γ ⊢ M_{1} : θ  Γ ⊢ M_{2} : V ar θ}{Γ ⊢ M_{1} =: M_{2} : Cmd ()}

(block)  \frac{Γ.v : V ar θ′ ⊢ M : Cmd θ}{Γ ⊢ var v.M : Cmd θ}

(bind) \frac{Γ ⊢ x.M_{2} : θ′ → Cmd θ Γ ⊢ M_{1} : Cmd θ′}{Γ ⊢ M_{1} ▷ x.M_{2} : Cmd θ}

(unit)  \frac{Γ ⊢ M : θ}{Γ ⊢ return M : Cmd θ}

(pure)  \frac{Γ_{τ} ⊢ M : Cmd τ}{Γ_{τ} ⊢ pure M : τ} M ≡ P [return N]

Fig. 3. Typing Rules for λ_{var}-terms.

set of substitution instances a single, polymorphic type. Furthermore, we impose the usual δ-typability condition to ensure type soundness for an unspecified set of constants:

τ′ → τ ∈ T ypeOf(f) and ⊢ V : τ′ ⇒ δ(f, V) is defined and ⊢ δ(f, V) : τ The rules for the purely functional part are standard. let-expressions are typed through term substitution (in Section 5, we will modify this to gain better average case efficiency of the type inferencer). All state transformer have type Cmd θ, where θ is the type of the state transformer’s result. For tag readers v?, θ is derived from v’s type, and for assignments, θ is the unit type (). The rules for introducing new tags (block) and binding state transformers (bind) are in their structure similar to the rules for function introduction (abs) and function application (app).

The most complex part of the type system has to do with typing pure constructs. This is not surprising, since the type system has to ensure that the dynamic side conditions on the reduction of a term pure M are always satisfied, which requires some amount of effect analysis. We adopt the following conservative conditions: First, we require that M ≡ P [return N] to ensure that something is returned from the state transformer M. Second, to ensure that the evaluation of M neither affects nor observes global storage we require that the type environment for M be applicative, i.e., ∀x ∈ fv(M), Γ (x) is applicative. This condition is expressed by writing Γ_{τ} in the premise and conclusion of the rule. Third, to ensure that the state prefix can be stripped from the result, we require that the result type is applicative.

4 Type Soundness

In the section, we prove the soundess of our type system with respect to λ_{var}’s operational semantics. We show that every λ_{var}-program of answer type either diverges, or evaluates to an answer value.

First, we show that standard reduction (⟼) preserves type. This is a direct consequence of the Replacement and Subject-Reduction lemmas.

Lemma 4.1 (Replacement) If (i) D is a deduction concluding Γ ⊢ C[M_{1}] : τ. (ii) D_{1} is a subdeduction of D concluding Γ′ ⊢ M_{1} : τ′. (iii) D_{1} occurs in D in the position corresponding to the hole ([]) in C, and (iv) Γ′ ⊢ M_{2} : τ′.

then Γ ⊢ C[M_{2}] : τ.

The following auxiliary lemmas help to establish the subject reduction property.

Lemma 4.2 (Assumption Weaking) If Γ (a) = Γ′(a) for all a ∈ fv(M), then Γ ⊢ M : θ iff Γ′ ⊢ M : θ.

Lemma 4.3 (Term Substitution) If Γ.x : θ ⊢ M : θ′ and x ∉ dom(Γ) and Γ ⊢ N : θ then Γ ⊢ [N/x]M : θ′.

We now show that all reduction rules are type-preserving.

Lemma 4.4 (Subject Reduction) If Γ ⊢ M_{1} : θ and M_{1} → M_{2} then Γ ⊢ M_{2} : θ.

Proof: The proof proceeds by case analysis on M_{1} → M_{2}. We show some typical cases here; the remainder of them follow similarly.

Case (x.M)N → [N/x]M. From Γ ⊢ (x.M)N : θ we have Γ ⊢ x.M : θ′ → θ and Γ ⊢ N : θ′ by (app). From the former, Γ.x: θ′ ⊢ M : θ follows by (abs). Hence Γ ⊢ [N/x]M : θ by Lemma 4.3.

Case N =: v ; v? ▷ x.M → N =: v ; (x.M)N. From Γ ⊢ N =: v ; v? ▷ x.M : Cmd θ_{3} we have Γ ⊢ z. (v? ▷ x.M) : () → Cmd θ_{3} for some fresh variable z and Γ ⊢ N =: v : Cmd () by (assign) and (bind).

From the former, Γ.z: () ⊢ x.M : θ_{2} → Cmd θ_{3} and Γ.z: () ⊢ v? : Cmd θ_{2} by (abs) and (bind). Hence Γ.z:() ⊢ v : V ar θ_{2} by (reader).

From the latter, Γ ⊢ N : θ_{1} and Γ ⊢ v : V ar θ_{1} by (assign). Hence Γ.z:() ⊢ v : V ar θ_{1} by Lemma 4.2.

So

θ_{1} = θ_{2}
Γ.z:() ⊢ N : θ_{1}  by Lemma 4.2
Γ.z:() ⊢ (x.M)N : Cmd θ_{3}  by (app)
Γ ⊢ z.(x.M)N : () → Cmd θ_{3}  by (abs)
Γ ⊢ N =: v ▷ z.(x.M)N : Cmd θ_{3} by (bind).

Case pure (S[return x.M]) → x . pure (S[return M]) . From Γ ⊢ pure (S[return x.M]) : τ, we have Γ_{τ} ⊢ S[return x.M] : Cmd τ by (pure). It is obvious from the definition of state prefix and rules (block) and (bind) that τ = τ_{1} → τ_{2}.

By a straightforward induction on pre-state prefix R’s structure, we can show that

If Γ ⊢ R[return x.M] : Cmd (τ_{1} → τ_{2})
then Γ.x:τ_{1} ⊢ R[return M] : Cmd τ_{2}.

Hence Γ.x : τ_{1} ⊢ S[return M] : Cmd τ_{2}. Now since fv(S[return M]) ⊆ fv(S[return x.M]) ∪ {x}, we must have Γ.x: τ_{1} ⊢ pure (S[return M]) : τ_{2} by (pure). Hence Γ ⊢ x.pure(S[return M]) : τ by (abs).

As a corollary, standard reduction preserves type.

Theorem 4.5 If Γ ⊢ M_{1} : θ and M_{1} ⟼ M_{2} then Γ ⊢ M_{2} : θ.

Next, we examine the “positive” effects the typing rules have on the evaluation of a program. We assume that there is a nullary type constructor Out that represents exactly the set of all answers. Programs in λ_{var} are, therefore, closed terms of type Out. The goal is to show that the evaluation of a program will never get stuck without producing an answer value.

Lemma 4.6 If ⊢ M : Out and M is irreducible (with respect to ⟼ defined in Section 2) then M = A for some answer A.

This lemma is actually a corollary of the following more general one:

Lemma 4.7 Let Γ be {v_{1} :V ar θ_{1}, …, v_{n}:V ar θ_{n}}, n ≥ 0. If Γ ⊢ M : θ and M is irreducible then M ∈ Λ, the language described by the following grammar:

Λ ::= f | x.M | c^{n} M_{1} … M_{k} (0 ≤ k ≤ n) | v | v? ▷ x.M | Θ
Θ ::= v? | M =: v | return M | var v. Θ | M =: v ; Θ

Proof: By induction on the possible structure of the term M:

Case M ≡ f, c^{n} or x.M . M ∈ Λ.

Case M ≡ M_{1} M_{2} . Apply the induction hypothesis to M_{1}. Since M_{1} is of → type, we need to consider only the following possibilities:

– M_{1} ≡ f . Impossible. Since M_{2} is of some applicative type, we must have M_{2} = V for some value V by applying the induction hypothesis to M_{2}. Then M would be reducible by rule (δ) according to the δ −typability assumption.

– M_{1} ≡ (c^{n} M_{1} … M_{k}), 0 ≤ k ≤ n . Since M ≡ M_{1} M_{2} is well-typed under Γ, we must have 0 ≤ k < n. Hence M ∈ Λ.

– M_{1} ≡ x.N . Impossible, since M would be reducible by rule (β).

Case M ≡ let y = M_{1} in M_{2} . Impossible, since M would be reducible by rule (let).

Case M ≡ v . Since Γ ⊢ M : θ, we must have v ≡ v_{i}, for some i. Hence M ∈ Λ.

Case M ≡ N? . Apply the induction hypothesis to N, which is of V ar type. We must have N ≡ v_{i}, for some i. Hence M ∈ Λ.

Case M ≡ M_{1} =: M_{2} . Apply the induction hypothesis to M_{2}, which is of V ar type. We must have M ≡ v_{i}, for some i. Hence M ∈ Λ.

Case M ≡ return N. M ∈ Λ.

Case M ≡ var v.N . From Γ ⊢ M : θ, we have Γ.v: V ar θ′ ⊢ N : θ. Now apply the induction hypothesis to N, which is of Cmd type. Either N ∈ Θ and hence M ∈ Λ, or N ≡ u? ▷ x.M′ rendering M reducible by rule (b_{2}) or (⊥).

Case M ≡ M_{1} ▷ x.M_{2}. Apply the induction hypothesis to M_{1}, which is of Cmd type. We need to consider the following possibilities:

– M_{1} ≡ v? ▷ y.N . Impossible, since M would be reducible by rule (▷▷).

– M_{1} ≡ return N . Impossible, since M would be reducible by rule (r▷).

– M_{1} ≡ var v.N . Impossible, since M would be reducible by rule (v▷).

– M_{1} ≡ v?. M ∈ Λ.

– M_{1} ≡ N =: v . Since M is irreducible, we must have x ∉ fv(M_{2}), for otherwise rule =:▷ would have been applicable before M_{1} became N =: v. Moreover, from Γ ⊢ M : θ, we have Γ ⊢ x.M_{2} : () → θ by (bind). Hence Γ ⊢ M_{2} : θ by Lemma 4.2. Now apply the induction hypothesis to M_{2}, which is of Cmd type. Either M_{2} ∈ Θ and hence M ∈ Λ, or M_{2} ≡ u? ▷ y.M_{3} rendering M reducible by rule (f) or (b_{1}).

Case M ≡ pure P [return N] . Impossible, since M would not be irreducible as we will argue. Suppose otherwise, then P [return N] must be irreducible, too. Moreover, from Γ ⊢ pure P [return N] : τ, we have ⊢ P [return N] : Cmd τ by (pure) and Lemma 4.2. Apply the induction hypothesis to P [return N], which is a closed term of Cmd type. We must have P ≡ S for some state prefix S. Hence N must be irreducible, and Γ′ ⊢ N : τ for some Γ′ = {u_{1} : V ar ν_{1}, …, u_{k}:V ar ν_{k}}, u_{i} ∈ bv(S). Now apply the induction hypothesis to N, which is of some applicative type. We must have N ≡ V for some value V , rendering M reducible by p_{c}, p_{λ}, or p_{f}.

With Theorem 4.5 and Lemma 4.6, the soundness theorem follows:

Theorem 4.8 (Type Soundness) If ⊢ M : Out then either M ⇑ or eval_{var}(M) = A for some answer A.

5 Type Reconstruction

In this section, we sketch an implementation scheme of our type system. Basically, a syntactic-directed type checker along the lines of [DM82] can be employed. The major concern here is how to type let-expressions without explicit term substitution.

As usual, we introduce type schemes to avoid such term substitution. In doing so, the major change is to modify the rule (pure) for typing pure terms. We first extend our type system with type schemes in the standard manner:

Type Schemes σ ::= θ | ∀\underline{α}.σ | ∀α.σ

In addition to the standard rules for generalizing type variables, we need the following two rules to instantiate type variables.

(inst_{p}) \frac{Γ ⊢ M : ∀α.σ}{Γ ⊢ M : [θ/α] σ}  (inst′_{p}) \frac{Γ ⊢ M : ∀\underline{α}.σ}{Γ ⊢ M : [τ/\underline{α}] σ}

All typing rules other than (let) and (pure) remain unchanged. Rule (let) is replaced by rule (let_{p}).

(let_{p})  \frac{Γ ⊢ N : σ  Γ.y:σ ⊢ e : τ}{Γ ⊢ let y = N in M : τ}

The new, polymorphic formulation of (let_{p}) requires some changes in rule (pure). Recall that, in typing pure M, we demand the type environment for M be applicative. In other words, only free variables of applicative type are allowed in M. Now since we will extend the type environment with polymorphic assumptions (y : σ), where σ is a type scheme, it seems that we need to extend our stratification of types to type schemes. A naive stratification would take ∀\underline{α}.σ to be applicative iff σ is applicative. But this would reject any procedure that uses a globally bound imperative value, which seems to be an overly drastic restriction. Fort instance:

let swap = x.y. x? ▷ z. y? ▷ w. z =: y ; w =: x

in pure ( var u. var v. 0 =: u ; 5 =: v ; swap u v ; u? ▷ x. return x)

would be rejected because of the reference to the non-local swap, whose most general type is ∀α.V ar α → V ar α → Cmd (), in the body of the pure. However, this term is perfectly safe, since swap affects only its arguments x, y. If we use the old rule, (let), the problem does not arise since then the body of swap is expanded within the scope of the pure. To correct this deficiency, we keep track of all possible non-applicative types as if all let’s in a term had been expanded.

Definition. Let LB(M) be the set of let-bound identifiers in a term M and for any let-bound y let defn(y) be the defining term of y. Then the closure set of free variables and tags of a term M is given by:

fv^{∗}(M) =^{def} fv(M) ∪ ⋃_{i}{fv^{∗}(defn(y_{i})) | y_{i} ∈ LB(M)}.

Furthermore, fv^{+}(M), the monomorphic closure set, denotes the subset of all λ and var bound identifiers in fv^{∗}(M).

In other words, the monomorphic closure set of a term is the union of its free variables and tags with all the variables and tags that will be introduced through the reduction of let-expressions at outer levels. Since all these variables and tags are λ or var bound and hence are monomorphically typed in the type environment, we can adapt rule (pure) as follows:

(pure_{p}) \frac{Γ ⊢ M : Cmd τ}{Γ ⊢ pure M : τ} M ≡ P [return N] and Safe Γ |_{fv^{+}(M)}

where Γ |_{V} is the restriction of Γ to the variables in V, and Safe Γ′ iff ∀x ∈ dom(Γ′), Γ′(x) is applicative for all x ∈ dom(Γ′).

According to the modified side condition, in order to determine whether a pure term is well-typed one needs to perform the applicative type check over its free variables and tags plus those variables and tags that would be introduced by reducing outer let-expressions. Under this rule, the preceding example program can be given a type using typing rules (let_{p}) and (pure_{p}), since neither swap nor the pure-body contains any unsafe free variables or tags.

Clearly, this modified side condition is derived from the substitution semantics of let-expressions and corresponds to the one we have for rule (pure). Furthermore, monomorphic closure sets of variables and tags can be easily collected as we traverse and type check the source term. One possible scheme is to have an extra variable/tag environment, which maps each let-bound identifier to the monomorphic closure set associated with its defining term, and which maps λ and var bound identifiers to a singleton set consisting of themselves. Thus, as we traverse the source term to any of its pure subterms, we can then obtain its monomorphic closure set to perform the required safety check.

Figure 4 contains a type inferencer for λ_{var}. The algorithm is called W_{v} because of its structural similarity to the algorithm W [DM82]. However, there are two major differences between W_{v} and W: First, W_{v} takes an extra variable/tag environment V to facilitate computing the monomorphic closure sets for pure subterms as we have just described. Second, since the type system has been stratified into two layers, we need to use a different unification algorithm. Indeed, the stratified type system corresponds naturally to an order-sorted signature of two sorts, app and cmd, with app ≤ cmd. Hence any order-sorted unification algorithm will serve our purpose. We conjecture that W_{v} is correct and computes the principal types for well-typed λ_{var}-terms.

6 Conclusion

We have presented a Hindley/Milner-style type system for λ_{var}, an imperative extension of the λ-calculus. The type system distinguishes between statedependent and state-independent terms by assigning them different types, clearly reflecting their intended meanings in λ_{var}. The conversion from state transformers back to pure expressions is restricted and moderated by the type system. We have proved the soundness of our type system with respect to λ_{var}’s operational semantics. In particular, any invalid coercion from a state-dependent term to a pure value would cause a static error to be detected. We also have presented a

W_{v} (M, Γ, V) = case M of

x ⇒ inst (S(Γ x), id)

x.N ⇒

let α a fresh type variable

(θ_{1}, S_{1}) = W_{v} (N, Γ.x:α, V.x:{x}) in (S_{1}α → θ_{1}, S_{1})

var v.N ⇒

let α, β fresh type variables (θ_{1}, S_{1}) = W_{v} (N, Γ.v:V ar α, V.v:{v}) S_{2} = mgu θ_{1} (Cmd β)

in (Cmd S_{2}β, S_{2}S_{1})

M_{1} M_{2} ⇒

let (θ_{1}, S_{1}) = W_{v} (M_{1}, Γ, V) (θ_{2}, S_{2}) = W_{v} (M_{2}, S_{1}Γ, V) α a fresh type variable S_{3} = mgu S_{2}θ_{1} (θ_{2} → α)

in (S_{3}α, S_{3}S_{2}S_{1})

M_{1} ▷ x.M_{2} ⇒

let α, β fresh type variables (θ_{1}, S_{1}) = W_{v} (M_{1}, Γ, V) (θ_{2}, S_{2}) = W_{v} (x.M_{2}, S_{1}Γ, V) S_{3} = mgu S_{2}θ_{1} (Cmd α) S_{4} = mgu S_{3}θ_{2} (S_{3}α → Cmd β)

in (Cmd S_{4}β, S_{4}S_{3}S_{2}S_{1})

N? ⇒

let (θ_{1}, S_{1}) = W_{v} (N, Γ, V) α a fresh type variable S_{2} = mgu S_{1}θ_{1} (V ar α)

in (Cmd S_{2}α, S_{2}S_{1})

M_{1} =: M_{2} ⇒

let (θ_{1}, S_{1}) = W_{v} (M_{1}, Γ, V) (θ_{2}, S_{2}) = W_{v} (M_{2}, S_{1}Γ, V) S_{3} = mgu θ_{2} (V ar S_{2}θ_{1})

in (Cmd (), S_{3}S_{2}S_{1})

Fig. 4. (a) A type inferencer for λ_{var}. let y = M_{1} in M_{2} ⇒

let (θ_{1}, S_{1}) = W_{v} (M_{1}, Γ, V)

σ = gen(θ_{1}, S_{1}Γ) in W_{v} (M_{2}, S_{1}Γ.x:σ, V.y:fvc(fv M_{2}, V))

pure M_{1} ⇒

let M_{1} ≡ P [return N] (θ_{1}, S_{1}) = W_{v} (P [return N)], Γ, V)

\underline{α} a fresh applicative type variable

S_{2} = mgu θ_{1} (Cmd \underline{α}) {y_{1}, …, y_{n}} = ⋃_{i}{Vx_{i} | x_{i} ∈ fv M_{1}}

in if ⋀_{i} ((S_{2}S_{1}Γ)y_{i} be applicative) then (S_{2}α, S_{2}S_{1})

else fail

return N ⇒ let (θ_{1}, S_{1}) = W_{v} (N, Γ, V) in (Cmd θ_{1}, S_{1})

where inst (∀\underline{α}.σ, S) = let \underline{β} a fresh applicative type variable
in inst ([\underline{β}/\underline{α}] σ, S)
inst (∀α.σ, S) = let β a fresh type variable
in inst ([β/α] σ, S)
inst (θ, S)  = (θ, S)
gen (θ, Γ)  = let {α_{i}} = ftv(θ)\ftv(Γ)
in ∀α_{i}.θ
fvc ({}, V)  = {}
fvc ({x} ∪ L, V) = Vx ∪ fvc (L, V)

Fig. 4. (b) A type inferencer for λ_{var}.

type reconstruction algorithm based on a straightforward extension of algorithm W.

As an interesting and useful extension of the current system one could try to improve its precision in typing pure-terms. For example, the following term is currently ill-typed because there is a reference to a non-local tag reader, rdr, in the body of pure. However, no run-time error would arise in its evaluation. return (x.x?) ▷ rdr. let res = pure (var v. 5 =: v ; rdr v ▷ z. return z) in return res

Apparently, as long as no global storage is accessed in evaluating the argument term of pure, the coercion is safe, but our type system does not distinguish between different kinds of effects for λ-bound identifiers. Notice that the equivalent formulation in terms of let,

let rdr = x.x? in let res = pure (var v. 5 =: v ; rdr v ▷ z. return z) in return res

would typecheck in our system. A better approximation to the effects of λ-bound identifiers could be obtained by incorporating a region analysis similar to that of [TJ94].

Acknowledgements

Part of this work was done while the second author was at Yale university, and was supported in part by grant N00014-91-J-4043 from DARPA. The use of a stratified type system of applicative types and command types was suggested by Uday Reddy. Thanks also to Vincent Dornic for his comments on an earlier draft of this paper.

References

[AM87] Andrew W. Appel and David B. MacQueen. A standard ML compiler. In Functional Programming and Computer Architecture, pages 301–324, August 1987. LNCS 274.

[Bar84] H. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984.

[Dam85] Luis Damas. Type assignment in programming languages. PhD thesis, Department of Computer Science, Edinburgh University, April 1985.

[DM82] L. Damas and Robin Milner. Principal type schemes for functional programs. In Proceedings of the Ninth ACM Symposium on Principles of Programming Languages, pages 207–212, January 1982.

[HMV93] My Hoang, John Mitchell, and Ramesh Viswanathan. Standard ML-NJ weak polymorphism and imperative constructs. In Eighth Annual IEEE Symposium on Logic in Computer Science, pages 15–25, June 1993.

[Ler93] Xavier Leroy. Polymorphism by name for references and continuations. In Proc. of 20th ACM Symp. on Principles of Programming Languages, pages 220–231, January 1993.

[LW91] Xavier Leroy and Pierre Weis. Polymorphic type inference and assignment. In Proc. of the 18th ACM Symp. on Principles of Programming Languages, pages 291–302, January 1991.

[Mai93] Harry G. Mairson. Quantifier elimination and parametric polymorphism in programming languages. To appear in the J. of Functional Programming, 1993.

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

[ORH93] Martin Odersky, Dan Rabin, and Paul Hudak. Call by name, assignment, and the lambda calculus. In Proc. of 20th ACM Symp. on Principles of Programming Languages, January 1993.

[Rey88] John C. Reynolds. Preliminary design of the programming language forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.

[SRI91] V. Swarup, U. Reddy, and E. Ireland. Assignments for applicative languages. In J. Hughes, editor, Proc. 5th ACM Conf. on Functional Programming and Computer Architecture, pages 192–214, August 1991. LNCS 582.

[TJ93] Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. To appear in the J. of Functional Programming, 1993.

[TJ94] Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. To appear in the J. of Information and Computation, 1994.

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

[Wad92] Philip Wadler. The essence of functional programming. In Proc.19th ACM Symposium on Principles of Programming Languages, pages 1–14, January 1992.

[WF92] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Department of Computer Science, Rice University, March 1992.

[WF93] Stephen Weeks and Matthias Felleisen. On the orthogonality of assignments and procedures in Algol. In Proc. of 20th ACM Symp. on Principles of

Programming Languages, January 1993.

[Wri92] Andrew K. Wright. Typing references by effect inferences. In B. Krieg-Brückner, editor, Prod. European Symposium on Programming, pages 473– 491, February 1992. LNCS 582.

[Wri93] Andrew K. Wright. Polymorphism for imperative languages without imperative types. Technical Report TR93-200, Rice University, February 1993.

This article was processed using the LaTEX macro package with LLNCS style