Information and Computation 155, 13400169 (1999) Article ID inco.1999.2830, available online at http://www.idealibrary.com

Semi-Explicit First-Class Polymorphism for ML^{†}

Jacques Garrigue

Kyoto University Research Institute for Mathematical Sciences, Kitashirakawa-Oiwakecho, Sakyo-ku, Kyoto 606-01, Japan

and

Didier Rémy

INRIA-Rocquencourt, BP 105, 78153 Le Chesnay Cedex, France

We propose a modest conservative extension to ML that allows semiexplicit first-class polymorphism while preserving the essential properties of type inference. In our proposal, the introduction of polymorphic types is fully explicit, that is, both introduction points and exact polymorphic types are to be specified. However, the elimination of polymorphic types is semiimplicit: only elimination points are to be specified as polymorphic types themselves are inferred. This extension is particularly useful in Objective ML where polymorphism replaces subtyping. \begin{matrix}c \\ ◯ \end{matrix}1999 Academic Press

INTRODUCTION

The success of the ML language is due to its combination of several attractive features. Undoubtedly, the polymorphism of ML [Damas and Milner, 1982] —or polymorphism à la ML— with the type inference it allows, is a major advantage. The ML type system stays in close correspondence with the rules of logic, following the Curry-Howard isomorphism between types and formulas, which provides a simple intuition, and a strong type discipline. Simultaneously, type inference relieves the user from the burden of writing types: an algorithm automatically checks whether the program is well-typed and, if true, returns a principal type. Based on this simple system, many extensions have been proposed: polymorphic records, first-class continuations, first-class abstract datatypes, type-classes, overloading, objects, etc. In all these extensions, type inference remains straightforward first-order unification with toplevel polymorphism. This shows the robustness of ML-style type inference.

134 There are of course cases where one would like to have first-class polymorphism, as in system F. ML allows for polymorphic definitions, but abstractions can only be monomorphic. Traditionally, ML polymorphism is used for definitions of firstclass functions such as folding or iteration over a parameterized datatype. Some higher-order functionals require polymorphic functions as arguments. These situations mostly appear in encodings, and occurrences in real programs can usually be solved by using functors of the module language. This simple picture, which relies on a clear separation between data and functions operating on data, has recently been invalidated by several extensions. For instance, data and methods are packed together inside objects. This decreases the need for polymorphism, since methods can be specialized to the piece of data they are embedded with. However, data transformers such as folding functions remain parameterized by the type of the output. For instance, a function fold with the ML type ∀β,α. β list → (β → α → α) → α → α should become a method for container objects, of type ∀α. (τ → α → α) → α → α where τ is the type of the elements of the container. The extension of ML with first-class abstract types [Läufer and Odersky, 1994, Rémy, 1994] also requires first-class polymorphic functions: for instance, an expression such as λf.open x as y in f y can only be typed if the argument f is polymorphic in its argument, so that the abstract representation of y is not revealed outside the scope of the open construct. First-class polymorphism seems to be also useful in Haskell to enable the composition of monads. First-class polymorphic values have been proposed in [Rémy, 1994, Odersky and Läufer, 1996] based on ideas developed in [Läufer and Odersky, 1994]. After de-sugaring, all these proposals reduce to the same idea of using explicit, mutually inverse introduction and elimination functions to coerce higher-order types into basic, parameterized type symbols and back. Therefore, they all face the same problem: types must be written explicitly, at both the introduction and the elimination of polymorphism. Recent results on the undecidability of type inference for system F [Wells, 1994, Kfoury and Wells, 1994, Pfenning, 1993] do not leave many hopes for finding a good subset of system F that significantly extends ML, moreover with decidable type inference and principal types. Previous attempts to accomplish this task were unsuccessful. This is not the path we choose here. We do not infer higher-order types and thus avoid higher-order unification, undecidable in general. Furthermore, we maintain the simplicity of the ML type system, following the premise that an extension of ML should not modify the ML polymorphism in its essence, even if it is an extension that actually increases the level of polymorphism. The original insight of our work is that, although ML polymorphism allows type inference, actual ML programs do already contain a lot of type information. All constants, all constructors, and all previously defined functions already have known types. This information is only waiting to be used appropriately. In comparison to previous works, we remove the requirement for type annotations at the elimination of polymorphism by using type inference to propagate explicit type information between different points of the program. In our proposal, tagging values of polymorphic types with type symbols becomes superfluous. A type annotation at the introduction of a polymorphic value is sufficient and can be propagated to the elimination site (following the data-flow view of programs). This makes the handling of such values considerably easier, and reasonably practical for use in a programming language. In a first section, we present our solution informally and explain how it simplifies the use of higher-order types in ML. Then, we develop this approach formally, proving all fundamental properties. In a third section, encodings are provided, both for previous formulations of first-class polymorphism, and for system F itself, along with some syntactic comparisons. Section 4 shows how our system can be used to provide polymorphic methods for Objective ML, in an almost transparent way. In section 5 we discuss how the value-only restriction to polymorphism can be applied here. Lastly, we compare with related works, and conclude. Proofs of main theorems are given in appendix.

†A preliminary version of this paper has been presented at the “Third International Symposium on Theoretical Aspects of Computer Software [Garrigue and Rémy, 1997].”

Copyright \begin{matrix}c \\ ◯ \end{matrix}1999 by Academic Press All rights of reproduction in any form reserved.

1 INFORMAL APPROACH

In this section we present our solution informally. We first introduce a naive straightforward proposal. We show that this solution needs to be restricted to avoid higherorder unification. Last, we describe a simple solution that allows for complete type inference. We write x =^{△} a to introduce a meta-level name x for a formal expression a.

1.1 A naive solution

The self-application term self =^{△} λf.ff cannot be typed in ML; however, we can easily type it in system F if we add proper type annotations. While this expression is not very interesting for itself, a few variations on it are sufficient to illustrate most aspects of type inference in the presence of higher-order types. Useful examples can be found in section 4 in addition to those suggested in the introduction. The expression let f = idin f f where id =^{△} λx.x (the polymorphic identity function) is typable in ML. One can see let-definitions as a special syntax, combined with a special typing rule, for the application (λx.a_{2}) a_{1}. Let us exercise by replacing the let polymorphic binding by first-class polymorphism. The identity id has type α → α where α can be universally quantified. We shall write [id : ∀α.α → α] for the creation (or introduction) of the polymorphic value wrapping id with the polymorphic type ∀α.α → α. As usual in ML, we distinguish between first-class simple types (or types for short) and polymorphic types. Thus, we explicitly coerce the polymorphic type ∀α.α → α to a simple type [∀α.α → α] using the type constructor [ ] for that purpose. We call [∀α.α → α] a polytype, which is (a particular form of) a simple type. Let id_{1} be the expression [id : ∀α.α → α], which has type [∀α.α → α]. As any first-class value, id_{1} can be passed to other functions, stored in data-structures, etc.

For instance (id_{1},1) is a pair of type ([∀α.α → α] × int). Such a wrapped function cannot be applied directly, since it is typed with a polytype, which is incompatible with an arrow type. We must previously open (or eliminate) the polytype. We introduce a new construct ⟨ ⟩ for that purpose. Hence, ⟨id_{1}⟩ is a function of type an instance of the polymorphic type ∀α.α → α, i.e. τ → τ for some type τ. Its principal type is α → α, making its typing behavior just the same as the polymorphic identity function id. The raw expression self is not well-typed. It should be passed a polymorphic value as argument, for instance, of type [∀α.α → α]. Here, we shall introduce polymorphism by a type constraint on the argument: λf:[∀α.α → α] .⟨f⟩ f. The first occurrence of f in the body is opened to eliminate polymorphism before it is applied. The following definition expression is well-typed:

self_{1} =^{△} λf:[∀α.α → α] .⟨f⟩ f : [∀α.α → α] → [∀α.α → α]

So are the two following variants:

self_{2} =^{△} λf:[∀α.α → α] .⟨f⟩ ⟨f⟩ : [∀α.α → α] → α′→ α′

self_{3} =^{△} λf:[∀α.α → α] .[⟨f⟩ ⟨f⟩: ∀α.α → α] : [∀α.α → α] → [∀α.α → α]

In self_{2}, the occurrence of f in the argument position is also opened, so the result type is no longer a polytype. In self_{3}, polymorphism is lost as in self_{2}, then it is recovered explicitly. Finally, we can apply self_{1} to the wrapped identity function id_{1}:

(λf:[∀α.α → α] .⟨f⟩ f) [λx.x: ∀α.α → α] : [∀α.α → α]

More interestingly, the following expression is also well-typed

(λu.u id_{1}) self_{1} : [∀α.α → α]

There is no term typable in ML that has the same erasure (untyped λ-term) as this one. Note that no type annotation is needed on u; although u has a polytype as result, it is not opened locally.

1.2 An obvious problem

The examples above mixed type-inference and type-checking (using type-annotations). The obvious problem of type inference in the presence of higher-order types remains to be solved: what happens when expressions of unknown type are opened. Should the program λf.⟨f⟩ f or simpler λx.⟨x⟩ be well-typed? In order to avoid higherorder types, we accept to reject those examples. Our modest goal is to keep track of user-provided polymorphism, but never guess polymorphism from scratch. On the other hand, forbidding lambda abstraction of an unspecified type to be a polytype is too restrictive. This would violate the assumption that polytypes are regular ML types, which can be substituted for any type variable. Thus, if λx.x has type α → α, it should also have type [σ] → [σ] for any polymorphic type σ. Actually, for practical programming, it is important that λx.x possesses all these types. For instance, both (λx.x) f and λx.f x should be typable and have the same type as f. The former expression is needed as soon as we are using polymorphic values inside generic data structures, such as lists, and use polymorphic functions to extract them. The later allows η-expansion, for instance to reorder the arguments of a function, without any superfluous type annotation. When typing λf.⟨f⟩ f, variable f is first given an unknown type τ. Guessing [∀α.α → α] for τ would be correct, but not principal, since [∀α.α → α → α] would also be a possible type for τ. Conversely, the expression λf.iftruethen ⟨f⟩ f else (f : [∀α.α → α]) would have as only possible type [∀α.α → α] → [∀α.α → α], since there is an explicit annotation on f. However, we prefer to also reject this program. Informally, type inference would imply backtracking: f is first assumed of unknown type τ; we cannot type ⟨f⟩ so we backtrack; typing the annotation forces f to be of type [∀α.α → α], then ⟨f⟩ can be typed, and so on. This causes two problems. Firstly, backtracking may lead to a combinatorial explosion of the search space^{1} and we would rather fail in every case where some inference order would fail. Worse, typing constraints may disappear during reduction. Traditionally, this is not a problem since this only allows to infer better types. However, in our case, the removal of polytype constraints will leave some polytypes unspecified and lead to failure. Consequently, we would lose the subject reduction property. The expression λf.iftruethen ⟨f⟩ f else (f : [∀α.α → α]) reduces to λf.⟨f⟩ f but the latter is not typable.

1.3 A simple solution

The essence of our proposal is a simple mechanism based on unification that distinguishes polytypes that have been user-provided from those that have just been guessed. Each occurrence of a polytype [σ] is labeled with a label variable ϵ (label for short). That is, we write [σ]^{ϵ} rather than [σ]. To ensure that an expression was correctly annotated, in an elimination ⟨a⟩, the type of a must be of the form ∀ϵ.[σ]^{ϵ}. This prevents negative occurrences of the type annotation (such as in the context or on the left hand-side of an arrow), so proving that it must have been user-provided. Expressions of the form λf.⟨f⟩ f are not allowed; the type of f is a simple type, which includes [σ]^{ϵ}, but not ∀ϵ.[σ]^{ϵ}. Annotations do introduce polymorphism. We may write λx.let f = (x: [σ]^{ϵ}) in ⟨f⟩ f, where the type annotation on x is a polytype. Such an annotation allows label variables to be renamed apart in the type of f and then abstracted over in generalizing the type of the let-definition, thus allowing f to be used polymorphically in the let body. For convenience, we write λx:τ.a as an abbreviation for λx.let x = (x: τ) in a. Hence λf:[∀α.α → α]^{ϵ} .⟨f⟩ f is well-typed.

1ML typability is exponentially hard in theory, but it is almost linear in practice; here, the combinatorial explosion would likely make type inference exponential in practice.

