Proofs about a Folklore Let-Polymorphic Type Inference Algorithm

OUKSEH LEE and KWANGKEUN YI Korea Advanced Institute of Science and Technology

The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the de facto standard Algorithm W that is bottom-up (or context-insensitive), and the other is a “folklore” algorithm that is top-down (or context-sensitive). Because the latter algorithm has not been formally presented with its soundness and completeness proofs, and its relation with the W algorithm has not been rigorously investigated, its use in place of (or in combination with) W is not well founded. In this article, we formally define the context-sensitive, top-down type inference algorithm (named “M”), prove its soundness and completeness, and show a distinguishing property that M always stops earlier than W if the input program is ill typed. Our proofs can be seen as theoretical justifications for various type-checking strategies being used in practice.

Categories and Subject Descriptors: D.3.3 [Programming Languages]: Language Constructs and Features—data types and structures; F.3.3 [Logics and Meaning of Programs]: Studies of Program Constructs—type structure

General Terms: Algorithms, Languages, Theory

Additional Key Words and Phrases: Type error, type inference algorithm

1. INTRODUCTION

Algorithm W, which is the standard presentation of the Hindley/Milner let-poly-morphic type inference system, fails late if the input program has a type error. Because the algorithm fails only at an application expression where its two subexpressions (function and argument) have conflicting types, an erroneous expression is often successfully type-checked long before its consequence collides at an application expression. This “bottom-up” Algorithm W thus reports the whole application expression as the problem area, implying some of its subexpressions are ill typed. Such a large type-error message does not help the programmer to find the cause of the type problem.

A different type inference algorithm, which has been used in an early ML compiler [Leroy 1993], can cure this problem. This folklore algorithm carries a type

This work is supported in part by Korea Science and Engineering Foundation grant KOSEF 961-0100-001-2, by Korea Ministry of Information and Communication grant 96151-IT2-12, by Samsung Electronics Corp., by LG Information & Communications, and by KAIST Center for Artificial Intelligence Research. Authors’ addresses: Department of Computer Science, KAIST, Taejon 305-701, Korea; email: {cookcu; kwang}@cs.kaist.ac.kr. Permission to make digital/hard copy of all or part of this material without fee is granted provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery, Inc. (ACM). To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.

2 · O. Lee and K. Yi

           #let rec fac n = if n = 0 then 1 else n *(fac(n=1));;
           Toplevel input:
           >let rec fac n = if n = 0 then 1 else n *(fac(n=1));;
           >        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
           This expression has type int -> int,
           but is used with type bool -> int.

(a) from W (CamlLight 0.71)

           #let rec fac n = if n = 0 then 1 else n *(fac(n=1));;
           Toplevel input
           >let rec fac n = if n = 0 then 1 else n *(fac(n=1));;
           >                                              ^
           Expression of type 'a -> 'a -> bool
           cannot be used with type 'a -> 'a -> int

(b) from M (CamlLight 0.61)

Fig. 1. Different type-error messages from W and M.

constraint (or an expected type) implied by the context of an expression down to its sub-or-sibling expressions. For example, for an application expression “e_{1} e_{2}” with a type constraint, say of int, the type constraint for e_{1} is α → int and the constraint for e_{2} is the type that the α becomes after the type inference of e_{1}. For a constant or a variable expression, its type must satisfy the type constraint that the algorithm has carried to that point. Because of this “top-down” nature we name this algorithm “M.”

In this article we formally define algorithm M, prove its soundness and completeness, and show that it finds type errors earlier than W. This property implies that this algorithm in combination with W can generate strictly more informative type-error messages than either of the two algorithms alone can.

As an example to show the difference of the two algorithms, see Figure 1. The program is a factorial function whose recursive call is mistakenly “fac(n=1),” instead of “fac(n-1).” Algorithm W (CamlLight 0.71 [Leroy 1995] and SML/NJ 0.93 [MacQueen and Appel 1993]) reports the whole definition as the problem area because the algorithm fails to unify the argument type bool inferred from the recursive call “fac(n=1)” with the type int inferred from the argument use “if n = 0· · ·.” On the other hand, algorithm M (CamlLight 0.61 [Leroy 1993]) pinpoints the operator “=” as the problem spot. This exact error message is possible because the type constraint of the function’s argument is int when the argument “(n=1)” of the recursive call is type-checked.

2. THE M ALGORITHM

2.1 Overview

Algorithm M carries a type constraint from the context of an expression and stops when the expression cannot satisfy the current type constraint. Consider the following expression:

      \underbrace{(fn x => x+1)}_{e_{1}}

                   (\overbrace{(fn y => if y then true else false)}^{e_{3}} \overbrace{false}^{e_{4}} )

e_{2}

Proofs about a Folklore Let-Polymorphic Type Inference Algorithm · 3

The expression e_{1} must be a function expression; thus M infers its type with the constraint α → β. The inference will succeed with substitution {α ↦int,β ↦int}. This imposes the constraint that the argument expression e_{2} must be type int. Thus M infers the type of e_{2} with the constraint int. This, in turn, makes M infer the type of e_{3} with the constraint γ → int. But the then-branch expression in the function’s body is boolean; thus M stops at the true expression with a type error.

One characteristic of M is that a type constraint that is derived from the current context dominates in subsequent steps. For example, given an expression “f(false,1,2)” where the type of the f is α × α × α → α, M reports that the 1 must have the bool type, because the constraint from the “false” expression forces the subsequent sibling expressions to have the same type. In comparison, Johnson and Walz’s unification algorithm [Johnson and Walz 1986] reports that the “false” expression must have the type int, because it selects the most “popular” types if multiple, conflicting types are bound to a type variable.

2.2 Notation

