Principal type-schemes for functional programs

Luis Damas and Robin Milner

1 Introduction

This paper is concerned with the polymorphic type discipline of ML, which is a general purpose functional programming language, although it was first introduced as a metalanguage (whence its name) for conducting proofs in the LCF proof system [GMW79]. The type discipline was studied in [Mil78], where it was shown to be semantically sound, in a sense made precise below, but where one important question was left open: does the type-checking algorithm—or more precisely, the type assignment algorithm (since types are assigned by the compiler, and need not be mentioned by the programmer)—find the most general type possible for every expression and declaration? Here we answer the question in the affirmative, for the purely applicative part of ML. It follows immediately that it is decidable whether a program is well-typed, in contrast with the elegant and slightly more permissive type discipline of Coppo [Cop80]. After several years of successful use of the language, both in LCF and other research and in teaching to undergraduates, it has become important to answer these questions—particularly because the combination of flexibility (due to polymorphism), robustness (due to semantic soundness) and detection of errors at compile time has proved to be one of the strongest aspects of ML.

The discipline can be well illustrated by a small example. Let us define in ML the function “map”, which maps a given function over a given list—that is,

map f [x_{1},…,x_{n}] [f(x_{1}),…,f(x_{n})]

The required declaration is

fun map f s =
if null s

                     then nil

else cons (f(hd s)) (map f (tl s))

The type-checker will deduce a type-scheme for “map” from existing typeschemes for “null”, “nil”, “cons”, “hd” and “tl”; the term “type-scheme” is

\begin{matrix}c \\ ◯ \end{matrix} 1982 ACM 0-89791-065-6/82/001/0207 $00.75

This is a reprint of a paper by Luis Damas and Robin Milner which appeared in the conference record of the Ninth Annual Symposium on Principles of Programming Languages, Albuquerque, New Mexico, 1982.

Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

appropriate since all these objects are polymorphic. In fact, from

null : ∀α(α list → bool)
nil : ∀α(α list)
cons : ∀α(α → (α list → α list))
hd : ∀α(α list → α)
tl : ∀α(α list → α list)

will be deduced

map : ∀α∀β((α → β) → (α list → β list)).

Types are built from type constants (bool, …) and type variables (α, β, …) using type operators (such as infixed → for functions and postfixed “list” for lists); a type-scheme is a type with (possibly) quantification over type variables at the outermost.

Thus, the main result of this paper is that the type-scheme deduced for such a declaration (and more generally, for any ML expression) is a principal typescheme, i.e. that any other type-scheme for the declaration is a generic instance of it. This is a generalisation of Hindley’s result for Combinatory Logic [Hin69].

ML may be contrasted with ALGOL 68, in which there is no polymorphism, and with Russell [DD79], in which parametric types appear explicitly as arguments to polymorphic functions. The generic types of Ada may be compared with type schemes. For simplicity, our definitions and results here are formulated for a skeletal language, since their extension to ML is a routine matter. For example, recursion is omitted since it can be introduced by simply adding the polymorphic fixed-point operator

fix : ∀α((α → α) → α)

and likewise for conditional expressions.

2 The language

Assuming a set Id of identifiers x, the language Exp of expressions e is given by the syntax

e ::= x | e e′ | λx.e | let x = e in e′

(where parentheses may be used to avoid ambiguity). Only the last clause extends the λ-calculus. Indeed, for type checking purposes every let expression could be eliminated (by replacing x by e everywhere in e′), except for the important consideration that in on-line use of ML declarations

let x = e

are allowed, whose scope (e′) is the remainder of the on-line session. As illustrated in the introduction, it must be possible to assign type-schemes to identifiers thus declared.

Note that types are absent from the language Exp. Assuming a set of type variables α and of primitive types ι, the syntax of types τ and of typeschemes σ is given by

τ ::= α | ι | τ → τ
σ ::= τ | ∀ασ

A type-scheme ∀α_{1} … ∀α_{n}τ (which we may write ∀α_{1} … α_{n}τ) has generic type variables α_{1}, …, α_{n}. A monotype μ is a type containing no type variables.

3 Type Instantiation

If S is a substitution of types for type variables, often written [τ_{1}/α_{1}, …, τ_{n}/α_{n}] or [τ_{i}/α_{i}], and σ is a type-scheme, then Sσ is the type-scheme obtained by replacing each free occurrence of α_{i} in σ by τ_{i}, renaming the generic variables of σ if necessary. Then Sσ is called an instance of σ; the notions of substitution and instance extend naturally to larger syntactic constructs containing typeschemes.