Annotations must be correctly introduced. The expression λf.if true then ⟨f⟩ f else (f : [∀α.α → α]^{ϵ}) fails to type. The type [σ]^{ϵ} of the else-branch is transmitted to the then-branch by unification. However, it is also simultaneously transmitted to the binding occurrence; hence, the label variable ϵ also appears in the type context and cannot be generalized; therefore ⟨f⟩ is ill-typed. An explicit type annotation is required on the then-branch: ⟨f : [σ]^{ϵ′}⟩ f. This has the effect of renaming ϵ into a fresh label variable ϵ′that does not occur in the context so that it can be generalized. For convenience, we write [σ] instead of [σ]^{ϵ} when the label ϵ is anonymous, i.e. when it does not appear anywhere else in the program, such as ϵ′ in the above example. Another subtle point is where to bind type variables that occur free in a type annotation (a : τ). Traditionally, these are shared between several type annotations, and thus implicitly bound at a higher level according to scoping rules that depend on the ML dialect. In our system, we chose to bind them (existentially) in the type constraint where they occur. That is, they are never shared between two different type annotations. This is simpler than defining specific scoping rules; and sharing a type variable between several annotations could lead to lose polymorphism unexpectedly.

2 FORMAL APPROACH

We formalize our approach as a small extension to core ML.

2.1 The core language

Types We assume given two collections of type variables α ∈ V, and labels ϵ ∈ E. The syntax of types is:

τ::= α | τ → τ | [σ]^{ϵ}  (Simple) types
σ::= τ | ∀α.σ  Polymorphic types
ς::= σ | ∀ϵ.ς  Type schemes
ξ::= α | ϵ  Variables

The construct [σ]^{ϵ} is used to coerce a polymorphic type σ to a type. We call [σ]^{ϵ} a weak polytype. The label variable ϵ is used to keep track of sharing between weak polytypes. When an expression has a polytype [σ]^{ϵ} and the label variable ϵ can be generalized, then the polytype can be eliminated and the expression can be given the polymorphic type σ. We do not allow polymorphic labels in polymorphic types σ, since this would not add any power to the system (it would be redundant with explicit type annotations —see section 2.5). Free type variables and free labels of a type scheme (which may be a simple type) ς are written F V (ς) and F L(ς) respectively and are defined as usual. In a type scheme ∀ξ.ς, ∀ acts as a quantifier, and the variable ξ is bound (i.e. not free) in ∀ξ.ς. We consider type schemes equal by renaming and reordering of bound variables and labels, and removal of useless quantifiers (i.e. ∀ξ.τ ≡ τ whenever variable ξ

\frac{x: ς ∈ A}{A ⊢ x: ς}^{(Var )}  \frac{A,x: τ_{0} ⊢ a: τ}{A ⊢ λx.a: τ_{0} → τ}^{(Fun )}  \frac{A ⊢ a_{1} : τ_{2} → τ_{1}  A ⊢ a_{2} : τ_{2}}{A ⊢ a_{1} a_{2} : τ_{1}}^{(App)}

\frac{A ⊢ a: σ  α ∉ F V (A)}{A ⊢ a: ∀α.σ}^{(Gen-V )}  \frac{A ⊢ a: ς  ϵ ∉ F L(A)}{A ⊢ a: ∀ϵ.ς}^{(Gen-E )}  \frac{A ⊢ a: ∀α.σ}{A ⊢ a: σ\{τ/α\}}^{(Inst-V )}

\frac{A ⊢ a: ∀ϵ.ς}{A ⊢ a: ς\{ϵ′/ϵ\}}^{(Inst-E )} (Let )

A ⊢ a_{1} : ς A,x: ς ⊢ a_{2} : τ
A ⊢ let x = a_{1} in a_{2} : τ

\frac{A ⊢ a: τ_{1} (τ_{1} : τ: τ_{2})}{A ⊢ (a: τ) : τ_{2}}^{(Ann )}

\frac{A ⊢ a: σ_{1}  (σ_{1} : σ: σ_{2})}{A ⊢ [a: σ] : [σ_{2}]^{ϵ}}^{(Intro )}  \frac{A ⊢ a: ∀ϵ.[σ]^{ϵ}}{A ⊢ ⟨a⟩: σ}^{(Elim )}

Figure 1: Typing rules

is not free in τ). We write {τ_{1},...τ_{n}/α_{1},...α_{n}} for the simultaneous substitution of variables α_{1}, …, α_{n} by τ_{1}, …, τ_{n}, respectively. As usual, bound variables and bound labels are renamed by substitutions so that free variables of τ_{i}’s can remain unchanged without being captured. For example (α → [∀β.β → α]^{ϵ}){τ/α} is τ → [∀β.β → τ]^{ϵ} provided β is not free in τ. An instance of a type scheme ∀ϵ̄,ᾱ.τ_{0} is τ{ϵ̄′,τ̄/ϵ̄,ᾱ}. A generic instance of a type scheme ς is a type scheme ∀ξ̄.τ such that τ is an instance of ς and bound variables ξ̄ do not occur free in ς.

Expressions are those of core ML (left) plus three new constructs (right): introduction and elimination of first-class polymorphism and type annotation.

a::= x | λx.a | a a | let x = a in a | [a: σ] | ⟨a⟩ | (a: τ)

Typing rules are given in figure 1. Typing judgments are of the form A ⊢ a : ς where A is a set of typing assumptions binding expression variables to type schemes. The extension of a set of typing assumptions A with a new binding x : ς is written A,x: ς; it overrides any previous binding of x in A. All typing rules but the last three ones are standard. Rules Ann and Intro use an auxiliary relation ( : : ). Given a polymorphic type σ, we write (σ_{1} : σ : σ_{2}) if there exists a substitution θ from type variables to simple types and two substitutions ρ_{1} and ρ_{2} from labels to labels, such that σ_{1} = θ(ρ_{1}(σ)) and σ_{2} = θ(ρ_{2}(σ)). The intuition is that if θ is the identity, then σ_{1} and σ_{2} are both equal to σ except maybe in their labels. Indeed, (ρ_{1}(σ) : σ: ρ_{2}(σ)) for any label renamings ρ_{1} and ρ_{2}. If σ does not contain any label, then (σ_{1} : σ: σ_{2}) is equivalent to σ_{1} and σ_{2} being the same generic instance of σ. The use of θ implements the local quantification of user-given type variables that we stated in the informal presentation. An important property of the relation ( : σ : ) is its stability by substitution. That is, if (σ_{1} : σ : σ_{2}), then (θ(σ_{1}) : σ : θ(σ_{2})) for any substitution θ. Note that σ is user-given and the substitution θ is not applied to σ. This relation is used to type explicit annotations. For typechecking purposes, the construct ( : τ) could have been replaced by a countable collection of primitives λx.(x: τ) indexed by τ and given with principal type scheme ∀ϵ̄_{1},ϵ̄_{2},F V (τ). τ{ϵ̄_{1}/ϵ̄} → τ{ϵ̄_{2}/ϵ̄} where ϵ̄_{1} and ϵ̄_{2} are different renamings of the tuple ϵ̄of all label variables of τ. That is, to type an expression (a : τ), let τ_{1} and τ_{2} be two copies of τ where their labels have been renamed, and θ be a substitution such that a has type θ(τ_{1}); then (a : τ) has type θ(τ_{2}). We kept annotation as a primitive construct because the dynamic semantics is simpler to define this way, but this is mainly a matter of exposition. Rule Intro uses the same relation, except that polymorphic types replace simple types. To type [a : σ], let σ_{1} and σ_{2} be two copies of σ where labels have been renamed; find a substitution θ such that a has type θ(σ_{1}) (i.e. θ(σ_{1}) is a generic instance of the principal type scheme of a); then [a : σ] has type [θ(σ_{2})]^{ϵ} for any label ϵ. Last, rule Elim says that polymorphism can be used only if the label of the polytype does not occur anywhere else. As an example, we have the following derivation, where σ abbreviates ∀α.α → α and A is f : [σ]^{ϵ_{1}}:

\underline{(Var )} ; A ⊢ f : [σ]^{ϵ_{1}} ([σ]^{ϵ_{1}} : [σ]^{ϵ}: [σ]^{ϵ_{2}}) \overline{(Ann )}

A ⊢ (f : [σ]^{ϵ}) : [σ]^{ϵ_{2}} \overline{(Gen-E )}

A ⊢ (f : [σ]^{ϵ}) : ∀ϵ_{2}.[σ]^{ϵ_{2}} (σ ≡ ∀α.α → α)  (Elim )

A ⊢ ⟨f : [σ]^{ϵ}⟩: ∀α.α → α (α ← [σ]^{ϵ_{1}})  (Inst-V )

A ⊢ ⟨f : [σ]^{ϵ}⟩: [σ]^{ϵ_{1}} → [σ]^{ϵ_{1}}

⋮ \overline{(Var )} ; A ⊢ f : [σ]^{ϵ_{1}} \overline{(App)}

A ⊢ ⟨f : [σ]^{ϵ}⟩ f : [σ]^{ϵ_{1}} \overline{(Fun )}

⊢ λf.⟨f : [σ]^{ϵ}⟩ f : [σ]^{ϵ_{1}} → [σ]^{ϵ_{1}}

2.2 Dynamic semantics

We give a reduction semantics for the core language. Actually we define two semantics: a free reduction semantics for which we prove only subject reduction, and a call-by-value semantics for which we prove full type soundness. A one step reduction is either an immediate reduction (the label on the reduction is indicative and optional):

(λx.a) b −→^{Fun} a{b/x}
let x = b in a −→^{Let} a{b/x}
⟨[a: ∀ᾱ.τ]⟩ −→^{Elim} (a: τ)
(a: τ_{2} → τ_{1}) b −→^{Tfun} (a (b: τ_{2}) : τ_{1})
([a: ∀ᾱ.τ] : [σ]^{ϵ}) −→^{Tint} [(a: τ) : σ]
(a: α) −→^{Tvar} a

or obtained by induction (E is any term context with a single hole):

a_{1} −→ a_{2}
E{a_{1}} −→ E{a_{2}}

Note that the meta variable α, in rule Tvar , stands for a type variable and not for an arbitrary type. It is a major difference with ML that type annotations are not just a means to restrict principal types to instances. On the opposite, they allow better typings. Thus, reduction must preserve type annotations as long as they provide useful typing information. Indeed, while terms are effectively reduced by rules Fun , Let , and Elim , we need the rules Tfun and Tint to maintain this type information. These rules are needed for the following example: λf.⟨(λx.x: [σ] → α) f⟩ reduces to λf.⟨f : [σ]⟩ which would not be typable but for the annotation. Rule Tvar erases vacuous type information. Although types are preserved during reduction, they do not actually participate in the reduction. In particular, it would be immediate to define an untyped reduction −→^{∼} and a type-erasure ∼ so that if a_{1} −→ a_{2}, then ã_{1} −→^{∼} ã_{2} or ã_{1} and ã_{2} are equal. We now define the call-by-value operational semantics by restricting the free reduction semantics. Evaluation contexts (used for the above induction rule) are then

E ::= {} | E a | v E | let x = E in a | [E : σ] | (E : τ) | ⟨E⟩

and the strategy is fixed so that inner redexes are reduced first. This is implemented by substituting a value meta variable v for term meta variables a or b when they appear at evaluable positions in the reduction rules. Values v are defined as follows:

\begin{matrix}v::= & w | [v: σ] \\ w::= & λx.a | (w: τ_{1} → τ_{2}) \end{matrix}

By default, reduction will always refer to free reduction.

2.3 Type soundness

We could easily show that evaluation cannot go wrong by means of translation into system F. We prefer to prove it in a more direct way. Subject reduction is an intermediate result of the direct proof that is neither required nor implied by type soundness. However, it is quite important for itself, since it shows that each reduction step preserves typings, and thus that the static semantics is tightly related to the dynamic semantics. Subject reduction is not obviously preserved by the introduction of polytypes; in particular, subject reduction would not hold if we threw away type constraints too early during reduction. Both subject reduction and type inference are simplified by restricting ourselves to canonical derivations. A similar result existed for the original Damas-Milner presentation of ML, but ML is now often presented in its syntax directed form. We chose a logic rather than a syntax directed presentation of typings rules, since this is here much more concise. We can still recover the benefits of a syntax directed presentation by using canonical derivations. Canonical derivations are those where occurrences of rules Gen and Inst are restricted as follows:

• rule Gen only occurs as the last rule of the derivation or right above rule Intro , Elim , the left premise of rule Let , or another rule Gen .

• rule Inst may only occur right after rule Var , rule Elim , or another rule Inst .

Canonical derivations have been defined to validate the following lemma.

Lemma 1 (Canonical derivations) A valid typing judgment A ⊢ a: τ has a canonical derivation.

Another classical key result is the stability of typing judgments by substitution:

Lemma 2 (Stability) If A ⊢ a: τ, then for any substitution θ, θ(A) ⊢ a: θ(τ).

It is important to notice that the substitution is not applied to the expression a; in particular, type constraints inside a are left unchanged: their free variables must be understood as if they were closed by existential quantification (see the last paragraph of section 1.3). We define a relation a_{1} ⊂ a_{2} between programs stating that all typings of a_{1} are also typings of a_{2}, i.e.

