A Theory of Type Polymorphism in Programming

1 INTRODUCTION

The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose no discipline of types (LISP is a perfect example), entails defining procedures which work well on objects of a wide variety (e.g., on lists of atoms, integers, or lists). Such flexibility is almost essential in this style of programming; unfortunately one often pays a price for it in the time taken to find rather inscrutable bugs—anyone who mistakenly applies CDR to an atom in LISP, and finds himself absurdly adding a property list to an integer, will know the symptoms. On the other hand a type discipline such as that of ALGOL 68 [22] which precludes the flexibility mentioned above, also precludes the programming style which we are talking about. ALGOL 60 was more flexible—in that it required procedure parameters to be specified only as "procedure" (rather than say "integer to real procedure")—but the flexibility was not uniform, and not sufficient.

An early discussion of such flexibility can be found in Strachey [19], who was probably the first to call it polymorphism. In fact he qualified it as "parametric" polymorphism, in contrast to what he called "adhoc" polymorphism. An example of the latter is the use of "+*" to denote both integer and real addition (in fact it may be further extended to denote complex addition, vector addition, etc.); this use of an identifier at several distinct types is often now called "overloading," and we are not concerned with it in this paper.

In this paper then, we present and justify one method of gaining type flexibility, but also retaining a discipline which ensures robust programs. We have evidence that this work is not just a theoretical exercise; the polymorphic type discipline which we discuss here has been incorporated in the LCF metalanguage ML [2, 3], and has been in use for nearly 2 years. The compile-time type checker for this language has proved to be a valuable filter which traps a significant proportion of programming errors.

The main body of the present paper is concerned with a technical account—both semantic and syntactic—of our discipline of types in the context of a simple illustrative language, but at this point it is helpful to characterize the approach informally. We outline its predominant features.

First, everything concerning types is done at compile time; once the type checker (part of the compiler) has accepted a program or program phrase, code may be generated which assumes that no objects carry their types at run-time. This is widely accepted as yielding efficient object code, though it does impose constraints on the use of types compared with, for example, the approach in EL1 [21].

Second, many nontrivial programs can avoid mentioning types entirely, since they be inferred from context. (In ML however, as in other languages, the user may—indeed often should—define his own types together with operations over these types. Recent languages which allow the user to define his own types in this manner are CLU [8], ALPHARD [23] and Euclid [6]). Although it can be argued convincingly that to demand type specification for declared variables, including the formal parameters of procedures, leads to more intelligible problems, it is also convenient—particularly in on-line programming—to be able to leave out these specifications. In any case, the type checker which we present is quite simple and could not be made much simpler even if the types of variables were always specified in declarations.

Third, polymorphism plays a leading role. For example, a procedure is assigned a polymorphic type (which we abbreviate to polytype) in general; only when the types of its arguments and result can be uniquely determined from the context is it monomorphic (i.e., assigned a monotype). Gries and Gehani [4], among others, have made a convincing case for controlled polymorphic programming (in contrast with the typeless programming in LISP or in SNOBOL); for them however, and also for Tennent [20], the presence of type variables or identifiers is needed to specify polymorphic types. For us, the polymorphism present in a program is a natural outgrowth of the primitive polymorphic operators which appear to exist in every programming language; such operators are assignment, function application, pairing and tupling, and list-processing operators. It is principally the type constraints on these operators, and in the declaration and use of variables, which determine for us the types of a program phrase and its subphrases.

We do not discuss in this paper—except briefly at the end—either coercions or the "overloading" of identifiers. Our view is that these concepts, and also run-time type manipulation, are somewhat orthogonal to a compile-time polymorphic type discipline, and may (to some extent) be incorporated without invalidating it.

In Section 2 we illustrate our type discipline by examples in a fragment of ML. This fragment should be self-explanatory, but an outline of ML is given in [3] and a full description appears in [2]. These illustrations should serve to make the point that we are able to handle useful languages. The remainder of the paper justifies the discipline using a very simple applicative language, Exp. The justification factors into two parts.

In Section 3 we define the notion of well typing (correct type assignment) and prove the Semantic Soundness Theorem, which says that a well-typed program is semantically free of type violation. If we were to give an operational definition of the language, this would imply that, for example, an integer is never added to a truth value or applied to an argument, and consequently need not carry its type around for run-time checking. In Section 4 we present a well-type algorithm $\mathcal{W}$ and prove the Syntactic Soundness Theorem, which states that $\mathcal{W}$, if it succeeds, produces a well typing of a program. We also give a more efficient algorithm $\mathcal{J}$, which simulates $\mathcal{W}$.

The types in Exp are just the hierarchy of purely functional types over a set of basic types. That is, the polymorphism in Exp is the natural outgrowth of a single primitive polymorphic operator, function application, together with variable binding. To add other primitive polymorphic operators, such as pairing and list-processing operators (as in ML), together with types built from basic ones $\times$ (Cartesian Product), list (list-forming), and $+$ (disjoint sum) in addition to (function type), presents no extra difficulty in the two soundness theorems. Indeed, adding an assignment operator is also easy as far as the Syntactic Soundness Theorem is concerned, but the Semantic Soundness Theorem is harder to extend in this case, due to the extra semantic complication of a memory or store which holds the current values of assignable variables. We discuss this further in Section 5.

Our work is a step towards solving the problem expressed by Morris [10] in his thesis as follows: "to design a language and a type system in which a programmer may define functions whose parameters may have different types for different calls of the function." We recommend Chapter 4 of this thesis as a lucid introduction to the problem. Although Morris does not discuss the semantics of types formally, or give a polymorphic type system, he describes how a valid type assignment may be found for a term of the $\lambda$-calculus by solving a set of simultaneous linear equations; we take this idea further in the next section.