We use conventional notation. Vector α⃗ is a shorthand for {α_{1}, ⋯, α_{n}}, and ∀α⃗.τ is for ∀α_{1} ⋯ α_{n}.τ. Equality of type schemes is up to renaming of bound variables. For a type scheme σ = ∀α⃗.τ, the set ftv(σ) of free type variables in σ is ftv(τ) \ α⃗, where ftv(τ) is the set of type variables in type τ. For a type environment Γ, ftv(Γ) = ⋃_{x∈dom(Γ)} ftv(Γ(x)). A substitution {τ_{i}/α_{i} | 1 ≤ i ≤ n} substitutes type τ_{i} for type variable α_{i}. We write {τ⃗/α⃗} as a shorthand for a substitution {τ_{i}/α_{i} | 1 ≤ i ≤ n}, where α⃗ and τ⃗ have the same length n and Rα⃗ for {Rα_{1}, ⋯, Rα_{n}}. For a substitution S, the support supp(S) is {α | Sα ≠ α}, and the set itv(S) of involved type variables is {α | β ∈ supp(S), α ∈ {β} ∪ ftv(Sβ)}. For a substitution S and a type τ, Sτ is the type resulting from applying every substitution component τ_{i}/α_{i} in S to τ. Hence, {}τ = τ. For a substitution S and a type scheme σ, Sσ = ∀β⃗.S{β⃗/α⃗}τ, where β⃗ ∩ (itv(S) ∪ ftv(σ)) = ∅. For a substitution S and a type environment Γ, SΓ = {x ↦ Sσ | x ↦ σ ∈ Γ}. The composition of substitutions S followed by R is written as RS, which is {R(Sα)/α | α ∈ supp(S)} ∪ {Rα/α | α ∈ supp(R)\supp(S)}. Two substitutions S and R are equal if and only if Sα = Rα for every α ∈ supp(S) ∪ supp(R). For a substitution P and a set of type variables V, we write P | -_{V} for {τ/α ∈ P | α ∉ V }. The notation ∀α⃗.τ′ ≻ τ means that there exists a substitution S such that Sτ′ = τ and supp(S) ⊆ α⃗. We write Γ + x: σ to mean {y ↦ σ′ | x ≠ y, y ↦ σ′ ∈ Γ} ∪ {x ↦ σ}. Clos_{Γ}(τ) is the same as Gen(Γ,τ) in Damas and Milner [1982], i.e., ∀α⃗.τ, where α⃗ = ftv(τ) \ ftv(Γ).

2.3 Algorithm Definition

The source language, its Hindley/Milner-style let-polymorphic type system, and Algorithm W are shown in Figure 2. Algorithm M is shown in Figure 3.

Algorithm M returns a substitution from three components: an expression, a type environment, and a type constraint. The inferred type of the expression is achieved by applying the result substitution to the type constraint of the expression. The type constraints are just types. Note that the algorithm does not unify types at application expressions. Instead, it unifies at constant, variable, and lambda

Abstract Syntax

Expr e ::= () constant
| x  variable
| λx.e  function
| e e  application

| let x = e in e

| fix f λx.e
Type τ ::= ι constant type
| α  type variable
| τ → τ  function type
TypeScheme σ ::= τ | ∀α⃗.σ
TypeEnv  Γ ∈ Var →^{fin} TypeScheme type environment

(CON)  Γ ⊢ () : ι
(VAR)  \frac{Γ(x) ≻ τ}{Γ ⊢ x: τ}
(FN)  \frac{Γ + x: τ_{1} ⊢ e : τ_{2}}{Γ ⊢ λx.e : τ_{1} → τ_{2}}
(APP)  \frac{Γ ⊢ e_{1} : τ_{1} → τ_{2} Γ ⊢ e_{2} : τ_{1}}{Γ ⊢ e_{1} e_{2} : τ_{2}}
(LET)  \frac{Γ ⊢ e_{1} : τ_{1} Γ + x: Clos_{Γ}(τ_{1}) ⊢ e_{2} : τ_{2}}{Γ ⊢ let x = e_{1} in e_{2} : τ_{2}}
(FIX)  \frac{Γ + f: τ ⊢ λx.e : τ}{Γ ⊢ fix f λx.e : τ}

W: TypEnv × Expr → Subst × Type

W(Γ, ())  = (id, ι)
W(Γ, x)  = (id, {β⃗/α⃗}τ) where Γ(x) = ∀α⃗.τ, new β⃗
W(Γ, λx.e)  = let (S_{1}, τ_{1}) = W(Γ + x: β, e), new β
in (S_{1}, S_{1}β → τ_{1})
W(Γ, e_{1} e_{2})  = let (S_{1}, τ_{1}) = W(Γ, e_{1})
(S_{2}, τ_{2}) = W(S_{1}Γ, e_{2})
S_{3} = U(S_{2}τ_{1}, τ_{2} → β), new β
in (S_{3}S_{2}S_{1}, S_{3}β)

W(Γ, let x = e_{1} in e_{2}) =

let (S_{1}, τ_{1}) = W(Γ, e_{1})
(S_{2}, τ_{2}) = W(S_{1}Γ + x: Clos_{S_{1}Γ}(τ_{1}), e_{2})
in (S_{2}S_{1}, τ_{2})
W(Γ, fix f λx.e) = let (S_{1}, τ_{1}) = W(Γ + f: β, λx.e), new β
S_{2} = U(S_{1}β, τ_{1})
in (S_{2}S_{1}, S_{2}τ_{1})

Fig. 2. The language, its type inference rule, and Algorithm W. Every new type variable is distinct from each other, and the set New of new type variables introduced at each recursive call to W(Γ, e) satisfies New ∩ ftv(Γ) = ∅.

expressions.

Consider the variable case (M.2). The current type constraint ρ and the x’s type Γ(x) must agree: U(ρ, {β⃗/α⃗}τ). For the lambda case (M.3), the first thing is to check if the current type constraint ρ is a function type. The unification

M: TypEnv × Expr × Type → Subst

M(Γ, (), ρ) =  U(ρ, ι)  (M.1)
M(Γ, x, ρ) =  U(ρ, {β⃗/α⃗}τ) where Γ(x) = ∀α⃗.τ, new β⃗  (M.2)
M(Γ, λx.e, ρ) =  let S_{1} = U(ρ, β_{1} → β_{2}), new β_{1}, β_{2}  (M.3)
S_{2} = M(S_{1}Γ + x: S_{1}β_{1}, e, S_{1}β_{2})  (M.4)
in S_{2}S_{1}
M(Γ, e_{1} e_{2}, ρ) = let S_{1} = M(Γ, e_{1}, β → ρ), new β (M.5)
S_{2} = M(S_{1}Γ, e_{2}, S_{1}β)  (M.6)
in S_{2}S_{1}
M(Γ, let x = e_{1} in e_{2}, ρ) =
let S_{1} = M(Γ, e_{1}, β), new β  (M.7)
S_{2} = M(S_{1}Γ + x: Clos_{S_{1}Γ}(S_{1}β), e_{2}, S_{1}ρ) (M.8)
in S_{2}S_{1}
M(Γ, fix f λx.e, ρ) = M(Γ + f: ρ, λx.e, ρ)  (M.9)