a_{1} ⊂ a_{2} =^{△} (∀A,ς, A ⊢ a_{1} : ς ⟹ A ⊢ a_{2} : ς)

This simplifies the statement of subject reduction, expressed for free reduction.

Theorem 1 (Subject reduction) Reduction preserves typings, i.e. if a_{1} −→ a_{2}, then a_{1} ⊂ a_{2}.

Subject reduction is not sufficient to prove type soundness, since the full relation (every program has every type in any context) satisfies subject reduction but does not prevent from type errors. It must be complemented by the following result, which we only express for call-by-value semantics.

Theorem 2 (Canonical forms) Irreducible programs (for call-by-value reduction) that are well-typed in the empty environment are values.

Type soundness of the call-by-value semantics is a straightforward combination of the two previous theorems.

2.4 Type inference

We present both unification and type inference as constraint solving using rewriting techniques. This formalism, now well-established [Jouannaud and Kirchner, 1991], has several significant advantages over older, more algorithmic presentations of unification algorithms: renaming and introduction of fresh variables is rigorously and simply formalized by existential binders; sharing, hence recursive types, is formally dealt with by the use of multi-equations instead of simple equations^{2}; the presentation with rewriting constraints is also more modular, which eases proofs as well as further extensions. The same framework can also be used for type inference, treating type inference problems as unification problems [Rémy, 1992]. Indeed, solutions of type inference problems are also sets of substitutions. All the previous benefits of treating unification as constraint solving also apply to type inference. In particular, type inference can be specified and proved correct independently of any strategy. A top-down, bottom-up, or any other —even non-deterministic— terminating strategy can be chosen later, or remain unspecified. First-order unification on simple types must be extended to handle polytypes. During unification, a polytype is treated as a rigid skeleton corresponding to the polymorphic part, on which hang simple types. Reusing the framework of constraint solving, we show that the addition of first-class polymorphism retain the flexibility and modularity of type inference. Simultaneously, we provide formal, general, and efficient unification and type inference algorithms (no use of “fresh variables”, preservation of sharing, treatment of recursive types^{3}). More precisely, the formalism used is that of conditional rewriting. For clarity of presentation, we distinguish between two kinds of conditions. Those that can always be satisfied are written let condition in rule; they amount to a convenient notation for pattern matching. Other conditions may fail, providing dynamic control during the inference process; they are written if condition then rule.

Unification for simple types First, we remind unification for simple types. In this part only, we exclude polytypes from simple types, still ranged over by letter τ. A unification problem, also called a unificand, is a formula U defined by the following grammar.

U ::= ⊥ | ⊤ | U ∧ U | ∃α.U | e  Unification problems
e::= τ | τ ≐ e  Multi-equations

The symbols ⊤ and ⊥ are respectively the trivial and unsatisfiable unification problems. We treat them as a unit and a zero for ∧. That is U ∧ ⊤ and U ∧ ⊥ are equal to U and ⊥, respectively. We also identify ⊤ with singleton multi-equations. That is, we can always consider that a unification problem U contains at least one multiequation α or α ≐ e for each variable α of U. A complex formula is the conjunction of other formulas or the existential quantification of another formula. The symbol ∧ is commutative and associative. The symbol ∃ will be needed later for polytypes. It acts as a binder, i.e. free variables of ∃α.U are free variables of U except α. Bound variables can freely be renamed. We identify ∃α_{1}.∃α_{2}.U and ∃α_{2}.∃α_{1}.U and simply write ∃α_{1},α_{2}.U. The symbol ≐ is associative and commutative. This makes multi-equations behave as multi-sets of types. The substitution of types is extended to unificands in a straightforward way. For existentials, the application of a substitution θ to a unificand ∃α.U is the unificand ∃α′.θ(U{α′/α}) where α′is chosen outside of both the domain and the codomain of θ and outside free variables of U. A substitution θ is a solution of a multi-equation if it sends all types of the multiequation to the same codomain. The substitution θ satisfies a conjunction of subproblems if it satisfies all subproblems; θ is a solution of ∃α.U if it can be extended on α′into a solution of U{α′/α} where α′is chosen outside of both the domain and the codomain of θ and outside free variables of U. Two unification problems are equivalent if they have the same set of solutions. All previous structural equalities are indeed equivalences. We write U_{1} ≡ U_{2} when the unification problems U_{1} and U_{2} are equivalent. We also write U_{1} −> U_{2} to mean that the unification problem U_{1} can be rewritten into the equivalent unification problem U_{2}. Finally, a solution θ is a principal solution of a unification problem U if any other solution can be obtained by (left) composition with the substitution θ. Given a unification problem U, we define the containment ordering ≺_{U} as the transitive closure of the immediate precedence ordering containing all pairs α ≺ α′ such that there exists a multi-equation α ≐ τ ≐ e in U where τ is a non-variable type that contains α′ as a free variable. A unification problem is strict if ≺_{U} is irreflexive. Note that strictness is syntactic and is not preserved by equivalence. Intuitively, strictness corresponds to the absence of immediate cycles. However, it does not detect potential cycles that may appear after some computation steps. Still, for fully merged and decomposed unification problems, i.e. when the rules Merge and Decompose cannot be applied anymore, strictness is equivalent to the fact that if there is a solution then there is a finite solution. A problem is in solved form if it is either ⊥ or ⊤, or if it is strict, merged, decomposed, and of the form ∃ᾱ. ⋀ _{i∈1..n} e_{i}. In particular, each multi-equation e_{i} contains at most one non-variable type, and if i ≠ j then e_{i} and e_{j} contain no variable type in common. An explicit principal solution θ can be read straightforwardly from a problem in solved form. We also write U −> ∃ξ̄.θ if θ is a principal solution of U and variables ξ̄ are not free in U, or by abuse of notation, if U is unsatisfiable and θ is ⊥. This is consistent with the previous notation since θ could be seen as ∧_{α∈dom(θ)} α ≐ θ(α) whenever its domain and codomain are disjoint. The unification algorithm is given as a set of rewriting rules that preserve equivalence in figure 2. There are implicit context rules that allow to rewrite complex Occur-Check if≺_{U} is not strict then U −> ⊥ Merge α ≐ e ∧ α ≐ e′−> α ≐ e ≐ e′ Absorb α ≐ α ≐ e −> α ≐ e Decompose if size(τ_{1} → τ_{2}) ≤ size(τ′_{1} → τ′_{2}) then τ_{1} → τ_{2} ≐ τ′_{1} → τ′_{2} ≐ e −> τ_{1} → τ_{2} ≐ e ∧ τ_{1} ≐ τ′_{1}∧ τ_{2} ≐ τ′_{2}

2Multi-equations can be easily mapped to equivalence classes as in [Huet, 1976], as well as to the mutable structures that are used in destructive unification algorithms.

3Recursive types are correctly handled by our algorithms, although they are not considered in the proofs.

Figure 2: First-order unification for simple types

formulas by rewriting any sub-formula. We write size(σ) the size of polymorphic type σ counted as the number of occurrences of symbols ( → ) or [ ] in σ. These rules are all standard. It is well-known that given an arbitrary unification problem, applying these rules always terminate with a unification problem in solved-formed. The rule Occur-Check rejects solutions with recursive types. If it were omitted the algorithm would infer recursive types.

Unification for simple-types with polytypes We now extend types to polytypes [σ]^{ϵ}. Consistently, we extend type variables with label variables. Hence, substitutions are from type variables to polytypes and from label variables to label variables, unless otherwise specified. In order to allow a natural decomposition of polytypes, we extend typing problems with equations between polymorphic types.

U ::= ... | σ =^{∀} σ

These are not multi-equations. In particular, a variable cannot be equated to an arbitrary polymorphic type. For instance, α′ =^{∀} ∀α.α → α does not have any solution. Thus, equations involving polymorphic types are never merged. A substitution θ is a solution of a polytype equation ∀ᾱ.τ =^{∀} ∀ᾱ′.τ′if θ(∀ᾱ.τ) = θ(∀ᾱ′.τ′), where equality is the usual equality for polymorphic types in ML, i.e. it is taken modulo reordering and renaming of universal quantifiers and removal of useless universal variables. This is equivalent to the existence of

• two injective substitutions ρ and ρ′ of respective domains ᾱ and ᾱ′ and of codomain ᾱᾱ′ and

• a renaming η from ᾱᾱ′ outside of free variables of θ, τ, τ′, and ᾱᾱ′

such that θ ∘ η is a solution of ρ(τ) = ρ′(τ′). We could solve such unification problems by first unifying ρ(τ) and ρ′(τ′) and then checking the constraints. However, Decompose-Poly if size(σ) ≤ size(σ′) then

[σ]^{ϵ} ≐ [σ′]^{ϵ′} ≐ e −> [σ]^{ϵ} ≐ e ∧ ϵ ≐ ϵ′∧ σ =^{∀} σ′

Clash [σ]^{ϵ} ≐ τ → τ′ ≐ e′−> ⊥ Polytypes let ᾱ∩ ᾱ′ = ∅ and ᾱ∩ F V (τ′) = ∅ and ᾱ′∩ F V (τ) = ∅ in

∀ᾱ.τ =^{∀} ∀ᾱ′.τ′−> ∃ᾱᾱ′.τ ≐ τ′∧ ᾱ ↔ ᾱ′

Renaming-True let ᾱ = (α_{i})^{i∈1..n+p} and ᾱ′ = (α′_{i})^{i∈1..n+q} in ∃ᾱᾱ′.(α_{i} ≐ α′_{i})^{i∈1..n} ∧ ᾱ ↔ ᾱ′ −> ⊤ Renaming-False if β ∈ ᾱ and τ ∉ ᾱ′∪ {β} then β ≐ τ ≐ e ∧ ᾱ ↔ ᾱ′ −> ⊥ if β ∈ ᾱ∩ F V (τ) and τ ≠ β then γ ≐ τ ≐ e ∧ ᾱ ↔ ᾱ′ −> ⊥

Figure 3: First-order unification for simple types with polytypes

this would force some unnecessary dependence. Note that η is only here for technical purposes, and can be omitted if θ is disjoint from ᾱᾱ′. This can be dealt with by existential quantification of unificands. Without loss of generality, we can restrict ourselves to the case where ᾱ ∩ ᾱ′, F V (τ) ∩ ᾱ′, and F V (τ′) ∩ ᾱ are all empty sets. We refer to these hypotheses by condition (H). We write the sum of two substitutions of disjoint domains θ + θ′that maps variables of dom(θ) and dom(θ′) to their image by θ or θ′, respectively. We write θ |` W for the restriction of the substitution θ to the set of variables W, that is, the substitution equal to θ on dom(θ) ∩ W and to the identity everywhere else. We write V \ W for the set difference between V and W, i.e. the set of all elements that are in V but not in W. Consistently, we write θ\W for the restriction of a substitution outside of a set of variables W, that is the restriction of θ to dom(θ)\W, or formally, θ |` (dom(θ) \ W). Let θ′be (η+η^{−1} )∘θ∘η∘(ρ+ρ′), which decomposes as (η∘θ\ᾱᾱ′)+(ρ+ρ′). (If θ is disjoint from ᾱᾱ′, then θ′ is simply θ ∘ (ρ + ρ′), which decomposes into θ + ρ + ρ′.) The substitution θ′satisfies the three following properties:

(1) θ′(τ) = θ′(τ′),

(2) θ′|`ᾱ and θ′|`ᾱ′ are injective in ᾱᾱ′, and

(3) no variable of ᾱᾱ′ appears in codom(θ′\ ᾱᾱ′).

Conversely, a substitution θ′satisfying these three conditions is a solution of ∀ᾱ.τ =^{∀} ∀α′.τ′. The condition (1) above is a unification problem. We introduce a new kind of unificands ᾱ ↔ ᾱ′ whose solutions are substitutions satisfying the conditions (2) and (3) simultaneously. We consider ᾱ and ᾱ′ as multi-sets (i.e. the comma is associative and commutative). In order to avoid special cases, we also require that no variable is listed twice in the sequence ᾱᾱ′ (in particular ᾱ∩ ᾱ′ is empty). The symbols =^{∀} and ↔ are commutative. Then θ is a solution of ∀ᾱ.τ =^{∀} ∀ᾱ′.τ′ under the assumption (H), if and only if it is a solution ∃ᾱᾱ′.(τ ≐ τ′∧ ᾱ ↔ ᾱ′). Note that unificands are no longer stable by arbitrary substitutions as long as they contain free variables appearing in renaming unificands (otherwise, renaming unificands could even become ill-formed.) Still, unificands remain stable by renamings. Indeed this is necessary to give meaning to existentially quantified unificands. Rules for unification with polytypes are those of figures 2 and 3 together. Rule Clash handles type incompatibilities. Rule Polytypes transforms polytype equations as described above. Rule Renaming-True allows to remove a satisfiable renaming constraint that became garbage, i.e. independent of all other multi-equations. On the opposite, rule Renaming-False detects unsolvable renaming constraints. In the first case, a solution θ of ᾱ ↔ ᾱ′ would identify a variable β of ᾱ with another variable of ᾱ (thus θ would not be injective) or with a term outside of ᾱ∪ ᾱ′. In the second case, the image of a variable γ would contain properly a variable β of ᾱ, making it leak into a wider environment (thus, violating condition 3). It can be easily checked that if U is merged and decomposed, then for every renaming constraint that remains, either rule Renaming-True or rule Renaming-False applies. Therefore, renaming constraints can always be eliminated.

