MLF

Raising ML to the Power of System F

Didier Le Botlan and Didier Rémy

INRIA-Rocquencourt 78153 Le Chesnay Cedex, France

���������������������������������������

Abstract

We propose a type system MLFthat generalizes ML with �rst-class polymorphism as in System F. Expressions may contain secondorder type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred. All expressions of ML are welltyped without any annotations. All expressions of System F can be mechanically encoded into MLF by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into MLFtypes. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated.

Categories and Subject Descriptors: D.3.3 Language Constructs and Features.

General Terms: Theory, Languages.

Keywords: Type Inference, First-Class Polymorphism, Second-Order Polymorphism, System F, ML, Type Annotations.

The quest for type inference with �rst-class polymorphic types

Programming languages considerably bene�t from static typechecking. In practice however, types may sometimes trammel programmers, for two opposite reasons. On the one hand, type annotations may quickly become a burden to write; while they usefully serve as documentation for toplevel functions, they also obfuscate the code when every local function must be decorated. On the other hand, since types are only approximations, any type system will reject programs that are perfectly well-behaved and that could be accepted by another more expressive one; hence, sharp programmers may be irritated in such situations.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for pro�t or commercial advantage and that copies bear this notice and the full citation on the �rst page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior speci�c permission and/or a fee. ICFP’03, August 25–29, 2003, Uppsala, Sweden. Copyright 2003 ACM 1-58113-756-7/03/0008 ...$5.00

Fortunately, solutions have been proposed to both of these problems. Type inference allows to elide most type annotations, which relieves the programmer from writing such details and simultaneously lightens programs. In parallel, more expressive type systems have been developed, so that programmers are less often exposed to their limitations.

Unfortunately, those two situations are often con�icting. Expressive type systems tend to require an unbearable amount of type decorations, thus many of them only remained at the status of prototypes. Indeed, full type inference for System F is undecidable [26]. Conversely, languages with simple type inference are still limited in expressiveness; more sophisticated type inference engines, such as those with subtyping constraints or higher-order uni�cation have not yet been proved to work well in practice.

The ML language [4] appears to be a surprisingly stable point of equilibrium between those two forces: it combines a reasonably powerful yet simple type system and comes with an effective type inference engine. Besides, the ML experience made it clear that expressiveness of the type system and a signi�cant amount of type inference are equally important.

Despite its success, ML could still be improved: indeed, there are real examples that require �rst-class polymorphic types [25, 20, 7] and, even though these may not occur too frequently, ML does not offer any reasonable alternative. (The inconvenience is often underestimated, since the lack of a full-�edged language to experiment with �rst-class polymorphism insidiously keeps programmers thinking in terms of ML polymorphism.)

A �rst approach is to extend ML with �rst-class second-order polymorphism [15, 25, 20, 7]. However, the existing solutions are still limited in expressiveness and the amount of necessary type declarations keeps �rst-class polymorphism uneasy to use.

An alternative approach, initiated by Cardelli [2], is to start with an expressive but explicitly typed language, say F_{< :}^{ω}, and perform a suf�cient amount of type inference, so that simple programs— ideally including all ML programs—would not need any type annotation at all. This lead to local type inference [24], recently improved to colored local type inference [21]. These solutions are quite impressive. In particular, they include subtyping in combination with higher-order polymorphism. However, they fail to type all ML programs. Moreover, they also fail to provide an intuitive and simple speci�cation of where type annotations are mandatory.

In this work, we follow the �rst approach. At least, by being conservative over ML, we are guaranteed to please programmers who are already quite happy with ML^{1}. We build on some previous work [7], which has been used to add polymorphic methods to OCaml [16]. Here, we retain the same primary goal, that is to type all expressions of System-F, providing explicit annotations when needed, and to keep all expressions of ML unannotated. In addition, we aim at the elimination of all backward coercions from polymorphic types to ML-types. In particular, our goal is not to guess polymorphic types.

Our track

Church’s style System-F and ML are quite different in nature. In ML, the elimination of polymorphism is implicitly performed at every use occurrence of a variable bound with a polymorphic type ∀ ¯ α. τ , which can then be given any instance, of the form τ [ ¯ τ/ ¯ α] . Indeed, a polymorphic type somehow represents the set of its instances. This induces an instance relation between polymorphic types themselves. For example, the (polymorphic) type ∀ ( α ) α → α is said to be more general than ∀ ( α ) ∀ ( β ) ( α → β ) → ( α → β ) and we write ∀ ( α ) α → α ≼ ∀ ( α ) ∀ ( β ) ( α → β ) → ( α → β ) because all instances of the latter are also instances of the former.

Conversely, in Church’s style System F, a type ∀ ( α ) α → α only stands for itself (modulo renaming of bound variables) and the elimination of polymorphism must be performed explicitly by type application (and abstraction) at the source level. A counter-part in System F is that bound type variables may be instantiated by polymorphic types, allowing for expressive impredicative second-order types. For example, an expression of type ∀ ( α ) α → α can be given type ( ∀ ( β ) β → β ) → ( ∀ ( β ) β → β ) by an explicit type-application to ∀ ( β ) β → β .

Unfortunately, combining implicit instantiation of polymorphic types with second-order types raises con�icts almost immediately. For illustration, consider the application of the function choose, de�ned as λ ( x) λ ( y) if true then x else y, to the identity function id. In ML, choose and id have principal types ∀ ( α ) α → α → α and ∀ ( α ) α → α , respectively. For conciseness, we shall write id_{α} for α → α and σ _{id} for ∀ ( α ) id_{α} . Should chooseid have type σ _{1} equal to ∀ ( α ) id_{α} → ∀ ( α ) id_{α} , obtained by keeping the type of id uninstantiated? Or, should it have type σ _{2} equal to ∀ ( α ) ( id_{α} → id_{α} ) , obtained by instantiating the type of id to the monomorphic type id_{α} and generalizing α only at the end? Indeed, both σ _{1} and σ _{2} are correct types for chooseid. However, neither one is more general than the other in System F. Indeed, the function auto de�ned as λ ( x : σ _{id}) x x can be typed with σ _{1}, as chooseid, but not with σ _{2}; otherwise auto could be applied, for instance, to the successor function, which would lead to a runtime error. Hence, σ _{1} cannot be safely coerced to σ _{2}. Conversely, however, there is a retyping function—a function whose type erasure η -reduces to the identity [19]—from type σ _{2} to type σ _{1}, namely, λ ( g : σ _{2}) λ ( x : σ _{id}) λ ( α ) g α ( x α ) . Actually, σ _{2} is a principal type for chooseid in F^{η ∗} (System F closed by η -expansion) [19].

While the argument of auto must be at least as polymorphic as σ _{id}, the argument of the function chooseid need not be polymorphic: it may be any instance τ of σ _{id} and the type of the return value is then τ . We could summarize these constraints by saying that:

auto : ∀ ( α = σ _{id}) α → α

            chooseid : ∀ ( α ≥ σ _{id}) α → α

The type given to chooseid captures the intuition that this appli-

1On a practical level, this would also ensure upward compatibility of existing code, although translating tools could always be provided. cation has type τ → τ for any instance τ of σ _{id}. This form of quanti�cation allows to postpone the decision of whether σ _{id} should be instantiated as soon as possible or kept polymorphic as long as possible. The bound of α in ∀ ( α ≥ σ _{id}) α → α , which is said to be �exible, can be weakened either by instantiating σ _{id} or by replacing ≥ by = . Both forms of weakening can be captured by an appropriate instance relation ≼ between types. In a binder of the form ( α = σ ) the bound σ , which is said to be rigid, cannot be instantiated any longer. Intuitively, the type ∀ ( α = σ ) σ ′ stands for the System-F type σ ′[ σ / α ] .

Finally, both chooseidsucc and chooseidauto are well-typed, taking int → int or σ _{id} for the type of α , respectively. In fact, the type ∀ ( α ≥ σ _{id}) α → α happens to be a principal type for chooseid in MLF. This type summarizes in a compact way the part of typechecking chooseid that depends on the context in which it will be used: some typing constraints have been resolved de�nitely and forgotten; others, such as “α is any instance of σ _{id}”, are kept unresolved. In short, MLFprovides richer types with constraints on the bounds of variables so that instantiation of these variables can be delayed until there is a principal way of instantiating them.

A technical road-map

The instantiations between types used above remain to be captured formally within an appropriate relation ≼. Indeed, the instance relation plays a crucial role in type inference, via a typing rule INST stating that any expression a of type σ in a context Γ has also type σ ′ in the same context whenever σ ≼ σ ′. Intuitively, the larger the relation ≼ is, the more �exibility is left for inference, and, usually, the harder the inference algorithm is.

Unsurprisingly, the “smallest reasonable relation” ≼ that validates all the instantiations used above leads to undecidable type inference, for full type inference in System-F is undecidable. Still, the relation ≼ induces an interesting variant UMLF that has the same expressiveness as MLFbut requires no type annotations at all. Fortunately, the relation ≼ can be split into a composition of relations ⊐ − ⊑ ⊐ − where uses of the relation ⊑ can be inferred as long as all applications of ⊐ − are fully explicit: this sets a clear distinction between explicit and inferred type information, which is the essence of MLF.

Unfortunately, subject reduction does not hold in MLFfor a simple notion of reduction (non local computation of annotations would be required during reduction). Thus, we introduce an intermediate variant MLF_{⋆} where only place holders for ⊐ − are indicated. For example, using the symbol ⋆ in place of polytypes, λ ( x : ⋆ ) x x belongs to MLF_{⋆} since λ ( x : σ _{id}) x x belongs to MLF(and of course, λ ( x) x x belongs to UMLF). Subject reduction and progress are proved for MLF_{⋆} and type soundness follows for MLF_{⋆} and, indirectly, for MLF.

