Extending ML with Semi-Explicit Higher-Order Polymorphism

Jacques Garrigue^{1} and Didier Rémy^{2}

1 Kyoto University Research Institute for Mathematical Sciences, Kitashirakawa-Oiwakecho, Sakyo-ku, Kyoto 606-01, Japan 2 INRIA-Rocquencourt, BP 105, 78153 Le Chesnay Cedex, France

Abstract. We propose a modest conservative extension to ML that allows semi-explicit higher-order polymorphism while preserving the essential properties of ML. In our proposal, the introduction of polymorphic types remains fully explicit, that is, both the introduction and the exact polymorphic type must be specified. However, the elimination of polymorphic types is now semi-implicit: only the elimination itself must be specified as the polymorphic type is inferred. This extension is particularly useful in Objective ML where polymorphism replaces subtyping.

Introduction

The success of the ML language is due to its combination of several attractive features. Undoubtedly, the polymorphism of ML [2] —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, it returns a principal type.

Upon 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.

There are of course cases where one would like to have higher-order polymorphism, as in system F. ML allows for polymorphic definitions, but abstractions can only be monomorphic. Traditionally, ML polymorphism is used for definitions of higher-order 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 cases that appear 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 parametric in 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 [6, 14] 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 so that the abstract representation of y is not revealed outside the scope of the open construct.

First-class polymorphic values have been proposed in [14, 9] following the ideas developed by Laüfer & Odersky in [6]. After de-sugaring, these proposals all 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 suffer the same problem: types must be written explicitly, both at the introduction and elimination of polymorphism.

Recent results on the undecidability of type inference for system F [16, 5, 11] also 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. On the contrary, we do not infer higherorder types and avoid higher-order unification, undecidable in general. We also 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 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 have already known types. This information only longs to be used appropriately.

In comparison to previous works, we remove the need for type annotations at the elimination of polymorphism, using type inference to propagate explicit type information between different points of the program. In our proposal, it becomes unnecessary to tag values of polymorphic types with type symbols. 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. In the next section, we present two extensions to the core language. The first extension restricts polymorphism to values. The second one allows a more comfortable syntax to manipulate objects with polymorphic methods.

Lastly, we compare with related works, and conclude. Proofs of main theorems are given in appendix.

1 Informal approach

In this section we will present our solution informally. We first present a naive straightforward proposal. We show that this solution needs to be restricted to avoid higher-order unification. Last, we describe a simple solution that allows for complete type inference.

1.1 A naive solution

Naively, ML types can be easily extended with polymorphic types. A typical program that cannot be typed in ML and could be typed in system F is λf. ff. This expression is not very interesting for itself. However, a few variations are sufficient to illustrate most aspects of type inference in the presence of higherorder types. Useful examples can be found in section 4.2 in addition to those suggested in the introduction.

Although λf. ff is not typable in ML, the expression let f = λx. x in f f is. One can see let-definitions as a special syntax, combined with a special typing rule, for the application (λf. ff) (λx. x). Let us exercise by replacing the Let polymorphic binding by first-class polymorphism. The identity λx. x of type α → α has also type scheme ∀α.α → α. We shall write [λx. x : ∀α.α → α] for the creation (or introduction) of the polymorphic value λx. x with type scheme ∀α.α → α. In order to avoid confusion with ML types, we explicitly coerce ∀α.α → α to a regular ML type [∀α.α → α], adding the type constructor [ ]. We call ∀α.α → α a polymorphic type or a type scheme and [∀α.α → α] a polytype.