Theorem 3 Given a unification problem U, there exists a most general unifier θ which is computed by the set of rules in figures 2 and 3, or there is no unifier and U reduces to ⊥.

Type inference For type inference, we extend unificands with typing problems. A typing problem is a triple, written A ▷ a : τ, of an environment A, a term a, and a type τ. A solution of a typing problem A ▷ a : τ is a substitution θ such that θ(A) ⊢ a : θ(τ). By lemma 2, the set of solutions of a typing problem is stable under substitution. Thus, typing problems can be treated as unification problems, following [Rémy, 1992]. The rules for solving typing problems are given in figure 4. The generalization Gen (σ,A) is, as usual, ∀ξ̄.σ where ξ̄ are all free variables and free labels of σ that do not occur in A. To lighten the presentation, we leave it implicit that whenever we write ∃ξ̄.θ, variables ξ̄ are assumed to be distinct from all other variables appearing in the rule. The rewriting for type inference closely follows typing rules given in 1, except that we are assuming a syntactic presentation enforcing canonical derivations where rules Var and Elim are combined with (followed by) rule Inst- and rules Let and Use are combined with (preceded by) rule Gen as in canonical forms. Rules Var , Fun , App, Let are the same as for ML [Rémy, 1992]. The remaining rules are new but unsurprising. Their close correspondence with rules of figure 1 is made in the proof of soundness and completeness of type inference given in appendix A.

Var let ∀ξ̄.τ′= A(x) and ξ̄∩ F V (τ) = ∅ in A ▷ x: τ −> ∃ξ̄.τ ≐ τ′ Fun let α_{1},α_{2} ∉ F V (A) ∪ F V (τ) in A ▷ λx.a: τ −> ∃α_{1},α_{2}.(A,x: α_{1} ▷ a: α_{2}) ∧ τ ≐ α_{1} → α_{2} App let α ∉ F V (A) ∪ F V (τ) in A ▷ a_{1} a_{2} : τ −> ∃α.(A ▷ a_{1} : α → τ) ∧ (A ▷ a_{2} : α) Let let α ∉ F V (A) in if A ▷ a_{1} : α −> ∃ξ̄.θ then

A ▷ let x = a_{1} in a_{2} : τ −> ∃ξ̄,α.θ ∧ A,x: Gen (θ(α),θ(A)) ▷ a_{2} : τ else A ▷ let x = a_{1} in a_{2} : τ −> ⊥

Ann let ϵ̄_{0} = F L(τ_{0}) and ϵ̄_{1} and ϵ̄_{2} be disjoint copies of ϵ̄_{0} outside of A and τ and ᾱ_{0} = F V (τ_{0}) and ᾱ_{1} be a copy of ᾱ_{0} outside of A and τ and τ_{1} = τ_{0}{ᾱ_{1}/ᾱ_{0}} in

A ▷ (a: τ_{0}) : τ −> ∃ϵ̄_{1},ϵ̄_{2},ᾱ_{1}.A ▷ a: τ_{1}{ϵ̄_{1}/ϵ̄_{0}} ∧ τ ≐ τ_{1}{ϵ̄_{2}/ϵ̄_{0}} Intro let σ = ∀ᾱ.τ_{0} and ᾱ∩ F V (A) = ∅ and ϵ̄_{0} = F L(σ) and ϵ̄_{1} and ϵ̄_{2} be disjoint copies of ϵ̄_{0} outside of A and τ and ᾱ_{0} = F V (σ) and ᾱ_{1} be a copy of ᾱ_{0} outside of A, τ and ᾱ and τ_{1} = τ_{0}{ᾱ_{1}/ᾱ_{0}} in if A ▷ a: τ_{1}{ϵ̄_{1}/ϵ̄_{0}} −> ∃ξ̄.θ and ᾱ∩ (dom(θ) ∪ F V (codom(θ))) = ∅ then

A ▷ [a: σ] : τ −> ∃ξ̄,ϵ̄_{1},ϵ̄_{2},ᾱ_{1},ϵ.θ ∧ τ ≐ [∀ᾱ.τ_{1}{ϵ̄_{2}/ϵ̄_{0}}]^{ϵ} else A ▷ [a: σ] : τ −> ⊥

Elim let α ∉ F V (A) in if A ▷ a: α −> ∃ξ̄.θ then

if θ(α) = [∀ᾱ′.τ′]^{ϵ} and ϵ ∉ F L(θ(A)) then A ▷ ⟨a⟩: τ −> ∃ξ̄,α,ᾱ′.θ ∧ τ′ ≐ τ

else if θ(α) = α′and α′ ∉ F V (θ(A)) then A ▷ ⟨a⟩: τ −> ∃ξ̄,α.θ
else A ▷ ⟨a⟩: τ −> ⊥

else A ▷ ⟨a⟩: τ −> ⊥

Figure 4: Rewriting rules for type inference.

Theorem 4 Given a typing problem (A ▷ a : τ) there exists a principal solution, which is computed by the set of rules described in figures 2, 3 and 4, or there is no solution and the rules reduce to ⊥.

2.5 Polymorphic labels in polytypes

We did not allow labels in polymorphic types σ. We show here that this would not increase expressiveness. In this section, we consider an alternative type system, called the extended type system, where extended polytypes are of the form [ς]^{ϵ} instead of [σ]^{ϵ}. Typing rules are unchanged. To show that this does not increase expressiveness, we define a translation ⟨⟨ ⟩⟩_{E} from extended type schemes to type schemes. The translation is parameterized by a set of label variables E that is omitted when empty. For simplicity, we suppose that all quantified labels have different names in the definition of the translation:

⟨⟨α⟩⟩_{E} =^{△} α
⟨⟨τ_{1} → τ_{2}⟩⟩_{E} =^{△} ∀ϵ̄_{1}ϵ̄_{2}.τ′_{1} → τ′_{2}  if ⟨⟨τ_{i}⟩⟩_{E} = ∀ϵ̄_{i}.τ′_{i}
⟨⟨[∀ϵ̄.σ]^{ϵ_{0}}⟩⟩_{E} =^{△} ∀ϵ̄ϵ̄′.[σ′]^{ϵ_{0}}  if ϵ_{0} ∈ E and ⟨⟨σ⟩⟩_{ϵ̄∪E} = ∀ϵ̄′.σ′
⟨⟨[∀ϵ̄.σ]^{ϵ_{0}}⟩⟩_{E} =^{△} ∀ϵ̄′.[σ′]^{ϵ_{0}}  if ϵ_{0} ∉ E and ⟨⟨σ⟩⟩_{E} = ∀ϵ̄′.σ′
⟨⟨∀α.σ⟩⟩_{E} =^{△} ∀ϵ̄.∀α.σ′  if ⟨⟨σ⟩⟩_{E} = ∀ϵ̄.σ′
⟨⟨∀ϵ̄.σ⟩⟩ =^{△} ∀ϵ̄.⟨⟨σ⟩⟩ϵ̄

Intuitively, the translation moves label quantifiers to the outer level. During this process however, label quantifiers that appear in a polytype whose label is itself not quantified are simply dropped. The translation is extended homomorphically to expressions and typing environments. Then, considering the judgment A ⊢ a: ς in the extended type system, it is translated into the judgment ⟨⟨A⟩⟩ ⊢ ⟨⟨a⟩⟩ : ⟨⟨ς⟩⟩ of our system. The latter has smaller type annotations since all label quantifiers are dropped in ⟨⟨a⟩⟩. It is then easy to prove (by induction on the size of the former derivation) that whenever the former judgment is valid, so is the later.

2.6 Printing labels as sharing constraints

In this section, we propose an alternative interface to the user aimed at enhancing readability of types. It is also robust. However, it is slightly harder to present, formally. Hence, we followed the other, more traditional approach above for simplicity of presentation. Labels are used to trace the sharing of polytypes. Types can be restricted so that two polytypes with the same label are necessarily equal. This property is not required in the present type system, but it is stable: if satisfied by all initial type assumptions in A and type annotations in a, then it remains valid in all types appearing in a principal derivation of A ⊢ a: τ. The grammar of types can be extended with a sharing construct^{4}:

τ::= ... | (τ where α = τ)

Using sharing, any type can always be written such that every label occurs at most once, and thus can be omitted. In fact, in our presentation, sharing of types is preserved during type inference. Sharing was just ignored when reading principal solutions from unificands in solved form. The where construct allows to read and print all sharing present in the solved form. Actually, only sharing involving polytypes needs to be printed; all other sharing can be ignored. For instance, the expression λx.(x : [σ]) has type [σ] → [σ], which would have previously been written ∀ϵ,ϵ′.[σ]^{ϵ} → [σ]^{ϵ′}. Conversely, the expression λx.let y = (x : [σ]^{ϵ}) in x has type (α → α where α = [σ]^{ϵ}) which would have been written ∀ϵ.[σ]^{ϵ} → [σ]^{ϵ}, where the two polytypes share the same label. Both notations (sharing constraints and label variables) actually coincide when all polytypes are anonymous (i.e. no label variable occur twice) and polytypes are simply written [σ]. For instance, λx.(x: [σ]) has type [σ] → [σ]. This is an important case, since the only types the user actually needs to write are of this form. Indeed, types written by the user are only type annotations, which become more general by removing sharing constraints. More precisely, if σ′is a polymorphic type obtained from σ by a label substitution ρ, then for any expression a, we have (a: [σ]) ⊂ (a: [σ′]) and [a: σ] ⊂ [a: σ′]. This is an easy consequence of σ being more general than σ′. Thus, the user never needs to write labels or sharing constraints, but he must read them in both inferred types and type-error messages.

4Alternatively, one could use the binding τ as α as in Objective ML, although the binding scope of as is less clear and harder to deal with, formally.

3 ENCODINGS

In this section, we give encodings in our language for both explicit polymorphism with datatypes and system F. This last encoding is direct, and makes our language an alternative to system F. We also compare the use of explicit type information between system F and our proposal.

3.1 Type annotation on arguments

It is convenient to allow λx:τ.a in expressions. We see such expressions as syntactic sugar for λx.let x = (x: τ) in a. The derived typing rule is:

\frac{A,(x: ∀ϵ̄.τ_{2}) ⊢ a: τ′ (τ_{1} : τ: τ_{2})  ϵ̄∩ F L(τ_{1}) = ∅}{A ⊢ λx:τ.a: τ_{1} → τ′}^{(Poly-Fun )}

The derived reduction is (λx:τ.a) b −→^{Fun} a{(b : τ)/x}. Note that τ_{1} and τ_{2} are not just the results of renaming label variables of τ. They may also be an instance of τ. Hence, the set ϵ of generalized labels contains only labels corresponding to copies of those of τ and do not include any label that would have been brought by the instance of a free type variable of τ (since those would also appear in τ_{1}).

3.2 Polymorphic datatypes

Previous works have used data types to provide ML with explicit polymorphism [Läufer and Odersky, 1994, Rémy, 1994, Odersky and Läufer, 1996]. Omitting other aspects that are irrelevant here, all these works amount to an extension of ML with expressions of the form:

t ::= α | t → t | T ᾱ  Types
s::= t | ∀α.s  Polymorphic types
M ::= x | M M | λx.M | T M | T^{−1} M  Terms
| type T ᾱ = s in M  Type declarations

where T ranges over datatype symbols. In expressions, T and T^{−1} act as mutually inverse introduction and elimination functions to coerce the polymorphic type s into the simple type T ᾱ. The translation is an inductive definition ⟨⟨ ⟩⟩_{ρ}. The environment ρ is a list of type definitions type T ᾱ = σ_{0} and ρ(T) is the function Λᾱ.σ_{0}, i.e. given type arguments τ̄, it returns the type σ_{0}{τ̄/ᾱ}, using the right most definition of T in ρ. The translation of these types into types of our language is straightforward. The translation does not actually use type annotations smartly, and uses a single label ϵ. (While the program uses only one label, the type derivation need at least two other labels to type the elimination patterns ⟨⟨⟨M⟩⟩_{ρ} : [ρ(T) ᾱ]^{ϵ}⟩, locally.) It could also make all labels of the translation different, i.e. anonymous, but this is not needed.