Fig. 3. Algorithm M. Every new type variable is distinct from each other, and the set New of new type variables introduced at each recursive call to M(Γ, e, ρ) satisfies New ∩ (ftv(Γ) ∪ ftv(ρ)) = ∅.

U(ρ, β_{1} → β_{2}), new β_{1}, β_{2} (M.3)

does this job. For the application case (M.5), the current type constraint ρ becomes the range part of the new constraint β → ρ for the function expression e_{1}:

M(Γ, e_{1}, β → ρ), new β. (M.5)

The constraint for the argument expression e_{2} is the type S_{1}β. For the let case (M.7), the type constraint for the binding expression e_{1} is null,

M(Γ, e_{1}, β), new β, (M.7)

because no constraint about the type of e_{1} is available. The constraint for the letbody e_{2} is the type S_{1}ρ. For the fix case (M.9), the constraint of the expression λx.e is the same as the given constraint ρ.

3. SOUNDNESS AND COMPLETENESS

Algorithm M is sound and complete with respect to the let-polymorphic type inference system of Figure 2.

Theorem 1 (Soundness of M). Let e be an expression and Γ be a type environment. If there exists a type ρ such that M(Γ, e, ρ) = S, then SΓ ⊢ e : Sρ.

The proof uses Lemma 1 and Lemma 2.

Lemma 1 [Damas and Milner 1982]. If S is a substitution and Γ ⊢ e : τ, then SΓ ⊢ e : Sτ.

Lemma 2 [Milner 1978]. Let S be a substitution, Γ be a type environment, and τ be a type. SClos_{Γ}(τ) = Clos_{S′Γ}(S′τ), where S′ = S{β⃗/α⃗}, α⃗ = ftv(τ) \ ftv(Γ) and β⃗ is new.

Proof of Theorem 1. We prove by structural induction on e.

—case (): Sρ = Sι = ι. So SΓ ⊢ () : Sρ by (CON).

—case x: Sρ = S{β⃗/α⃗}τ ≺ SΓ(x). By (VAR), SΓ ⊢ x : Sρ.

—case λx.e:

(1) By induction, (M.4) implies

S_{2}S_{1}Γ + x: S_{2}S_{1}β_{1} ⊢ e : S_{2}S_{1}β_{2}.

(2) By (FN), S_{2}S_{1}Γ ⊢ λx.e : S_{2}S_{1}β_{1} → S_{2}S_{1}β_{2}; that is, by (M.3),

S_{2}S_{1}Γ ⊢ λx.e : S_{2}S_{1}ρ.
—case e_{1} e_{2}:

(1) By induction, (M.5) implies S_{1}Γ ⊢ e_{1} : S_{1}(β → ρ). By Lemma 1, we can apply S_{2} to both sides.

S_{2}S_{1}Γ ⊢ e_{1} : S_{2}S_{1}β → S_{2}S_{1}ρ

(2) By induction, (M.6) implies

S_{2}S_{1}Γ ⊢ e_{2} : S_{2}S_{1}β.

Hence by the (APP) rule, S_{2}S_{1}Γ ⊢ e_{1} e_{2} : S_{2}S_{1}ρ. —case let x = e_{1} in e_{2}: Let S′_{2} = S_{2}{β⃗/α⃗}, where α⃗ = ftv(S_{1}β) \ ftv(S_{1}Γ), and

let β⃗ be new type variables.

(1) By induction, (M.7) implies S_{1}Γ ⊢ e_{1} : S_{1}β. By Lemma 1 we can apply S′_{2} to both sides.

S′_{2}S_{1}Γ ⊢ e_{1} : S′_{2}S_{1}β

(2) By induction, (M.8) implies S_{2}S_{1}Γ + x: S_{2}Clos_{S_{1}Γ}(S_{1}β) ⊢ e_{2} : S_{2}S_{1}ρ. By Lemma 2 and the fact that S′_{2}S_{1}Γ = S_{2}S_{1}Γ because S′_{2} differs from S_{2} only on nonfree variables of S_{1}Γ,

S′_{2}S_{1}Γ + x: Clos_{S′_{2}S_{1}Γ}(S′_{2}S_{1}β) ⊢ e_{2} : S_{2}S_{1}ρ.

Hence by the (LET) rule, S′_{2}S_{1}Γ ⊢ let x = e_{1} in e_{2} : S_{2}S_{1}ρ; that is,

S_{2}S_{1}Γ ⊢ let x = e_{1} in e_{2} : S_{2}S_{1}ρ.

—case fix f λx.e: Let S = M(Γ + f: ρ, λx.e, ρ).

(1) By induction, (M.9) implies

SΓ + f: Sρ ⊢ λx.e : Sρ.

(2) By (FIX), SΓ ⊢ fix f λx.e : Sρ.

Definition 1 [Damas and Milner 1982]. Let σ and σ′ be type schemes such that σ = ∀α⃗.τ and σ′ = ∀β⃗.τ′. If there exists a substitution R such that supp(R) ⊆ α⃗ and τ′ = Rτ, and ftv(σ) ⊆ ftv(σ′), we say that σ′ is a generic instance of σ, and we write σ ≻ σ′. We also write Γ ≻ Γ′ if and only if dom(Γ) = dom(Γ′) and Γ(x) ≻ Γ′(x) for all x ∈ dom(Γ).

Theorem 2 (Completeness of M). Let e be an expression, and let Γ be a type environment. If there exist a type ρ and a substitution P such that P Γ ⊢ e : P ρ, then M(Γ, e, ρ) = S is defined, and there exists a substitution R such that P | -_{New} = (RS)| -_{New} where New is the set of new type variables used by M(Γ, e, ρ).

Completeness means that if an expression e has a type τ that satisfies a type constraint ρ (i.e., ∃P.τ = P ρ), then algorithm M for the expression with the constraint ρ succeeds with substitution S such that the result type Sρ subsumes τ (i.e., the principality, ∃R.τ = R(Sρ)).

The completeness proof uses Lemmas 3–7.

Lemma 3. Let S be a substitution, Γ be a type environment, and τ be a type. Then SClos_{Γ}(τ) ≻ Clos_{SΓ}(Sτ).

Proof. See Appendix A.

Lemma 4 [Damas and Milner 1982]. Let Γ and Γ′ be type environments such that Γ ≻ Γ′. If Γ′ ⊢ e : τ, then Γ ⊢ e : τ.

Lemma 5. If S = U(τ, τ′) then itv(S) ⊆ ftv(τ) ∪ ftv(τ′).