In fact, we abstract the presentation of MLF_{⋆} over a collection of primitives so that MLFcan then be embedded into MLF_{⋆} by treating type-annotations as an appropriate choice of primitives and disallowing annotation place holders in source terms. Thus, although our practical interest is the system MLF, most of the technical developments are pursued in MLF_{⋆}.

Unsurprisingly, neither UMLF nor MLF_{⋆} admits principal types. Conversely, every expression typable in MLF admits a principal type. Of course, principal types depend on type annotations in

Figure 1. Syntax of Types

τ ::= α | g^{n} τ _{1} . . τ _{n}  Monotypes
σ ::= τ | ⊥ | ∀ ( α ≥ σ ) σ | ∀ ( α = σ ) σ  Polytypes

the source term. More precisely, if an expression is not typable in MLF, it may sometimes be typable by adding extra type annotations. Moreover, two different type annotations may lead to two incomparable principal types. As an example, the expression λ ( x) x x is not typable in MLF, while both expressions λ ( x : ∀ α . α ) x x and λ ( x : ∀ α . α → α ) x x are typable, with incomparable types. Adding a (polymorphic) type annotation to a typable expression may also lead to a new type that is not comparable with the previous one. This property should not be surprising since it is inherent to secondorder polymorphism, which we keep explicit—remember that we only infer �rst-order polymorphism in the presence of second-order types. Still, the gain is the elusion of most type annotations, via the instance relation ⊑ .

The paper is organized as follows. In Section 1, we describe types and instance relations ⊏ − and ⊑ . The syntax and the static and dynamic semantics of MLF_{⋆} are described in Section 2. Section 3 presents formal properties, including type soundness for MLF_{⋆} and type inference for MLF. Section 4 introduces explicit type annotations. A comparison with System-F is drawn is Section 5. In Section 6, we discuss expressiveness, language extensions, and related works. For the sake of readability, uni�cation and type inference algorithms have been moved to the appendices. Due to lack of space, all proofs are omitted.

“Monomorphic abstraction of polymorphic types”

In our proposal, ML-style polymorphism, as in the type of choose or id, can be fully inferred. (We will show that all ML programs remain typable without type annotations.) Unsurprisingly, some polymorphic functions cannot be typed without annotations. For instance, λ ( x) x x cannot be typed in MLF. In particular, we do not infer types for function arguments that are used polymorphically. Fortunately, such arguments can be annotated with a polymorphic type, as illustrated in the de�nition of auto given above. Once de- �ned, a polymorphic function can be manipulated by another unannotated function, as long as the latter does not use polymorphism, which is then retained. This is what we qualify “monomorphic abstraction of polymorphic types”. For instance, both idauto and chooseidauto remain of type ∀ ( α = σ _{id}) α → α (the type σ _{id} of auto is never instantiated) and neither choose nor id require any type annotation. Finally, polymorphic functions can be used by implicit instantiation, much as in ML.

To summarize, a key feature of MLF is that type variables can always be implicitly instantiated by polymorphic types. This can be illustrated by the killer-app(lication) ( λ ( x) x id) auto. This expression is typable in MLF as such, that is without any type application nor any type annotation—except, of course, in the definition of auto itself. In fact, a generalization of this example is the app function λ ( f) λ ( x) f x, whose MLF principal type is ∀ ( α , β ) ( α → β ) → α → β . It is remarkable that whenever a_{1} a_{2} is typable in MLF, so is app a_{1} a_{2}, without any type annotation nor any type application. This includes, of course, cases where a_{1} expects a polymorphic value as argument, such as in appautoid. We �nd such examples quite important in practice, since they model iterators (e.g. app) applied to polymorphic functions (e.g. auto) over structures holding polymorphic values (e.g. id).

1 Types

1.1 Syntax of types

The syntax of types is given in Figure 1. The syntax is parameterized by an enumerable set of type variables α ∈ ϑ and a family of type symbols g ∈ G given with their arity | g| . To avoid degenerated cases, we assume that G contains at least a symbol of arity two (the in�x arrow → ). We write g^{n} if g is of arity n. We also write ¯ τ for tuples of types. The polytype ⊥ corresponds to ( ∀ α . α ) , intuitively. More precisely, it will be made equivalent to ∀ ( α ≥ ⊥ ) α .

We distinguish between monotypes and polytypes. By default, types refer to the more general form, i.e. to polytypes. As in ML, monotypes do not contain quanti�ers. Polytypes generalize ML type schemes. Actually, ML type schemes can be seen as polytypes of the form ∀ ( α _{1} ≥ ⊥ ) … ∀ ( α _{n} ≥ ⊥ ) τ with outer quanti�ers. Inner quanti�ers as in System F cannot be written directly inside monotypes. However, they can be simulated with types of the form ∀ ( α = σ ) σ ′, which stands, intuitively, for the polytype σ ′ where all occurrences of α would have been replaced by the polytype σ . However, our notation contains additional meaningful sharing information. Finally, the general form ∀ ( α ≥ σ ) σ ′ intuitively stands for the collection of all polytypes σ ′ where α is an instance of σ .

Notation. We say that α has a rigid bound in ( α = σ ) and a �exible bound in ( α ≥ σ ) . A particular case of �exible bound is the unconstrained bound ( α ≥ ⊥ ) , which we abbreviate as ( α ) . For convenience, we write ( α ⋄ σ ) for either ( α = σ ) or ( α ≥ σ ) . The symbol ⋄ acts as a meta-variable and two occurrences of ⋄ in the same context mean that they all stand for = or all stand for ≥ . To allow independent choices we use indices ⋄ _{1} and ⋄ _{2} for unrelated occurrences.

Conversion and free variables. Polytypes are considered

equal modulo α -conversion where ∀ ( α ⋄ σ ) σ ′ binds α in σ ′, but not in σ . The set of free variables of a polytype σ is written ftv( σ ) and de�ned inductively as follows:

ftv( α ) = { α }  ftv( g^{n} τ _{1}… τ _{n}) = ⋃_{i= 1. . n}ftv( τ _{i})  ftv( ⊥ ) = /0