Let f be the expression [λx. x : ∀α.α → α], which has type [∀α.α → α]. As any first-class value, f can be passed to other functions, be stored in datastructures, etc. For instance (f, 1) is a pair of type ([∀α.α → α]× int). A polymorphic function (e.g. a polymorphic value that is a 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, ⟨f⟩ is a function of type an instance of the polymorphic type ∀α.α → α, i.e. τ → τ for some type τ. Its principal type is α → α.

The raw expression λf. ff is not well typed. It should be passed a polymorphic value as argument, for instance, of type [∀α.α → α]. Here, we shall introduce polymorphism only 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 of g is well-typed

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

So are the two following variants:

{h =^{△} λf: [∀α.α → α]. ⟨f⟩ ⟨f⟩ : [∀α.α → α] → α′ → α′ \atop k =^{△} λf: [∀α.α → α]. [⟨f⟩ ⟨f⟩ : ∀α.α → α] : [∀α.α → α] → [∀α.α → α]}

In h, the occurrence of f in the argument position is also opened, so the result type is no longer a polytype. In k, polymorphism is lost as in h, then it is recovered explicitly. Finally, we can apply g to f:

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

More interestingly, the following expression is also well-typed

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

There is no term typable in ML that has the same erasure (untyped λ-term) as the above term. Note that no type annotation is needed on g since although g has a polytype as result, it is never opened.

1.2 An obvious problem

The examples above mixed type-inference and type-checking (using type-annota-tions). 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 typed?

The answer is clearly negative, since this would amount to inferring higherorder types, which we choose to avoid here. We should keep all user-provided polymorphism, but never guess polymorphism.

The attempt to forbid lambda abstraction of unspecified type to be a polytype does not work. It would violate the assumption that polytypes are regular ML types. Thus, if λx. x has type α → α, it should also have type [σ] → [σ] for any polymorphic type σ. Actually, it is important that λx. x has all these types. For instance, both (λx. x) f and λx. f x should be typable and have the same type as f.

When typing λf. ⟨f⟩ f, variable f is first given an unknown type α′. Guessing ∀α.α → α for α′ would be correct, but not principal. More subtle, the expression λf. ⟨f⟩ (g f) may only be typed with [∀α.α → α] → [∀α.α → α] and has a principal derivation. However, we should 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 application g f 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, and we would rather fail in every case where some inference order would fail. More theoretically, constraints imported from other branches may disappear whenever a reduction occurs on the expression containing them, making the term untypable by lack of principality. We would loose the subject reduction property.

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 ϵ. That is, we write [σ]^{ϵ} rather than [σ]. Actually, we keep [σ] as an abbreviation for [σ]^{ϵ} where ϵ is an anonymous label, i.e. one that does not appear anywhere else. Intuitively, labels indicate sharing of polytype nodes.

The elimination of polymorphism ⟨a⟩ is possible whenever a can be typed with [σ]^{ϵ} where ϵ does not appear anywhere else. Informally, we could just say when a has polytype [σ] (since ϵ is anonymous). The intuition is that an anonymous label ϵ ensures that the corresponding polytype does not appear anywhere else and a fortiori does not appear as an hypothesis (i.e. in a negative occurrence, such as the context or the left hand-side of an arrow); thus, it must have been user-provided.

For instance, in the expression λf. ⟨f⟩ f, the lambda-bound variable f can be given the polytype [∀α.α → α]^{ϵ}, with a monomorphic ϵ; since all instances of f will share the same label ϵ, the label cannot be anonymous as required when typing ⟨f⟩. Indeed, the type of the variable f in ⟨f⟩ is a polytype only under the assumption that the binding occurrence of f is typed with exactly the same polytype.

On the contrary, when a polytype has been confirmed, we want to propagate it, following the definition order. We use polymorphism to generate new anonymous labels from older ones. We allow quantification on anonymous labels, and later instantiation of quantified labels to new anonymous labels.

When typing the expression λf: [∀α.α → α]. ⟨f⟩ f, the type assumption f : ∀ϵ.[∀α.α → α]^{ϵ} is added to the context in which ⟨f⟩ f is typed. Thus, variable f has type [∀α.α → α]^{ϵ_{1}} with a different, anonymous, label ϵ_{1}, and therefore ⟨f⟩ is well-typed. For technical reasons we chose not to allow type annotation of abstracted variables in our system, but instead λx: τ. a can be seen as λx. let x = (x : τ) in a. Type annotation ( : τ) renames all ϵ’s free in τ into fresh ones.

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:

τ ::= α | τ → τ | [σ]^{ϵ}  Monotypes
σ ::= τ | ∀α.σ  Type schemes
ς ::= σ | ∀ϵ.ς  Generic schemes
ξ ::= α | ϵ  Variables

The construct [σ]^{ϵ} is used to coerce a type scheme σ to a monotype. We call [σ]^{ϵ} a weak polytype. The label ϵ is used to keep track of sharing between weak polytypes, or allow them to be usable polytypes, when it is quantified as ∀ϵ.[σ]^{ϵ}. We do not quantify labels in σ, since this would not add any power to the system (it would be redundant with explicit type annotations).

Free type variables and free labels of a generic scheme, type scheme, or monotype ς are written F V (ς) and F L(ς), and are defined as usual. In a type scheme ∀ξ.ς, ∀ acts as a quantifier, and the variable or label ξ is bound (i.e. not free) in ∀ξ.ς. We consider type schemes equal by renaming of bound variables and labels. As usual substitutions leave bound variables and labels unchanged. For example (α → [∀α′.α′ → α]^{ϵ}){τ/α} is τ → [∀α′.α′ → τ]^{ϵ} provided α′ is not free in τ. An instance of a type scheme ∀ϵ̄, ᾱ.τ_{0} is τ{ϵ̄′, τ̄/ϵ̄, ᾱ}.

Expressions

\begin{matrix}a ::= & x | λx. a | a a | let x = a in a \\ | & [a : σ] | ⟨a⟩ | (a : τ) \end{matrix}

The first line corresponds exactly to core ML. We then introduce three new constructs: introduction and elimination of first-class polymorphism and type annotation.

Typing rules are given in figure 1. All typing rules but the last three ones are

\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)

\frac{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}]^{ϵ}}^{(Poly)}

\frac{A ⊢ a : ∀ϵ.[σ]^{ϵ}}{A ⊢ ⟨a⟩ : σ}^{(Use)}

Fig. 1. Typing rules