Proof. By the definition of the unification algorithm [Robinson 1965].

Lemma 6. If S = M(Γ, e, ρ) then itv(S) ⊆ ftv(Γ) ∪ ftv(ρ) ∪ New, where New is the set of new type variables used by M(Γ, e, ρ).

Proof. See Appendix B.

Lemma 7. If itv(S) ∩ A = ∅, then (RS)| -_{A} = R| -_{A}S.

Proof. See Appendix C.

Proof of Theorem 2. We prove by the structural induction on e. For a rigorous treatment of new type variables, we assume that every new type variable used throughout algorithm M is distinct from each other, and moreover, the set New of new type variables used by each call M(Γ, e, ρ) satisfies New ∩(ftv(Γ)∪ftv(ρ)) = ∅.

—case (): Let the given judgment be P Γ ⊢ () : P ρ. By (CON), P ρ = ι. Because P ι = ι = P ρ, P is a unifier of ρ and ι. M(Γ, (), ρ) succeeds with the most general unifier S of ρ and ι (M.1). Hence there exists a substitution R such that P = RS.

—case x: Let the given judgment be P Γ ⊢ x : P ρ, and let β⃗ be the new type variables used at (M.2). First, we prove that a unifier of ρ and {β⃗/α⃗}τ exists, where Γ(x) = ∀α⃗.τ. By the (VAR) rule,

P Γ(x) ≻ P ρ.  (1)

Let γ⃗ be type variables such that (ftv(Γ) ∪ ftv(ρ) ∪ itv(P) ∪ β⃗) ∩ γ⃗ = ∅. Then

P Γ(x) = P ∀α⃗.τ = ∀γ⃗.P {γ⃗/α⃗}τ.  (2)

From (1) and (2), there exists a substitution B such that supp(B) ⊆ γ⃗ and

BP {γ⃗/α⃗}τ = P ρ.  (3)

The right-hand side of (3) gives us

P ρ = P {γ⃗/β⃗}ρ  because ftv(ρ) ∩ β⃗ = ∅
= BP {γ⃗/β⃗}ρ because supp(B) ⊆ γ⃗ and γ⃗ ∩ (itv(P) ∪ ftv(ρ)) = ∅.

The left-hand side of (3) gives us

BP {γ⃗/α⃗}τ = BP {γ⃗/β⃗}{β⃗/α⃗}τ because β⃗ ∩ ftv(∀α⃗.τ) = ∅.

Thus BP {γ⃗/β⃗} is a unifier of ρ and {β⃗/α⃗}τ. Note that (BP {γ⃗/β⃗})| -_{γ⃗} is also a unifier because (ftv(ρ) ∪ ftv({β⃗/α⃗}τ)) ∩ γ⃗ = ∅. That is, (M.2) succeeds with the most general unifier S of ρ and {β⃗/α⃗}τ, and there exists a substitution R such that

RS = (BP {γ⃗/β⃗})| -_{γ⃗}.  (4)

Then

(RS)| -_{β⃗} = (BP {γ⃗/β⃗})| -_{γ⃗∪β⃗}
= (BP)| -_{γ⃗∪β⃗}
= (B| -_{γ⃗}P)| -_{β⃗}  by Lemma 7 and because itv(P) ∩ γ⃗ = ∅
= P | -_{β⃗}  because supp(B) ⊆ γ⃗.

—case λx.e: Let the given judgment be P Γ ⊢ λx.e : τ_{1} → τ_{2} where τ_{1} → τ_{2} = P ρ and New be {β_{1}, β_{2}} ∪ New_{1} , where β_{1} and β_{2} are the new type variables used at (M.3) and where New_{1} is the set of the new type variables used by M(S_{1}Γ + x: S_{1}β_{1}, e, S_{1}β_{2}) at (M.4). First, we prove the unification U(ρ, β_{1} → β_{2}) at (M.3) succeeds. Let P′ be {τ_{1}/β_{1}, τ_{2}/β_{2}} ∪ P | -_{{β_{1} ,β_{2} }}. Then P′ is a unifier of ρ and β_{1} → β_{2} because

P′ρ = P ρ  because {β_{1}, β_{2}} ∩ ftv(ρ) = ∅
= τ_{1} → τ_{2}
= P′(β_{1} → β_{2}).

Thus there exists a substitution R_{1} such that

R_{1}S_{1} = P′.  (5)

By the (FN) rule,

P Γ + x: τ_{1} ⊢ e : τ_{2}.  (6)

To apply induction to M(S_{1}Γ + x: S_{1}β_{1}, e, S_{1}β_{2}) at (M.4) and (6), we must prove that there exists a substitution P_{1} such that τ_{2} = P_{1}S_{1}β_{2} and P Γ + x: τ_{1} = P_{1}(S_{1}Γ + x: S_{1}β_{1}). Such P_{1} is the R_{1} at (5) because

\begin{aligned}R_{1}S_{1}β_{2} & = & P′β_{2} & by (5) \\ & = & τ_{2} \end{aligned}

and

R_{1}(S_{1}Γ + x: S_{1}β_{1}) = P′(Γ + x: β_{1})
= P Γ + x: τ_{1}  because {β_{1}, β_{2}} ∩ ftv(Γ) = ∅.

Thus by induction, (M.4) and (6) imply that there exists a substitution R_{2} such that

R_{1}| -_{New_{1}} = (R_{2}S_{2})| -_{New_{1}} .  (7)

Let R = R_{2}. Then

(RS)| -_{New} = (R_{2}S_{2}S_{1})| -_{New}
= ((R_{2}S_{2}S_{1})| -_{New_{1}} )| -_{{β_{1} ,β_{2} }}.  (8)

Note that itv(S_{1}) ∩ New_{1} = ∅ because itv(S_{1}) ⊆ ftv(ρ) ∪ {β_{1}, β_{2}} by Lemma 5, ftv(ρ) ∩ New_{1} ⊆ ftv(ρ) ∩ New = ∅, and {β_{1}, β_{2}} ∩ New_{1} = ∅ by the assumption that all new type variables are distinct from each other. Therefore, by Lemma 7, Eq. (8) becomes