ftv( ∀ ( α ⋄ σ ) σ ′) = \{ \begin{matrix}ftv( σ ′) & if α ∉ ftv( σ ′) \\ ftv( σ ′) \ \{ α \} ∪ ftv( σ ) & otherwise \end{matrix}

The capture-avoiding substitution of α by τ in σ is written σ [ τ / α ] .

EXAMPLE 1. The syntax of types only allows quanti�ers to be outermost, as in ML, or in the bound of other bindings. Therefore, the type ∀ α · ( ∀ β · ( τ [ β ] → α ) ) → α of System F^{2} cannot be written directly. (Here, τ [ β ] means a type τ in which the variable β occurs.) However, it could be represented by the type ∀ ( α ) ∀ ( β ′ = ∀ ( β ) τ [ β ] → α ) β ′ → α . In fact, all types of System F can easily be represented as polytypes by recursively binding all occurrences of inner polymorphic types to fresh variables beforehand— an encoding from System F into MLFis given in Section 5.1.

Types may be instantiated implicitly as in ML along an instance relation ≼. As explained above, we decompose ≼ into ⊐ − ⊑ ⊐ − . In

2We write ∀ α · τ for types of System F, so as to avoid confusion.

Section 1.2, we �rst de�ne an equivalence relation between types, which is the kernel of both ⊏ − and ⊑ . In Section 1.3, we de�ne the relation ⊏ − that is the inverse of ⊐ − . The instance relation ⊑ , which contains ⊏ − , is de�ned in Section 1.4.

1.2 Type equivalence

The order of quanti�ers and some other syntactical notations are not always meaningful. Such syntactic artifacts are captured by a notion of type equivalence. Type equivalence and all other relations between types are relative to a pre�x that speci�es the bounds of free type variables.

DEFINITION 1 (PREFIXES). A pre�x Q is a sequence of bindings ( α _{1} ⋄ _{1} σ _{1}) … ( α _{n} ⋄ _{n} σ _{n}) where variables α _{1}, … α _{n} are pairwise distinct and form the domain of Q, which we write dom( Q) . The order of bindings in a pre�x is signi�cant: bindings are meant to be read from left to right; furthermore, we require that variables α _{j} do not occur free in σ _{i} whenever i ≤ j. Since α _{1}, … α _{n} are pairwise distinct, we can unambiguously write ( α ⋄ σ ) ∈ Q to mean that Q is of the form ( Q_{1}, α ⋄ σ , Q_{2}) . We also write ∀ ( Q) σ for the type ∀ ( α _{1}⋄ _{1}σ _{1}) … ∀ ( α _{n}⋄ _{n}σ _{n}) σ . (Note that α _{i}’s can be renamed in the type ∀ ( Q) σ , but not in the pre�x Q.)

DEFINITION 2 (EQUIVALENCE). The equivalence under pre�x is a relation on triples composed of a pre�x Q and two types σ _{1} and σ _{2}, written ( Q) σ _{1} ≡ σ _{2}. It is de�ned as the smallest relation that satis�es the rules of Figure 2. We write σ _{1} ≡ σ _{2} for ( /0) σ _{1} ≡ σ _{2}.

Rule EQ-COMM allows the reordering of independent binders; Rule EQ-FREE eliminates unused bound variables. Rules EQ-CONTEXT-L and EQ-CONTEXT-R tell that ≡ is a congruence; Reasoning under pre�xes allows to break up a polytype ∀ ( Q) σ and “look inside under pre�x Q”. For instance, it follows from iterations of Rule EQ-CONTEXT-R that ( Q) σ ≡ σ ′ suf�ces to show ( /0) ∀ ( Q) σ ≡ ∀ ( Q) σ ′.

Rule EQ-MONO allows to read the bound of a variable from the pre�x when it is (equivalent to) a monotype. An example of use of EQ-MONO is ( Q, α = τ _{0}, Q′) α → α ≡ τ _{0} → τ _{0}. Rule EQ-MONO makes no difference between ≥ and = whenever the bound is (equivalent to) a monotype. The restriction of Rule EQ-MONO to the case where σ _{0} is (equivalent to) a monotype is required for the well-formedness of the conclusion. Moreover, it also disallows ( Q, α = σ _{0}, Q′) α ≡ σ _{0} when τ is a variable α : variables with non trivial bounds must be treated abstractly and cannot be silently expanded. In particular, ( Q) ∀ ( α = σ _{0}, α ′ = σ _{0}) α → α ′ ≡ ∀ ( α = σ _{0}) α → α does not hold.

Rule EQ-VAR expands into both ∀ ( α = σ ) α ≡ σ and ∀ ( α ≥ σ ) α ≡ σ . The former captures the intuition that ∀ ( α = σ ) σ ′ stands for σ ′[ σ / α ] , which however, is not always well-formed. The latter may be surprising, since one could expect ∀ ( α ≥ σ ) α ⊑ σ to hold, but not the converse. The inverse part of the equivalence could be removed without changing the set of typable terms. However, it is harmless and allows for a more uniform presentation.

The equivalence ( Q) ∀ ( α ⋄ τ ) σ ≡ σ [ τ / α ] follows from Rules EQ-MONO, context rules, transitivity, and EQ-FREE, which we further refer to as the derived rule EQ-MONO^{⋆}.

The equivalence under (a given) pre�x is a symmetric operation. In other words, it captures reversible transformations. Irreversible transformations are captured by an instance relation ⊑ . Moreover, we distinguish a subrelation ⊏ − of ⊑ called abstraction. Inverse of Figure 2. Type equivalence under pre�x All rules are considered symmetrically.

\begin{matrix}E & Q & - & R & E & FL \\ ( Q) σ ≡ σ \end{matrix}

EQ-TRANS

\frac{\begin{matrix}( Q) σ _{1} ≡ σ _{2} \\ ( Q) σ _{2} ≡ σ _{3} \end{matrix}}{( Q) σ _{1} ≡ σ _{3}}

EQ-CONTEXT-R

\frac{( Q, α ⋄ σ ) σ _{1} ≡ σ _{2}}{( Q) ∀ ( α ⋄ σ ) σ _{1} ≡ ∀ ( α ⋄ σ ) σ _{2}}

EQ-CONTEXT-L

\frac{( Q) σ _{1} ≡ σ _{2}}{( Q) ∀ ( α ⋄ σ _{1}) σ ≡ ∀ ( α ⋄ σ _{2}) σ}

EQ-FREE

\frac{α ∉ ftv( σ _{1})}{( Q) ∀ ( α ⋄ σ ) σ _{1} ≡ σ _{1}}

EQ-COMM

\frac{α _{1} ∉ ftv( σ _{2}) α _{2} ∉ ftv( σ _{1})}{( Q) ∀ ( α _{1}⋄ _{1}σ _{1}) ∀ ( α _{2}⋄ _{2}σ _{2}) σ ≡ ∀ ( α _{2}⋄ _{2}σ _{2}) ∀ ( α _{1}⋄ _{1}σ _{1}) σ}

EQ-VAR ( Q) ∀ ( α ⋄ σ ) α ≡ σ

EQ-MONO

\frac{( α ⋄ σ _{0}) ∈ Q ( Q) σ _{0} ≡ τ _{0}}{( Q) τ ≡ τ [ τ _{0}/ α ]}

Figure 3. The abstraction relation

A-EQUIV \frac{( Q) σ _{1} ≡ σ _{2}}{( Q) σ _{1} ⊏ − σ _{2}}

A-TRANS

\frac{\begin{matrix}( Q) σ _{1} ⊏ − σ _{2} \\ ( Q) σ _{2} ⊏ − σ _{3} \end{matrix}}{( Q) σ _{1} ⊏ − σ _{3}}

A-CONTEXT-R

\frac{( Q, α ⋄ σ ) σ _{1} ⊏ − σ _{2}}{( Q) ∀ ( α ⋄ σ ) σ _{1} ⊏ − ∀ ( α ⋄ σ ) σ _{2}}

A-HYP \frac{( α _{1}= σ _{1}) ∈ Q}{( Q) σ _{1} ⊏ − α _{1}}

A-CONTEXT-L

\frac{( Q) σ _{1} ⊏ − σ _{2}}{( Q) ∀ ( α = σ _{1}) σ ⊏ − ∀ ( α = σ _{2}) σ}

abstractions are sound relations for ≼ but made explicit so as to preserve type inference, while inverse of instance relations would, in general, be unsound for ≼.

1.3 The abstraction relation

DEFINITION 3. The abstraction under pre�x, is a relation on triples composed of a pre�x Q and two types σ _{1} and σ _{2}, written^{3} ( Q) σ _{1} ⊏ − σ _{2}, and de�ned as the smallest relation that satis�es the rules of Figure 3. We write σ _{1} ⊏ − σ _{2} for ( /0) σ _{1} ⊏ − σ _{2}.

Rules A-CONTEXT-L and A-CONTEXT-R are context rules; note that Rule A-CONTEXT-L does not allow abstraction under �exible bounds. The interesting rule is A-HYP, which replaces a polytype σ _{1} by a variable α _{1}, provided α _{1} is rigidly bound to σ _{1} in Q.

Remarkably, rule A-HYP is not reversible. In particular, ( α = σ ) ∈ Q does not imply ( Q) α ⊏ − σ , unless σ is (equivalent to) a monotype. This asymmetry is essential, since uses of ⊏ − will be inferred, but uses of ⊐ − will not. Intuitively, the former consists in abstracting the polytype σ as the name α (after checking that α is declared as an alias for σ in Q). The latter consists in revealing the polytype abstracted by the name α . An abstract polytype, i.e. a variable bound to a polytype in Q, can only be manipulated by its name, i.e. abstractly. The polytype must be revealed explicitly (by using the relation ⊐ − ) before it can be further instantiated (along the relation ⊏ − or ⊑ ). (See also examples 6 and 7.)

3Read σ _{2} is an abstraction of σ _{1}—or σ _{1} is a revelation of σ _{2}— under pre�x Q.

Figure 4. Type instance

I-ABSTRACT \frac{( Q) σ _{1} ⊏ − σ _{2}}{( Q) σ _{1} ⊑ σ _{2}}

I-TRANS

\frac{\begin{matrix}( Q) σ _{1} ⊑ σ _{2} \\ ( Q) σ _{2} ⊑ σ _{3} \end{matrix}}{( Q) σ _{1} ⊑ σ _{3}}

I-CONTEXT-R

\frac{( Q, α ⋄ σ ) σ _{1} ⊑ σ _{2}}{( Q) ∀ ( α ⋄ σ ) σ _{1} ⊑ ∀ ( α ⋄ σ ) σ _{2}}

I-HYP \frac{( α _{1}≥ σ _{1}) ∈ Q}{( Q) σ _{1} ⊑ α _{1}}

I-CONTEXT-L

\frac{( Q) σ _{1} ⊑ σ _{2}}{( Q) ∀ ( α ≥ σ _{1}) σ ⊑ ∀ ( α ≥ σ _{2}) σ}

( Q) ⊥ ⊑ σ^{I-BOT}  \overline{( Q) ∀ ( α ≥ σ _{1}) σ ⊑ ∀ ( α = σ _{1}) σ}^{I-RIGID}

EXAMPLE 2. The abstraction ( α = σ ) ∀ ( α = σ ) σ ′ ⊏ − σ ′ is derivable: on the one hand, ( α = σ ) σ ⊏ − α holds by A-HYP, leading to ( α = σ ) ∀ ( α = σ ) σ ′ ⊏ − ∀ ( α = α ) σ ′ by A-CONTEXT-L; on the other hand, ( α = σ ) ∀ ( α = α ) σ ′ ≡ σ ′ holds by EQ-MONO^{⋆}. Hence, we conclude by A-EQUIV and A-TRANS.

1.4 The instance relation

DEFINITION 4. The instance under pre�x, is a relation on triples composed of a pre�x Q and two types σ _{1} and σ _{2}, written^{4} ( Q) σ _{1} ⊑ σ _{2}. It is de�ned as the smallest relation that satis�es the rules of Figure 4. We write σ _{1} ⊑ σ _{2} for ( /0) σ _{1} ⊑ σ _{2}.

Rule I-BOT means that ⊥ behaves as a least element for the instance relation. Rules I-CONTEXT-L and I-RIGID mean that �exible bounds can be instantiated and changed into rigid bounds. Conversely, instantiation cannot occur under rigid bounds, except when it is an abstraction, as described by Rule A-CONTEXT-L.

The interesting rule is I-HYP—the counter-part of rule A-HYP, which replaces a polytype σ _{1} by a variable α _{1}, provided σ _{1} is a �exible bound of α _{1} in Q.

EXAMPLE 3. The instance relation ( α ≥ σ ) ∀ ( α ≥ σ ) σ ′ ⊑ σ ′ holds. The derivation follows the one of Example 2 but uses I-HYP and I-CONTEXT-L instead of A-HYP and A-CONTEXT-L. More generally, ( QQ′) ∀ ( Q′) σ ⊑ σ holds for any Q, Q′, and σ , which we refer to as Rule I-DROP.

The relation ( Q) ∀ ( α _{1}≥ ∀ ( α _{2}⋄ σ _{2}) σ _{1}) σ ⊑ ∀ ( α _{2}⋄ σ _{2}) ∀ ( α _{1}≥ σ _{1}) σ holds whenever α _{2} ∉ ftv( σ ) , which we further refer to as the derived rule I-UP.

As expected, the equivalence is the kernel of the instance relation:

LEMMA 1 (EQUIVALENCE). For any pre�xes Q and types σ and σ ′, we have ( Q) σ ≡ σ ′ if and only if both ( Q) σ ⊑ σ ′ and ( Q) σ ′ ⊑ σ hold.

The instance relation coincide with equivalence on monotypes, which captures the intuition that “monotypes are really monomorphic”.

LEMMA 2. For all pre�xes Q and monotypes τ and τ ′, we have ( Q) τ ⊑ τ ′ if and only if ( Q) τ ≡ τ ′.

4Read σ _{2} is an instance of σ _{1}—or σ _{1} is more general than σ _{2}— under pre�x Q.

The instance relation also coincides with the one of ML on MLtypes. In particular, ∀ ( ¯ α) τ _{0} ⊑ τ _{1} if and only if τ _{1} is of the form τ _{0}[ ¯ τ/ ¯ α] .

EXAMPLE 4. The instance relation covers an interesting case of type isomorphism [3]. In System F, type ∀ α · τ ′ → τ is isomorphic^{5} to τ ′ → ∀ α · τ whenever α is not free in τ ′. In MLF, the two corresponding polytypes are not equivalent but in an instance relation. Precisely, ∀ ( α ′ ≥ ∀ ( α ) τ ) τ ′ → α ′ is more general than ∀ ( α ) τ ′ → τ , as shown by the following derivation:

∀ ( α ′ ≥ ∀ ( α ) τ ) τ ′ → α ′
⊑ ∀ ( α ) ∀ ( α ′ ≥ τ ) τ ′ → α ′  by I-UP
≡ ∀ ( α ) τ ′ → τ  by EQ-MONO^{⋆}

(However, as opposed to type containment [19], the instance relation cannot express any form of contravariance.)

1.5 Operation on pre�xes and uni�cation

Rules A-CONTEXT-L and I-CONTEXT-L show that two types ∀ ( Q) σ and ∀ ( Q′) σ with the same suf�x can be in an instance relation, for any suf�x σ . This suggests a notion of inequality between pre�xes alone. However, because pre�xes are “open” this relation must be de�ned relatively to a set of variables that lists (a superset of) the free type variables of σ . In this context, a set of type variables is called an interface and is written with letter I .

DEFINITION 5 (PREFIX INSTANCE). A pre�x Q is an instance of a pre�x Q′ under the interface I , and we write Q ⊑ ^{I} Q′, if and only if ∀ ( Q) σ ⊑ ∀ ( Q′) σ holds for all types σ whose free variables are included in I . We omit I in the notation when it is equal to dom( Q) . We de�ne Q ≡ ^{I} Q′ and Q ⊏ − ^{I} Q′ similarly.

Pre�xes can be seen as a generalization of the notion of substitutions to polytypes. Then, Q ⊑ Q′ captures the usual notion of (a substitution) Q being more general than (a substitution) Q′.

DEFINITION 6 (UNIFICATION). A pre�x Q′ uni�es monotypes τ _{1} and τ _{2} under Q if and only if Q ⊑ Q′ and ( Q) τ _{1} ≡ τ _{2}.

The uni�cation algorithm, called unify, is de�ned in Appendix A.

THEOREM 1. For any pre�x Q and monotypes τ _{1} and τ _{2}, unify ( Q, τ _{1}, τ _{2}) returns the smallest pre�x (for the relation ⊑ ^{dom( Q)} ) that uni�es τ _{1} and τ _{2} under Q, or fails if there exists no pre�x Q′ that uni�es τ _{1} and τ _{2} under Q.

The following lemma shows that �rst-order uni�cation lies under MLFuni�cation.

LEMMA 3. If ( Q) τ _{1} ≡ τ _{2}, then there exists a substitution Q̂ (depending only on Q) that uni�es τ _{1} and τ _{2}.

2 The core language

As explained in the introduction we formalize the language MLF as a restriction to the more permissive language MLF_{⋆}. We assume given a countable set of variables, written with letter x, and a countable set of constants c ∈ C . Every constant c has an arity | c| . A constant is either a primitive f or a constructor C. The distinction

5That is, there exists a function ( η , β ) -reducible to the identity that transforms one into the other, and conversely.

Figure 5. Expressions of MLF_{⋆}

a ::= x | c | λ ( x) a | a a | let x = a in a  Terms
| ( a : ⋆ )  Oracles
c ::= f | C  Constants
z ::= x | c  Identi�ers

between constructors and primitives lies in their dynamic semantics: primitives (such as + ) are reduced when fully applied, while constructors (such as ����) represent data structures, and are not reduced. We use letter z to refer to identi�ers, i.e. either variables or constants.

Expressions of MLF_{⋆}, written with letter a, are described in Figure 5. Expressions are those of ML extended with oracles. An oracle, written ( a : ⋆ ) is simply a place holder for an implicit type annotation around the expression a. Intuitively, oracles are places where the type inference algorithm must call an “oracle” to �ll the hole with a type annotation. Equivalently, the oracles can be replaced by explicit type annotations before type inference. Explicit annotations ( a : σ ) , which are described in Section 4, are actually syntactic sugar for applications ( σ ) a where ( σ ) are constants. Examples in the introduction also use the notation λ ( x : σ ) a, which do not appear in Figure 5, because this is, again, syntactic sugar for λ ( x) let x = ( x : σ ) in a. Similarly, λ ( x : ⋆ ) a means λ ( x) let x = ( x : ⋆ ) in a.

The language MLFis the restriction of MLF_{⋆} to expressions that do not contain oracles.

2.1 Static semantics

Typing contexts, written with letter Γ are lists of assertions of the form z : σ . We write z : σ ∈ Γ to mean that z is bound in Γ and z : σ is its rightmost binding in Γ . We assume given an initial typing context Γ _{0} mapping constants to closed polytypes.

Typing judgments are of the form ( Q) Γ ⊢ a : σ . A tiny difference with ML is the presence of the pre�x Q that assigns bounds to type variables appearing free in Γ or σ . By comparison, this pre�x is left implicit in ML because all free type variables have the same (implicit) bound ⊥ . In MLF, we require that σ and all polytypes of Γ be closed with respect to Q, that is, ftv( Γ ) ∪ ftv( σ ) ⊆ dom( Q) .

Typing rules. The typing rules of MLF_{⋆} and MLFare described in Figure 6. They correspond to the typing rules of ML modulo the richer types, the richer instance relation, and the explicit binding of free type variables in judgments. In addition, Rule ORACLE allows for the revelation of polytypes, that is, the transformation of types along the inverse of the abstraction relation. (This rule would has no effect in ML where abstraction is the same as equivalence.) For UMLF, it suf�ces to replace Rule ORACLE by U-ORACLE given below or, equivalently, combine ORACLE with INST into U-INST.

U-ORACLE

\frac{( Q) Γ ⊢ a : σ ( Q) σ ⊐ − σ ′}{( Q) Γ ⊢ a : σ ′}

U-INST

\frac{( Q) Γ ⊢ a : σ ( Q) σ ⊐ − ⊑ ⊐ − σ ′}{( Q) Γ ⊢ a : σ ′}

As in ML, there is an important difference between rules FUN and LET: while typechecking their bodies, a let-bound variable can be assigned a polytype, but a λ -bound variable can only be assigned

Figure 6. Typing rules for MLF and MLF_{⋆}

VAR \frac{z : σ ∈ Γ}{( Q) Γ ⊢ z : σ} APP

\frac{( Q) Γ ⊢ a_{1} : τ _{2} → τ _{1} ( Q) Γ ⊢ a_{2} : τ _{2}}{( Q) Γ ⊢ a_{1} a_{2} : τ _{1}}

FUN

\frac{( Q) Γ , x : τ _{0} ⊢ a : τ}{( Q) Γ ⊢ λ ( x) a : τ _{0} → τ}

LET

\frac{\begin{matrix}( Q) Γ ⊢ a_{1} : σ \\ ( Q) Γ , x : σ ⊢ a_{2} : τ \end{matrix}}{( Q) Γ ⊢ let x = a_{1} in a_{2} : τ}

GEN

\frac{( Q, α ⋄ σ ) Γ ⊢ a : σ ′ α ∉ ftv( Γ )}{( Q) Γ ⊢ a : ∀ ( α ⋄ σ ) σ ′}

INST

\frac{\begin{matrix}( Q) Γ ⊢ a : σ \\ ( Q) σ ⊑ σ ′ \end{matrix}}{( Q) Γ ⊢ a : σ ′}

ORACLE

\frac{\begin{matrix}( Q) Γ ⊢ a : σ \\ ( Q) σ ⊐ − σ ′ \end{matrix}}{( Q) Γ ⊢ ( a : ⋆ ) : σ ′}

a monotype in Γ . Indeed, the latter must be guessed while the former can be inferred from the type of the bound expression. This restriction is essential to enable type inference. Notice that a λ - bound variable can refer to a polytype abstractly via a type variable α bound to a polytype σ in Q. However, this will not allow to take different instances of σ while typing the body of the abstraction, unless the polytype bound σ of α is �rst revealed by an oracle. Indeed, the only possible instances of α under a pre�x Q that contains the binding ( α = σ ) are types equivalent to α under Q. However, ( Q) α ≡ σ does not hold. Thus, if x : α is in the typing context Γ , the only way of typing x (modulo equivalence) is ( Q) Γ ⊢ x : α , whereas ( Q) Γ ⊢ x : σ is not derivable. Conversely, ( Q) Γ ⊢ ( x : ⋆ ) : σ is derivable, since ( Q) α ⊐ − σ .

ML as a subset of MLF. ML can be embedded into MLF by restricting all bounds in the pre�x Q to be unconstrained. Rules GEN and INST are then exactly those of ML. Hence, any closed program typable in ML is also typable in MLF.

EXAMPLE 5. This �rst example of typing illustrates the use of polytypes in typing derivations: we consider the simple expression K ′ de�ned by λ ( x) λ ( y) y. Following ML, one possible typing derivation is (we recall that ( α , β ) stands for ( α ≥ ⊥ , β ≥ ⊥ ) ):

GEN

FUN ( α , β ) x : α , y : β ⊢ y : β

FUN \frac{( α , β ) x : α ⊢ λ ( y) y : β → β}{( α , β ) ⊢ K ′ : α → ( β → β )}
⊢ K ′ : ∀ ( α , β ) α → ( β → β )

There is, however, another typing derivation that infers a more general type for K ′ in MLF(for conciseness we write Q for α , β ≥ σ _{id}):

INST GEN \frac{^{FUN} \frac{( Q, γ) x : α , y : γ ⊢ y : γ}{( Q, γ) x : α ⊢ λ ( y) y : γ → γ}}{( Q) x : α ⊢ λ ( y) y : σ _{id}} ( Q) σ _{id} ⊑ β

FUN ( Q) x : α ⊢ λ ( y) y : β

GEN \frac{( Q) ⊢ K ′ : α → β}{⊢ K ′ : ∀ ( Q) α → β}

Notice that the polytype ∀ ( α , β ≥ σ _{id}) α → β is more general than ∀ ( α , β ) α → ( β → β ) , which follows from Example 4.

Figure 7. Syntax directed typing rules

VAR^{▽} \frac{z : σ ∈ Γ}{( Q) Γ ⊢ ^{▽} z : σ} FUN^{▽}

( QQ′) Γ , x : τ _{0} ⊢ ^{▽} a : σ  dom( Q′) ∩ Γ = /0

( Q) Γ ⊢ ^{▽} λ ( x) a : ∀ ( Q′, α ≥ σ ) τ _{0} → α

APP^{▽}

\frac{( Q) Γ ⊢ ^{▽} a_{1} : σ _{1}  ( Q) Γ ⊢ ^{▽} a_{2} : σ _{2} ( Q) σ _{1} ⊑ ∀ ( Q′) τ _{2} → τ _{1}  ( Q) σ _{2} ⊑ ∀ ( Q′) τ _{2}}{( Q) Γ ⊢ ^{▽} a_{1} a_{2} : ∀ ( Q′) τ _{1}}

LET^{▽}

\frac{\begin{matrix}( Q) Γ ⊢ ^{▽} a_{1} : σ _{1} \\ ( Q) Γ , x : σ _{1} ⊢ ^{▽} a_{2} : σ _{2} \end{matrix}}{( Q) Γ ⊢ ^{▽} let x = a_{1} in a_{2} : σ _{2}}

ORACLE^{▽}

\frac{\begin{matrix}( Q) Γ ⊢ ^{▽} a : σ \\ ( Q) σ ⊐ − σ ′ \end{matrix}}{( Q) Γ ⊢ ^{▽} ( a : ⋆ ) : σ ′}

2.2 Syntax directed presentation

As in ML, we can replace the typing rules of MLF_{⋆} by a set of equivalent syntax-directed typing rules, which are given in Figure 7. Naively, a sequence of non-syntax-directed typing Rules GEN and INST should be placed around any other rule. However, many of these occurrences can be proved unnecessary by following an appropriate strategy. For instance, in ML, judgments are maintained instantiated as much as possible and are only generalized on the left-hand side of Rule LET. In MLF_{⋆}, this strategy would require more occurrences of generalization. Instead, we prefer to maintain typing judgments generalized as much as possible. Then, it suf�ces to allow Rule GEN right after Rule FUN and to allow Rule INST right before Rule APP (see Rules FUN^{▽} and APP^{▽}).

EXAMPLE 6. As we claimed in the introduction, a λ -bound variable that is used polymorphically must be annotated. Let us check that λ ( x) x x is not typable in MLF by means of contradiction. A syntax-directed type derivation of this expression would be of the form:

APP^{▽}

V^{A}^{R}^{▽} ( Q) x : τ _{0} ⊢ ^{▽} x : τ _{0}

( Q) τ _{0} ⊑ ∀ ( Q′) τ _{2} → τ _{1} ( 2)

( Q) x : τ _{0} ⊢ ^{▽} x : τ _{0}^{V}^{A}^{R}^{▽}

( Q) τ _{0} ⊑ ∀ ( Q′) τ _{2} ( 1)

FUN^{▽} \frac{( Q) x : τ _{0} ⊢ ^{▽} x x : ∀ ( Q′) τ _{1}}{( Q) /0 ⊢ λ ( x) x x : ∀ ( α ≥ ∀ ( Q′) τ _{1}) τ _{0} → α}

Applying Rule I-DROP to (2) and (1), we get respectively ( QQ′) τ _{0} ⊑ τ _{2} → τ _{1} and ( QQ′) τ _{0} ⊑ τ _{2}. Then ( QQ′) τ _{2} → τ _{1} ≡ τ _{2} follows by Lemma 2 and EQ-TRANS. Thus, by Lemma 3, there exists a substitution θ such that θ ( τ _{2}) = θ ( τ _{2} → τ _{1}) , that is, θ ( τ _{2}) = θ ( τ _{2}) → θ ( τ _{1}) , which cannot be the case.

This example shows the limit of type inference, which is actually the strength of our system! That is, to maintain principal types by rejecting examples where type inference would need to guess second-order types.

EXAMPLE 7. Let us recover typability by introducing an oracle and build a derivation for λ ( x) ( x : ⋆ ) x. Taking ( α = σ _{id}) for Q and α for τ _{0}, we obtain:

APP^{▽} ORACLE^{▽} \frac{^{V}^{A}^{R}^{▽} ( Q) x : α ⊢ ^{▽} x : α ( Q) α ⊐ − σ _{id} ( 3)}{( Q) x : α ⊢ ^{▽} ( x : ⋆ ) : σ _{id}}

( Q) σ _{id} ⊑ α → α
( Q) x : α ⊢ ^{▽} x : α ^{V}^{A}^{R}^{▽}

FUN^{▽} \frac{( Q) x : α ⊢ ^{▽} ( x : ⋆ ) x : α}{⊢ λ ( x) ( x : ⋆ ) x : ∀ ( α = σ _{id}) α → α}

The oracle plays a crucial role in (3)—the revelation of the type scheme σ _{id} that is the bound of the type variable α used in the type of x. We have ( Q) σ _{id} ⊑ α , indeed, but the converse relation does not hold, so rule INST cannot be used here to replace α by its bound

σ _{id}.

2.3 Dynamic semantics

The semantics of MLF_{⋆} is the standard call-by-value semantics of ML. We present it as a small-step reduction semantics. Values and call-by-value evaluation contexts are described below.

v ::= λ ( x) a
| f v_{1} … v_{n}  n < | f|
| C v_{1} … v_{n}  n ≤ | C|
| ( v : ⋆ )
E ::= [ ] | E a | v E | ( E : ⋆ ) | let x = E in a

The reduction relation − → is parameterized by a set of δ -rules of the form ( δ ) below:

f v_{1} … v_{n} − → a  when | f| = n  ( δ )
( λ ( x) a) v − → a[ v/ x]  ( β _{v})
let x = v in a − → a[ v/ x]  ( β _{let})
( v_{1} : ⋆ ) v_{2} − → ( v_{1} v_{2} : ⋆ )  ( ⋆ )

The main reduction is the β -reduction that takes two forms Rule ( β _{v}) and Rule ( β _{let}) . Oracles are maintained during reduction to which they do not contribute: they are simply pushed out of applications by rule ( ⋆ ) . Finally, the reduction is the smallest relation containing ( δ ) , ( β _{v}) , ( β _{let}) , and ( ⋆ ) rules that is closed by E-congruence:

E[ a] − → E[ a′] if a − → a′  ( CONTEXT)

3 Formal properties

We verify type soundness for MLF_{⋆} and address type inference in MLF.

3.1 Type soundness

Type soundness for MLF_{⋆} is shown as usual by a combination of subject reduction, which ensures that typings are preserved by reduction, and progress, which ensures that well-typed programs that are not values can be further reduced.

To ease the presentation, we introduce a relation ⊆ between programs: we write a ⊆ a′ if and only if every typing of a, i.e. a triple ( Q, Γ , σ ) such that ( Q) Γ ⊢ a : σ holds, is also a typing of a′. A relation R on programs preserves typings whenever it is a sub-relation of ⊆ .

Of course, type soundness cannot hold without some assumptions relating the static semantics of constants described by the initial typing context Γ _{0} and their dynamic semantics.

DEFINITION 7 (HYPOTHESES). We assume that the following three properties hold for constants.

(H0) (Arity) Each constant c ∈ dom( Γ _{0}) has a closed type Γ _{0}( c) of the form ∀ ( Q) τ _{1} → … τ _{| c|} → τ and such that the top symbol of ∀ ( Q) τ is not in { → , ⊥ } whenever c is a constructor.

(H1) (Subject-Reduction) All δ -rules preserve typings.

(H2) (Progress) Any expression a of the form f v_{1}… v_{| f|} , such that ( Q) Γ _{0} ⊢ a : σ is in the domain of ( δ ) .

THEOREM 2 (SUBJECT REDUCTION). Reduction preserves typings.

THEOREM 3 (PROGRESS). Any expression a such that ( Q) Γ _{0} ⊢ a : σ is a value or can be further reduced.

Combining theorems 2 and 3 ensures that the reduction of welltyped programs either proceeds for ever or ends up with a value. This holds for programs in MLF_{⋆} but also for programs in MLF, since MLFis a subset of MLF_{⋆}. Hence MLFis also sound. However, MLF does not enjoy subject reduction, since reduction may create oracles. Notice, however, that oracles can only be introduced by δ -rules.

3.2 Type inference

A type inference problem is a triple ( Q, Γ , a) , where all free type variables in Γ are bound in Q. A pair ( Q′, σ ) is a solution to this problem if Q ⊑ Q′ and ( Q′) Γ ⊢ a : σ . A pair ( Q′, σ ′) is an instance of a pair ( Q, σ ) if Q ⊑ Q′ and ( Q′) σ ⊑ σ ′. A solution of a type inference problem is principal if all other solutions are instances of the given one.

Figure 9 in the Appendix B de�nes a type inference algorithm WF for MLF. This algorithm proceeds much as type inference for ML: the algorithm follows the syntax-directed typing rules and reduces type inference to uni�cation under pre�xes.

THEOREM 4 (TYPE INFERENCE). The set of solutions of a solvable type inference problem admits a principal solution. Given any type inference problem, the algorithm WFeither returns a principal solution or fails if no solution exists.

4 Type annotations

In this section, we restrict our attention to MLF, i.e. to expressions that do not contain oracles. Since expressions of MLF are exactly those of ML, its expressiveness may only come from richer types and typing rules. However, the following lemma shows that this is not suf�cient:

LEMMA 4. If the judgment ( Q) Γ ⊢ a : σ holds in MLF where the typing context Γ contains only ML types and Q contains only type variables with unconstrained bounds, then there exists a derivation of Γ ⊢ a : ∀ ( ¯ α) τ in ML where ∀ ( ¯ α) τ is obtained from σ by moving all inner quanti�ers ahead.

The inverse inclusion has already been stated in Section 2.1. In the particular case where the initial typing context Γ _{0} contains only ML types, a closed expression can be typed in MLFunder Γ _{0} if and only if it can be typed in ML under Γ _{0}. This is not true for MLF_{⋆} in which the expression λ ( x) ( x : ⋆ ) x is typable. Indeed, as shown below, all terms of System F can be typed in MLF_{⋆}. Fortunately, there is an interesting choice of constants that provides MLF with the same expressiveness as MLF_{⋆} while retaining type inference. Precisely, we provide type annotations as a collection of coercion primitives, i.e. functions that change the type of expressions without changing their meaning. The following example, which describes a single annotation, should provide intuition for the general case.

EXAMPLE 8. Let f be a constant of type σ equal to ∀ ( α = σ _{id}, α ′ ≥ σ _{id}) α → α ′ with the δ -reduction f v − → ( v : ⋆ ) . Then, the expression a de�ned as λ ( x) ( f x) x behaves as λ ( x) x x and is well-typed, of type ∀ ( α = σ _{id}) α → α . To see this, let Q and Γ stand for ( α = σ _{id}, α ′ = σ _{id}) and x : α . By Rules INST, VAR, and APP ( Q) Γ ⊢ f x : α ′; hence by rule GEN, ( α = σ _{id}) Γ ⊢ f x : ∀ ( α ′ = σ _{id}) α ′ since α ′ is not free in the Γ . By rule EQ-VAR, we have ∀ ( α ′ = σ _{id}) α ′ ≡ σ _{id} (under any pre�x); besides, σ _{id} ⊑ α → α under any pre�x that binds α . Thus, we get ( α = σ _{id}) Γ ⊢ f x : α → α by Rule INST. The result follows by Rules APP, FUN, and GEN.

Observe that the static effect of f in f x is (i) to enforce the type of x to be abstracted by a variable α bound to σ _{id} in Q and (ii) to give f x, that is x, the type σ _{id}, exactly as the oracle ( x : ⋆ ) would. Notice that the bound of α in σ is rigid: the function f expects a value v that must have type σ _{id} (and not a strict instance of σ _{id}). Conversely, the bound of α ′ is �exible: the type of f v is σ _{id} but may also be any instance of σ _{id}.

DEFINITION 8. We call annotations the denumerable collection of primitives ( ∃ ( Q) σ ) , of arity 1, de�ned for all pre�xes Q and polytypes σ closed under Q. The initial typing environment Γ _{0} contains these primitives with their associated type:

( ∃ ( Q) σ ) : ∀ ( Q) ∀ ( α = σ ) ∀ ( β ≥ σ ) α → β  ∈ Γ _{0}

We may identify annotation primitives up to the equivalence of their types.

Besides, we write ( a : ∃ ( Q) σ ) for the application ( ∃ ( Q) σ ) a. We also abbreviate ( ∃ ( Q) σ ) as ( σ ) when all bounds in Q are unconstrained. Actually, replacing an annotation ( ∃ ( Q) σ ) by ( σ ) preserves typability and, more precisely, preserves typings.

While annotations are introduced as primitives for simplicity of presentation, they are obviously meant to be applied. Notice that the type of an annotation may be instantiated before the annotation is applied. However, the annotation keeps exactly the same “revealing power” after instantiation. This is described by the following technical lemma (the reader may take /0 for Q_{0} at �rst).

LEMMA 5. The judgment ( Q_{0}) Γ ⊢ ( a : ∃ ( Q) σ ) : σ _{0} is valid if and only if there exists a type ∀ ( Q′) σ ′_{1} such that the judgment ( Q_{0}) Γ ⊢ a : ∀ ( Q′) σ ′_{1} holds together with the following relations: Q_{0}Q ⊑ Q_{0}Q′, ( Q_{0}Q′) σ ′_{1} ⊐ − σ , and ( Q_{0}) ∀ ( Q′) σ ⊑ σ _{0}.

The pre�x Q of the annotation ∃ ( Q) σ may be instantiated into Q′. However, Q′ guards σ ′_{1} ⊐ − σ in ( Q_{0}Q′) σ ′_{1} ⊐ − σ . In particular, the lemma would not hold with ( Q_{0}) ∀ ( Q′) σ ′_{1} ⊐ − ∀ ( Q′′) σ and ( Q_{0}) ∀ ( Q′′) σ ′_{1} ⊑ σ _{0}. Lemma 5 has similarities with Rule ANNOT of Poly-ML [7].

COROLLARY 6. The judgment ( Q) Γ ⊢ ( a : ⋆ ) : σ _{0} holds if and only if there exists an annotation ( σ ) such that ( Q) Γ ⊢ ( a : σ ) : σ _{0} holds.

Hence, all expressions typable in MLF_{⋆} are typable in MLFas long as all annotation primitives are in the initial typing context Γ _{0}.

Reduction of annotations. The δ -reduction for annotations just replaces explicit type information by oracles.

( v : ∃ ( Q) σ ) − → ( v : ⋆ )

LEMMA 7 (SOUNDNESS OF TYPE ANNOTATIONS). All three hypotheses (H0, arity), (H1, subject-reduction), and (H2, progress) hold when primitives are the set of annotations, alone.

The annotation ( ∃ ( Q) σ ) can be simulated by λ ( x) ( x : ⋆ ) in MLF_{⋆}, both statically and dynamically. Hence annotations primitives are unnecessary in MLF_{⋆}.

Syntactic sugar. As mentioned in Section 2, λ ( x : σ ) a is syntactic sugar for λ ( x) let x = ( x : σ ) in a. The derived typing rule is:

FUN^{⋆}

\frac{( Q) Γ , x : σ ⊢ a : σ ′ Q′ ⊑ Q}{( Q) Γ ⊢ λ ( x : ∃ ( Q′) σ ) a : ∀ ( α = σ ) ∀ ( α ′ ≥ σ ′) α → α ′}

This rule is actually simpler than the derived annotation rule suggested by lemma 5, because instantiation is here left to each occurrence of the annotated program variable x in a.

The derived reduction rule is ( λ ( x : ∃ ( Q) σ ) a) v − →^{β_{⋆}} let x = ( v : ∃ ( Q) σ ) in a. Values must then be extended with expressions of the form λ ( x : ∃ ( Q) σ ) a, indeed.

5 Comparison with System-F

We have already seen that all ML programs can be written in MLF without annotations. In Section 5.1, we provide a straightforward compositional translation of terms of System-F into MLF. In Section 5.2, we then identify a subsystem of MLF, called Shallow-MLF_{⋆}, whose let-binding free version is exactly the target of the encoding of System-F.

5.1 Encoding System-F into MLF

The types, terms, and typing contexts of system F are given below:

t ::= α | t → t | ∀ α · t
M ::= x | M M | λ ( x :t) M | Λ ( α ) M | M t
A ::= /0 | A, x : t | A, α

The translation of types of System-F into MLFtypes uses auxiliary rigid bindings for arrow types. This ensures that there are no inner polytypes left in the result of the translation, which would otherwise be ill-formed. Quanti�ers that are present in the original types are translated to unconstrained bounds.

{[ [ α ] ] = α [ [ ∀ α · t] ] = ∀ ( α ) [ [ t] ] \atop [ [ t_{1} → t_{2}] ] = ∀ ( α _{1}= [ [ t_{1}] ] ) ∀ ( α _{2}= [ [ t_{2}] ] ) α _{1} → α _{2}}

In order to state the correspondence between typing judgments, we must also translate typing contexts. We write A ⊢ M : t to mean that M has type t in typing context A in System F. The translation of A, written [ [ A] ] , returns a pair ( Q) Γ of a pre�x and a typing context and is de�ned inductively as follows:

[ [ /0] ] = ( ) /0 \frac{[ [ A] ] = ( Q) Γ}{[ [ A, x : t] ] = ( Q) Γ , x : [ [ t] ]}

\frac{[ [ A] ] = ( Q) Γ α ∉ dom( Q)}{[ [ A, α ] ] = ( Q, α ) Γ}

The translation of System F terms into MLF terms forgets type abstraction and type applications, and translates types in termabstractions.

[ [ Λ ( α ) M] ] = [ [ M] ]  [ [ M t] ] = [ [ M] ]  [ [ x] ] = x

[ [ M M′] ] = [ [ M] ] [ [ M′] ] [ [ λ ( x :t) M] ] = λ ( x : [ [ t] ] ) [ [ M] ]

Finally, we can state the following lemma:

LEMMA 8. For any closed typing context A (that does not bind the same type variable twice), term M, and type t of system F such that A ⊢ M : t, there exists a derivation ( Q) Γ ⊢ [ [ M] ] : τ such that ( Q) Γ = [ [ A] ] and [ [ t] ] ⊏ − τ .

Remarkably, translated terms contain strictly fewer annotations than original terms—a property that was not true in Poly-ML. In particular, all type Λ -abstractions and type applications are dropped and only annotations of λ -bound variables remain. Moreover, some of these annotations are still super�uous.

5.2 Shallow-MLF_{⋆}

Types whose �exible bounds are always ⊥ are called F-types (they are the translation of types of System F). Types of the form ∀ ( α ≥ σ ) τ , where σ is not equivalent to a monotype nor to ⊥ , have been introduced to factor out choices during type inference. Such types are indeed used in a derivation of let f = choose id in ( f auto) ( f succ) . However, they are never used in the encoding of System-F. Are they needed as annotations?

Let a type be shallow if and only if all its rigid bounds are F-types. More generally, pre�xes, typing contexts, and judgments are shallow if and only if they contain only shallow types. A derivation is shallow if all its judgments are shallow and Rule ORACLE is only applied to F-types. Notice that the explicit annotation ( σ ) has a shallow type if and only if σ is an F-type. We call Shallow-MLF_{⋆} the set of terms that have shallow derivations. Interestingly, subject reduction also holds for Shallow-MLF_{⋆}.

Let-bindings do not increase expressiveness in MLF_{⋆}, since they can always be replaced by λ -bindings with oracles or explicit annotations. This is not true for Shallow-MLF_{⋆}, since shallow-types that are not F-types cannot be used as annotations. Therefore, we also consider the restriction Shallow-F of Shallow-MLF_{⋆} to programs without let-bindings.

The encoding of System-F into MLF given in Section 5.1 is actually an encoding into Shallow-F. Conversely, all programs typable into Shallow-F are also typable in System-F. Hence, Shallow-F and System-F have the same expressiveness.

6 Discussion

6.1 Expressiveness of MLF

By construction, we have the chain of inclusions Shallow-F ⊆ Shallow-MLF_{⋆} ⊆ MLF_{⋆}. We may wonder whether these languages have strictly increasing power. That is, ignoring annotations and the difference in notation between let-bindings and λ -redexes, do they still form a strict chain of inclusions? We conjecture that this is true.

Still, MLF_{⋆} remains a second-order system and in that sense should not be signi�cantly more expressive than System F. In particular, we conjecture that the term ( λ ( y) y I ; y K ) ( λ ( x) x x) that is typable in F^{ω} but not in F [9] is not typable in MLFeither. Conversely, we do not know whether there exists a term of MLFthat is not typable in F^{ω}.

Reducing all let-bindings in a term of Shallow-MLF_{⋆} produces a term in Shallow-F. Hence, terms of Shallow-MLF_{⋆} are strongly normalizable. We conjecture that so are all terms of MLF.

6.2 Simple language extensions

Because the language is parameterized by constants, which can be used either as constructors or primitive operations, the language can import foreign functions de�ned via appropriate δ -rules. These could include primitive types (such as integers, strings, etc.) and operations over them. Sums and products, as well as prede�ned datatypes, can also be treated in this manner, but some extension is required to declare new data-types within the language itself.

The value restriction of polymorphism [28] that allows for safe mutable data-structures in ML should carry over to MLF by allowing only rigid bounds that appear in the type of expansive expressions to be generalized. However, this solution is likely to be disappointing in MLF, as it is in Poly-ML, which uses polymorphism extensively. An interesting relaxation of the value-only restriction has been recently proposed [6] and allows to always generalize type variables that never appears on the left hand-side of an arrow type; this gave quite satisfactory results in the context of Poly-ML and we can expect similar bene�ts for MLF.

6.3 Related works

Our work is related to all other works that aim at some form of type inference in the presence of higher-order types.The closest of them is unquestionably Poly-ML [7], with which close connections have already been made. Poly-ML also subsumes previous proposals that encapsulate �rst-class polymorphic values within datatypes [25]. Odersky and Laufer’s proposal [20] also falls into this category; however, a side mechanism simultaneously allows a form of toplevel rank-2 quanti�cation, which is not covered by Poly-ML but is, we think, subsumed by MLF.

Rank-2 polymorphism actually allows for full type inference [13, 11]. However, the algorithm proceeds by reduction on source terms and is not very intuitive. Rank-2 polymorphism has also been incorporated in the Hugs implementation of Haskell [17], but with explicit type annotations. The GHC implementation of Haskell has recently been released with second-order polymorphism at arbitrary ranks [8]; however, types at rank 2 or higher must be given explicitly and the interaction of annotations with implicit types remains unclear. Furthermore, to the best of our knowledge, this has not yet been formalized. Indeed, type inference is undecidable as soon as universal quanti�ers may appear at rank 3 [14].

Although our proposal relies on the let-binding mechanism to introduce implicit polymorphismand �exible bounds in types to factorize all ways of obtaining type instances, there may still be some connection with intersection types [12], which we would like to explore. Our treatment of annotations as type-revealing primitives also resembles retyping functions (functions whose type-erasure η - reduces to the identity) [19]. However, our annotations are explicit and contain only certain forms of retyping functions. Type inference for System F modulo η -expansion is known to be undecidable as well [27].

Several people have considered partial type inference for System F [10, 1, 23] and stated undecidability results for some particular variants that in all cases amount—directly or indirectly—to permitting (and so forcing) inference of the type of at least one variable that can be used in a polymorphic manner, which we avoid.

Second-order uni�cation, although known to be undecidable, has been used to explore the practical effectiveness of type inference for System F by Pfenning [22]. Despite our opposite choice, that is not to support second-order uni�cation, there are at least two comparisons to be made. Firstly, Pfenning’s work does not cover the language ML per se, but only the λ -calculus, since let-bindings are expanded prior to type inference. Indeed, ML is not the simplytyped λ -calculus and type inference in ML cannot, in practice, be reduced to type inference in the simply-typed λ -calculus after expansion of let-bindings. Secondly, one proposal seems to require annotations exactly where the other can skip them: in [22], markers (but no type) annotations must replace type-abstraction and typeapplication nodes; conversely, this information is omitted in MLF, but instead, explicit type information must remain for (some) arguments of λ -abstractions.

Our proposal is implicitly parameterized by the type instance relation and its corresponding uni�cation algorithm. Thus, most of the technical details can be encapsulated within the instance relation. We would like to understand our notion of uni�cation as a particular case of second-order uni�cation. One step in this direction would be to consider a modular constraint-based presentation of secondorder uni�cation such as [5]. Flexible bounds might partly capture, within principal types, what constraint-based algorithms capture as partially unresolved multi-sets of uni�cation constraints. Another example of restricted uni�cation within second-order terms is uni- �cation under a mixed pre�x [18]. However, our notion of pre�x and its role in abstracting polytypes is quite different.

Actually, none of the above works did consider subtyping at all. This is a signi�cant difference with proposals based on local type inference [2, 24, 21] where subtyping is a prerequisite. The addition of subtyping to our framework remains to be explored.

Furthermore, beyond its treatment of subtyping, local type inference also brings the idea that explicit type annotations can be propagated up and down the source tree according to �xed well-de�ned rules, which, at least intuitively, could be understood as a preprocessing of the source term. Such a mechanism is being used in the GHC Haskell compiler, and could in principle be added on top of MLFas well.

Conclusions

We have proposed an integration of ML and System F that combines the convenience of type inference as present in ML and the expressiveness of second-order polymorphism. Type information is only required for arguments of functions that are used polymorphically in their bodies. This speci�cation should be intuitive to the user. Besides, it is modular, since annotations depend more on the behavior of the code than on the context in which the code is placed; in particular, functions that only carry polymorphism without using it can be left unannotated.

The obvious potential application of our work is to extend ML-like languages with second-order polymorphism while keeping full type inference for a large subset of the language, containing at least all ML programs. Indeed, we implemented a prototype of MLF and veri�ed on a variety of examples that few annotations are actually required and always at predictable places. However, further investigations are still needed regarding the syntactic-value polymorphism restriction and its possible relaxation.

Furthermore, on the theoretical side, we wish to better understand the concept of “�rst-order uni�cation of second-order terms”, and, if possible, to con�ne it to an instance of second-order uni�cation. We would also like to give logical meaning to our types and to the abstraction and instance relations.

7 References

[1] H.-J. Boehm. Partial polymorphic type inference is undecidable. In 26th Annual Symposium on Foundations of Computer Science, pages 339–345. IEEE Computer Society Press, Oct. 1985.

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

[3] R. D. Cosmo. Isomorphisms of Types: from lambda-calculus to information retrieval and language design. Birkhauser, 1995.

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

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

[6] J. Garrigue. Relaxing the value-restriction. Presented at the third Asian workshop on Programmaming Languages and Systems (APLAS), 2002.

[7] J. Garrigue and D. Rémy. Extending ML with semi-explicit higher-order polymorphism. Journal of Functional Programming, 155(1/2):134–169, 1999. A preliminary version appeared in TACS’97.

[8] The GHC Team. The Glasgow Haskell Compiler User’s Guide, Version 5.04, 2002. Chapter Arbitrary-rank polymorphism.

[9] P. Giannini and S. R. D. Rocca. Characterization of typings in polymorphic type discipline. In Third annual Symposium on Logic in Computer Science, pages 61–70. IEEE, 1988.

[10] J. James William O’Toole and D. K. Gifford. Type reconstruction with �rst-class polymorphic values. In SIGPLAN ’89 Conference on Programming Language Design and Implementation, Portland, Oregon, June 1989. ACM. also in ACM SIGPLAN Notices 24(7), July 1989.

[11] T. Jim. Rank-2 type systems and recursive de�nitions. Technical Report MIT/LCS/TM-531, Massachusetts Institute of Technology, Laboratory for Computer Science, Nov. 1995.

[12] T. Jim. What are principal typings and what are they good for? In ACM, editor, ACM Symposium on Principles of Programming Lan-

guages (POPL), St. Petersburg Beach, Florida, pages 42–53, 1996.

[13] A. J. Kfoury and J. B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second-order lambda -calculus. In ACM Conference on LISP and Functional Programming, 1994.

[14] A. J. Kfoury and J. B. Wells. Principality and decidable type inference for �nite-rank intersection types. In ACM Symposium on Principles of Programming Languages (POPL), pages 161–174. ACM, Jan. 1999.

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

[16] X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system, documentation and user’s manual - release 3.05. Technical report, INRIA, July 2002. Documentation distributed with the Objective Caml system.

[17] Mark P Jones, Alastair Reid, the Yale Haskell Group, and the OGI School of Science & Engineering at OHSU. An overview of hugs extensions. Available electronically, 1994-2002.

[18] D. Miller. Uni�cation under a mixed pre�x. Journal of Symbolic Computation, 14:321–358, 1992.

[19] J. C. Mitchell. Polymorphic type inference and containment. Information and Computation, 2/3(76):211–249, 1988.

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

[21] M. Odersky, C. Zenger, and M. Zenger. Colored local type inference. ACM SIGPLAN Notices, 36(3):41–53, Mar. 2001.

[22] F. Pfenning. Partial polymorphic type inference and higher-order uni- �cation. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 153–163. ACM Press, July 1988.

[23] F. 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.

[24] B. C. Pierce and D. N. Turner. Local type inference. In Proceedings of the 25th ACM Conference on Principles of Programming Languages, 1998. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), January 2000, pp. 1–44.

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