quite standard. Rules Ann and Poly use an auxiliary relation ( : : ). Given a type scheme σ, we write (σ_{1} : σ : σ_{2}) if there exists a substitution θ from type variables to 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}(σ)). If σ does not contain any label, then (σ_{1} : σ : σ_{2}) is equivalent to σ_{1} and σ_{2} being the same generic instance of σ. An important property of the relation ( : σ : ) is its stability by substitution. That is, if (σ_{1} : σ : σ_{2}), then (θ(σ_{1}) : σ : θ(σ_{2})) for any substitution θ.

This relation is used to type explicit annotations. The construct ( : τ) could have been replaced by a countable collection of primitives λx. (x : τ) indexed by τ and given with principal type schemes ∀ϵ̄_{1}, ϵ̄_{2}, F V (τ). τ{ϵ̄_{1}/ϵ̄} → τ{ϵ̄_{2}/ϵ̄} where ϵ̄_{1} and ϵ̄_{2} are different renamings of the labels ϵ̄. That is, to type an expression (a : τ), let τ_{1} and τ_{2} be two copies of τ where labels have been been renamed, and θ be a substitution such that a has type θ(τ_{1}); then (a : τ) has type θ(τ_{2}).

Rule Poly uses the same relation, except that types schemes replace types. To type [a : σ], let σ_{1} and σ_{2} be two copies of σ where labels have been been renamed; find a generic instance σ′ of the principal type scheme of a and a substitution θ such that θ(σ′) and θ(σ_{1}) are equal, and return [θ(σ_{2})]^{ϵ}.

Last, rule Use 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}} \overline{(Use)}

A ⊢ ⟨f : [σ]^{ϵ}⟩ : ∀α.α → α \overline{(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 call-by-value semantics for the core language. Values and evaluations contexts are:

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

One step is either a reduction of the form:

(λx. a) v ⟶^{Fun} a{v/x}
let x = v in a ⟶^{Let} a{v/x}
⟨[v : ∀ᾱ.τ]⟩ ⟶^{Use} (v : τ)
(v_{1} : τ_{2} → τ_{1}) v_{2} ⟶^{Tfun} (v_{1} (v_{2} : τ_{2}) : τ_{1})
([v : ∀ξ̄.τ] : [σ]^{ϵ}) ⟶^{Tpol} [(v : τ) : σ]
(v : α) ⟶^{Tvar} v

or an inner reduction obtained by induction:

\frac{a_{1} ⟶^{r} a_{2}}{E\{a_{1}\} ⟶^{r} E\{a_{2}\}}

Note that α, in rule Tvar, is really a variable and not a meta-variable. 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 only reduced by rules Fun, Let, and Use, we need the rules Tfun and Tpol to maintain this type information. Rule Tvar erases empty 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 E, and to show that if a_{1} ⟶ a_{2}, then (E(a_{1}) ⟹ E(a_{2})) or E(a_{1}) and E(a_{2}) are equal.

2.3 Type soundness

We could easily show that evaluation cannot go wrong by means of translation in system F. Subject reduction is an intermediate result of a 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 extension to polytypes: the new constructions allow more programs to be typed, but simultaneously the reduction of those expressions requires more programs to be typable. 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.

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 Poly, Use, the left premise of rule Let, or another rule Gen.

– rule Inst may only occur right after rule Tvar, rule Use, or another rule Inst.

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

Another classical 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.

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} : ς)

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 preserve from type errors. It must be complemented by the following result:

Theorem 2 (Canonical forms). Irreducible programs that are well-typed in the empty environment are values.

Type soundness is a straightforward combination of the two previous theorems.

2.4 Type inference

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. We present both unification and type inference as solving unification constraints following [4].

Unification on simple types First, we remind unification for simple types. In this part we exclude polytypes from types τ. A unification problem 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 unsatisfiable and trivial unification problems. We treat them as a unit and a zero for ∧. That is U ∧⊤ and U ∧⊥ are respective equal to U and ⊥. We also identify ⊤ with singleton multi-equations. That is, we can always consider that unification problems U contain at least one multi-equation α ˙= 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 ∃ 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. Thats is, multiequations are in fact multi-sets of terms.

A substitution θ is a solution of a multi-equation if it sends all terms of the multi-equation to the same image. 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.

Two unification problems are equivalent if they have the same set of solutions. One can check that all previous structural equalities are indeed equivalences.

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 term that contains α′. A unification problem is strict if ≺_{U} is strict. Remark that strictness is syntactic and is not preserved by equivalence. The idea is that strictness detects cycles, only on fully merged and decomposed unification problems.

A problem is in solved form if it is either ⊥ or ⊤, or if it is strict and of the form ∃ ᾱ. ⋀_{i∈1..n} e_{i}, merged and decomposed. In particular, multi-equations e_{i} contain at most one non-variable term, and if i ≠ j then e_{i} and e_{j} contain no variable term in common. An explicit principal solution θ can be read straightforwardly from a problem in solved form. We 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 ⊥.

Occur-Check if≺_{U} is not strict then U − > ⊥