{⟨⟨α⟩⟩_{ρ} =^{△} α  ⟨⟨t_{1} → t_{2}⟩⟩_{ρ} =^{△} ⟨⟨t_{1}⟩⟩_{ρ} → ⟨⟨t_{2}⟩⟩_{ρ}  ⟨⟨T t̄⟩⟩_{ρ} =^{△} [⟨⟨ρ(T) t̄⟩⟩_{ρ}]^{ϵ} \atop ⟨⟨∀α.s⟩⟩_{ρ} =^{△} ∀α.⟨⟨s⟩⟩_{ρ}}

We translate programs as follows.

⟨⟨x⟩⟩_{ρ} =^{△} x  ⟨⟨type T ᾱ = t in M⟩⟩_{ρ} =^{△} ⟨⟨M⟩⟩_{ρ,type T ᾱ=t}
⟨⟨λx.M⟩⟩_{ρ} =^{△} λx.⟨⟨M⟩⟩_{ρ}  ⟨⟨M_{1} M_{2}⟩⟩_{ρ}=^{△} ⟨⟨M_{1}⟩⟩_{ρ} ⟨⟨M_{2}⟩⟩_{ρ}
⟨⟨T M⟩⟩_{ρ} =^{△} [⟨⟨M⟩⟩_{ρ} : ρ(T) ᾱ]  ⟨⟨T^{−1} M⟩⟩_{ρ} =^{△} ⟨(⟨⟨M⟩⟩_{ρ} : [ρ(T) ᾱ]^{ϵ})⟩

Indeed, the pattern ⟨( : [σ])⟩ amounts to the explicit elimination of polymorphism (the explicit polytype annotation ( : [σ]) ensures that the polytype is anonymous.) Since the elimination of polymorphism is always explicit in the translated terms, it can easily be shown that the translation of a well-typed term is well-typed. More precisely, we extend the translation ⟨⟨ ⟩⟩ to typing environments as follows.

⟨⟨∅⟩⟩_{ρ} =^{△} ∅  ⟨⟨A,x: τ⟩⟩_{ρ} =^{△} ⟨⟨A⟩⟩_{ρ},x: ⟨⟨τ⟩⟩_{ρ,⌈A⌉}  ⟨⟨A,type T ᾱ = s⟩⟩_{ρ} =^{△} ⟨⟨A⟩⟩_{ρ}
⌈∅⌉ =^{△} ∅  ⌈A,x: τ⌉ =^{△} ⌈A⌉  ⌈A,type T ᾱ = s⌉ =^{△} (⌈A⌉,type T ᾱ = s)

For any term M, if A ⊢ M : t, then ⟨⟨A⟩⟩ ⊢ ⟨⟨M⟩⟩_{⌈A⌉}: ⟨⟨t⟩⟩_{⌈A⌉}. As we noticed above, the translation does not use type annotations smartly. Indeed, all eliminations are explicitly typed and the translation could have been given in a weaker language with explicit elimination of polymorphism.

3.3 Encoding system F

Laüfer and Odersky have shown an encoding of system F into polymorphic datatypes [Odersky and Läufer, 1996]. This guarantees by composition that system F can be encoded into semi-explicit polymorphism. We give here a direct encoding of system F, which is much simpler than the encoding into polymorphic datatypes. The types and the terms of system F are

t ::= α | t → t | ∀α.t  Types
M ::= x | M M | λx:t.M | Λα.M | M t  Terms

The translation of types of system F into types of our language is again straightforward, and may use a single label ϵ:

⟨⟨α⟩⟩ =^{△} α  ⟨⟨t_{1} → t_{2}⟩⟩ =^{△} ⟨⟨t_{1}⟩⟩ → ⟨⟨t_{2}⟩⟩  ⟨⟨∀α.t⟩⟩ =^{△} [∀α.⟨⟨t⟩⟩]^{ϵ}

The translation ⟨⟨ ⟩⟩ is extended to typing environments in an homomorphic way. The translation of typing derivations of terms of system F into terms of our language is given by the following inference rules:

\frac{x: t ∈ A}{A ⊢ x: t ⇒ x}  \frac{A,x: t ⊢ M : t′⇒ a}{A ⊢ λx:t.M : t → t′⇒ λx:⟨⟨t⟩⟩ .a}

\frac{A ⊢ M : t′→ t ⇒ a  A ⊢ M′: t′⇒ a′}{A ⊢ M M′: t ⇒ a a′}  \frac{A ⊢ M : t ⇒ a  α ∉ F V (A)}{A ⊢ Λα.M : ∀α.t ⇒ [a: ∀α.⟨⟨t⟩⟩]}
A ⊢ M : ∀α.t′⇒ a
A ⊢ M t : t′{t/α} ⇒ ⟨a⟩

Since the translation rules copy the typing rules of system F, the translation is defined for all well-typed terms. There is no ambiguity and the translation is deterministic.

Lemma 3 For any term M of system F, if A ⊢ M : t ⇒ a, then ⟨⟨A⟩⟩ ⊢ a: ⟨⟨t⟩⟩.

\underline{Proof}: The proof is by structural induction on M. The only potential difficulty is to ensure that when typing ⟨a⟩ the polytype [σ]^{ϵ} of a is always anonymous. This is immediate: since the translation of an abstraction is always annotated with the exact type of the variable, all type schemes of the typing environment may be fully generalized with respect to label variables; therefore there should be a derivation with no free labels in the typing environment where rule Elim will always succeed.

If we choose for system F the semantics where abstraction does not stop evaluation, then the translation preserves the semantics in a strong sense (reduction steps of a term can be mapped to reduction steps of the translated term). Another semantics would need easy adjustment, either of the translation or of the semantics of our system.

The simplicity of our encoding of system F compared to its encoding into polymorphic datatypes [Odersky and Läufer, 1996] mainly results from having polytypes as first-class types. We have used a single label in the translation, as in the previous section. However, the derivation now relies on polymorphism of label variables in the construction λx:τ.a and the elimination sites are left unannotated.

3.4 Comparison with system F

The above encoding shows that our system is a possible alternative to system F. Thus, it is interesting to compare a term M of system F with its translation a in our language, syntactically. Our types differ by having an extra type constructor [ ] surrounding every polymorphic type. Term variables do not carry type information in either M or a. Lambda abstractions carry exactly the same type information in both M and a. The type information at elimination of polymorphism is always omitted in a. The counterpart is that type information at introduction of polymorphism appears explicitly in [a: ∀α.⟨⟨τ⟩⟩]. In Λα.M, only the variable α is mentioned; the type τ is deduced from the type information located at abstraction and application nodes in M. The comparison can be illustrated on the following two abstract examples:

⟨⟨λ(f:∀α.t).M{f t′}⟩⟩ = λf:[∀α.τ].a{⟨f⟩}

⟨⟨M_{1}{Λα.M_{2}}⟩⟩ = a_{1}{[a_{2} : ∀α.τ]}

The first example corresponds to the abstraction and use of a polymorphic value f in a function. Type annotations are similar in system F and our system, and we are even shorter since we can omit the instantiation types at polymorphism elimination. For such cases, our approach appears to be more comfortable than system F. In the second example we introduce polymorphism somewhere inside a term. While system F can do it just by giving the type variable to quantify, we have to give an explicit polymorphic type. Indeed, our system provides no way to identify a type variable outside of an explicit type. Which of the two syntaxes will be longer depends on which one of the two patterns dominates the other. We believe that the former pattern is more frequent in user programs, and that conversely the latter is more frequent in libraries. Hence, our system may provide a reasonable alternative syntax for higher-order programming. Notice also that we have been comparing here a system F term and its direct translation in our system. Terms directly written in our system can omit much more type information. For instance, we do not actually need to provide a full type in our second example, but only a skeleton containing all occurrences of α in τ. And since we are extending ML, we do not need explicit type abstraction and instantiation for toplevel polymorphism. We may also develop specific idioms. One of them is the simultaneous use of multiple type abstractions, as in [a: ∀α_{1},α_{2}.τ]. Since type application is explicit in system F, the expression Λα_{1},α_{2}.M would be ambiguous; thus it is not allowed.

This does not give us more concision than system F, but it allows to avoid the common pattern [[f : ∀α.τ] : ∀α′.∀α.τ]. In most cases, instantiation of all variables will be simultaneous and we can simply write [f : ∀α′.∀α.τ].

3.5 Fully explicit type annotations

Considering the inherent difficulties of our semi-implicit elimination scheme, we present a sublanguage where elimination of polymorphism is fully explicit. This highlights the first stage of our proposal, i.e. making polymorphism explicit, while the second stage was dedicated to propagating type information. This sublanguage is theoretically interesting. We do not lose any expressive power by enforcing explicit elimination of polymorphism, i.e. adding an explicit type annotation to all eliminations. Indeed, the encoding of polymorphic data types into polytypes has been done in such a restricted sublanguage. Simultaneously, the restriction to the sublanguage removes the need for labels, and hereby significantly simplifies the type system. The encoding of system F is also possible and as easy in this restricted language. We just have to change the abstraction and type application rules.

\frac{A ⊢ M : ∀α.t′⇒ a}{A ⊢ M t : t′\{t/α\} ⇒ ⟨a: ⟨⟨∀α.t′⟩⟩⟩} \frac{A,x: t ⊢ M : t′⇒ a}{A ⊢ λx:t.M : t → t′⇒ λx.a}

Changing the abstraction rule is not required, but annotating abstractions would be superfluous in this new translation. Notice however that terms encoded in the sublanguage are more verbose. Finally, let us compare terms translated from our system into this restricted system. It looks like we would just have to move annotations from abstraction to elimination nodes, occasionally duplicating them. However, we see two main cases where this gets worse. Firstly, when an annotation contains several polytypes, like will often be the case for objects, we must split the annotation into pieces, and use a different type annotation to eliminate each polytype. Secondly, in our system we did not need any annotation at all for let-defined identifiers. For a complete example, let τ_{1} =^{△} [σ_{1}], τ_{2} =^{△} [σ_{2}], τ_{3} =^{△} [σ_{3}] and τ =^{△} τ_{1} × τ_{2}. Using semi-implicit elimination we can write:

let y = [a: σ_{3}] in λx:τ.(⟨fst x⟩,⟨snd x⟩,⟨a⟩)

but if we had only explicit elimination we would have to write:

let y = [a: σ_{3}] in λx.(⟨fst x: τ_{1}⟩,⟨snd x: τ_{2}⟩,⟨a: τ_{3}⟩)

One could argue that some annotations in the second term are actually smaller than in the first one. We think however, that the number of annotations matters more than their size (which could always be shortened using type abbreviations). In summary, restricting to fully-explicit polymorphism is interesting for its simplicity, but cannot stick syntactically to system F as much as semi-explicit polymorphism allows. It is also less convenient to use than the full system.

4 APPLICATION TO Objective ML

In this section we show how the core language can be used to provide polymorphic methods in Objective ML^{5} [Rémy and Vouillon, 1997]. Polymorphic methods are useful in parameterized classes. Indirectly, they may also reduce the need for explicit coercions. While Objective ML has parameterized classes, it does not allow methods to be polymorphic. For instance, the following class definition fails to type.

 let α collection = class (l)
   val contents = l
   meth mem = λx. mem x contents
   meth fold : (β → α → β) → β → β
             = λf.λx. fold left f x contents
 end

The reason is that variable β is free in the type for method fold and it is not bound to a class parameter. The solution is to have the method fold be polymorphic in β. With polytypes, we can write

 meth fold =
   [λf.λx. fold left f x contents : ∀β. (β → α → β) → β → β]

Still, we have to distinguish between polymorphic and monomorphic methods, in particular when sending a message to the object. The aim of the remainder of this section is to make invocation of polymorphic and monomorphic methods similar and also to make the invocation of polymorphic methods lighter. The first step is to give polytypes to all methods. This is easily done by wrapping monomorphic methods into polytypes. For instance, we shall write

 meth mem = [λx. mem x l : α]

However, we still want to be able to use monomorphic methods without type annotations. There is a small but very convenient extension to the core language that solves this problem. We add a new typing rule Elim-M :

\frac{A ⊢ a: [τ]^{ϵ}}{A ⊢ ⟨a⟩: τ}^{(Elim-M )}

As opposed to rule Elim , this one allows ϵ to appear in A. Inference problems are solved by forcing the polytype to be monomorphic. Both rules Elim and Elim-M apply when ϵ is anonymous and the polytype is monomorphic, but they produce the same derivation. If either ϵ is free in A or the polytype is polymorphic, then only one of the two rules may be used. As a result, principal types are preserved. The type inference algorithm can be modified as shown in figure 5. The subject reduction property is also preserved.