[26] 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, July 1994.

[27] J. B. Wells. Type Inference for System F with and without the Eta Rule. PhD thesis, Boston University, 1996.

[28] A. K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343–355, 1995.

A Uni�cation algorithm

The algorithm unify is speci�ed in Section 1.5; it takes a pre�x Q and two types τ and τ ′ and returns a pre�x that uni�es τ and τ ′ under Q (as described in Theorem 1) or fails. In fact, the algorithm unify is recursively de�ned by an auxiliary uni�cation algorithm for polytypes: polyunify takes a pre�x Q and two type schemes σ _{1} and σ _{2} and returns a pair ( Q′, σ ′) such that Q ⊑ Q′ and ( Q′) σ _{1} ⊑ σ ′ and ( Q′) σ _{2} ⊑ σ ′.

The algorithms unify and polyunify are described in Figure 8. For the sake of comparison with ML, think of the input pre�x Q

Figure 8. Uni�cation algorithm

unify ( Q, τ ′′, τ ′′′)

— �rst rewrites all bounds of Q in normal form and proceeds by case analysis on ( τ ′′, τ ′′′) :

Case ( α , α ) : return Q.

Case ( g τ _{1}^{1} . . τ _{1}^{n}, g τ _{2}^{1} . . τ _{2}^{n}) :