Merge

α ˙= e ∧ α ˙= e′ − > α ˙= e ˙= e′ Absorb

α ˙= α ˙= e − > α ˙= e Decompose

τ_{1} → τ_{2} ˙= τ′_{1} → τ′_{2} ˙= e − > τ_{1} → τ_{2} ˙= e ∧ τ_{1} ˙= τ′_{1} ∧ τ_{2} ˙= τ′_{2}

Fig. 2. First-order unification of simple types

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 formulas by rewriting any sub-formula. 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 with polytypes We now allow polytypes [σ]^{ϵ}. The rule Decompose is naturally extended by adding a case for polytypes. Thus we have to extend typing problems with equations between type schemes.

U ::= … | σ ˙= σ

Notice that these are not multi-equations, since a variable cannot be equated to a polymorphic type scheme, and as a result equations involving type schemes are never merged.

Decompose

[σ]^{ϵ} ˙= [σ′]^{ϵ′} ˙= e − > [σ]^{ϵ} ˙= e ∧ ϵ ˙= ϵ′ ∧ σ ˙= σ′ Clash

[σ]^{ϵ} ˙= τ → τ′ ˙= e′ − > ⊥ Polytypes

if ᾱ ∩ ᾱ′ = ∅ then

∀ᾱ.τ ˙= ∀ᾱ′.τ′ − > ∃ ᾱ, ᾱ′. τ ˙= τ′ ∧ ᾱ ↔ ᾱ′

Renaming-True if ᾱ = (α_{i})^{i∈1..n+p} and ᾱ′ = (α′_{i})^{i∈1..n+q} then

∃ ᾱ, ᾱ′. (α_{i} ˙= α′_{i})^{i∈1..n} ∧ ᾱ ↔ ᾱ′ − > ⊤

Renaming-False if β ∈ ᾱ and τ ∉ ᾱ′ ∪ {β} then β ˙= τ ˙= e ∧ ᾱ ↔ ᾱ′ − > ⊥

if β ∈ ᾱ ∩ F V (τ) and τ ≠ β then β′ ˙= τ ˙= e ∧ ᾱ ↔ ᾱ′ − > ⊥

Fig. 3. First-order unification of simple types with polytypes

A substitution θ is solution of a polytype equation σ ˙= σ′ if θ(σ) = θ(σ′), where equality is the usual equality for type schemes in ML, i.e. it is taken modulo reordering and renaming of universal variables, and removal of useless universal variables. Clearly, ∀ᾱ.τ = ∀ᾱ′.τ′ if and only if there exists a substitution θ such that

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

2. θ | ` ᾱ and θ |` ᾱ′ are injective in ᾱ ∪ ᾱ′, and

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

We could have solved such unification problems by first unifying τ and τ′ and then checking the constraints. However, this would force some unnecessary dependence. Indeed, the condition 1 above can be treated as a unification problem θ. We introduce another kind of unificands ᾱ ↔ ᾱ′ whose solutions are substitutions satisfying the conditions 2 and 3. We consider ᾱ and ᾱ′ as multisets (i.e. the comma is associative and commutative). In order to avoid special cases, we require that no variable is listed twice in the sequence ᾱ, ᾱ′ (in particular ᾱ ∩ ᾱ′ is empty). The symbols ˙= (in polytype equations) and ↔ are commutative.

Rules for unification with polytypes are those of figure 2 plus those of figure 3. Rule Clash handles type incompatibilities. Rule Polytypes transforms polytype equations as described above. Rule Renaming-True allows to remove a satisfiable renaming constraints that became independent. 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 -False applies. Therefore, renaming constraints can always be eliminated.

Type inference For type inference, we extend atomic formulas 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 substitutions. Thus, typing problems can be treated as unification problems, following [13]. 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.

Theorem 3. 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.

2.5 Printing labels as sharing constraints

We propose here an alternative interface to the system, potentially enhancing readability of types shown to the user. It is robust, and could also have been used in the presentation of our type system.

Labels are used to trace the sharing of polytypes. Types could be restricted so that two polytypes with the same label are necessarily equal. This was not required in the present type system, although this property remains valid in all types appearing in a principal derivation of a judgment for which the property is already valid.

The grammar of types can be extended with a sharing construct^{1}:

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

Using bindings, 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

1 Alternatively, 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.

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 existing in the solved form. Actually, only sharing involving polytypes needs to be printed, and other sharing could still be ignored as before.

For instance, the expression λx. (x : [σ]) has type [σ] → [σ], since the two polytypes have different labels, but the expression λx. let y = (x : [σ]) in x has type (α → α where α = σ).

3 Encodings

In this section, we give encodings in our language for both explicit polymorphism through data-types, and system F. This last encoding is direct, and makes our language an alternative to system F, which allows for more explicit type information than ML, but also for more polymorphism.

Syntactic sugar

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 : ∀F L(τ_{2}) \ F L(τ_{1}).τ_{2}) ⊢ a : τ′ (τ_{1} : τ : τ_{2})}{A ⊢ λx: τ. a : τ_{1} → τ′}^{(Poly-Fun)}