((R_{2}S_{2}S_{1})| -_{New_{1}} )| -_{{β_{1} ,β_{2} }} = ((R_{2}S_{2})| -_{New_{1}} S_{1})| -_{{β_{1} ,β_{2} }}
= (R_{1}| -_{New_{1}} S_{1})| -_{{β_{1} ,β_{2} }}  by (7)
= ((R_{1}S_{1})| -_{New_{1}} )| -_{{β_{1} ,β_{2} }}  by Lemma 7
= (R_{1}S_{1})| -_{New}
= P′| -_{New}  by (5)
= P | -_{New}  because {β_{1}, β_{2}} ⊆ New.

—case e_{1} e_{2}: Let the given judgment be P Γ ⊢ e_{1} e_{2} : P ρ and New = {β} ∪ New_{1} ∪ New_{2} , where β is the new type variable used at (M.5) and New_{1} and New_{2} are the sets of the new type variables used by M(Γ, e_{1}, β → ρ) at (M.5) and M(S_{1}Γ, e_{2}, S_{1}β) at (M.6), respectively. By the (APP) rule, there exists a type τ such that

P Γ ⊢ e_{1} : τ → P ρ  (9)

and

P Γ ⊢ e_{2} : τ.  (10)

Let P′ = {τ/β} ∪ P | -_{{β}}. Then τ → P ρ = P′(β → ρ) and P Γ = P′Γ because β ∉ ftv(Γ) ∪ ftv(ρ). Hence, applying induction to M(Γ, e_{1}, β → ρ) at (M.5) and (9), there exists a substitution R_{1} such that

P′| -_{New_{1}} = (R_{1}S_{1})| -_{New_{1}} .  (11)

Similarly, we can apply induction to M(S_{1}Γ, e_{2}, S_{1}β) at (M.6) and (10) because

τ = P′β = R_{1}S_{1}β because β ∉ New_{1} and by (11)

and

P Γ = P′Γ  because β ∉ ftv(Γ)
= R_{1}S_{1}Γ because ftv(Γ) ∩ New_{1} = ∅ and by (11).

Thus by induction, there exists a substitution R_{2} such that

R_{1}| -_{New_{2}} = (R_{2}S_{2})| -_{New_{2}} .  (12)

Let R = R_{2}. Then

(RS)| -_{New} = (R_{2}S_{2}S_{1})| -_{New}
= ((R_{2}S_{2}S_{1})| -_{New_{2}} )| -_{New_{1} ∪{β}}.  (13)

Note that itv(S_{1}) ∩ New_{2} = ∅ because itv(S_{1}) ⊆ ftv(Γ) ∪ ftv(ρ) ∪ New_{1} ∪ {β} by Lemma 6, (ftv(Γ) ∪ ftv(ρ)) ∩ New_{2} ⊆ (ftv(Γ) ∪ ftv(ρ)) ∩ New = ∅, and (New_{1} ∪ {β}) ∩ New_{2} = ∅ by the assumption that all new type variables are distinct from each other. Therefore, by Lemma 7, Eq. (13) becomes

((R_{2}S_{2}S_{1})| -_{New_{2}} )| -_{New_{1} ∪{β}} = ((R_{2}S_{2})| -_{New_{2}} S_{1})| -_{New_{1} ∪{β}}
= (R_{1}| -_{New_{2}} S_{1})| -_{New_{1} ∪{β}}  by (12)
= (R_{1}S_{1})| -_{New}  by Lemma 7
= ((R_{1}S_{1})| -_{New_{1}} )| -_{New_{2} ∪{β}}
= P′| -_{New}  by (11)
= P | -_{New}  because β ∈ New.

—case let x = e_{1} in e_{2}: Let the given judgment be P Γ ⊢ let x = e_{1} in e_{2} : P ρ and New = {β} ∪ New_{1} ∪ New_{2} , where β is the new type variable used at (M.7) and where New_{1} and New_{2} are the sets of the new type variables used by M(Γ, e_{1}, β) at (M.7) and M(S_{1}Γ + x: Clos_{S_{1}Γ}(S_{1}β), e_{2}, S_{1}ρ) at (M.8), respectively. By the (LET) rule, there exists a type τ such that

P Γ ⊢ e_{1} : τ  (14)

and

P Γ + x: Clos_{P Γ}(τ) ⊢ e_{2} : P ρ.  (15)

Let P′ = {τ/β} ∪ P | -_{{β}}. Then τ = P′β and P Γ = P′Γ because β ∉ ftv(Γ). Hence by induction, (M.7) and (14) imply that there exists a substitution R_{1} such that

P′| -_{New_{1}} = (R_{1}S_{1})| -_{New_{1}} .  (16)

Note

Clos_{P Γ}(τ) = Clos_{P′Γ}(P′β)
= Clos_{R_{1}S_{1}Γ}(R_{1}S_{1}β) by (16) and (ftv(Γ) ∪ {β}) ∩ New_{1} = ∅
≺ R_{1}Clos_{S_{1}Γ}(S_{1}β) by Lemma 3

and P Γ = P′Γ = R_{1}S_{1}Γ because New_{1} ∩ ftv(Γ) = ∅. Thus

P Γ + x: Clos_{P Γ}(τ) ≺ R_{1}(S_{1}Γ + x: Clos_{S_{1}Γ}(S_{1}β)).

By Lemma 4 and (15),

R_{1}(S_{1}Γ + x: Clos_{S_{1}Γ}(S_{1}β)) ⊢ e_{2} : P ρ.

Because R_{1}S_{1}ρ = P′ρ = P ρ,

R_{1}(S_{1}Γ + x: Clos_{S_{1}Γ}(S_{1}β)) ⊢ e_{2} : R_{1}S_{1}ρ.  (17)

Thus by induction, (M.8) and (17) imply that there exists a substitution R_{2} such that

R_{1}| -_{New_{2}} = (R_{2}S_{2})| -_{New_{2}} .  (18)

Let R = R_{2}. Then, using (16) and (18) and following exactly the same steps in the proof for the application expression, we have

(RS)| -_{New} = P | -_{New}.

—case fix f λx.e: Let the given judgment be P Γ ⊢ fix f λx.e : P ρ. By the

(FIX) rule,

P Γ + f: P ρ ⊢ λx.e : P ρ.

By induction, M(Γ+f: ρ, λx.e, ρ) succeeds with a substitution S, and there exists a substitution R such that P | -_{New} = (RS)| -_{New}, where New is the set of new type variables used by M(Γ + f: ρ, λx.e, ρ) at (M.9). By (M.9), M(Γ, fix f λx.e, ρ) also succeeds with the S and P | -_{New} = (RS)| -_{New}.

4. M STOPS EARLIER THAN W DOES