5The examples of objects and classes given below are rather intuitive, and could be translated in other class-based object-oriented languages; the reader shall refer to [Rémy and Vouillon, 1997] for a

Elim let α ∉ F V (A) in if A ▷ a: α −> ∃ξ̄.θ then

if θ(α) = [∀ᾱ′.τ′]^{ϵ} and ϵ ∉ F L(θ(A)) then A ▷ ⟨a⟩: τ −> ∃ξ̄,α,ᾱ′.θ ∧ τ′= τ else if θ(α) = α′and α′ ∉ F V (θ(A)) then A ▷ ⟨a⟩: τ −> ∃ξ̄,α.θ else let ϵ′∉ (F L(A) ∪ F L(τ)) in A ▷ ⟨a⟩: τ −> ∃ξ̄,ϵ′,α.θ ∧ α ≐ [τ]^{ϵ′}

else A ▷ ⟨a⟩: τ −> ⊥

Figure 5: Type inference rule for use of monomorphic polytypes

The expression (λx.λy.⟨x#mem⟩ y) is then typable with principal type ⟨mem : [α → β];..⟩ → α → β. Since all methods are now given polytypes, we shall change our notations (the new notations are given in term of the old ones): in types, we now write m: σ for m: [σ]; in expressions, we now write m: σ = a for m = [a: σ], m = a for m = [a: α], and a#m for ⟨a#m⟩. With the new notations, the collection example is written:

 let α collection = class (l)
   val contents = l
   meth mem = λx. mem x contents
   meth fold : ∀β. (β → α → β) → β → β
             = λf.λx. fold left f x contents
 end;;
 value collection : class α (α list)
   meth mem : α → bool
   meth fold : ∀β. (β → α → β) → β → β
 end

A monomorphic method is used exactly as before.

 let coll mem c x = c#mem x
 coll mem : ⟨mem : α → β; ..⟩ → α → β

However, when polymorphic methods are used under abstractions, the type of the object should be provided as an annotation,

 let simple and double (c : α collection) =
   let l1 = c#fold (λx.λy. x::y) [] in
   let l2 = c#fold (λx.λy. (x,x)::y) [] in
   (l1, l2);;
 simple and double : α collection → (α list * (α * α) list)

Since the method fold is used with two different types, this example could not be typed without first-class polymorphism.

formal presentation of Objective ML, allowing a deeper reading of this section.

Polymorphic methods also appear to be useful to limit the need for explicit coercions. In Objective ML, coercions are explicit. For instance, assume that objects of class point have the interface ⟨x : int;y : int⟩, and that we want to define a class circle with a method giving the distance from the circle to a point.

 let circle = class (x,y,r)  ...
   meth distance = λp:point. ...
 end;;
 value circle : class (int * int * int)  ...
   meth distance : point → float
 end

Given a point p and a circle c, we compute their distance by c#distance p. However, an object cp of a class color point where color point is a subtype of point (e.g. its interface is ⟨x : int;y : int;color : color⟩) needs to be explicitly coerced to point before its distance to the circle can be computed:

 c#distance (cp : color point :> point)

This coercion could be avoided if distance were a toplevel function rather than a method:

 let distance c p = c#distance (p :> point);;
 value distance : ⟨distance : point → α ; ..⟩ → #point → α

The type expression #point represents any subtype of point. Actually, it is an abbreviation for the type ⟨x : int;y : int;ρ⟩. Here, #point contains a hidden row variable that is polymorphic in the function distance. This allows different applications to use different instances of the polymorphic row variable and thus to accept different objects all matching the type of points. Explicit polymorphism allows to recover the same power inside methods:

 meth distance : ∀α:#point. α → float = λp. ...

Then, c#distance cp is typable just by instantiation of these row variables, without explicit coercion. Of course, we must know here that c is a circle before using method distance, like would happen in more classical object-oriented type systems. There is an alternative between using explicit coercions or providing more type information. The advantage of type information is that it occurs at more convenient places. That is, it is necessary in method definitions and at the invocation of a method of an object of unknown type. On the opposite, explicit coercions must be repeated at each invocation of a method even when all types are known.

5 VALUE-ONLY POLYMORPHISM

For impure functional programming languages, value-only polymorphism has become the standard way to handle the ubiquity of side-effects. It preserves typesoundness in the presence of side-effects, without making the type system overly complex. It is based on a very simple idea —if an expression is expansive, i.e. its evaluation may produce side-effects, then its type should not be polymorphic [Wright, 1993]. This is usually incorporated by restricting the Gen rule to a class of expressions b, called non-expansive, composed of variables and functions. Equivalently, this restriction can be put on the Let rule: both ways give exactly the same canonical derivations in the core language. We actually prefer the latter, since we also need rule Gen to precede rules Elim and Intro . Thus, we replace rules Intro and Let by the following four rules, each rule being split in its expansive and non-expansive versions.

\frac{A ⊢ b: σ_{1}  (σ_{1} : σ: σ_{2})}{A ⊢ [b: σ] : [σ_{2}]^{ϵ}}^{(Poly-V )}  \frac{A ⊢ a: τ_{1}  (τ_{1} : τ: τ_{2})}{A ⊢ [a: τ] : [τ_{2}]^{ϵ}}^{(Poly-E )}

(Let-V )

A ⊢ b: ς A,x: ς ⊢ a: τ A ⊢ let x = b in a: τ

(Let-E )

A ⊢ a_{1} : τ′ A,x: τ′⊢ a_{2} : τ A ⊢ let x = a_{1} in a_{2} : τ

The class of non-expansive expressions can be refined, provided the evaluation cannot produce side-effects and preserves non-expansiveness. For instance, in ML, we can consider let-bindings of non-expansive expressions in non-expansive expressions as non-expansive. In our calculus, type annotations are also non-expansive. More generally, any expression where every application is protected (i.e. appears) under an abstraction is non-expansive (creation of mutable data-structure would be the application of a primitive):

b::= x | λx.a | let x = b in b | (b: τ) | [b: σ] | ⟨b⟩

This system works perfectly, and all properties are preserved. However, it seems too weak in practice. Since we use polymorphism of labels to denote confirmation of polytypes, as soon as we let-bind an expansive expression, all its labels become monomorphic, and all its polytypes need an explicit type annotation before they can be eliminated. For instance, the following program is not typable, because labels in the type of the binding occurrence of g cannot be generalized.

let f = [λx.x: ∀α.α → α] inlet g = (λx.x) f in ⟨g⟩ g

When ML polymorphism is restricted to values, the result of an application is monomorphic (here, the result of applying λx.x to f). Traditionally, the typical situation when a polymorphic result is restricted to be monomorphic is partial application. There, polymorphism is easily recoverable by η-expansion. However, the same problem appears when objects are represented as records of methods, with no possibility of η-expansion. In our core language, the only way to recover at least explicit polymorphism in such a case is to annotate the use of let-bound variables with their own types:

let f = [λx.x: ∀α.α → α] inlet g = (λx.x) f in ⟨g: [∀α.α → α]⟩ g In practice, with objects, this means recalling explicit polymorphism information at each method invocation. The strength of our system being its ability to omit such information, its interest would be significantly reduced by this limitation. One might think that allowing quantification on labels in Let-E , i.e. write ∀ϵ̄.τ′in place of τ′, is harmless. Indeed, label polymorphism does not allow type mismatches like usual polymorphism would: verifying identity of polymorphic types is done separately. However, this rule would break principal types. Consider, for instance, the following expression:

 let x = id []inlet y = ⟨hd x⟩ in x

It can be assigned the polytype [σ]^{ϵ} list for any polymorphic type σ. However, the ordering of polymorphic types does not induce a corresponding ordering of polytypes, two polytypes with different polymorphic structure are unordered. Therefore, this expression has no principal type. This problem is pathological, since such patterns will rarely occur. However, it is serious and significant machinery is required to fix it. It can be solved by restricting judgments to minimal ones. That is, we replace Let-V and Let-E by the restricted versions defined below. We write A ⊢^{⋆} a: ς to mean that ς is a minimal type scheme for a under assumptions A. That is, A ⊢ a : ς and there exists no ς′strictly greater than ς in the instantiation order, such that A ⊢ a: ς′. (Since we happen to be keeping principality, ς is the principal type scheme for a under assumptions A.)

(Let-V^{⋆} )
A ⊢^{⋆} b: ς A,x: ς ⊢ a: τ
A ⊢ let x = b in a: τ

(Let-E^{⋆} )

\frac{A ⊢^{⋆} a_{1} : ∀ϵ̄ᾱ.τ′ a_{1} ≢ b A,x: (∀ϵ̄.τ′)\{τ̄/ᾱ\} ⊢ a_{2} : τ}{A ⊢ let x = a_{1} in a_{2} : τ}

The rule Let-E^{⋆} may seem strange, since it is not an instance of the original Let rule, but rather a combination of Inst and Let . The original derivation would have been:

\frac{\frac{\frac{A ⊢ a_{1} : ∀ϵ̄ᾱ.τ′}{⋮}}{A ⊢ a_{1} : ∀ϵ̄.τ′′} A,x: ∀ϵ̄.τ′′⊢ a_{2} : τ}{A ⊢ let x = a_{1} in a_{2} : τ}

The restriction to minimal judgments is not new: it has already been used for the typing of dynamics in ML [Leroy and Mauny, 1991], for instance. One has to reject the program λx.(dynamic x) because, in the principal judgment x: α ⊢ x: α, some variable of the type of x occurs free in the context. A non principal judgment obtained by choosing int for α would be correct, but arbitrary. More recently, it has been used for local type inference in system F_{≤} [Pierce and Turner, 1998].

Type inference is only allowed locally at application nodes, and upon the condition there is a principal solution to the local inference problem. Without this condition, choices made at an application node would influence other nodes, and inference would lose its locality. We use minimality here in a somewhat different way. In the above two systems, requiring a principal solution was a way to have the inference fail on some ambiguous cases. Contrary to dynamics, our types do not need to be ground; they may share variables with the environment. Contrary to local type inference, all our satisfiable inference problems have principal solutions. Thus, our minimality condition never makes a type inference problem fail, but only restricts the set of types that can be assigned to a variable in a let statement. Notice that ⊢^{⋆} judgments do not actually require the derivation to be principal, but only minimal; they do not eliminate all different derivations, but only those that would be obtained by unnecessarily instantiating some types. We may then prove the existence of principal types by showing that all minimal type schemes are equal modulo renaming of bound variables, and as a result our minimality condition happens to be a principality condition. This condition is not harmful when reasoning about derivations: the property of minimality of a derivation is kept by global substitution of free type variables, so that the stability lemma is still valid in the extended system. Still, we do not consider this solution as fully satisfactory, and we view it as an example of the difficulties inherent to value-only polymorphism.

6 RELATED WORK

Full type inference of polymorphic types is undecidable [Wells, 1994]. Several works have studied the problem of partial type inference in system F. Some implementations of languages based on system F relieve the user from the burden of writing all types down. In Cardelli’s implementation of the language Fun [Cardelli, 1993] polymorphic types are marked either as implicit (actually their variables are marked) and they are automatically instantiated when used, or as explicit and they remain polymorphic until they are explicitly instantiated. This mechanism turns out to be quite effective in inferring type applications. However, types of abstracted values are never inferred. Thus, the expression λx.x cannot be typed without providing a type annotation on the variable x, which shows that this is not an extension to ML. Pierce and Turner have extended this partial inference mechanism to F_{≤}^{ω} in the design of the language Pict [Pierce and Turner, 1997b]. By default they also assign “unification variables” to parameters of functions with no type annotations. Their solution requires surprisingly little type information in practice, especially in the absence of subtyping. Still, as for Cardelli’s solution, it is quite difficult to know exactly the set of well-typed programs, since the description is only algorithmic. Conscious of this problem, they more recently proposed to replace this unpredictable approach by one based on predictable local inference [Pierce and Turner, 1998, Pierce and Turner, 1997a]. Their approach is somewhat opposite of ours: while we provide some inference-free type checking without modifying ML type inference, they add some type inference to F_{≤} and keep a checking based system. In their approach, the uniqueness of typing is still valid at every step. As we, they distinguish between the specification and the algorithm of type inference, but this distinction is only limited to one rule, the one doing local inference. This rule has two provably equivalent versions: one is a specification of the inferred type in terms of a universal property; the other one is algorithmic and is presented in a constraint-solving style. The difference of approach and the fact that they also handle subtyping make it difficult to compare the respective strength of the two systems. A different approach is taken by Pfenning [Pfenning, 1988]. Instead of providing type annotations on lambda’s, he indicates possible type applications (this corresponds to the notation ⟨ ⟩ in our language). Then, he shows that partial type inference in system F corresponds to second-order unification and is thus undecidable [Pfenning, 1993]. As in our system, his solution is an extension of ML. His solution is also more powerful than ours; the price is the loss of principal types and decidability of type inference. A decidable subcase of higher-order unification has also been considered in [Dowek et al., 1996]. Neither solution handles subtyping yet. Kfoury and Wells show that type inference could be done for the rank-2 fragment of system F [Kfoury and Wells, 1994]. However, they do not have a notion of principal types. It is also unclear how partial type information could be added. In [Odersky and Läufer, 1996], Läufer and Odersky actually present two different mechanisms. First, as we explained in the introduction they add higher-order polymorphism with fully explicit introduction and elimination. As we have seen in section 3.2, our framework subsumes theirs. They also introduce another mechanism that allows annotations of abstractions by polymorphic types as in λx:σ.x together with a type containment relation on polymorphic types similar to the one of Mitchell [Mitchell, 1984] but with some serious restriction. Polymorphic types may be of the form ∀α.σ_{1} → σ_{2}, where σ_{i} are polymorphic types themselves. However, universal variables such as α can only be substituted by simple types. Thus, the only way to apply a function of type ∀α.α → α to a polymorphic value remains to embed the argument inside an explicitly defined polytype. Actually, one of the reasons for complementing universal-datatype polymorphism by restricted type-containment is to obtain an encoding of system F. In our case, the encoding of system F is permitted by the use of polytypes. In [Duggan, 1995], Duggan proposes an extension to ML with objects and polymorphic methods. His solution heavily relies on the use of kinds and type annotations. These are carried by method names that must be declared before being used. In this regard, his solution is similar to having fully explicit polymorphism both at introduction and elimination, as in [Odersky and Läufer, 1996]. His use of recursive kinds allows some programs that cannot be typed in our proposal (section 4). However, this is due to a different interpretation of object types rather than a stronger treatment of polymorphism.

CONCLUSION

We have presented a conservative extension to ML that allows for first-class polytypes and first-class polymorphic values. In our proposal as in ML, let-polymorphism remains implicit. While first-class polymorphism must be introduced explicitly, type information is inferred at the elimination point. This allows for polymorphic methods in Objective ML, which are particularly useful in parameterized classes. We have also shown that polymorphism can be restricted to values, so as to be sound in the presence of side-effects. This naive standard restriction weakens the propagation of first-class polymorphism, and forces some type annotations, unnecessarily. Thus, we have also proposed an extension that covers all useful cases and does not present any known limitations. Even though the specification of typechecking becomes technically more difficult, since it involves the notion of minimal judgments, the principal-type property is preserved. Although practically insignificant, this difficulty exposes a drawback of the value-only restriction of polymorphism. As future work, three extensions of importance are to be studied. While second order polymorphism is sometimes quite useful for programming, it is not always enough. Indeed, this is only one step further on the scale of abstraction. There are few but serious situations when system F^{ω} is needed to accomplish the desired abstraction. Extending our solution to F^{ω} might be possible, but certainly trickier because of β-reduction at the level of types. Secondly, we should consider applying our technique to existential types. The encoding of these into universal types introduces inner quantifiers, which removes all opportunities for inference. It remains unclear whether primitive existential types could benefit from our work. Thirdly, the replacement of the core ML type system by one with subtyping constraints as in [Aiken and Wimmers, 1993, Eifrig et al., 1995a], would combine first-order generic polymorphism and subtyping polymorphism in an ML-like language. The issues of constraint checking and type generalization are rather orthogonal. However, some recent and more general presentation [Pottier, 1996, Eifrig et al., 1995b] significantly differs from ML. Thus, more investigation is required. The principle of our approach has been to keep within first-order type inference. While we believe this to be sufficient in practice, we would still like to formulate our type system in terms of partial type inference for second-order lambda-calculus.

References

[Aiken and Wimmers, 1993] Aiken, A. and Wimmers, E. L. (1993). Type inclusion constraints and type inference. In Conference on Functional Programming Languages and Computer Architecture, pages 31–41. ACM press.

[Cardelli, 1993] Cardelli, L. (1993). An implementation of FSub. Research Report 97, Digital Equipment Corporation Systems Research Center.

[Damas and Milner, 1982] Damas, L. and Milner, R. (1982). Principal typeschemes for functional programs. In Proceedings of the Ninth ACM Conference on Principles of Programming Langages, pages 207–212.

[Dowek et al., 1996] Dowek, G., Hardin, T., Kirchner, C., and Pfenning, F. (1996). Higher-order unification via explicit substitutions: the case of higher-order patterns. In Maher, M., editor, Joint international conference and symposium on logic programming, pages 259–273.

[Duggan, 1995] Duggan, D. (1995). Polymorphic methods with self types for MLlike languages. Technical report cs-95-03, University of Waterloo.

[Eifrig et al., 1995a] Eifrig, J., Smith, S., and Trifonov, V. (1995a). Sound polymorphic type inference for objects. In OOPSLA.

[Eifrig et al., 1995b] Eifrig, J., Smith, S., and Trifonov, V. (1995b). Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics.

[Garrigue and Rémy, 1997] Garrigue, J. and Rémy, D. (1997). Extending ML with semi-explicit higher-order polymorphism. In Ito, T. and Abadi, M., editors, Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 20–46. Springer-Verlag.

[Huet, 1976] Huet, G. (1976). Résolution d’équations dans les langages d’ordre 1,2,...,ω. Thèse de doctorat d’état, Université Paris 7.

[Jouannaud and Kirchner, 1991] Jouannaud, J.-P. and Kirchner, C. (1991). Solving equations in abstract algebras: a rule-based survey of unification. In Lassez, J.-L. and Plotkin, G., editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257–321. MIT-Press, Cambridge (MA, USA).

[Kfoury and Wells, 1994] Kfoury, A. J. and Wells, J. B. (1994). A direct algorithm for type inference in the rank-2 fragment of the second-order λ-calculus. In Proceedings of the ACM Conference on Lisp and functional programming, pages 196–207, Orlando, Florida.

[Läufer and Odersky, 1994] Läufer, K. and Odersky, M. (1994). Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems, 16(5):1411–1430.

[Leroy and Mauny, 1991] Leroy, X. and Mauny, M. (1991). Dynamics in ML. In Hughes, J., editor, Conference on Functional Programming and Computer Achitecture, volume 523 of Lecture Notes in Computer Science, pages 406–426. Springer-Verlag.

[Mitchell, 1984] Mitchell, J. C. (1984). Polymorphic type inference and containment. In Proceedings of the International Symposium on Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 257–278, Sophia-Antipolis, France. Springer-Verlag. Full version in Information and Computation, 76(2/3):211–249, 1988. Reprinted in Logical Foundations of Functional Programming, ed. G. Huet, pages 153–194, Addison-Wesley, 1990.

[Odersky and Läufer, 1996] Odersky, M. and Läufer, K. (1996). Putting type annotations to work. In Proceedings of the 23rd ACM Conference on Principles of Programming Languages, pages 54–67.

[Pfenning, 1988] Pfenning, F. (1988). Partial polymorphic type inference and higher-order unification. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 153–163, Snowbird, Utah. ACM Press.

[Pfenning, 1993] Pfenning, F. (1993). On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 19(1/2):185–199. Preliminary version available as Technical Report CMU-CS-92-105, School of Computer Science, Carnegie Mellon University, January 1992.

[Pierce and Turner, 1997a] Pierce, B. C. and Turner, D. N. (1997a). Local type argument synthesis with bounded quantification. Technical Report 495, Computer Science Department, Indiana University.

[Pierce and Turner, 1997b] Pierce, B. C. and Turner, D. N. (1997b). Pict: A programming language based on the pi-calculus. Technical report, Computer Science Department, Indiana University.

[Pierce and Turner, 1998] Pierce, B. C. and Turner, D. N. (1998). Local type inference. In Proceedings of the 25th ACM Conference on Principles of Programming Languages. Full version available as Indiana University CSCI Technical Report 493.

[Pottier, 1996] Pottier, F. (1996). Simplifying subtyping constraints. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP ’96), pages 122–133.