The derived reduction is (λx: τ. a) v ⟶^{Fun} a{(v : τ)/x}.

Encoding polymorphic data-type

Previous works have used data types to provide explicit polymorphism [6, 14, 9]. 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
M ::= x | M M | λx. M | T M | T^{−1} M  Terms
| type T ᾱ = σ in e  Type declarations

where T ranges over data type symbols. In expressions, T and T^{−1} act as mutually inverse introduction and elimination functions to coerce the higher-order types σ into the simple type T ᾱ. For simplicity, we can assume without loss of generality that every type symbol T occurs only once, and we write (Λᾱ. σ) for the type symbol T associated with the definition type T ᾱ = σ.

The translation of types into types of our language is straightforward.

⟨⟨α⟩⟩ = α  ⟨⟨t → t⟩⟩ = ⟨⟨t⟩⟩ → ⟨⟨t⟩⟩  ⟨⟨(Λᾱ. σ) τ̄⟩⟩ = [σ{τ/ᾱ}]

Note that all type schemes are translated as polytypes with anonymous labels. We translate programs as follows.

{⟨⟨x⟩⟩ = x  ⟨⟨λx. a⟩⟩ = λx. ⟨⟨a⟩⟩  ⟨⟨a_{1} a_{2}⟩⟩ = ⟨⟨a⟩⟩_{1} ⟨⟨a⟩⟩_{2} \atop ⟨⟨(Λᾱ. σ) M⟩⟩ = [⟨⟨M⟩⟩ : σ]  ⟨⟨(Λᾱ. σ)^{−1} M⟩⟩ = ⟨M : [σ]⟩}

Indeed, the pattern ⟨ : [σ]⟩ amounts to the explicit elimination of polymorphism. Since, in the translation, the elimination of polymorphism is always explicit, it can easily be shown that the translation of a well-typed term is always welltyped.

Encoding system F

Laüfer and Odersky have shown an encoding of system F into polymorphic datatypes [9]. 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 data-types.

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:

⟨⟨α⟩⟩ = α  ⟨⟨t → t⟩⟩ = ⟨⟨t⟩⟩ → ⟨⟨t⟩⟩  ⟨⟨∀α.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 : ⟨⟨t⟩⟩)}  \frac{A ⊕ (x : t) ⊢ M : t′ ⇒ a}{A ⊢ λx: t. M : t → t′ ⇒ λx. a}

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

\frac{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⟩⟩.

Proof (sketch). The proof is by structural induction on M. The only difficulty is to ensure that when typing ⟨a⟩ the polytype [σ]^{ϵ} of a is always anonymous. Since the translation of all variables is a type constraint, which renames all labels of its type, it can easily be shown that the type of an expression never shares any label with the typing environment.

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

Using the extended syntax λx: τ. a, we could replace the two first rules by:

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

This allows for a closer comparison between system F and our language. Let us compare a term M and its translation a. The type information on lambda abstractions is the same in both terms. The type information at the elimination of polymorphism is always omitted in a. The counterpart is that type information at the introduction of polymorphism is richer in a, since it must give the full type of the expression, not just the type variable that is abstracted.

Our language is also more flexible: annotations of abstractions are not mandatory and, in particular, ML programs do not require any explicit type information at all; multiple abstractions can also be introduced simultaneously, 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.

The simplicity of our encoding compared to the encoding into polymorphic data-types is permitted by the introduction of polytypes as first-class types, and does not rely on the inference of polytypes at the elimination. If we leave the elimination of polymorphism fully explicit, we could keep first-class polytypes but omit all labels in polytypes. We would obtain a weaker but simpler proposal that would extend ML and be as powerful as system F, but more verbose.

4 Extensions to the core language

In this section, we describe two independent extensions to the core language. First, we study the restriction of polymorphism to values, which is commonly accepted as the best solution for keeping type-soundness in the presence of side effects. Then, we extend rule Use to allow a more uniform treatment of monomorphic and polymorphic polytypes; polymorphic methods in Objective ML are an important application.

4.1 Value-only polymorphism

For impure functional programming languages, value-only polymorphism has become the standard way to handle the ubiquity of side-effects. 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 [17].

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 this way, since it still allows us to generalize ϵ before the Use rule, which is needed and correct.

Thus, we replace rules Poly 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)

\frac{A ⊢ b : ς A ⊕ x : ς ⊢ a : τ}{A ⊢ let x = b in a : τ}

(Let-E)