We model the behaviors of the two type inference algorithms by their call strings. The call string of W(Γ, e) (written [[W(Γ, e)]]) is constructed by starting with the empty call string ϵ and appending a tuple (Γ_{1}, e_{1})^{d} (respectively, (Γ_{1}, e_{1})^{u}) whenever W(Γ_{1}, e_{1}) is called (respectively, returned). The d or u superscript indicates the downward or upward movement of the stack pointer when the inference algorithm is recursively called or returned. When the algorithm stops because of a unification failure the call string does not have matching returns (u tuples) for some calls (d tuples). We similarly define call strings for algorithm M.

For example, given an expression

                            \overbrace{(\underbrace{(fn x=>x)}_{e_{1}} 2)}^{e},

the call string [[W(Γ, e)]] is

(Γ, e)^{d}(Γ, e_{1})^{d}(Γ + x : β, x)^{d}(Γ + x : β, x)^{u}(Γ, e_{1})^{u}(Γ, 2)^{d}(Γ, 2)^{u}(Γ, e)^{u}.

For the ill-typed expression (1 2), the call string is

(Γ, 1 2)^{d}(Γ, 1)^{d}(Γ, 1)^{u}(Γ, 2)^{d}(Γ, 2)^{u}.

Note that tuple (Γ, 1 2)^{u} is missing because the algorithm stops because of the unification failure at the application.

Note that call strings [[W(Γ, e)]] and [[M(Γ, e, ρ)]] are always finite because, for any expression e, type environment Γ, and a type ρ, at most one call to W (respectively, M) occurs for each subexpression of e during W(Γ, e) (respectively, M(Γ, e, ρ)).

We say that “W (respectively, M) fails at an expression e” whenever the current argument expression to W (respectively, M) is e when the unification fails:

Definition 2. Let Γ be a type environment, e be an expression that has a type error, and β be a new type variable. “W(Γ, e) fails at e′” whenever the rightmost unmatching tuple in its call string [[W(Γ, e)]] is (Γ′, e′)^{d}. Similarly, “M(Γ, e, β) fails at e′” whenever the rightmost unmatching tuple in its call string [[M(Γ, e, β)]] is (Γ′, e′, ρ′)^{d}.

Example 1. Consider an expression ((λx.x^"a") true). W fails at the top expression ((λx.x^"a") true) after it succeeded at every proper subexpression. Meanwhile M fails at true.

Example 2. Consider an expression (1 (2 3)). W fails at (2 3). M fails at 1, which is earlier than W does because the left expression 1 is checked before the right expression (2 3).

Example 3. Consider an expression ((λx.x+1) λy.(1 1)). W fails at (1 1). M fails at (λy.(1 1)), which is before it checks the body expression (1 1).

As the above examples indicate, algorithm M always stops earlier than Algorithm W:

Theorem 3 (Earliness). Let Γ be a type environment, e be an expression, and β be a new type variable. Then

|[[M(Γ, e, β)]]| ≤ |[[W(Γ, e)]]|,

where |s| is the number of tuples in call string s.

The proof of Theorem 3 uses the completeness of Algorithm W and Lemmas 8–11.

Theorem 4 (Completeness of W) [Damas and Milner 1982]. Given Γ and e, let Γ′ be an instance of Γ and σ a type scheme such that Γ′ ⊢ e : σ. Then W(Γ, e) succeeds, and if W(Γ, e) = (S, τ) then, for some substitution R, Γ′ = RSΓ and RClos_{SΓ}(τ) ≻ σ.

Lemma 8. Let Γ and Γ′ be type environments and τ be a type. If Γ ≻ Γ′, then Clos_{Γ}(τ) ≻ Clos_{Γ′}(τ).

Proof. See Appendix D.

Lemma 9 [Damas and Milner 1982]. If σ ≻ σ′ then Sσ ≻ Sσ′.

Lemma 10. Let e be an expression, Γ be a type environment, and β be a new type variable. If [[W(Γ, e)]] has (Γ^{W}, e′)^{d} and [[M(Γ, e, β)]] has (Γ^{M}, e′, ρ)^{d}, then there exists a substitution R such that RΓ^{W} ≻ Γ^{M}. (Note that because W and M are called only once for each subexpression of e, such Γ^{W} and Γ^{M} are well defined.)

Proof. We prove by induction on the length of the prefixes (Γ, e)^{d} ⋯ (Γ^{W}, e′)^{d} of [[W(Γ, e)]] and (Γ, e, β)^{d} ⋯ (Γ^{M}, e′, ρ)^{d} of [[M(Γ, e, β)]]. Note that the prefixes have the same length because W and M check the sub-expressions of e in the same order. The symbols of both algorithms are identified by their superscripts.

—base case: When the prefixes are of length 1, they represent the initial calls where e′ is e and where Γ^{W} and Γ^{M} are identical. Then the identity substitution R satisfies RΓ^{W} ≻ Γ^{M}.

Followings are inductive cases.

—case e′ of e_{1} in “λx.e_{1}”: Let the type environment parameters be Γ^{W} and Γ^{M} when λx.e is visited. By induction, RΓ^{W} ≻ Γ^{M}; that is, by Lemma 9, S_{1}^{M}RΓ^{W} ≻ S_{1}^{M}Γ^{M}. Let R_{1} = S_{1}^{M}(R| -_{{β^{W} }} ∪ {β_{1}^{M}/β^{W}}). Then

R_{1}(Γ^{W} + x: β^{W}) = S_{1}^{M}RΓ^{W} + x: S_{1}^{M}β_{1}^{M} because β^{W} ∉ ftv(Γ^{W})
≻ S_{1}^{M}Γ^{M} + x: S_{1}^{M}β_{1}^{M}.

—case e′ of e_{1} in “e_{1} e_{2}”: The call at e_{1} occurs with the same environment as the one that accompanied the call at e_{1} e_{2}. Thus the case holds by the induction hypothesis.

—case e′ of e_{2} in “e_{1} e_{2}”:

(1) By the soundness of M, (M.5) implies

S_{1}^{M}Γ^{M} ⊢ e_{1} : S_{1}^{M}(β^{M} → ρ^{M}).

(2) By induction, RΓ^{W} ≻ Γ^{M}; that is, by Lemma 9, S_{1}^{M}RΓ^{W} ≻ S_{1}^{M}Γ^{M}. By Lemma 4,

S_{1}^{M}RΓ^{W} ⊢ e_{1} : S_{1}^{M}(β^{M} → ρ^{M}).