[Rémy, 1992] Rémy, D. (1992). Extending ML type system with a sorted equational theory. Research Report 1766, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France.

[Rémy, 1994] Rémy, D. (1994). Programming objects with ML-ART: An extension to ML with abstract and record types. In Hagiya, M. and Mitchell, J. C., editors, Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 321–346. Springer-Verlag.

[Rémy and Vouillon, 1997] Rémy, D. and Vouillon, J. (1997). Objective ML: A simple object-oriented extension to ML. In Proceedings of the 24th ACM Conference on Principles of Programming Languages, pages 40–53. ACM Press.

[Wells, 1994] Wells, J. B. (1994). Typability and type checking in the second order λ-calculus are equivalent and undecidable. In Ninth annual IEEE Symposium on Logic in Computer Science, pages 176–185, Paris, France.

[Wright, 1993] Wright, A. K. (1993). Polymorphism for imperative languages without imperative types. Technical Report 93–200, Rice University.

A PROOFS OF MAIN THEOREMS

Lemmas 1 (canonical derivations) and 2 (stability by substitution) are tedious but essential in ML. Their proofs easily carry over with the three new rules, Ann , Intro , and Elim .

Proof of type soundness for the core language

Lemma 4 (Term substitution) If A,x : σ_{2} ⊢ a : σ_{1} and A ⊢ b : σ_{2} hold, then A ⊢ a{b/x}: σ_{1} also holds.

\underline{Proof}: The proof is by induction on the structure of the first derivation.

Theorem 1 (Subject reduction) Reduction preserves typings, i.e. if a_{1} −→ a_{2}, then a_{1} ⊂ a_{2}.

\underline{Proof}: We show that every rule in the definition of −→ is satisfied by the relation ⊂. Since −→ is the smallest relation verifying those rules, then ⊂ must be a superrelation of −→ . All cases are independent. In each case but Context , we assume that A ⊢ a_{1} : ς (1) and that a_{1} −→ a_{2}, (the structure of a_{1} depending on the case) and we show that A ⊢ a_{2} : ς (2). We first assume that the derivation does not end with a rule Gen . If the derivation ends with a rule Gen , it is of the form:

Δ ; A ⊢ a_{1} : ς_{0} ; \overline{(Gen* )} ; A ⊢ a_{1} : ∀ξ̄.ς_{0}

where the derivation Δ of (1) does not end with a rule Gen . Thus we have A ⊢ a_{2} : ς_{0} and (2) follows by the same sequence of generalizations.

Case Fun and Let : This is a straightforward application of term-substitution lemma.

Case Elim : A canonical derivation of (1) ends with

A ⊢ a: σ_{1} (σ_{1} : σ_{0} : σ_{2}) \overline{(Intro )}

A ⊢ [a: σ_{0}] : [σ_{2}]^{ϵ} \overline{(Gen )}

A ⊢ [a: σ_{0}] : ∀ϵ.[σ_{2}]^{ϵ} \overline{(Elim )}

A ⊢ ⟨[a: σ_{0}]⟩: σ_{2} The polymorphic types σ_{1}, σ_{0}, and σ_{2} are of the form ∀ᾱ.τ_{1}, ∀ᾱ.τ_{0}, and ∀ᾱ.τ_{2}, and such that (τ_{1} : τ_{0} : τ_{2}). Choosing variables ᾱ that do not occur free in A, we can contract this derivation into the following derivation of (2):

A ⊢ a: σ_{1} ; \overline{(Inst* )} ; A ⊢ a: τ_{1} (τ_{1} : τ_{0} : τ_{2}) \overline{(Ann )}

A ⊢ (a: τ_{0}) : τ_{2} \overline{(Gen* )}

A ⊢ (a: τ_{0}) : σ_{2}

Case Tfun : A canonical derivation of A ⊢ a_{1} : σ ends with

A ⊢ a: τ′_{2} → τ′_{1} (τ′_{2} → τ′_{1} : τ_{2} → τ_{1} : τ′′_{2}→ τ′′_{1}) (3) ; \overline{(Ann )} ; A ⊢ (a: τ_{2} → τ_{1}) : τ′′_{2}→ τ′′_{1} A ⊢ b: τ′′_{2} \overline{(App)}

A ⊢ (a: τ_{2} → τ_{1}) b: τ′′_{1}

Since the relation (3) implies both (τ′′_{2}: τ_{2} : τ′_{2}) and (τ′_{1} : τ_{1} : τ′′_{1}), we can build the derivation:

A ⊢ a: τ′_{2} → τ′_{1}  A ⊢ b: τ′′_{2} (τ′′_{2}: τ_{2} : τ′_{2}) ; \overline{(Ann )} ; A ⊢ (b: τ_{2}) : τ′_{2} ; \overline{(App)} ; A ⊢ a (b: τ_{2}) : τ′_{1} (τ′_{1} : τ_{1} : τ′′_{1}) \overline{(Ann )}
A ⊢ (a (b: τ_{2}) : τ_{1}) : τ′′_{1}