After doing this work we became aware of Hindley's [5] method for deriving the "principal type scheme" (which is what we call a polymorphic type) for a term in combinatory logic. Hindley appears to have been the first to notice that the Unification Algorithm of Robinson [14] is appropriate to this problem. Our work can be regarded as an extension of Hindley's method to programming languages with local declarations, and as a semantic justification of the method.

In summary, we present a polymorphic type discipline which is syntactically well understood and justified for a currently used programming language with imperative features, and is also semantically explained for a nontrivial, though nonimperative, sublanguage.

2 ILLUSTRATIONS OF THE TYPE DISCIPLINE

We illustrate our notion of polymorphism by means of some simple examples. They are written in a fragment of ML which we hope is self-explanatory; this fragment is indeed no more than Landins ISWIM [7], and we refer the reader to Burge's book [1] in which he uses this style of programming almost exactly. We use no imperative constructs here (assignments or jumps). The constructs

are used to give $x$ the value of $e$, and to give $f$ the value of the abstraction $\lambda(x_1, ..., x_n) \cdot e$, throughout $e'$. For recursive functions letrec is used in place of let, and when the part in e' is omitted we have a declaration.

The fully determined types (i.e., the monotypes) of ML are built from a set of basic types (int, bool, etc.) by the binary infix operators $\times$ (Cartesian product), $+$ (disjoint sum) and $\rightarrow$ (function type), and the unary postfixed operator list. Polymorphic types (polytypes) are obtained by admitting type variables, which here are represented by $\alpha, \beta, \gamma \cdots$. We represent arbitrary types by $\rho, \sigma, \tau$. For this section we leave the meaning of types to the reader's intuition; it is made precise in the next section.

Example 1. Mapping a function over a list.

Intuitively, the function map so declared takes a function from things of one sort to things of another sort, and a list of things of the first sort, and produces a list of things of the second sort. So we say that map has type

where $\alpha, \beta$ are type variables.

How is this type determined from the bare declaration of map? First, the generic types (we discuss "generic" later) of the identifiers occurring free in the declaration are given by null: $\alpha\ list \rightarrow bool$, nil: $\alpha\ list$, hd: $\alpha\ list \rightarrow \alpha$, tl: $\alpha\ list \rightarrow \alpha\ list$, cons: $(\alpha \times \alpha\ list) \rightarrow \alpha\ list$, that is, they are polymorphic, because their types contain one or more type variables, and our rule is: To every occurrence of such an identifier is assigned a type which is a substitution instance (substituting types for type variables) of its generic type.

Now each of these identifiers occurs just once in the declaration, so if we denote by $\sigma_{id}$ the type assigned to an identifier id we must have for some types $\tau_1, ..., \tau_5$,

The other identifiers (map, f, m) each occur more than once, and our rules demand that each occurrence is assigned the same type. The rules also demand that the following equations are satisfied for some types $\rho_1, \rho_2, ...$,

The first of these conditions relates the type of a function to those of its formal parameters; each of the other conditions arises from some subterm which is a function application, except the last, which is because a conditional expression has the same type as its two arms, and because the definiens and definiendum of a declaration have the same type.

Now these equations may be solved for the variables $\rho_i, \tau_i$, and $\sigma_{id}$; Morris [10] discusses the solution of such equations. Indeed, the situation is entirely appropriate for the use of the Unification Algorithm of Robinson [14]; our well-typing algorithm is based upon this algorithm, and (since in this case nothing more than unification is needed) we may conclude from Robinson's work that the most general type of map is obtained, i.e., any other type $\sigma_{map}$ which satisfies the equations must be a substitution instance of the type obtained. In fact, the solution of the above equations is

where $\gamma, \delta$ are any distinct type variables. So this is the generic type of map, that is, to any occurrence of map within the scope of this declaration must be assigned some substitution instance of this type.

These instances need not be the same. Suppose that tok is a basic type (a token being a sequence of characters) and that we have available the identifiers (with their types) and tokl: tok list (a variable), length: tok \rightarrow int, sqroot: int \rightarrow real, two obvious functions.

Then in the expression map(sqroot, map(length, tokl)) the two occurrence of map will have types

Similarly, if null, for example, had occurred twice in the definition of map, its types could have been different instances of

but our rules demand that different occurrences of a formal parameter ($f$, for example), or of an identifier (map) being recursively defined, shall have the same type.

In passing, note that the occurrences of map mentioned above can be regarded as uses of two separately declared (and monomorphic!) map functions, which differ only in that different types are explicitly provided for their arguments and results. As Gries and Gehani remark, the compiler could be given the task of generating these distinct declarations—or more accurately (since the programmer need not see the replication or even be aware of it), the task of generating different code for the body of the map function for use at distinct types. This would indeed be necessary in the above example if, for efficiency, token lists were implemented differently from integer lists (and the primitive polymorphic functions hd, tl etc., were correspondingly different). We are concerned with a conceptual framework in which these map functions may all be regarded semantically as the same object; then the implementor is left with the freedom to implement as few or many variants as he wishes.

It is clear from our example that the rules of typing need to be carefully framed. We leave this task until the next section, but here we look at one more example to illustrate what happens when let or letrec is used locally.

Example 2. Tagging. Suppose we want a function tagpair, such that tagpair ($a$) is a function under which

Of course, we can easily write