By contrast, a type scheme σ = ∀α_{1} … α_{m}τ has a generic instance σ′ = ∀β_{1} … β_{n}τ′ if τ′ = [τ_{i}/α_{i}]τ for some types τ_{1}, …, τ_{m}, and the β_{j} are not free in σ. In this case we shall write σ > σ′. Note that instantiation acts on free variables, while generic instantiation acts on bound variables. It follows that σ > σ′ implies Sσ > Sσ′.

4 Semantics

The semantic domain V for Exp is a complete partial order satisfying the following equations up to isomorphism, where B_{i} is a cpo corresponding to primitive type ι_{i}:

V = B_{0} + B_{1} + ⋯ + F + W (disjoint sum)
F = V → V  (function space)
W = { · }  (error element)

To each monotype μ corresponds a subset of V, as detailed in [Mil78]; if v ∈ V is in the subset for μ, we write v : μ. Further, we write v : τ if v : μ for every monotype instance μ of τ, and we write v : σ if v : τ for every τ which is a generic instance of σ.

Now let Env = Id → V be the domain of environments η. The semantic function E : Exp → Env → V is given in [Mil78]. Using it, we wish to attach meaning to assertions of the form

A ⊧ e : σ

where e ∈ Exp and A is a set of assumptions of the form x : σ′, x ∈ Id. If the assertion is closed, i.e. if A and σ contain no free type variables, then the sentence is said to hold iff, for every environment η, whenever η[[x]] : σ′ for each

TAUT:  A ⊢ x : σ  (x : σ in A)
INST:  \frac{A ⊢ e : σ}{A ⊢ e : σ′}  (σ > σ′)

GEN:  \frac{A ⊢ e : σ}{A ⊢ e : ∀ασ}  (α not free in A)

COMB:  \frac{A ⊢ e : τ′ → τ  A ⊢ e′ : τ′}{A ⊢ (e e′) : τ}

ABS:  \frac{A_{x} ∪ \{ x : τ′ \} ⊢ e : τ}{A ⊢ (λx.e) : τ′ → τ}

LET:  \frac{A ⊢ e : σ  A_{x} ∪ \{ x : σ \} ⊢ e′ : τ}{A ⊢ (let x = e in e′) : τ}

Figure 1: Inference rules for the language

member x : σ′ of A, it follows that E[[e]]η : σ. Further, an assertion holds iff all its closed instances hold. Thus, to verify the assertion

x : α, f : ∀β(β → β) ⊧ (fx) : α

It is enough to verify it for every monotype μ in place of α. This example illustrates that free type-variables in an assertion are implicitly quantified over the whole assertion, while explicit quantification in a type scheme has restricted scope.

The remainder of this paper proceeds as follows. First we present an inference system for inferring valid assertions. Next we present an algorithm W for computing a type-scheme for any expression, under assumptions A. We then show that W is sound, in the sense that any type-scheme which it yields is derivable in the inference system. Finally we show that W is complete, in the sense that derivable type-scheme is an instance of that computed by W.

5 Type Inference

From now on we shall assume that A contains at most one assumption about each identifier x. A_{x} stands for the result of removing any assumption about x from A.

For assumptions A, expression e and type-scheme σ we write

A ⊢ e : σ

if this sentence may be derived from the inference rules in Figure 1.

The derivation in Figure 2 is organised as a tree in which each node follows from those immediately above it by an inference rule. The following proposition, stating the semantic soundness of inference, can be proved by induction on e.

i : ∀α(α → α) ⊢ i : ∀α(α → α) INST i : ∀α(α → α) ⊢ i : (α → α) → (α → α) COMB  i : ∀α(α → α) ⊢ i : ∀α(α → α) INST i : ∀α(α → α) ⊢ i : α → α x : α ⊢ x : α ABS ⊢ λx.x : α → α GEN ⊢ λx.x : ∀α(α → α) LET  i : ∀α(α → α) ⊢ i i : α → α ⊢ (let i = λx.x in i i) : α → α

Figure 2: A sample derivation

Proposition 1 (soundness of inference) If A ⊢ e : σ then A ⊧ e : σ. We will also require later the two following properties of the inference system.

Proposition 2 If S is a substitution and A ⊢ e : σ then SA ⊢ e : Sσ. Moreover if there is a derivation of A ⊢ e : σ of height n then there is also a derivation of SA ⊢ e : Sσ of height less or equal to n.

Proof by induction on n. □

Lemma 1 If σ > σ′ and A_{x} ∪ {x : σ′} ⊢ e : σ_{0} then also A_{x} ∪ {x : σ} ⊢ e : σ_{0}.