• let Q^{1} be Q in

• let Q^{i+ 1} be unify ( Q^{i}, τ _{1}^{i}, τ _{2}^{i}) for 1 ⩽ i ⩽ n in

• return Q^{n+ 1}.

Case ( g_{1} τ _{1}^{1} . . τ _{1}^{p}, g_{2} τ _{2}^{1} . . τ _{2}^{q}) with g_{1} ≠ g_{2}: fail.

Case ( α , τ ) or ( τ , α ) when ( α ⋄ τ ′) ∈ Q:

• return unify ( Q, τ , τ ′) .

Case ( α , τ ) or ( τ , α ) when ( α ⋄ σ ) ∈ Q and τ ∉ dom( Q) and σ ∉ T

• let ( Q′, _) be polyunify ( Q, σ , τ ) in

• fail if ( α ⋄ σ ) ∉ Q′.

• return ( Q′) ⇐ ( α = τ )

Case ( α _{1}, α _{2}) when ( α _{1}⋄ _{1}σ _{1}) ∈ Q and ( α _{2}⋄ _{2}σ _{2}) ∈ Q and

α _{1} ≠ α _{2} and σ _{1}, σ _{2} are not in T .

• let ( Q′, σ _{3}) be polyunify ( Q, σ _{1}, σ _{2}) in