\frac{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 nonexpansive. More generally, any expression where every application is protected (i.e. appears) under an abstraction is non-expansive (creation of mutable datastructure 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 ϵ’s to denote confirmation of polytypes, as soon as we let-bind an expansive expression, all its ϵ’s become monomorphic, and all its polytypes weak. 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. Polymorphism is there easily recovered 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 : ∀α.α → α] in
let 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, this limitation would significantly reduce its interest.

One might think that allowing quantification on ϵ in Let-E, i.e. write ∀ϵ̄.τ′ in place of τ′, is harmless. Indeed, ϵ’s polymorphism does not allow type mismatches like α’s polymorphism would: verifying identity of type schemes 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 type [σ]^{ϵ} list for any type scheme σ. Since type schemes of polytypes are not ordered, there is no principal type for this expression.

This problem is pathological, but not anecdotical. It can be solved by using principal judgments. That is, we replace Let-V and Let-E by the following restricted rules. A ⊢^{⋆} a : ς means that ς is the most general scheme for a under assumptions A.

(Let-V^{⋆})

\frac{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} : τ}

This restriction to principal judgments is not new: it has already been used for the typing of dynamics in ML [7] or value-only polymorphism in Standard ML’96 to disallow monomorphic variables at toplevel. In the former case, the program λx. (dynamics x) is rejected because, in the principal judgment x : α ⊢ x : α, some variable of the type of x occurs free in the context. Similarly, (λx. x) (λx. x) fails to type in Standard ML’96 because the non generalizable variable α is free in the principal type α → α. In both cases, a non principal judgment obtained by choosing int for α would be correct, were it not for the principality condition.

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.

4.2 An extended language

In this section we show how the core language can be used to provide polymorphic methods in Objective ML^{2} [15]. Polymorphic methods are useful in parameterized classes. Indirectly, they may also reduce the need for explicit coercions.

2 The examples of objects and classes given below are rather intuitive, and could be translated in other class-based object-oriented languages; the reader may refer to [15] for a formal presentation of Objective ML.

While Objective ML has parametric 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, but 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 we send a message to the object. The aim of the remainder of this section is to make use of polymorphic and monomorphic methods similar, and more generally the use of polymorphic methods smoother.

The first step is to give all methods polytypes. This is easily done by wrapping monomorphic methods in polytypes. For instance,

       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 of the core language thats solves this problem. We add a new typing rule Use-M:

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

As opposed to rule Use, this one allows ϵ to appear in A. Inference problems are solved by forcing the polytype to be monomorphic.

Both rules Use and Use-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. Subject reduction property is also preserved.