Case Tint : The last derivation of (1) ends with:

A ⊢ a: σ′_{1} (3) (σ′_{1} : σ_{1} : σ′′_{1}) (4) ; \overline{(Intro )} ; A ⊢ [a: σ_{1}] : [σ′′_{1}]^{ϵ_{1}} ([σ′′_{1}]^{ϵ_{1}} : [σ_{2}]^{ϵ_{2}} : [σ_{3}]^{ϵ_{3}}) (5) \overline{(Ann )}

A ⊢ ([a: σ_{1}] : [σ_{2}]^{ϵ_{2}}) : [σ_{3}]^{ϵ_{3}}

Let ∀ᾱ.τ_{1} be σ_{1}. From (4), we know that we can write σ′_{1} and σ′′_{1}as ∀ᾱ.τ′_{1} and ∀ᾱ.τ′′_{1}. Moreover, we have (τ′_{1} : τ_{1} : τ′′_{1}). From (5), we also get (σ′′_{1}: σ_{2} : σ_{3}). Thus, we have

\begin{matrix}(3) \\ & (Inst* ) \\ A ⊢ a: τ′_{1} \end{matrix} (τ′_{1} : τ_{1} : τ′′_{1}) \overline{(Ann )} \begin{aligned}A ⊢ (a: τ_{1}) : τ′′_{1} \\ & (Gen* ) \\ A ⊢ (a: τ_{1}) : σ′′_{1} \end{aligned} (σ′′_{1}: σ_{2} : σ_{3}) \overline{(Intro )}

A ⊢ [(a: τ_{1}) : σ_{2}] : [σ_{3}]^{ϵ_{3}}

Case Tvar : Annotating with a type variable does nothing.

Case Context : Here, we need to show that if a_{1} ⊂ a_{2} then for any evaluation context E we also have E{a_{1}} ⊂ E{a_{2}}. The proof, which we can directly take from usual ML, is by structural induction on E.

Theorem 2 (Canonical forms) Irreducible programs (for call-by-value reduction) that are well-typed in the empty environment are values.

\underline{Proof}: We first relate the shape of types and the shape of values. Let v be a value of type τ. By considering all possible canonical derivations, we see that:

• if v is a poly expression, possibly with a type constraint, then τ is a polytype;

• otherwise, v is of the form w and τ is a functional type.

Since polytypes and functional types are incompatible, we can invert the property:

• if τ is a polytype, then v is a poly expression, possibly with a typed constraint.

• otherwise, τ is a functional type, and v is of the form w.

Then, the theorem follows: considering a program a that is well-typed in the empty environment and that cannot be reduced, it can easily be shown by structural induction that a is a value.

Proof of the principal type property

Lemma 5 (Unification) Each of the rules given in figures 2 and 3, is correct and complete.

\underline{Proof}:

Cases Occur-Check , Merge , Absorb , and Decompose : those are standard rules for first-order unification.

Case Decompose-Poly and Clash : immediate.

Case Polytypes : This case amounts to fully formalizing the discussion in section 2.4. Assume that ᾱ∩ ᾱ′, ᾱ∩ F V (τ′), and ᾱ′∩ F V (τ) are all empty (1). Soundness: Assume that θ is a solution of ∃ᾱᾱ′.τ ≐ τ′∧ ᾱ ↔ ᾱ′. Let η be a renaming of ᾱᾱ′ into variables outside of free variables of θ, τ, τ′, and ᾱᾱ′. The substitution η ∘ θ is also a solution of the same unificand. Since its image has no variable in common with ᾱᾱ′, the substitution η ∘ θ \ ᾱᾱ′ can be extended by a substitution ρ of domain ᾱᾱ′ such that the substitution θ′equal to η ∘ θ \ ᾱᾱ′+ ρ is a solution of τ ≐ τ′∧ ᾱ ↔ ᾱ′. Since θ′is a solution of ᾱ ↔ τ̄′, the substitution ρ is injective on ᾱ and ᾱ′ taken separately. Moreover, its image is in ᾱᾱ′. The substitution (η+η^{−1} )∘θ′decomposes as (θ\ᾱᾱ′)+(η∘ρ), which is actually equal to θ ∘ η ∘ ρ; it must be a solution of τ ≐ τ′. Therefore the substitution θ is a solution

of ∀ᾱ.τ =^{∀} ∀ᾱ′.τ′.

Completeness: Let θ be a solution of ∀ᾱ.τ =^{∀} ∀ᾱ′.τ′. Reusing the reasoning and the definitions of section 2.4, the substitution (η ∘ θ \ ᾱᾱ′) + ρ is a solution of τ ≐ τ′∧ ᾱ ↔ ᾱ′ where η is a renaming of ᾱᾱ′ into variables taken outside of free variables of θ, τ, τ′, and ᾱᾱ′. Thus, η ∘ θ is a solution of ∃ᾱᾱ′.τ ≐ τ′∧ ᾱ ↔ ᾱ′ and so is θ by composition with η^{−1} .

Case Renaming-True : The completeness is obvious. For the soundness, let θ be any substitution. Let η be a renaming of ᾱᾱ′ outside of ᾱᾱ′ and free variables of θ. The substitution (η ∘ θ) \ ᾱᾱ′ can be extended with the substitution (α_{i} ↦ α′_{i})^{i∈1..n}. Clearly, this extension satisfies both (α_{i} ≐ α′_{i})^{i∈1..n} and ᾱ ↔ ᾱ′. Thus θ is a solution of ∃ᾱᾱ′.(α_{i} ≐ α′_{i})^{i∈1..n} ∧ ᾱ ↔ ᾱ′.

Case Renaming-False : The soundness is obvious. For the completeness let us consider the two following cases: β ∈ ᾱ and τ ∉ ᾱ′∪ {β}: Assume that there exists a solution θ of both β ≐ τ ≐ e and ᾱ ↔ ᾱ′. Since θ(τ) is equal to θ(β), it must be a variable, and so should τ itself. Since θ \ ᾱᾱ′ should not have variables in common with ᾱᾱ′, τ must be in ᾱᾱ′. However, since it is not in ᾱ′, it must be another variable γ of ᾱ distinct from β, which contradicts with the fact that θ |`ᾱ must be injective (condition 2). β ∈ ᾱ ∩ F V (τ) and τ ≠ β: In particular, τ must be a proper term. Assume that there exists a solution θ of both γ ≐ τ ≐ e and ᾱ ↔ ᾱ′. The term θ(γ), equal to θ(τ), is a proper term; thus, γ cannot be a variable of ᾱᾱ′. However, θ(γ) contains the variable θ(β) that belongs to ᾱᾱ′. This contradicts condition 3.

Theorem 4 Given a typing problem (A ▷ a : τ) there exists a principal solution, which is computed by the set of rules described in figures 2, 3 and 4, or there is no solution and the problem reduces to ⊥.

\underline{Proof}: We first show the soundness and completeness of each rewriting rule:

Cases Var , Fun , App, and Let : are as in ML.

Case Ann : The case Ann is not special since the construct ( : τ) could be treated as the application of a primitive.

Case Intro : We assume that all the conditions of the first four lines are satisfied. We write σ_{i} for σ{ᾱ_{1} ϵ̄_{i}/ᾱ_{0} ϵ̄_{0}}. Soundness: Let us assume that A ⊢ a : τ_{1}{ϵ̄_{1}/ϵ̄_{0}} −> ∃ξ.θ and ᾱ ∩ dom(θ) ∪ F V (codom(θ)) = ∅. We have θ(A) ⊢ a: θ(σ_{1}) by generalization of ᾱ in the judgment θ(A) ⊢ a : θ(τ_{1}{ϵ̄_{1}/ϵ̄_{0}}). Since by construction (θ(σ_{1}) : σ : θ(σ_{2})), we also have θ(A) ⊢ [a : σ] : θ([σ_{2}]^{ϵ}). That is, θ is a solution of A ⊢ [a : σ] : [σ_{2}]^{ϵ}. Thus, a solution of θ ∧ τ = [σ_{2}]^{ϵ} is a solution of A ⊢ [a: σ] : τ. Moreover, no variable of ϵ̄_{1},ϵ̄_{2},ϵ,ᾱ_{1} appears in A or τ.

Completeness: Let us assume that θ′is a solution of A ▷ [a : σ] : τ. A canonical derivation of θ′(A) ⊢ [a : σ] : θ′(τ) must end with rule Intro . Thus, there exists some polymorphic types σ′_{1} and σ′_{2} and some label ϵ such that θ′(A) ⊢ a : σ′_{1} (1), (σ′_{1} : σ: σ′_{2}) (2), and θ′(τ) = [σ′_{2}]^{ϵ} (3). By definition of the relation ( : σ: ) the pair (σ′_{1},σ′_{2}) must be of the form (θ′′(σ_{1}),θ′′(σ_{2})) for some substitution θ′′of domain ϵ̄_{1}ϵ̄_{2}ᾱ_{0}. A canonical derivation of (1) must end with a succession of rules Gen . Thus we have θ′(A) ⊢ a: θ′′(τ_{1}{ϵ̄_{1}/ϵ̄_{0}}). On the one hand, the substitution θ′+ θ′′ is a solution of A ⊢ a : τ_{1}{ϵ̄_{1}/ϵ̄_{0}}, and consequently a solution of θ. On the other hand, it is a solution of τ = [τ_{1}{ϵ̄_{2}/ϵ̄_{0}}]^{ϵ}. Moreover, it extends θ′on ᾱ_{0}, ϵ̄_{0}, ϵ̄_{1}, ϵ, and ξ̄. The completeness of the else branch is straightforward; The proof above actually applies if θ is ⊥. If θ is not ⊥, the right condition may always be satisfied since ᾱ is disjoint from free variables of the typing problem.

Case Elim : We assume that the condition of the first line is satisfied. Soundness: If θ(α) = [∀ᾱ′.τ′]^{ϵ} and ϵ ∉ F L(θ(A)) then rule Elim applies, and an extension of θ such that θ(τ) = θ(τ′) is a solution of A ▷ ⟨a⟩: τ. If θ(α) = α′and α′ ∉ F V (θ(A)) then from θ(A) ⊢ a: α′we deduce θ(A) ⊢ a: [τ]^{ϵ} for some ϵ not in F V (θ(A)). By generalization of ϵ and rule Elim , we get θ(A) ⊢ ⟨a⟩ : θ(τ). The substitution θ is thus a solution of A ▷ ⟨a⟩: τ. Completeness: Let us assume that θ′ is a solution of A ⊢ ⟨a⟩ : τ. The canonical derivation of θ′(A) ⊢ ⟨a⟩ : θ′(τ) must end with rule Elim . Thus, we must have θ′(A) ▷ a : [σ]^{ϵ′} for some ϵ′ that does not appear in θ′(A) and some polymorphic type σ of which θ′(τ) is an instance. Since ∃ξ̄.θ is a principal solution of A ▷ a: α, θ′can be extended on ξ̄ into a solution of θ ∧ θ(α) ≐ [σ]^{ϵ′}(1). Therefore θ(α) cannot be an arrow type. If it is a variable, then it cannot belong to θ(A), otherwise ϵ′would belong to θ′(A). Hence, together with (1) the completeness of the second and third cases. If θ(α) = [∀ᾱ′.τ′]^{ϵ} then ϵ cannot belong to F L(θ(A)), otherwise ϵ′would belong to F L(θ′(A)). Since θ′ is a solution of [σ]^{ϵ′} ≐ [∀ᾱ′.τ′]^{ϵ}, it is also a solution of σ = ∀ᾱ′.τ. Since θ′(τ) is an instance of σ, it is an instance of ∀ᾱ′.τ. Thus θ′can be extended on ᾱ′ into a solution of τ = τ′. Together with (1), θ′ is a solution of θ ∧ τ = τ′.

Termination: We now show that applying the rules in any order always terminates, with a unification problem in solved form. Each rule of the algorithm decreases of the lexicographic ordering composed of successively

1. the sum of sizes of program components,

2. the sum of monomials X^{size(σ)} for all type and polymorphic type components of the system,

3. the number of polymorphic constraints, 4. the number of multi-equations,

5. the sum of the lengths of multi-equations, and

6. the number of renaming problems.

Moreover, unification problems that cannot be reduced are in solved form. Clearly, there cannot remain any typing problem since for each construction of the language some rule applies. Similarly, polytypes can always be decomposed. Let us consider a renaming problem ᾱ ↔ ᾱ′ for which rule Renaming-False would not apply. Then variables of ᾱᾱ′ could only appear in multi-equations composed of the variables in ᾱᾱ′. Moreover at most one variable of each set ᾱ and ᾱ′ could appear in each of these multi-equations. Therefore rule Renaming-True would apply. The remaining rules are standard rules for unification for simple types.