• fail if ( α _{1}⋄ _{1}σ _{1}) ∉ Q′ or if ( α _{2}⋄ _{2}σ _{2}) ∉ Q′

• return ( Q′) ⇐ ( α _{1}⋄ _{1}σ _{3}) ⇐ ( α _{2}⋄ _{2}σ _{3}) ⇐ α _{1}∧ α _{2}.

polyunify ( Q, σ _{1}, σ _{2})

— requires σ _{1}, σ _{2}, and all bounds in Q to be in normal form^{1} :

Case ( ⊥ , σ ) or ( σ , ⊥ ) : return ( Q, σ )

Case ( ∀ ( Q_{1}) τ _{1}, ∀ ( Q_{2}) τ _{2}) with Q_{1}, Q_{2}, and Q having disjoint domains (which usually requires renaming σ _{1} and σ _{2})

• let Q_{0} be unify ( QQ_{1}Q_{2}, τ _{1}, τ _{2}) in

• let ( Q_{3}, Q′) be Q_{0}↑ dom( Q) in

• return ( Q_{3}, ∀ ( Q′) τ _{1})

1Actually, only need to replace types of the form ∀ ( α ⋄ σ ) α by σ , which can always be done lazily.

given to unify as a substitution and of the result pre�x Q′ as an instance of Q (i.e. a substitution of the form Q′′ ∘ Q) that uni�es τ and τ ′. First-order uni�cation of polytypes essentially follows the general structure of �rst-order uni�cation of monotypes. The main differences are that (i) the computation of the unifying substitution is replaced by the computation of a unifying pre�x, (ii) additional work must be performed when a variable bound to a strict polytype (i.e. other than ⊥ and not equivalent to a monotype) is being uni- �ed: bounds must be further uni�ed (last case of polyunify) and the pre�x updated accordingly. Auxiliary algorithms are used for this purpose.