(3) By the completeness of W, there exists a substitution R′ such that R′S_{1}^{W}Γ^{W} = S_{1}^{M}RΓ^{W}. So, R′S_{1}^{W}Γ^{W} = S_{1}^{M}RΓ^{W} ≻ S_{1}^{M}Γ^{M}.

—case e′ of e_{1} in “let x = e_{1} in e_{2}”: The call at e_{1} occurs with the same environment as the one that accompanied the call at let x = e_{1} in e_{2}. Thus the case holds by the induction hypothesis.

—case e′ of e_{2} in “let x = e_{1} in e_{2}”:

(1) By the soundness of M, (M.7) implies

S_{1}^{M}Γ^{M} ⊢ e_{1} : S_{1}^{M}β^{M}.

(2) By induction, RΓ^{W} ≻ Γ^{M}; that is, by Lemma 9, S_{1}^{M}RΓ^{W} ≻ S_{1}^{M}Γ^{M}. By Lemma 4,

S_{1}^{M}RΓ^{W} ⊢ e_{1} : S_{1}^{M}β^{M}.

(3) By the completeness of W, there exists a substitution R′ such that R′τ_{1}^{W} = S_{1}^{M}β^{M} and R′S_{1}^{W}Γ^{W} = S_{1}^{M}RΓ^{W}. Therefore,

R′S_{1}^{W}Γ^{W} ≻ S_{1}^{M}Γ^{M}

and

R′Clos_{S_{1}^{W} Γ^{W}} (τ_{1}^{W}) ≻ Clos_{R′S_{1}^{W} Γ^{W}} (R′τ_{1}^{W}) by Lemma 3
= Clos_{R′S_{1}^{W} Γ^{W}} (S_{1}^{M}β^{M})
≻ Clos_{S_{1}^{M}Γ^{M}}(S_{1}^{M}β^{M}) by Lemma 8.

The above two facts imply that this case is proven. —case e′ of λx.e in “fix f λx.e”: By induction, there exists a substitution R

such that RΓ^{W} ≻ Γ^{M}. Let R′ = R| -_{{β^{W} }} ∪ {ρ^{M}/β^{W}}. Then

R′(Γ^{W} + f: β^{W}) = RΓ^{W} + f: ρ^{M} because β^{W} ∉ ftv(Γ^{W})
≻ Γ^{M} + f: ρ^{M}.

Lemma 11. Let e be an expression, Γ be a type environment, and β be a new type variable. Suppose [[W(Γ, e)]] has (Γ^{W}, e′)^{d} and [[M(Γ, e, β)]] has (Γ^{M}, e′, ρ)^{d}. If W(Γ^{W}, e′) fails, then M(Γ^{M}, e′, ρ) fails.

Proof. Assume for contradiction that M(Γ^{M}, e′, ρ) succeeds; that is, M(Γ^{M}, e′, ρ) = S is defined. By the soundness of M,

SΓ^{M} ⊢ e′ : Sρ.

By Lemma 10, there exists a substitution R such that RΓ^{W} ≻ Γ^{M}; that is, by Lemma 9, SRΓ^{W} ≻ SΓ^{M}. By Lemma 4,

SRΓ^{W} ⊢ e′ : Sρ.

And, finally, by the completeness of W, W(Γ^{W}, e′) succeeds. It contrasts with the given condition, so the assumption is not true.

Now we prove Theorem 3.

Proof of Theorem 3. The case that e has no type error is trivially true, because it is obvious that |[[W(Γ, e)]]| = |[[M(Γ, e, β)]]|.

Let us consider the case that e has a type error. Let W(Γ, e) fail at an application expression (e_{1} e_{2}). Then

[[W(Γ, e)]] = ⋯ (Γ_{1}^{W}, e_{1} e_{2})^{d} ⋯ (Γ_{2}^{W}, e_{2})^{u}

because W fails right after it returned from an application’s operand. Suppose for contradiction that

|[[W(Γ, e)]]| < |[[M(Γ, e, β)]]|.

That is,

[[M(Γ, e, β)]] = ⋯ (Γ_{1}^{M}, e_{1} e_{2}, ρ_{1})^{d} ⋯ (Γ_{2}^{M}, e_{2}, ρ_{2})^{u} · κ

and

κ ≠ ϵ

because the order of visiting subexpressions is the same for W and M. The next call/return after the return from e_{2} is the return from e_{1} e_{2}. So κ is (Γ_{1}^{M}, e_{1} e_{2}, ρ_{1})^{u}· κ′. It means that M(Γ_{1}^{M}, e_{1} e_{2}, ρ_{1}) succeeds. However, it is impossible by Lemma 11 because W(Γ_{1}^{W}, e_{1} e_{2}) fails.

5. CONCLUSION

The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the de facto standard W algorithm [Milner 1978; Damas and Milner 1982] that is bottom-up (or context-insensitive) and the other is a “folklore” algorithm that is top-down (or context-sensitive).

In this article, we formally defined the folklore algorithm (named M), proved its soundness and completeness, and showed that M always finds type errors earlier (considers a less number of expressions) than W.

Our proofs can be seen as theoretical justifications for various type-checking strategies. For example, a compiler can let the user switch between the two algorithms, which may help in situations where it is hard to find the cause of the type error. The two algorithms will always stop at different expressions reporting different causes of the type problem. Already, a combination of a variant of M with W is being implemented in practice [Rideau and Théry 1997]. A compiler can also mix the two algorithms on-the-fly, choosing one algorithm against the other, depending on the current subexpression to type check. For example, when type-checking the definitions of recursive functions the compiler may switch to algorithm M, because it generates a better type diagnostic than W if the recursive calls have ill-typed arguments (as seen in Figure 1). A variant of this technique is implemented in the SML/NJ compiler system version 110. Similar bidirectional type-checking ideas have been formalized in the setting of subtyping and impredicative polymorphism [Pierce and Turner 1998].

Our formalization enables us to see clearly that algorithm M can unobtrusively adapt the existing techniques of generating informative type error messages, which were developed with Algorithm W in mind. The techniques of Wand [1986], Beaven and Stansifer [1993], Duggan and Bent [1996], and Rideau and Théry [1997] essentially record the history of the type instantiations (unifications) in the resulting substitutions. Because the type instantiation in M is via the same standard unification algorithm, these approaches can be directly used in M. For the same reason, inferring the types of free variables [Bernstein and Stark 1995], by which the programmer can probe the types of some puzzling points in his/her program, is also straightforward to implement inside M, by making such free variables all distinct and initially bound to fresh type variables. The idea in the destructive implementation of Algorithm W [Cardelli 1987], in which type variables are destructively updated during unification and free variables are remembered for quickly computing the type closure, can also be used in a practical implementation of algorithm M.