The expression (λx.λy. ⟨x#mem⟩ y) is then typable with principal type ⟨mem : [α → β]; ..⟩ → α → β. Since all methods are now given polytypes, we will 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.

Polymorphic methods also appear to be useful to limit the need for explicit coercions. In Objective ML, coercions are explicit. For instance suppose 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 can get 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 generic 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, this also means that we have to know that c is a circle before using method distance, like would happen in more classical object-oriented type systems. There is a choice here between using explicit coercions and giving more type information. The advantage of type information is that it occurs at more convenient places, i.e. at method definitions and invocation of a method on 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.

Related Work

Full type inference of polymorphic types is undecidable [16]. 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 [1] some polymorphic polytypes may be marked as implicit (actually their variables are marked) and automatically instantiated when used, or marked to stay polymorphic. 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 on x, which shows that this is not an extension of ML. Pierce and Turner have extended this partial inference mechanism to F_{<:}^{ω} in the design of the language Pict [12]. 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.

A different approach is taken by Pfenning [10]. 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 [11]. As ours, his solution is an extension of ML. It is also more powerful; the price is the loss of principal types and decidability of type inference. As explained in the introduction, we designed our system never to guess higher-order types.

Kfoury and Wells show that type inference could be done for the rank-2 fragment of system F [5]. However, they do not have a notion of principal types. It is also unclear how partial type information could be added.

In [9], 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, our framework subsumes theirs. They also introduce another mechanism that allows annotations of abstractions by type schemes as in λx: σ. x together with a type containment relation on type schemes similar to the one of Mitchell [8]. Type schemes may be of the form ∀α.σ_{1} → σ_{2}, where σ_{i} are type scheme 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.

In [3], 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 fully explicit polymorphism both at introduction and elimination, as the one of Läufer and Odersky. 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

Our extension of ML allows a more convenient use of polymorphic types. Polytypes are created with explicit type annotations, and can be used without specifying their types, except under abstraction. This is particularly useful in Objective ML to allow methods to be polymorphic.

Our solution is practical, since it can be used with the value-only polymorphism restriction, that is, in the presence of side-effects. We propose two options. The first, standard solution preserves all fundamental properties, but is weaker. The second solution is stronger, covers all useful cases, and does not present any new limitations. However, it keeps principal types only under some restriction. This is insignificant in practice, but reveals the limitation of value-only polymorphism.

Our approach is to keep type inference first-order, since we believe that this is sufficient in practice. Still, we allow the explicit introduction of higher-order polymorphism and its smooth interaction with ML polymorphism. As future work we would like to present our type system closer to the framework of partial type inference for second-order lambda-calculus.

The possible application to a similar simplification of first-class existential polymorphism in ML also remains to be investigated.

References

1. Luca Cardelli. An implementation of FSub. Research Report 97, Digital Equipment Corporation Systems Research Center, 1993.

2. Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the Ninth ACM Conference on Principles of Programming Langages, pages 207–212, 1982.

3. Dominic Duggan. Polymorphic methods with self types for ML-like languages. Technical report cs-95-03, University of Waterloo, 1995.

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

5. A. J. Kfoury and J. B. Wells. 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, June 1994.

6. Konstantin Läufer and Martin Odersky. Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems, 16(5):1411–1430, September 1994.

7. Xavier Leroy and Michel Mauny. Dynamics in ML. In John Hughes, editor, Conference on Functional Programming and Computer Achitecture, volume 523 of Lecture Notes in Computer Science, pages 406–426. Springer-Verlag, 1991.

8. John C. Mitchell. 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, June 1984. 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.

9. Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Proceedings of the 23rd ACM Conference on Principles of Programming Languages, pages 54–67, January 1996.

10. Frank Pfenning. Partial polymorphic type inference and higher-order unification. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 153–163, Snowbird, Utah, July 1988. ACM Press.

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

12. Benjamin C. Pierce and David N. Turner. Pict: A programming language based on the pi-calculus. Technical report, Computer Science Department, Indiana University, 1997.

13. Didier Rémy. 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, 1992.

14. Didier Rémy. Programming objects with ML-ART: An extension to ML with abstract and record types. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 321–346. Springer-Verlag, April 1994.

15. Didier Rémy and Jerôme Vouillon. 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, January 1997.

16. J. B. Wells. 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, July 1994.

17. Andrew K. Wright. Polymorphism for imperative languages without imperative types. Technical Report 93–200, Rice University, February 1993.

A Proofs of main theorems

Proof of type soundness for the core language

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

Proof. The proof is an easy induction on the structure of v.

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

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 super-relation of ⟶. All cases are independent. In each case, 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, then it is of the form:

A ⊢ a : ς ; \overline{(Gen*)} ; A ⊢ a : ∀ξ̄.ς

and there is a derivation of (1) that does not end with a rule Gen. Thus we have A ⊢ a_{2} : σ and (2) follows by the same application of rule Gen*.

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

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

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

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

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

A ⊢ ⟨[a : σ_{0}]⟩ : σ_{2}

The type schemes σ_{1}, σ_{0}, and σ_{2} are of the form ∀ᾱ.τ_{1}, ∀ᾱ.τ_{0}, and ∀ᾱ.τ_{2}, and such that (τ_{1} : τ_{0} : τ_{2}). Choosing ᾱ such that they do not occur free in A, we can contract this derivation into

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 ⊢ v_{1} : τ′_{2} → τ′_{1} (τ′_{2} → τ′_{1} : τ_{1} → τ_{2} : τ′′_{2} → τ′′_{1}) (3) ; \overline{(Ann)} ; A ⊢ (v_{1} : τ_{2} → τ_{1}) : τ′′_{2} → τ′′_{1} A ⊢ v_{2} : τ′′_{2} \overline{(App)}

A ⊢ (v_{1} : τ_{2} → t_{1}) v_{2} : τ′′_{1}

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

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

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

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

A ⊢ ([v : σ_{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}) (6). From (5), We also get (σ′′_{1} : σ_{2} : σ_{3}) (7). Thus, we have

\begin{matrix}(3) \\ & (Inst*) \\ A ⊢ v : τ′_{1} \end{matrix} (6) \overline{(Ann)} \begin{aligned}A ⊢ (v : τ_{1}) : τ′′_{1} \\ & (Gen*) \\ A ⊢ (v : τ_{1}) : σ′′_{1} \end{aligned} (7) \overline{(Poly)}

(2)

Case Tvar: Annotating with a variable does nothing.

Theorem 5 (Canonical forms). Irreducible programs that are well-typed in the empty environment are values.

Proof. We first relate the shape of types and the shape of values. Let v be a value of type τ. By considering the possible canonical derivations, we can show that:

– if v is a poly expression, or a poly expression with a type constraint, then τ is a polytype;

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

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

– if τ is a polytype, then v is a poly expression.

– otherwise, τ is a functional type, and v is of he form w.

Then we can easily prove the theorem: we consider a program a that is welltyped in the empty environment, and that cannot be reduced. We easily show by induction on the structure of a that it is a value.

Proof of the principal type property

Theorem 6. 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.

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 Poly: We assume that all the conditions of the first two lines are satisfied. We write σ_{i} for σ{ᾱ_{1}ϵ̄_{i}/ᾱ_{0}ϵ̄_{0}}.

Soundness: If ᾱ ∩ dom (θ) ∪ F V (codom (θ)) = ∅, we have θ(A) ⊢ a : θ(σ_{1}) by generalization of ᾱ in the judgement θ(A) ⊢ a : θ(τ_{1}{ϵ̄_{1}/ϵ̄_{0}}). Since (θ(σ_{1}) : σ : θ(σ_{2})), we 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 : σ] : τ. The canonical derivation of θ′(A) ⊢ [a : σ] : θ′(τ) must end with rule Poly. Thus, θ′(A) ⊢ a : θ′(σ_{1}) (1) for some extension of θ′ to ᾱ_{1}, and θ′(τ) is of the form [θ′(σ_{2})]^{ϵ′}, that is θ′ is a solution of τ ˙= [σ_{2}]^{ϵ′} (2).

From (1), we have θ′(A) ⊢ a : θ′(τ_{1}{ϵ̄_{1}/ϵ̄_{0}}). Since θ′ is a solution of A ⊢ a : (τ_{1}{ϵ̄_{1}/ϵ̄_{0}}). it is also a solution of ∃ ξ̄. θ. That is, it can be extended on ξ̄ into a solution of θ. Together with (2), this shows the completeness of the first case. No variable of ᾱ appears in dom (θ′) nor in codom (θ′), otherwise (1) could not hold. Therefore, no variable of ᾱ can either appear in dom (θ) nor in codom (θ). This shows the completeness of the failure case.

Case Use: We assume that all the conditions of the first line are satisfied .

Soundness: If θ(α) = [∀ᾱ′.τ′]^{ϵ} and ϵ ∉ F L(θ(A)) then an extension of θ such that θ(τ) = θ(τ′) is clearly 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 Use, 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 Use. Thus, we must have θ′(A) ▷ a : [σ]^{ϵ′} for some ϵ′ that does not appear in θ′(A) and some type scheme σ 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 θ′(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 the lexicographic ordering composed of successively the total size of program components, the total size of types, the number of polymorphic constraints, the number of multi-equations, and the number of renaming problems.

Moreover, unification problems that cannot be reduced are in solved form, since the side conditions of type-inference rules can never fail. Thus, a general unification problem in normal form is a unification problem in normal form, i.e. it is in solved form.

Var if ∀ξ̄.τ′ = A(x) and ξ̄∩ F V (τ) = ∅ then A ▷ x : τ − > ∃ ξ̄. τ ˙= τ′

Fun if α_{1}, α_{2} ∉ F V (A) ∪ F V (τ) then A ▷ λx. a : τ − > ∃ α_{1}, α_{2}. (A ⊕ x : α_{1} ▷ a : α_{2}) ∧ τ ˙= α_{1} → α_{2}

App if α ∉ F V (A) ∪ F V (τ) then A ▷ a_{1} a_{2} : τ − > ∃ α. (A ▷ a_{1} : α → τ) ∧ (A ▷ a_{2} : α)

Let if α ∉ F V (A) and A ▷ a_{1} : α − > ∃ ξ̄. θ then A ▷ let x = a_{1} in a_{2} : τ − > ∃ ξ̄, α. θ ∧ A ⊕ x : Gen (θ(α), θ(A)) ▷ a_{2} : τ

Ann if ϵ̄_{0} = F L(τ_{0}) and ϵ̄_{1} and ϵ̄_{2} are disjoint copies of ϵ̄_{0} outside of A and τ and ᾱ_{0} = F V (τ_{0}) and ᾱ_{1} is a copy of ᾱ_{0} outside of A and τ and τ_{1} = τ_{0}{ᾱ_{1}/ᾱ_{0}} then

A ▷ (a : τ_{0}) : τ − > ∃ ϵ̄_{1}, ϵ̄_{2}, ᾱ_{1}. A ▷ a : τ_{1}{ϵ̄_{1}/ϵ̄_{0}} ∧ τ ˙= τ_{1}{ϵ̄_{2}/ϵ̄_{0}}

Poly if ϵ̄_{0} = F L(τ_{0}) and ϵ̄_{1} and ϵ̄_{2} are disjoint copies of ϵ̄_{0} outside of A and τ and ᾱ_{0} = F V (τ_{0}) and ᾱ_{1} is a copy of ᾱ_{0} outside of A and τ and τ_{1} = τ_{0}{ᾱ_{1}/ᾱ_{0}} and σ = ∀ᾱ.τ_{0} and ᾱ ∩ F V (A) = ∅ and A ▷ a : τ_{1}{ϵ̄_{1}/ϵ̄_{0}} − > ∃ ξ. θ then

if ᾱ ∩ (dom (θ) ∪ F V (codom (θ))) = ∅ then

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

Use

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

if θ(α) = [∀ᾱ′.τ′]^{ϵ} and ϵ ∉ F L(θ(A)) then

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

Fig. 4. Type inference algorithm

Use

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

if θ(α) = [∀ᾱ′.τ′]^{ϵ} and ϵ ∉ F L(θ(A)) then

A ▷ ⟨a⟩ : τ − > ∃ ξ̄, α, ᾱ′. θ ∧ τ′ = τ

else if θ(α) = α′ and α′ ∉ F V (θ(A)) then

A ▷ ⟨a⟩ : τ − > ∃ ξ̄, α. θ

else if ϵ′ ∉ F V (A) then A ▷ ⟨a⟩ : τ − > ∃ ξ̄, ϵ′, α. θ ∧ α ˙= [τ]^{ϵ′} Fig. 5. Type inference rule for use of monomorphic polytypes