Let a rearrangement of a pre�x Q be a pre�x equivalent to Q obtained by a permutation of bindings of Q.

DEFINITION 9. The split algorithm Q↑ ¯ α takes a pre�x Q and returns a pair of pre�xes ( Q_{1}, Q_{2}) such that (i) Q_{1}Q_{2} is a rearrangement of Q, (ii) ¯ α ⊆ dom( Q_{1}) , and (iii) dom( Q_{1}) is minimal (in other words, Q_{1} contains only bindings of Q useful for exporting the interface ¯ α, and Q_{2} contains the rest).

Figure 9. Algorithm WF

infer ( Q, Γ , a) :

— proceeds by case analysis on expression a :

Case x: return Q, Γ ( x)

Case λ ( x) a:

• let Q_{1} = ( Q, α ≥ ⊥ ) with α ∉ dom( Q)

• let ( Q_{2}, σ ) = infer ( Q_{1}, Γ , x : α , a)

• let β ∉ dom( Q_{2}) and ( Q_{3}, Q_{4}) = Q_{2}↑ dom( Q)

• return Q_{3}, ∀ ( Q_{4}) ∀ ( β ≥ σ ) α → β

Case a b:

• let ( Q_{1}, σ _{a}) = infer ( Q, Γ , a)

• let ( Q_{2}, σ _{b}) = infer ( Q_{1}, Γ , b)