Now we can explain, without setting up equations, how our well-typing algorithm tackles this declaration. It first assigns "unknown" types (i.e., type variables) $\alpha, \beta,$ and $\gamma$ to $a, b,$ and $c$. Then $((a, b), (a, c))$ acquires type $(\alpha \times \beta) \times (\alpha \times \gamma)$, and the $\lambda$-expression acquires $\beta \times \gamma \rightarrow (\alpha \times \beta) \times (\alpha \times \gamma)$; finally tagpair acquires

$(*)$

(no type equations have placed any constraint upon the types of $a, b,$ and $c$).

But consider another way of defining tagpair, using the (infixed) function

such that $(f \# g)(a, c) = (f(a), g(c))$, and the pairing function

such that pair(a)(b) = (a, b). We could write

We might then expect the well-typing algorithm to proceed as follows. First, $\alpha$ is assigned to $a$. Then, using the generic type of pair, pair(a) acquires $\delta \to \alpha \times \delta$. This is then used as the local generic type of tag, and the two occurrences of tag in tag $\#$ tag are assigned $\beta \to \alpha_1 \times \beta, \gamma \to \alpha_2 \times \gamma$, respectively. The occurrence of $\#$ is assigned an instance of its generic type (again using new type variables) and the type equation for function application will cause the type

to be assigned to tag $\#$ tag, and to the body of the $\lambda$-expression, so that tagpair acquires the type

Now comparing () with (*), something has gone wrong; the second type is too general. The problem is that tag and its generic type depend upon the $\lambda$-bound variable $a$ and its type $\alpha$, and we do not allow different bound occurrences of a $\lambda$-bound variable to have different type. Indeed, as far as type is concerned, we should get the same as if tagpair were defined in yet a third way, by

and the reader may be able to obtain (by setting up some equations as in Example 1) the expected type (*) in this case.

The solution is fortunately straightforward. We decree that in instantiating the type of a variable bound by let or by letrec. only those type variables which do not occur in the types of enclosing $\lambda$-bindings (or formal parameter bindings) may be instantiated. We call such instantiable variables (in a generic type) generic type variables.

Now in the second definition of tagpair, the locally defined tag acquired a generic type $\delta \to \alpha \times \delta$, in which $\delta$ is generic but $\alpha$ is not. Thus $\alpha$ should not have been instantiated in assigning types to the occurrences of tag, and then (**) would have been identical with (*). This example may appear a little contrived; indeed, our experience has been that almost always either all or none of the type variables of a generic type are generic. But there seem to be no simple syntactic constraints which would eliminate the exceptions, nor does it seem desirable to do so.

From the examples it becomes clear that the rules for typing variables bound, respectively, by let (or letrec) and by $\lambda$ are going to be different. Thus, although our semantics for the two expressions

may be (and are) equivalent, it may be possible to assign types correctly to the former but not to the latter. An example is the pair

A (partial) intuition for this is that a $\lambda$-abstraction may often occur without an argument; the second expression above contains a special (and rather unnecessary) use of abstraction, in that an explicit argument—$(\lambda x \cdot x)$—is present. Since the let construct (when translated) involves this restricted use of an abstraction, it is not unnatural that its rule for type assignment is less constrained. A compiler could, of course, treat all explicit occurrences of $(\lambda x \cdot e')e$ in the less constrained manner.

The treatment of types in the interaction between $\lambda$-bindings (i.e., formal parameter bindings) and let bindings is really the core of our approach. It gives a consistent treatment of the nonglobal declaration of a procedure which may contain, as a free variable, a formal parameter of an enclosing procedure. This appears to be one of the more crucial difficulties with polymorphism, and therefore we feel justified in presenting our analysis in terms of a simple language (Exp) which excludes as much as possible that is irrelevant to the difficulty.

The reader may still feel that our rules are arbitrarily chosen and only partly supported by intuition. We certainly do not claim that the rules are the only possible ones, but the results given later demonstrate that they are semantically justified. In fact, we show that a program which admits a correct type assignment cannot fail at run-time due to a type error—or more precisely, that type constraints encoded in its semantics are always satisfied. It follows from this that compile-time type checking (i.e., the attempt to discover a correct type assignment) obviates the need to carry types at run-time, with an obvious gain in the efficiency of implementation.

This is of course a principal aim in compile-time type checking; another is the early detection of programming errors (many of which result in ill-typed programs). Our achievement is to extend type checking to embrace polymorphism. Moreover the type-checking algorithm in its final form (Algorithm $J$ in Section 3) is remarkably simple, even though the proof of the Syntactic Soundness Theorem, which states that—if it succeeds—it produces a correct type assignment, is rather tedious.

We would like to give an independent characterization of the class of programs which can be well typed in our system, but we have no idea how to do this. However, we can give some pointers. At the suggestion of a referee we looked at Burge [1, Chapt. 3] concerning general functions for processing data structures. All of the functions there (with the exception of Section 3.11 which we did not examine) acquired the expected types from the ML type checker after they had been modified in two respects. First, Burge leaves implicit the coercion functions between a disjoint sum type and its summand types; we needed to make these explicit (this point was mentioned in our Introduction). Second, we used the ML abstract type construct (see Section 5 for an example) to formulate the recursive type definitions used by Burge. In this construct, the isomorphism between a defined abstract type and its representation is made explicit and must be used explicitly. To see the need for this requirement consider the case of an $\alpha$-stream, which is defined to be a function which yields a pair consisting of an $\alpha$ and an $\alpha$-stream. The type equation

cannot be solved by unification (unless we allow infinite type expressions). But by treating the equation as an isomorphism, and using two functions to convert back and forth between an abstract type and its representation, this difficulty is removed. We claim that this solution is in keeping with the notion of abstract type (see [8], for example).

On the negative side, there are certainly useful expressions which we cannot well type, though we are not clear how burdensome it is to do without them. An obvious example is Curry's $Y$ combinator.

since self-application is ill typed for us. But letrec avoids the need for $Y$. More practically, consider

which—it may be argued—should accept as argument a function which is polymorphic enough to operate upon $a$ and $b$ of different type. For example,

produces a pair of reversed lists of different type if $x$ and $y$ are lists of different type. Our system rejects such a use of $F$ (since it requires $a$ and $b$ to have the same type), but admits

or any other specialization of the function argument of $F$.

We feel that this example illustrates the main limitation of our system, but that we may have kept as much flexibility as is possible without the use of explicit type parameters. When these are introduced, the problem arises of the type of types; Reynolds [12] has made some progress in solving this problem, but we were anxious to see how much could be done while avoiding it.

3 A Simple Applicative Language and Its Types

3.1. The Language Exp

Let $x$ range over identifiers, that is

Then the expression language Exp is generated by the following grammar:

Here $(ee')$ means application, fix $x \cdot e$ stands for the least fixed point of $\lambda x \cdot e$, and the last clause binds $x$ to the value of $e$ throughout $e'$. We often use $d, e, f$—with primes and suffixes—to range over Exp. Constants are omitted; we can imagine instead some standard bindings for certain identifiers in an initial environment.

We give an ordinary denotational semantics for Exp, in which we include a value "wrong," which corresponds to the detection of a failure at run-time. In this small language, the only failures are the occurrence of a non-Boolean value as the condition of a conditional, and the occurrence of a nonfunctional value as the operator of an application.

Our semantic domains may be taken to be complete partial orders (cpos); a cpo $D$ (see [9]) is a partially ordered set such that (a) there exist a minimum element, $\bot_D$, (b) every directed subset of $D$ has a least upper bound in $D$. Take as given a set $\{ B_i \}$ of basic domains, with $B_0 = T$, the three element truth value domain

Figure.

and we define recursively

The solution (up to isomorphism) of such a set of domain equations is assured by Scott [15]. Although he worked with complete lattices, the solution also exists in cpos (see Plotkin [11]).

The semantic function is $\mathcal{E} \in \text{Exp} \rightarrow \text{Env} \rightarrow V$, where $\text{Env} = \text{Id} \rightarrow V$, the domain of environments. We use $\eta$ to range over Env. In defining $\mathcal{E}$, and later, we use some familiar notation of Scott and Strachey [16], illustrated by these examples (where $D$ is some summand of $V$):

(i) If $d \in D$, then $d$ in $V$ is the image of $d$ under the injection of $D$ into $V$.

(ii) If $v \in V$, then

(iii) If $v \in V$, then

The environment $\eta' = \eta\{v/x\}$ is identical with $\eta$ except that $\eta'(x) = v$. The value $\cdot$ in $V$ ($\cdot \in W$) is written "wrong." We require the conditional function $\mathrm{COND} \in T \to V \to V \to V$, where $\mathrm{COND}\ tvv'$ is written $t \to v, v'$ and takes the value

3.2. Semantic Equations for Exp

In these equations, the open brackets [ ] indicate syntactic arguments.

Notes. (i) $Y$ is the least fixed-point operation. In many languages the $e$ in $\text{fix } f \cdot e$ would be restricted to be an abstraction $\lambda y \cdot e'$, and then

might receive the syntax

(ii) It is easy to see that "let $x = e_1$ in $e_2$" has the same meaning under $\mathcal{E}$ as "$(\lambda x \cdot e_2)e_1$". But part of our aim is a type discipline which admits certain expressions in the first form and yet rejects their translations into the second form; this is because $\lambda$-abstractions may in general occur without an explicit operand, and need more careful treatment.

(iii) The semantics for $(e_1e_2)$ corresponds to call-by-value, since the test "$v_2 \mathbf{E} W$" ensures that the meaning of $(e_1e_2)$ is $\bot_v$ if the meaning of $e_2$ is $\bot_v$. The omission of this test gives a call-by-name semantics (a similar test may be omitted in the semantics of the let construct), and the Semantic Soundness Theorem goes through equally in this case.

3.3. Discussion of Types

We now proceed, in outline, as follows. We define a new class of expressions which we shall call types; then we say what is meant by a value possessing a type. Some values have many types, and some have no type at all. In fact "wrong" has no type. But if a functional value has a type, then as long as it is applied to the right kind (type) of argument it will produce the right kind (type) of result—which cannot be "wrong"!

Now we wish to be able to show that—roughly speaking—an Exp expression evaluates (in an appropriate environment) to a value which has a type, and so cannot be wrong. In fact, we can give a sufficient syntactic condition that an expression has this robust quality; the condition is just that the expression has a "well-typing" with respect to the environment, which means that we can assign types to it and all its subexpressions in a way which satisfies certain laws.

So there are two main tasks, once the laws of type assignment are given. The first—to show that an expression (or program) with a legal type assignment cannot "go wrong"—is tackled in this section; surprisingly enough, it is the easier task (at least for an applicative language). The second task is to discover a legal type assignment, given a program with incomplete type information. This task is often called type checking. Of course, this term can also mean just verifying that a given type assignment is legal; in a practical situation we probably require something between the two, since one cannot expect a programmer to attach a type to every subexpression. In Section 4 we look at the class of legal type assignments for a given program (the class is infinite in general, since we admit polymorphism), and we give an algorithm which, if it succeeds, produces a legal type assignment. We conjecture that if the latter exists then the algorithm finds one which is most general, in the sense that any other legal type assignment is a substitution instance of it (substituting types for type variables).

3.4. Types and their Semantics

The syntax of types is as follows.

(1) $\iota_0, \iota_1, ...$ are (basic) types; one for each $B_i$. (2) There is a denumerable set of type variables, which are types. We use $\alpha, \beta, \gamma, ...$ to range over type variables. (3) If $\rho$ and $\sigma$ are types, so is $\rho \rightarrow \sigma$.

A monotype is a type containing no type variables. We use $\mu, \nu, \pi, ...$ to range over monotypes. We use the word polytype when we wish to imply that a type may, or does, contain a variable.

We first give the semantics of monotypes; that is, we give the conditions under which a value $v \in V$ possesses a monotype $\mu$, which we write $v : \mu$.

(i) $v : \iota_i$ iff $v = \bot_\nu$ or $v \mathbf{E} B_i$ (ii) $v : \mu \rightarrow \nu$ iff either $v = \bot_\nu$, or $v \mathbf{E} F$ and $(v | F)u : \nu$ whenever $u : \mu$.

It is clear then that many values have no type. Examples are wrong, $(\lambda v \in V \cdot \text{wrong})$ in $V$, $(\lambda v \in V \cdot v \mathbf{E} B_0 \rightarrow (v | B_0 \rightarrow x \text{ in } V, y \text{ in } V), \text{wrong})$ in $V$ (where $x \in B_1, y \in B_2$ for example).

But in the last example if $y \in B_1$ instead, then the function has type $\iota_0 \rightarrow \iota_1$ (and no other).

Some values have many types; the identity function

$(\lambda v \in V \cdot v)$ in $V$ for example has type $\mu \rightarrow \mu$ for every $\mu$. And of course $\bot_v$ has every type (it is the only value which has every type).

This notion of type is derived from Scott [17]. In fact, it is what Scott calls functionality (after Curry), and is distinct from the notion of a retract. If we temporarily identify a type with the set of values which possess it, then it is easy to show that types are downward closed and directed complete, that is

(i) $\forall v, v' \in V \cdot (v : \mu \text{ and } v' \sqsubseteq v) \Rightarrow v' : \mu,$ (ii) For each directed subset $X$ of $V$, $(\forall v \in X \cdot v : \mu) \Rightarrow \sqcup X : \mu.$

Retracts share the second property, but not the first. Recently Shamir and Wadge [18] have defined a type to be any set with these two properties, and they investigate the consequences of identifying a value $v$ with the type $\{v' | v' \sqsubseteq v\}$.

The semantics of polytypes is as follows. First, we use $\rho \leq \sigma$ to mean that $\rho$ may be obtained from $\sigma$ by substituting types for type variables ($\leq$ is clearly reflexive and transitive). For example,

but

Then we define

For example,

$(\lambda v \cdot v)$ in $V : \alpha \rightarrow \alpha.$

Polytypes thereby also stand for subsets of $V$, and these are also directed complete. The reader may like to think of each type variable in a polytype as universally quantified at the outermost; for example,

where the bound $\alpha$ ranges over monotypes. In fact, it is because $\alpha$ here ranges over monotypes (not all types) and because we do not admit expressions like

as types—though we can see they “mean” if the bound variables are taken to range over monotypes—that we avoid the difficulties (and also some of the interest) of Reynolds [12] in his richer notion of type.

We need the following simple properties, which are immediate from our definitions.

PROPOSITION 1. If v : σ and τ ≤ σ then v : τ.

PROPOSITION 2. If v : σ → τ and v' : σ, then (v | F)v' : τ.

In each case, a property of monotypes is lifted to polytypes.

3.5. Type Assignments

To prepare the ground for the theorem that well-typed expressions cannot “go wrong,” we need to define what is meant by typing an expression. We need first some notion of a type environment to give types to the free variables in an expression.

A prefix p is a finite sequence whose members have the form let x, fix x, or λx, where x is a variable. A prefixed expression (pe) has the form p | e, where every variable free in e occurs in a member of p. We separate the members of a prefix by a period (·).

Every pe has sub-pe’s given by the following, together with transitive reflexive closure:

(i) p | x has no sub-pe’s except itself, (ii) p | (ee') has sub-pe’s p | e and p | e', (iii) p | (if e then e' else e") has sub-pe’s p | e, p | e' and p | e", (iv) p | (λx · e) has sub-pe p · λx | e, (v) p | (fix x · e) has sub-pe p · fix x | e, (vi) p | (let x = e in e') has sub-pe’s p | e and p · let x | e'.

For example, λy | (let f = λx · (xy) in (fy)) has sub-pe’s (besides itself)

so a sub-pe is just a subexpression prefixed with all the variable bindings which enclose it. Note that λx · (xy) in the above is not enclosed by let f—it is not in the scope of this binding.

We say that a member let x or fix x or λx of p is active in p just if no x occurs to the right of it in p.

Now a typing of a pe p | e is an assignment of a type to each element of p, and to each subexpression and each λx, fix x, or let x in e, with the constraint that in a subexpression (let x = e' in e") the same type is assigned to let x and e'. Thus one typing of the illustrated pe (it is nearly, but not quite, a well typing in the sense later defined) is as follows:

We denote a typing of p | e by p̄ | ē, or by p̄ | ē_σ when we want to indicate the type σ assigned to e itself.

In any $\bar{p} \mid \bar{e}$, and any binding let $x_{\sigma}$ in either $\bar{p}$ or $\bar{e}$, a type variable in $\sigma$ which does not occur in (the type of) any enclosing $\lambda y_{\tau}$ or fix $y_{\tau}$ binding is called a generic type variable for the binding let $x_{\sigma}$. In the example above, $\beta$ is generic, but $\alpha$ is not, for the binding let $f_{(\alpha \rightarrow \beta) \rightarrow \beta}$. Intuitively, the generic type variables in a binding let $x_{\sigma}$ represent degrees of freedom for the types at which $x$ may be used; they represent the local polymorphism of $x$. Notice that if no $\lambda$ or fix bindings enclose let $x_{\sigma}$, then all the type variables in $\sigma$ are generic. A generic instance of $\sigma$ is an instance of $\sigma$ in which only generic type variables are instantiated.

For technical reasons we require that generic type variables occur in a controlled manner. We say that $\bar{p} \mid \bar{d}$ is standard if for every typed sub-pe $\bar{p}' \mid \bar{d}'$ (with induced typing) the generic type variables of each member let $x_{\sigma}$ of $\bar{p}'$ occur nowhere else in $\bar{p}' \mid \bar{d}'$. Thus in particular, if let $x_{\rho} = \bar{e}_{\rho}$ in $\bar{e}'_{\sigma}$ is a subexpression of $\bar{d}$, with induced typing, then the generic type variables in $\rho$ may not occur in $\bar{e}'_{\sigma}$ (though they must of course occur in $\bar{e}_{\rho}$).

We now define the notion of a well-typed (wt) pe as follows:

(i) $\bar{p} \mid x_{\tau}$ is wt iff it is standard, and either

(a) $\lambda x_{\tau}$ or fix $x_{\tau}$ is active in $\bar{p}$, or

(b) let $x_{\sigma}$ is active in $\bar{p}$, and $\tau$ is a generic instance of $\sigma$.

(ii) $\bar{p} \mid (\bar{e}_{\rho}\bar{e}'_{\sigma})_{\tau}$ is wt iff $\bar{p} \mid \bar{e}$ and $\bar{p} \mid \bar{e}'$ are both wt, and $\rho = \sigma \rightarrow \tau$.

(iii) $\bar{p} \mid (if \bar{e}_{\rho} \text{ then } \bar{e}'_{\sigma} \text{ else } \bar{e}''_{\sigma})_{\tau'}$ is wt iff $\bar{p} \mid \bar{e}$, $\bar{p} \mid \bar{e}'$ and $\bar{p} \mid \bar{e}''$ are all wt, $\rho = \iota_{0}$, and $\sigma = \tau = \tau'$.

(iv) $\bar{p} \mid (\lambda x_{\rho} \cdot \bar{e}_{\sigma})_{\tau}$ is wt iff $\bar{p} \cdot \lambda x_{\rho} \mid \bar{e}$ is wt and $\tau = \rho \rightarrow \sigma$.

(v) $\bar{p} \mid (fix x_{\rho} \cdot \bar{e}_{\sigma})_{\tau}$ is wt iff $\bar{p} \cdot fix x_{\rho} \mid \bar{e}$ is wt and $\rho = \sigma = \tau$.

(vi) $\bar{p} \mid (let x_{\rho} = \bar{e}_{\rho} \text{ in } \bar{e}'_{\sigma})_{\tau}$ is wt iff $\bar{p} \mid \bar{e}$ and $\bar{p} \cdot let x_{\rho} \mid \bar{e}'$ are both wt, and $\sigma = \tau$.

Although this recursive definition is useful for some proofs, an alternative characterization of wt is sometimes useful. The proof of the next proposition is fairly straightforward, and we omit it. Note that a wt $\bar{p} \mid \bar{d}$ is necessarily standard, by an easy structural induction.

Proposition 3. $\bar{p} \mid \bar{d}$ is wt iff the following conditions hold:

(A) It is standard.

(B) For every (bound) occurrence $x_{\sigma}$, the corresponding binding occurrence is either $\lambda x_{\sigma}$, or fix $x_{\sigma}$, or let $x_{\tau}$, where $\sigma$ is a generic instance of $\tau$.

(C) The following conditions hold for all subexpressions (with induced typing) of $\bar{d}$

The typing which we illustrated above therefore fails to be wt for only one reason: The subexpression $(f_{(\alpha \to \gamma) \to \gamma} y_\alpha)_\gamma$ violates the first of conditions (C) in Proposition 3.

Consider another example. The following (with $\bar{p}$ empty) is a well typing:

Note that $\alpha$ is generic in the type $\alpha \to \alpha$ of the declaration of $I$, so may be instantiated (possibly differently) in the types of bound occurrences of $I$.

To illustrate the need to instantiate only generic type variables, for variables declared by let, notice first that in $\lambda x_\alpha \cdot x_\beta$ we must have $\alpha = \beta$, by condition (B) of Proposition 3. Indeed, we can argue intuitively for this as follows: if we declare

then we wish to have that any expression (Ie) in the scope of this declaration receives the same type as the subexpression e. But now suppose we write (with assigned types)

then—since this is semantically equivalent to the simpler declaration—we should again demand that $\alpha = \beta$. But this is imposed in our definition of well typing, just because $\alpha$ is not generic for the binding let $y_\alpha$, so may not be instantiated in a bound occurrence of $y$.

3.6. Substitutions

A substitution $S$ is a map from type variables to types. $S$ may be extended in a natural way to yield a map from types to types, from typed pe’s to typed pe’s, etc.

We say that $S$ involves a type variable $\alpha$ if either $S\alpha \neq \alpha$, or for some $\beta \neq \alpha$, $\alpha \in S\beta$. ($\alpha \in \tau$ means $\alpha$ occurs in $\tau$.)

We need substitutions extensively in the second part of this paper, but for the present we need only one property relating substitutions and wt.

Proposition 4. If S involves no generic variables of a wt $\bar{p} \mid \bar{d}$, then $S(\bar{p} \mid \bar{d})$ is also a wt.

Proof. We use Proposition 3. First, observe that the assumption on $S$ yields that the generic variables for each binding in $S(\bar{p} \mid \bar{d})$ are exactly those for the corresponding binding in $\bar{p} \mid \bar{d}$. Since $S\beta$ contains no generic variable when $\beta$ is not generic, $S(\bar{p} \mid \bar{d})$ is standard.

Second, if $x_\sigma$ is bound by $\lambda x_\sigma$ or fix $x_\sigma$ in $\bar{p} \mid \bar{d}$, then $x_{S\sigma}$ is bound by $\lambda x_{S\sigma}$ or fix $x_{S\sigma}$ in $S(\bar{p} \mid \bar{d})$. If $x_\sigma$ is bound by let $x_\tau$, and $\sigma = [\rho_1/\alpha_1, ..., \rho_n/\alpha_n]_\tau$, where $\alpha_i$ are the generic variables of $\tau$, then in $S(\bar{p} \mid \bar{d})$ $x_{S\sigma}$ is bound by let $x_{S\tau}$, and $S\sigma = S\rho_1/\alpha_1, ..., S\rho_n/\alpha_n$ is a generic instance of $S\tau$.

Third, conditions (C) of Proposition 3 are easily verified for $S(\bar{p} \mid \bar{d})$, using identities like $S(\sigma \to \tau) = S\sigma \to S\tau$.

3.7. Well-Typed Expressions Do Not Go Wrong

First we need a simple relation between semantic environments $\eta$ and our type environments—which are typed prefixed $\bar{p}$. We say

Theorem 1 (Semantic Soundness). If $\eta$ respects $\bar{p}$ and $\bar{p} | d_\tau$ is well typed then $\mathcal{E}[d]\eta : \tau$.

Proof. A fairly simple structural induction. Take the six cases for $d_\tau$.

(i) $x_\tau$. Then either $\lambda x_\tau$ or fix $x_\tau$ is active in $\bar{p}$, and $\eta[x] : \tau$, so $\mathcal{E}[x]\eta : \tau$, or let $x_\sigma$ is active in $\bar{p}$, and $\eta[x] : \sigma$; but then $\tau \leq \sigma$, so $\mathcal{E}[x]\eta = \eta[x] : \tau$, by Proposition 1.

(ii) $(\bar{e}_{\sigma \to \tau} \bar{e}_\sigma)_\tau$. Then $\bar{p} | \bar{e}_{\sigma \to \tau}$ is wt, so $\mathcal{E}[e]\eta : \sigma \to \tau$, and similarly $\mathcal{E}[e']\eta : \sigma$. Then from the semantic equation (remembering that wrong has no type) and by Proposition 2 we get $\mathcal{E}[d]\eta : \tau$.

(iii) (if $\bar{e}_{t_0}$ then $\bar{e}'_{\sigma}$ else $\bar{e}''_{\sigma}$). Straightforward; the only extra detail needed here is that $\bot_\nu$ has every type.

(iv) $(\lambda x_\rho \cdot \bar{e}_\sigma)_{\rho \to \sigma}$. Then $\bar{p} \cdot \lambda x_\rho | \bar{e}_\sigma$ is wt. Now we require $(\lambda v \cdot \mathcal{E}[e] \eta\{v/x\})$ in $V : \rho \to \sigma$. Denote this function by $f$ in $V$. The inverse of Proposition 2 does not hold, that is, to show $f$ in $V : \rho \to \sigma$ it is not sufficient (though it is necessary) that whenever $v : \rho, fv : \sigma$. What is required is that for every $\eta \to \nu \leq \rho \to \sigma, f$ in $V : \mu \to \nu$.

Suppose then that $\mu \to \nu \leq \rho \to \sigma$. Then there is a substitution $S$, involving only the type variables in $\rho$ and $\sigma$, such that $\mu \to \nu = S(\rho \to \sigma)$. Then, since none of these type variables is generic in $\bar{p} \cdot \lambda x_\rho | \bar{e}_\sigma$, it follows that $S(\bar{p}) \cdot \lambda x_\mu | S(\bar{e})_\nu$ is wt by Proposition 4. Moreover $\eta$ respects $S(\bar{p})$ (since by Proposition 1 whenever $\eta[x] : \sigma'$ and $\tau' \leq \sigma', \eta[x] : \tau'$) so for any $v : \mu$ we also have $\eta\{v/x\}$ respects $S(\bar{p}) \cdot \lambda x_\mu$.

It then follows by induction that $\mathcal{E}[e] \eta\{v/x\} : \nu$, so we have shown that $v : \mu$ implies $fv : \nu$, and this yields $f$ in $V : \mu \to \nu$ as required.

(v) $(fix x_\rho \cdot \bar{e}_\rho)_\rho$. Then $\bar{p} \cdot fix x_\rho | \bar{e}_\rho$ is wt. Now we require that $v : \rho$, where

Now $v = \bigcup_i v_i$, where $v_0 = \bot_\nu, v_{i+1} = \mathcal{E}[e] \eta\{v_i/x\}$, and by the directed completeness of types we only have to show $v_i : \rho$ for each $i$.

Clearly $v_0 : \rho$. Assume $v_i : \rho$. Since $\eta$ respect $\bar{p}$, we have that $\eta\{v_i/x\}$ respects $\bar{p} \cdot fix x_\rho$, so by the main induction hypothesis $v_{i+1} : \rho$ also, and we are done.

(vi) (let $x = \bar{e}_\rho$ in $\bar{e}'_\sigma$)_\sigma . Then $\bar{p} | \bar{e}_\rho$ is wt, so we immediately have $v : \rho$, where $v = \mathcal{E}[e]\eta$. We require $\mathcal{E}[e'] \eta\{v/x\} : \sigma$.

Now $\bar{p} \cdot let x_\rho | \bar{e}'_\sigma$ is also wt, and because $v : \rho$ we have that $\eta\{\sigma/x\}$ respects $\bar{p} \cdot let x_\rho$; the rest follows by the induction hypothesis.

As a corollary, under the conditions of the theorem we have

since wrong has no type.

4 A Well-Typing Algorithm and Its Correctness

4.1. The Algorithm $\mathcal{W}$

In this section we tackle the question of finding a well typing for a prefixed expression. We present an algorithm $\mathcal{W}$ for this. We would like to prove that $\mathcal{W}$ is both syntactically sound and (in some sense) complete. By syntactic soundness, we mean that whenever $\mathcal{W}$ succeeds it produces a wt; by completeness, we mean that whenever a wt exists, $\mathcal{W}$ succeeds in finding one which is (in some sense) at least as general.

Although $\mathcal{W}$ is probably complete, it is difficult to find a simple proof. So we concentrate on soundness, and then comment on implementation of $\mathcal{W}$ and on extending it to deal with richer languages. Since a type-checking algorithm which simulates $\mathcal{W}$ has been working successfully for nearly 2 years in the context of the LCF metalanguage ML [2], we have evidence for its usefulness and even—to some extent—for its completeness.

$\mathcal{W}$ is based on the unification algorithm of Robinson [14]. Indeed, the only feature of well typing which does not fall directly within the framework of unification is the condition that $\tau$ should be a generic instance of $\sigma$ whenever $x_{\tau}$ is bound by let $x_{\sigma}$. The completeness (in some sense) of $\mathcal{W}$ should follow from the second part of the following proposition concerning unification, but we need only the first half for our proof that $\mathcal{W}$ is sound.

Proposition 5 (Robinson). There is an algorithm $\mathcal{U}$, taking a pair of expressions (over some alphabet of variables) and yielding a substitution, such that for any pair of expressions $\sigma$ and $\tau$

(A) If $\mathcal{U}(\sigma, \tau)$ succeeds, yielding $U$, then $U$ unifies $\sigma$ and $\tau$ (i.e., $U\sigma = U\tau$).

(B) If $R$ unifies $\sigma$ and $\tau$, then $\mathcal{U}(\sigma, \tau)$ succeeds yielding a $U$ such that for some substitution $S$, $R = SU$.

Moreover, $U$ involves only variables in $\sigma$ and $\tau$.

To find a well typing of a complete program $f$, we would expect to supply also a typed prefix $\bar{p}$, containing only let bindings, giving the types of values bound to predefined identifiers. We would then expect $\mathcal{W}$ to yield $\vec{f}$ such that $\bar{p} \mid \vec{f}$ is a wt.

To state (and prove) $\mathcal{W}$ recursively however, prefixes containing all types of binding occur, and $\mathcal{W}$ in general needs to modify the nongeneric type variables in the prefix to meet constraints imposed on the program. We therefore make $\mathcal{W}$ return also a substitution $T$, indicating the necessary transformation.

To be precise, we show that if $\mathcal{W}(\bar{p}, f)$ succeeds and returns $(T, \vec{f})$, then $(T\bar{p})|\vec{f}$ is a wt.

We first state $\mathcal{W}$. At certain points $\mathcal{W}$ requires type variables which have not previously occurred; such new type variables are denoted by $\beta$ or $\beta_i$. $\mathcal{W}(\bar{p}, f)$ is defined by induction on the structure of $f$; the algorithm is expressed in a purely applicative programming style, in contrast with the more efficient algorithm $\mathcal{J}$ presented later, which is expressed more in the style of imperative programming.

Algorithm $\mathcal{W}$

(i) If $f$ is $x$, then: if $\lambda x_\sigma$ or $fix\ x_\sigma$ is active in $\bar{p}$ then $T = I, \vec{f} = x_\sigma$; if let $x_\sigma$ is active in $\bar{p}$ then $T = I, \vec{f} = x_\tau$ where $\tau = [\beta_i/\alpha_i]\sigma$, $\alpha_i$ are the generic variables of $\sigma$, and $\beta_i$ are new variables.

(ii) If $f$ is $(de)$, then: let $(R, \vec{d}_\rho) = \mathcal{W}(\bar{p}, d)$, and $(S, \vec{e}_\sigma) = \mathcal{W}(R\bar{p}, e)$; let $U = \mathcal{U}(S\rho, \sigma \to \beta)$, $\beta$ new; then $T = USR$, and $\vec{f} = U(((S\vec{d})\vec{e})_\beta)$.

(iii) If $f$ is $(if\ d\ then\ e\ else\ e')$, then: let $(R, \vec{d}_\rho) = \mathcal{W}(\bar{p}, d)$ and $U_0 = \mathcal{U}(\rho, i_0)$; let $(S, \vec{e}_\sigma) = \mathcal{W}(U_0R\bar{p}, e)$, and $(S', \vec{e}'_\sigma) = \mathcal{W}(SU_0R\bar{p}, e')$; let $U = \mathcal{U}(S'\sigma, \sigma')$; then $T = US'SU_0R$, and $\vec{f} = U((if\ S'SU_0\vec{d}\ then\ S'\vec{e}\ else\ \vec{e}')_\sigma)$.