Proof: We construct a derivation of A_{x} ∪ {x : σ} ⊢ e : σ_{0} from that of A_{x} ∪ {x : σ′} ⊢ e : σ_{0} by substituting each use of TAUT for x : σ′ with x : σ followed by an INST step to derive x : σ′. Note that GEN steps remain valid since if α occurs free in σ then it also occurs free in σ′. □

6 The type assignment algorithm W

The type inference system by itself does not provide an easy method for finding, given A and e, a type-scheme σ such that A ⊢ e : σ. We now present an algorithm W for this purpose. In fact, W goes a step further. Given A and e, if W succeeds it finds a substitution S and a type τ, which are most general in a sense to be made precise below, such that

SA ⊢ e : τ

To define W we require the unification algorithm of Robinson [Rob65].

Proposition 3 (Robinson) There is an algorithm U which, given a pair of types, either returns a substitution V or fails; further

(1) If U(τ, τ′) returns V, then V unifies τ and τ′, i.e. V τ = V τ′.

(2) If S unifies τ and τ′, then U(τ, τ′) returns some V and there is another substitution R such that S = RV.

Moreover, V involves only variables in τ and τ′.

We also need to define the closure of a type τ with respect to assumptions A;

\overline{A}(τ) = ∀α_{1} … α_{n}τ

where α_{1}, …, α_{n} are the type-variables occurring free in τ but not in A.

Algorithm W

W (A, e) = (S, τ) where

(1) If e is x and there is an assumption x : ∀α_{1} … α_{n}τ′ in A then S = Id and τ = [β_{i}/α_{i}]τ′ where the β_{i}’s are new.

(2) If e is e_{1}e_{2} then let W (A, e_{1}) = (S_{1}, τ_{1}) and W (S_{1}A, e_{2}) = (S_{2}, τ_{2}) and U(S_{2}τ_{1}, τ_{2} → β) = V where β is new; then S = V S_{2}S_{1} and τ = V β.

(3) If e is λx.e_{1} then let β be a new type variable and W (A_{x} ∪ {x : β}, e_{1}) = (S_{1}, τ_{1}); then S = S_{1} and τ = S_{1}β → τ_{1}.

(4) If e is let x = e_{1} in e_{2} then let W (A, e_{1}) = (S_{1}, τ_{1}) and W (S_{1}A_{x} ∪ \{x : \overline{S_{1}A}(τ_{1})\}, e_{2}) = (S_{2}, τ_{2}); then S = S_{2}S_{1} and τ = τ_{2}.

NOTE: When any of the conditions above is not met W fails.

The following proposition proves that W meets our requirements.

Proposition 4 (Soundness of W) If W (A, e) succeeds with (S, τ) then there is a derivation of SA ⊢ e : τ.

Proof By induction on e using proposition 2. □

It follows that there is also a derivation of SA ⊢ e : \overline{SA}(τ). We refer to \overline{SA}(τ) as a type-scheme computed by W for e under SA.

7 Completeness of W

Given A and e, we will call σ_{P} a principal type-scheme of e under assumptions A iff

(1) A ⊢ e : σ_{P}

(2) Any other σ for which A ⊢ e : σ is a generic instance of σ_{P}.

Our main result, restricted to the simple case in which A contains no free typevariables, may be stated as follows:

If A ⊢ e : σ, for some σ, then W computes a principal type scheme for e under A.

This is a direct corollary of the following general theorem, which is a stronger result suited to inductive proof:

Theorem (Completeness of W) Given A and e, let A′ be an instance of A and σ a type-scheme such that

A′ ⊢ e : σ

Then

(1) W (A, e) succeeds

(2) If W (A, e) = (S, τ) then, for some substitution R, A′ = RSA and R\overline{SA}(τ) > σ. □

In fact, from the theorem one also derives as corollaries that it is decidable whether e has any type at all under assumptions A, and that, if so, it has a principal type scheme under A.

The detailed proofs of results in this paper, and related results, will appear in the first author’s forthcoming PhD Thesis.

References

[Cop80] M. Coppo. An extended polymorphic type system for applicative languages. In LNCS 88, pages 194–204. Springer-Verlag, 1980.

[DD79] A. Demers and J. Donahue. Report on the programming language Russell. Technical Report TR 79-371, Computer Science Department, Cornell University, 1979.

[GMW79] M.J. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF. Springer LNCS 78, Berlin, 1979.

[Hin69] J.R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc, 146:29–60, 1969.

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

[Rob65] J.A. Robinson. A machine oriented logic based on the resolution principle. JACM, 12(1):23–41, 1965.