APPENDIX

A. PROOF OF LEMMA 3

Let α⃗ = ftv(τ)\ftv(Γ), and let β⃗ be type variables such that β⃗ ∩ (itv(S) ∪ ftv(τ)) = ∅ and |α⃗| = |β⃗|. Then

SClos_{Γ}(τ) = S∀α⃗.τ = ∀β⃗.S{β⃗/α⃗}τ.

Let R = {Sα⃗/β⃗}. Then Sτ = RS{β⃗/α⃗}τ and supp(R) ⊆ β⃗; thus, the first condition of generic instance is satisfied. The second condition holds as follows

ftv(SClos_{Γ}(τ)) = ⋃_{γ∈ftv(τ)∩ftv(Γ)} ftv(Sγ)

⊆ ( ⋃_{γ∈ftv(τ)} ftv(Sγ)) ∩ ( ⋃_{γ∈ftv(Γ)} ftv(Sγ))
= ftv(Sτ) ∩ ftv(SΓ)
= ftv(Clos_{SΓ}(Sτ)).

B. PROOF OF LEMMA 6

The proof uses Lemma 12.

Lemma 12 [Milner 1978]. Let R and S be substitutions and τ be a type. Then

—itv(RS) ⊆ itv(R) ∪ itv(S) and

—ftv(Sτ) ⊆ ftv(τ) ∪ itv(S).

The proof is by the structural induction on e.

—case (): By Lemma 5, itv(U(ρ, ι)) ⊆ ftv(ρ) ∪ ftv(ι) ⊆ ftv(ρ).

—case x:
itv(U(ρ, [β_{i}/α_{i}]τ)) ⊆ ftv(ρ) ∪ ftv({β⃗/α⃗}τ)  by Lemma 5
⊆ ftv(ρ) ∪ (ftv(τ) \ α⃗) ∪ β⃗
= ftv(ρ) ∪ ftv(∀α⃗.τ) ∪ β⃗
= ftv(ρ) ∪ ftv(Γ(x)) ∪ β⃗
⊆ ftv(ρ) ∪ ftv(Γ) ∪ New.

—case λx.e: By Lemma 5, itv(S_{1}) ⊆ ftv(ρ) ∪ ftv(β_{1} → β_{2}). By induction,

itv(S_{2}) ⊆ ftv(S_{1}Γ + x: S_{1}β_{1}) ∪ ftv(S_{1}β_{2}) ∪ New_{1}
⊆ itv(S_{1}) ∪ ftv(Γ) ∪ New_{1} ∪ {β_{1}, β_{2}}  by Lemma 12.

Hence, itv(S_{2}S_{1}) ⊆ itv(S_{1}) ∪ itv(S_{2}) ⊆ ftv(Γ) ∪ ftv(ρ) ∪ New_{1} ∪ {β_{1}, β_{2}}.

Other cases can be similarly proven.

C. PROOF OF LEMMA 7

We prove that (RS)| -_{A}α = R| -_{A}Sα for all α.

—case α ∈ A: (RS)| -_{A}α = α, and because itv(S) ∩ A = ∅, R| -_{A}Sα = R| -_{A}α = α. —case α ∉ A: (RS)| -_{A}α = RSα. When α ∈ supp(S), R| -_{A}Sα = RSα because

itv(S) ∩ A = ∅. When α ∉ supp(S), R| -_{A}Sα = Rα = RSα.

D. PROOF OF LEMMA 8

By the definition, Γ(x) ≻ Γ′(x) for ∀x ∈ dom(Γ). This implies ftv(Γ(x)) ⊆ ftv(Γ′(x)) for ∀x ∈ dom(Γ), that is, ftv(Γ) ⊆ ftv(Γ′). Therefore,

ftv(Clos_{Γ}(τ)) = ftv(τ) ∩ ftv(Γ) ⊆ ftv(τ) ∩ ftv(Γ′) = ftv(Clos_{Γ′}(τ)).

ACKNOWLEDGMENTS

We thank anonymous referees and the associate editor for their valuable suggestions and corrections that substantially improved our presentation. We thank David MacQueen for his encouragement on an early draft of this article, and Laurent Théry, Xavier Leroy, and Pierre Weis for sharing their experiences of the two type inference algorithms. We thank Hyunjun Eo, Hyunsok Oh, and Sukyoung Ryu for their comments during this work.

REFERENCES Beaven, M. and Stansifer, R. 1993. Explaining type errors in polymorphic languages. ACM

Lett. Program. Lang. Syst. 2, 17–30. Bernstein, K. L. and Stark, E. W. 1995. Debugging type errors (full version). Tech. Rep.,

State University of New York at Stony Brook. Cardelli, L. 1987. Basic polymorphic typechecking. Sci. Comput. Program. 8, 2 (Apr.). Damas, L. and Milner, R. 1982. Principal type-scheme for functional programs. In Proceedings of

the 9th Annual ACM Symposium on Principles of Programming Languages. ACM, New York, 207–212.

Duggan, D. and Bent, F. 1996. Explaining type inference. Sci. Comput. Program. 27, 1 (July),

37–83. Johnson, G. F. and Walz, J. A. 1986. A maximal-flow approach to anomaly isolation in

unification-based incremental type inference. In Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages. ACM, New York, 44–57.

Leroy, X. 1993. The caml light system, release 0.6. Institut National de Recherche en Informatique

et en Automatique. Leroy, X. 1995. The caml light system, release 0.7. Institut National de Recherche en Informatique

et en Automatique. MacQueen, D. B. and Appel, A. W. 1993. Standard ML of New Jersey. Tech. Memo., AT&T

Bell Labs. Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17,

348–375. Pierce, B. C. and Turner, D. N. 1998. Local type inference. In Proceedings of the 25th Annual

ACM Symposium on Principles of Programming Languages. ACM, New York. Rideau, L. and Théry, L. 1997. Interactive programming environment for ML. Tech. Rep. 3139,

Institut National de Recherche en Informatique et en Automatique. March. Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1

(Jan.), 23–41. Wand, M. 1986. Finding the source of type errors. In Proceedings of the 13th Annual ACM

Symposium on Principles of Programming Languages. ACM, New York, 38–43.

Received July 1997; revised March 1998; accepted July 1998