• let α _{a}, α _{b}, β ∉ dom( Q_{2})

• let Q_{3} = unify ( ( Q_{2}, α _{a} ≥ σ _{a}, α _{b}≥ σ _{b}, β ≥ ⊥ ) ,

α _{a}, α _{b} → β )

• let ( Q_{4}, Q_{5}) = Q_{3}↑ dom( Q)

• return ( Q_{4}, ∀ ( Q_{5}) β )

Case let x = a_{1} in a_{2}: • let ( Q_{1}, σ _{1}) = infer ( Q, Γ , a_{1})

• return infer ( Q_{1}, ( Γ , x : σ _{1}) , a_{2})

DEFINITION 10. The abstraction-check algorithm ( Q) σ ⊏ − ^{?} σ ′ takes a pre�x Q and two polytypes σ and σ ′ such that ( Q) σ ⊑ σ ′ and checks that ( Q) σ ⊏ − σ ′ or fails otherwise.

DEFINITION 11. The update algorithm Q ⇐ ( α ⋄ σ ) takes a pre�x Q and a binding ( α ⋄ σ ) such that α is in the domain of Q and returns a pre�x ( Q_{0}, α ⋄ σ , Q_{1}) such that (i) ( Q_{0}, α ⋄ ′ σ ′, Q_{1}) is a rearrangement of Q and (ii) dom( Q_{1}) ∩ ftv( σ ) = /0. The algorithm fails when there is not such decomposition (because of circular dependencies) or when ⋄ ′ is = and ( Q) σ ′ ⊏ − ^{?} σ fails.

DEFINITION 12. The merge algorithm Q ⇐ α ∧ α ′ takes two variables α and α ′ and a pre�x of the form ( Q_{0}, α ⋄ σ , Q_{1}, α ′ ⋄ ′ σ ′, Q_{2}) and returns the pre�x ( Q_{0}, α ⋄ ′′ σ , Q_{1}, α ′ = α , Q_{2}) where ⋄ ′′ is ≥ if both ⋄ and ⋄ ′ are ≥ , and ⋄ ′′ is = otherwise.

The implementation of algorithms split, update, and merge is straightforward. The algorithm abstraction-check can be reduced to a simple check on the structure of paths, thanks to the assumption ( Q) σ ⊑ σ ′. By lack of space, they are all omitted.

B Type inference algorithm

Figure 9 de�nes the type-inference algorithm WF for MLF. The algorithm follows the algorithm W for ML, with only two differences: �rst, the algorithm builds a pre�x Q instead of a substitution; second, all free type variables not in Γ are quanti�ed at each abstraction or application. Since free variables of Γ are in dom( Q) , �nding quanti�ed variables consists in splitting the current pre�x according to dom( Q) , as described by De�nition 9.