UNITÉ DE RECHERCHE INRIA-ROCQUENCOURT

Institut National de Recherche en Informatique et en Automatique

Domaine de Voluceau

Rocquencourt B.P. 105

78153 Le Chesnay Cedex

France Tél.:(1)39 63 55 11

Rapports de Recherche

N^{∘}1766

Programme 2

Calcul symbolique, Programmation et Génie logiciel

EXTENSION OF ML TYPE SYSTEM WITH A SORTED EQUATIONAL THEORY ON TYPES

Didier Rémy

Octobre 92

Extension of ML type system with a sorted equational theory on types

Didier Rémy INRIA-Rocquencourt^{∗}

∗Author’s address: INRIA, B.P. 105, F-78153 Le Chesnay Cedex. Email: Didier.Remy@inria.fr

Extension of ML type system with a sorted equational theory on types

Abstract

We extend the ML language by allowing a sorted regular equational theory on types for which unification is decidable and unitary. We prove that the extension keeps principal typings and subject reduction. A new set of typing rules is proposed so that type generalization is simpler and more efficient. We consider typing problems as general unification problems, which we solve with a formalism of unificands. Unificands naturally deal with sharing between types and lead to a more efficient type inference algorithm. The use of unificands also simplifies the proof of correctness of the algorithm by splitting it into more elementary steps.

Extension du système de type de ML par une théorie équationnelle avec sortes sur les types

Résumé

Le typage du langage ML est étendu en considérant les types modulo une théorie équationnelle régulière avec sortes pour laquelle l’unification est décidable. Cette extension conserve la propriété d’avoir un type principal ainsi que la conservation de la propriété d’être bien typé par β-réduction des programmes. Un nouvel ensemble de règles de typage est proposé de telle sorte que la généralisation de type est à la fois plus simple et plus efficace. Les problèmes de typage sont considérés comme des problèmes généraux d’unification que nous résolvons en utilisant le formalisme des unificandes. Les unificandes expriment naturellement le partage entre les types et conduit à un algorithme d’inférence de types plus efficace. L’utilisation des unificandes simplifie également les preuves de correction des algorithmes en les séparant des étapes élémentaires.

Introduction

The ML language introduced by R. Milner in 1978 has become very poplular, which is partly due to the possibility of inferring principal types for programs [DM82, Dam85]. This is a consequence of the restriction of arbitrary quantification as in the polymorphic lambda calculus to prenex-quantification in ML. However, viewing ML as a restriction of the polymorphic lambda calculus is sometimes misleading: ML terms are untyped terms (Church’s view) while terms of the polymorphic lambda calculus are usually considered as typed terms (Curry’s view). A consequence of the Church view of ML is that the order in which quantifiers appear in types is insignificant, and useless quantifications over non free variables can be removed, which leads to a simpler formulation of the typing rules, where type schemes are simply pairs of a set of bound variables and a simple type.

Some presentations of the ML typing rules, called “syntax directed”, are such that all typing derivations of the same program have the same structure. They are usually used as the basis for finding type inference algorithms. Typechecking in ML can also be defined as typechecking with simple types after reduction of all Let redexes. This approach, which is closer to the conjunctive-type discipline than to the polymorphic lambda-calculus, simplifies the typing rules, but unfortunately, it leads to inefficient algorithms. All these variants of the typing rules have been used in the literature, but their equivalence with the Damas-Milner’s formulation has not always been shown. Moreover, some of them have been taken as the basis for extensions of ML for which complete proofs of the main properties are often omitted.

The main goal of this article is to study one of these extensions: Types of ML are taken modulo an equational theory. The main result is theorem 4 that claims principal typings in such an extension. The proof is constructive and comes with the accompanying algorithm 3 for type inference. This extension nicely formalizes type abbreviations in ML. More importantly, there is a type system for extensible records in ML that uses an equational theory on types [Rém91].

The typing rules are those of the Damas Milner type system, and the most common variations from the original presentation are shown equivalent. Indeed this includes the core ML language as an instance. All classical results of the core ML language also hold for this extension.

Type inference is closely related to unification by considering typing problems as unificands. In this presentation, proofs of soundness and correctness of the type inference algorithm are simpler. The algorithm itself is described as a set of transformations on unificands. This approach is more general and control is flexible. The standard algorithm is obtained when priority is given to unification problems and typing problems are reduced in a leftmost outermost order. With fewer control, transformation rules can be easily interpreted as a logic program, similarly to the one given for Mini-ML [CDDK86]. But the benefit of treating typing problems as unificands is essentially the efficiency obtained by sharing as much as possible between types, and in all phases of type inference. This results from the possibility of viewing canonical system of multi-equations as terms, substitutions or graphs, interchangeably.

Another contribution of this work is to avoid a source of inefficiency that is present in the classical syntax-directed typing rules: Generalizable variables are defined as those that do not appear in the typing context. The cost of generalization may increase with the size of the context, and especially with the size of types bound in the context. By assigning ranks to variables as a measure of their freshness we obtain a new syntax-directed system where generalization only applies to freshest variables. Ranks can be computed incrementally by extending unification to ranked unification.

In the first section, we present our extension of ML and the typing rules with different formulations that are shown equivalent. In section 2, a more efficient syntax-directed system is presented and proved equivalent to the previous formulations. Unification as transformations of unificands is recalled in section 3 and extended to ranked unification. In section 4, we study type inference as the simplification of typing problems; we give a set of transformation rules that reduce all typing problems to unification problems. A few extensions to the core language, and some instances with practical equational theories are described in the last section. A real implementation of the algorithm based on unificands and ranked unification is described in the appendix A.

Definitions are not delimited by theorem like structures, but are indicated by emphasizing the defining occurrences of mathematical words.

1 The original Damas-Milner’s system and its many variants

In this section, we present the original Damas-Milner’s, and some of its many variants. We prove the equivalence of all presentations.

The language of expressions of ML is defined by the following BNF grammar:

M ::=  Terms  M, N
x  Variable  x, y  Var
| λ x. M  Abstraction  Fun
| M M  Application  App
| let x = M in M  Let binding  Let

The expressions of ML are considered modulo α-conversion. The substitution of x by N in M is noted [N/x]M. If necessary, it renames bound variables of M in order to avoid capture.

When adding axioms to types it is sometime useful to restrict types by sorts: they may restrict the equality on terms by leaving fewer instances of the axioms. An example is given in section 5. Thus we consider sorted types.

Let K be a set of atoms called sorts, containing at least one element ι. Letter κ ranges over sorts. Signatures are non empty sequences of sorts. We write κ for an atomic signature, and κ_{1} ⊗ … κ_{p} ⇒ κ_{0} for a longer sequence. We are also given a set of symbols C with a mapping Σ from C to signatures, also called the signature of C. The arity of a symbol is the predecessor of the length of its signature. Letters f, g and h range over symbols. We assume that C contains at least a distinguished infix arrow symbol → of signature ι ⊗ ι ⇒ ι. Let V be an enumerable set of variables with infinitely many variables of every sort V_{κ∈K}^{κ}. We write W the set of subsets of V. Types of ML are terms of the free sorted algebra T (Σ, V). We abbreviate T (Σ, V) as T , and write for T (W) the set of terms whose variables are in W, and T^{κ} the set of terms of sort κ. Letters τ, σ and ρ range over arbitrary types. We write V(τ) the set of (free) variables of τ and V^{κ}(τ) those of sort κ.

The non sorted case is obviously an instance of the restricted sorted case where K is reduced to the sort ι, and signatures are reduced to arities. The signature of the arrow symbol and the restriction on the signature of typing judgements below make it possible to think in term of arities, identifying the sets T^{ι} and T . Places were the sorted case has to be considered more carefully are emphasized everywhere.

Substitutions are sort preserving mappings from a finite set of variables to terms. There are extended to mappings from terms to terms by compatibility with the structure of algebra. Letters μ, ν and ξ range over substitutions of T ; D(μ) and I(μ) are the domain and the codomain of μ, respectively. We also write μ : X → Y for a substitution of domain X that ranges in Y. The one element substitution that sends α to τ is simply written α ↦ τ. If W is a set of variables, μ |` W is the restriction of μ to W and μ \ W is the restriction of μ outside of W, i.e. μ |` (V \ W).

We extend types of ML by taking them modulo an equational theory. A regular equational theory E is one such that two equal terms always have the same set of variables. We assume that a regular equational theory E on the algebra T is provided. We write T /E for the terms taken modulo the equations. We often consider the terms of T and manipulate their equality explicitly.

Since different type systems will use slightly different definition of type schemes, we parameterize the definitions by a set of type schemes Q. Type schemes are sorted just like types of T . A Q-context with respect to a set Q is a partial function from the set of term variables to Q. If A is a Q-context, x is a variable and q is an element of Q, we write A[x : q] the function that is equal to A everywhere except on x to which it associates q. A one-element context [x : q] is called an assertion. We write C(Q) for the set of Q-contexts.

Contexts need not have finite domains. For type inference though, there must exist an algorithm that given a term variable returns the type to which it is bound in the context, or fails if the variable is not bound in the the context, and a semi-algorithm that enumerates type variables that are not in the free variables ofa the context. A typing relation ( ⊢ : ) is a subset of C(Q^{ι}) × ML × Q^{ι}.

Typing relations are only defined for contexts and type-objects of the sort ι. An inference rule is an implication R, parameterized by a relation ⊢ in C(Q^{ι}) × ML × Q^{ι}, written \frac{A}{B} (R) where A and B are typing relations. The notation ⊢ stands for an arbitrary relation: it does not make sense to ask whether a rule that depends on ⊢ is true or false until the parameter ⊢ is filled with a defined relation ⊢_{R}. A typing relation ⊢_{R} is defined as the smallest relation that satisfies a set of inference rules R. In typing rules, we use concrete syntax for ML terms. However the typing relation must be stable with respect to α-conversion of programs. This will be the case for all typing relations that will be defined here. In fact, terms could be represented using De Bruijn indices; contexts would then be just sequences of type schemes.

A derivation of a judgement A ⊢_{R} M : q is a constructive proof of this judgement where each step is an instance of an inference rules. Any valid judgement has at least one derivation. A proof of a judgement by structural induction is a proof by induction on the number of steps then by cases on the last rule used in a derivation of the judgement.

The set of Damas-Milner type schemes is the smallest set S that contains T and that is closed by

s ∈ S, α ∈ V ⟹ ∀ α · s ∈ S

The free variable function V is extended to type schemes by

V(∀ α · s) = V(s) \ {α}

Substitutions are also extended to type schemes by

μ(∀ α · s) = ∀ α · (μ \ {α})(s)

and to contexts as pointwise substitution. The sort of a type scheme is the one of the type obtained by stripping all quantifiers.

The original Damas-Milner typing relation for ML is defined on C(S^{ι}) × ML × S^{ι} by the set of the inference rules of figure 1.

Originally, type schemes are not equal modulo the re-ordering of quantifiers and renaming of bound variables. We define ∀-equality on type schemes as the smallest congruence that contains all pairs

∀ α · ∀ β · s =_{∀} ∀ β · ∀ α · s
∀ β · s =_{∀} s  and  ∀ α · s =_{∀} ∀ β · (α ↦ β)(s) if β ∉ V(s)

We naturally extend ∀-equality to contexts.

\begin{aligned}x : s ∈ A \\ & (Var) \\ A ⊢_{DM} x : s \end{aligned} A ⊢_{DM} x : ∀ α · s (Inst)

A ⊢_{DM} x : (α ↦ σ)(s)

\begin{aligned}A[x : τ] ⊢_{DM} M : σ τ ∈ T \\ & (Fun) \\ A ⊢_{DM} λ x. M : τ → σ \end{aligned} A ⊢_{DM} M : σ → τ A ⊢_{DM} N : σ (App)

A ⊢_{DM} M N : τ

\begin{aligned}A ⊢_{DM} x : s α ∉ V(A) \\ & (Gen) \\ A ⊢_{DM} x : ∀ α · s \end{aligned} A ⊢_{DM} M : s A[x : s] ⊢_{DM} N : σ (Let)

A ⊢_{DM} let x = M in N : σ

A ⊢_{DM} M : σ σ =_{E} τ (Equal)

A ⊢_{DM} M : τ

Figure 1: Damas-Milner’s Typing rules (DM)

It is immediate to prove

\frac{A ⊢_{DM} M : s  s =_{∀} s′}{A ⊢_{DM} M : s′}  (∀-Equal)

Moreover, the property extends to contexts:

\frac{A ⊢_{DM} M : s  A =_{∀} B}{B ⊢_{DM} M : s}  (∀-Context)

The proof is an easy structural induction on the derivation of A ⊢_{DM} M : s. Therefore, type schemes can be taken modulo ∀-equality. We now consider substitutions modulo ∀-equality. We write ∀ {α} ∪ W · τ for ∀ α · ∀ W · τ or also ∀ α, W · τ when W does not contain α. Consistently, with ∀-equality, we take ∀ W · τ to be ∀ (V(τ) ∩ W) · τ when W is infinite. We write ∀ W · T the set of type schemes modulo ∀-equality.

We call DM′ the set of rules DM modulo ∀-equality. It is defined on C(∀ W · T^{ι}) × ML × ∀ W · T^{ι} by the set of inference rules of figure 2. Using lemmas ∀-Equal and ∀-Context,

\begin{aligned}x : ∀ W · τ \\ & (Var) \\ A ⊢_{DM}′ x : ∀ W · τ \end{aligned} A ⊢_{DM}′ x : ∀ α, W · τ (Inst)

A ⊢_{DM}′ x : ∀ W · (α ↦ σ)(τ)

\begin{aligned}A[x : τ] ⊢_{DM}′ M : σ τ ∈ T \\ & (Fun) \\ A ⊢_{DM}′ λ x. M : τ → σ \end{aligned} A ⊢_{DM}′ M : σ → τ A ⊢_{DM}′ N : σ (App)

A ⊢_{DM}′ M N : τ

A ⊢_{DM}′ x : ∀ W · τ α ∈ V(τ) \ W \ V(A) (Gen)

A ⊢_{DM}′ x : ∀ α, W · s

A ⊢_{DM}′ M : s A[x : s] ⊢_{DM}′ N : σ (Let)

A ⊢_{DM}′ let x = M in N : σ

A ⊢_{DM}′ M : σ σ =_{E} τ (Equal)

A ⊢_{DM}′ M : τ

Figure 2: Variant of Damas Milner’s typing rules (DM)

the relations ⊢_{DM} and ⊢′_{DM} are easily proved equal modulo ∀-equality. The system DM′ has still unnecessary freedom on places where generalization and instantiation may occur.

We now consider typing relations in C(∀ W · T^{ι}) × ML × T^{ι}, where type schemes may appear only in contexts. The system S, composed of the rules Fun, App and Equal of figure 2 plus the rules of figure 3, is such that at most one rule other than the equality rule can apply for each syntactic construct of the language; it is said syntax-directed.

\frac{x : ∀ W · τ ∈ A  μ : W → T}{A ⊢_{S} x : μ(τ)}  (Var-Inst)

\frac{A ⊢_{S} M : τ  A[x : ∀ W · τ] ⊢_{S} N : σ  W ∩ V(A) = ∅}{A ⊢_{S} let x = M in N : σ} (Gen-Let)

Figure 3: Syntax-directed rules for system (S)

Lemma 1 (Substitution lemma in S) The relation ⊢_{S} is stable by substitution.

\frac{A ⊢_{S} M : τ}{μ(A) ⊢_{S} M : μ(τ)}  (Sub)

A weaker instance of the lemma is often used:

\frac{A ⊢_{S} M : τ  D(μ) ∩ V(A) = ∅}{A ⊢_{S} M : μ(τ)}  (Sub’)

\underline{Proof}: See section 2.1.

Lemma 2 If W is disjoint from V(A), the judgements A ⊢_{DM}′ M : ∀ W · τ and A ⊢_{S} M : τ are equivalent.

\underline{Proof}: The rule Var-Inst can be proved for ⊢_{DM}′, using the rules Var and Inst. The rule Gen-Let can be proved for ⊢_{DM}′ using the rules Gen and Let. This shows that ⊢_{S} is a subrelation of ⊢_{DM}′. Conversely, we reason by structural induction on the judgement A ⊢_{DM}′ M : ∀ W · τ.

Case Var, Fun, App, Equal: The judgement A ⊢_{S} M : τ follows from the induction hypothesis applied to all premises of the last rule in the derivation of A ⊢_{DM}′ M : τ, and the corresponding rule in S.

Case Gen: The judgement A ⊢_{S} M : τ follows directly from the induction hypothesis applied to the premise.

Case Inst: After renaming, the derivation in DM′ ends with

\frac{A ⊢_{DM}′ M : ∀ α, W · τ}{A ⊢_{DM}′ M : ∀ W · (α ↦ σ)(τ)}

where W and α are disjoint from V(A). By the induction hypothesis, we know that A ⊢_{S} M : τ holds. We conclude by applying the Sub’ rule with the substitution α ↦ σ

Case Let: The derivation in DM′ is of the form

\frac{A ⊢_{DM}′ M : ∀ W · τ  A[x : ∀ W · τ] ⊢_{DM}′ N : σ}{A ⊢_{DM}′ let x = M in N : σ}  (Let)

After renaming, we assume that W is disjoint from A. Applying the induction hypothesis to both premises produces:

A ⊢_{S} M : τ  and  A[x : ∀ W · τ] ⊢_{S} N : σ

Since W is disjoint from A, the conclusion follows by applying the Gen-Let rule.

2 A simple and efficient presentation of ML type system

The inference rules of system S are syntax directed, that is, there is only one rule other than the equality rule that can end the derivation of all typings of one construct of the language. There is an obvious type inference algorithm W obtained by reading the rules from bottom to top as rewriting rules. Directed by the syntax of the program, the algorithm finds the unique non equality rule that can be used last, instantiate it appropriately, and recursively calls the algorithm with smaller typing inference problems or unification problems.

Typing the program let x = M in N in an environment A first requires typing M in A, which returns some type τ and a substitution μ, then typing N in μ(A)[x : ∀ V(τ) \ V(A) · τ]. This requires the computation of the set of variables V(τ) \ V(A) that can be quantified in τ, which can be excessively expensive, since it does not only depend on the expression M but also on the size and the structure of the context A. The term M may contain a free variable x that is assigned a large monomorphic type σ. The part of τ that comes from σ only contains variables that are also in A and thus are inspected unnecessarily.

There is another, even simpler, presentation of the ML type system that leads to an algorithm where typing M in a context A only depends on the polymorphic parts of types assigned to the free variables of M.

Let ϕ be a mapping, called rank, of V into IN such that there are infinitely many variables of every rank. We write V^{n} the set of variables of rank exactly n and V_{n} the set of variables of rank at most n. We extend rank to terms: the rank of a term is the maximum rank of its variables. We write T_{n} the set of terms of rank at most n, that is T (V_{n}). Substitutions are restricted to rank decreasing ones, which are stable by composition.

Type schemes ∀ W · T_{n} are taken modulo α-conversion in T , without taking ranks of bound variables into account. We recall that ∀ V^{n+1} · τ is ∀ (V^{n+1}(τ)) · τ by definition. It is in T_{n} provided τ is in T_{n+1}. A type scheme of ∀ W · T_{n} can always be written indefferently ∀ V^{n+1} · τ with τ in T_{n+1}, or ∀ W · τ with W and τ in V^{n}.

We recursively define the typing relations ⊢_{n} in C(∀ W · T_{n}^{ι}) × ML × T_{n}^{ι} by the rules of figure 4:

x : ∀ W · τ ∈ A μ : W → T_{n} \overline{(Var-Inst)}

A ⊢_{n} x : μ(τ)

A[x : τ] ⊢_{n} M : σ ; \overline{(Fun)} ; A ⊢_{n} λ x. M : τ → σ  A ⊢_{n} M : σ → τ  A ⊢_{n} N : σ ; \overline{(App)} ; A ⊢_{n} M N : τ

A ⊢_{n+1} M : τ A[x : ∀ V^{n+1} · τ] ⊢_{n} N : σ \overline{(Gen-Let)}

A ⊢_{n} let x = M in N : σ

A ⊢_{n} M : σ σ =_{E} τ \overline{(Equal)}

A ⊢_{n} M : τ

Figure 4: Hierachical typing rules

Lemma 3 (Substitution lemma) The relations ⊢_{n} are stable under substitution. That is the rule

\frac{A ⊢_{n} M : τ}{μ(A) ⊢_{n} M : μ(τ)}  (Sub)

is provable.

\underline{Proof}: We prove “for all substitutions μ, for all integers n, if A ⊢_{n} M : τ is derivable by Δ, then μ(A) ⊢_{n} M : μ(τ) is derivable”, first by induction on the structure of Δ, then by cases on the last rule of Δ.

Case Equal: Equality is stable by substitution.

Case Var: We know from the hypothesis A ⊢_{n} x : τ that there exists x : ∀ W · σ is in A and a substitution ν : W → T_{n} that sends σ to τ. We can choose W be V^{n+1}. Let ξ be (μ ∘ ν) |` V^{n+1}. It sends W into T_{n}. Since the domain of ν is disjoint from V_{n}, the substitution ξ ∘ (μ |` V_{n}) is equal to μ ∘ ν. Thus ξ sends (μ \ W)(σ) to μ(τ). Therefore we can derive the conclusion μ(A) ⊢_{n} x : μ(τ).

Case App, Fun: Apply the induction hypothesis to the premises, and conclude with the same rule.

Case Let: We know from the hypothesis that there exists σ in V_{n+1} such that A ⊢_{n+1} M : σ and A[x : ∀ V^{n+1}(σ) · σ] ⊢_{n} N : τ are derivable. The conclusion follows by applying the Letrule to the substitution of both judgements by μ |` V_{n}.

The assertion x : ∀ V^{n+1} · τ is said to be smaller at rank n than the assertion x : ∀ V^{n+1} · σ if τ can be taken in T_{n+1} such that there exists a substitution μ with domain V^{n+1} that maps τ to σ. A context A is said to be smaller at rank n than a context B if it is pointwise smaller at rank n. We write A ⊂_{n} B.

Lemma 4 (Generalization of context) The relation ⊢_{n} is stable under generalization of context.

\frac{A ⊢_{n} M : τ  B ⊂_{n} A}{B ⊢_{n} M : τ}  (C-Gen)

\underline{Proof}: The proof is by structural induction on the premise.

Case Var: We know from the hypothesis A ⊢ x : τ that there is an assertion x : ∀ W · σ in A and a substitution μ with domain W that takes σ to τ. The set W can always be taken in V^{n+1}. Since B is smaller than A at rank n, there is a substitution ν of domain V^{n+1} that takes ρ to σ such that x : ∀ V^{n+1} · ρ is in B. The substitution μ ∘ ν with domain included in V^{n+1} takes ρ to τ, therefore we can conclude B ⊢_{n} M : τ.

Others cases: They are immediate.

Lemma 5 The relations ⊢_{n} are stable under E-equality.

\frac{A ⊢_{n} M : τ  A =_{E} B}{B ⊢_{n} M : τ}  (C-Equal)

\underline{Proof}: Intuitively, replace every Var-Inst rules in a derivation by a Var-Inst rule followed by an equality rule. Formally, the proof is by structural induction.

2.1 Equivalences

Lemma 6 For any context A and any type τ both of rank at most n, the judgements A ⊢_{n} M : τ and A ⊢_{S} M : τ are equivalent.

\underline{Proof}: The typing relations ⊢_{n} are clearly sub-relations of ⊢_{S}. Conversely, we reason by structural induction on the judgement A ⊢_{S} M : τ.

Case Let: We could derive

\frac{A ⊢_{S} M : τ A[x : ∀ W · τ] ⊢_{S} N : σ}{A ⊢_{S} let x = M in N : σ}

where W is equal to V(τ) \ V(A). We cannot use the rule Sub in S here, since we want to use the equivalence that we are presently proving to deduce rule Sub in S from rule Sub in H. However, the derivations of S are stable by global α-conversion. Therefore the restricted case of Sub for renamings is obviously true in S, and we can rename variables of W so that they are of rank n + 1. Then, both premises are well-formed and by the induction hypothesis we derive

A ⊢_{n+1} M : τ  and  A[x : ∀ W · τ] ⊢_{n} N : σ

in ML. Since W is exactly V^{n+1}(τ), we conclude A ⊢_{n} let x = M in N : σ.

Case Var, Fun, App, Equal: All cases are easy or similar to the Let case.

Using this equivalence, the lemmas C-Gen and Sub of H can easily be prooved in S. The substitution lemma for ⊢_{S} (lemma 1) is:

\frac{A ⊢_{S} M : τ}{μ(A) ⊢_{S} M : μ(τ)}  (Sub)

\underline{Proof}: Assume that A ⊢_{S} M : τ is valid. We can always choose the function rank such that the free variables of A and τ and variables of both the domain and the range μ are of rank 0. Applying the substitution lemma in H proves the judgement μ(A) ⊢_{0} M : μ(τ) which is equivalent to the judgement μ(A) ⊢_{S} M : μ(τ).

The assertion x : ∀ W · τ is said to be smaller than the assertion of x : ∀ W′ · τ′ if there exists a substitution μ with domain W that takes τ to τ′, and W′ is included in the range of μ. A context A is said to be smaller that B if it is pointwise smaller.

Lemma 7 (Generalization of context) The relation ⊢_{S} is stable under generalization of context.

\frac{A ⊢_{S} M : τ  B ⊂ A}{B ⊢_{S} M : τ}  (C-Gen)

\underline{Proof}: Assume that A ⊢_{S} M : τ and B ⊂ A. We can always choose the function rank such that free variables of A, B and τ are of rank 0. Then A ⊢_{0} M : τ and B ⊂_{0} A. By lemma C-Gen for H, we conclude B ⊢_{0} M : τ and by the equivalence of H and S, we get B ⊢_{S} M : τ.

2.2 Typing and reduction

Lemma 8 (Context restriction) If A and B are equal on free variables of M, the judgements A ⊢_{S} M : τ and B ⊢_{S} M : τ are equivalent.

\underline{Proof}: By symmetry, it is only necessary to show one direction. The proof is an easy structural induction on the premise.

We define a relation on C(∀ W · T^{ι}) × ML × ML as

A ⊢ M ⊂ M′ ⟺ ∀σ ∈ T^{ι}, A ⊢_{S} M : σ ⟹ A ⊢_{S} M′ : σ

Theorem 1 (Term substitution)

\frac{A ⊢_{S} [M/x]N : τ A ⊢ M ⊂ M′}{A ⊢_{S} [M′/x]N : τ}

\underline{Proof}: We assume A ⊢ M ⊂ M′ and we show

\frac{A′ ⊢_{S} [M/x]N : τ}{A′ ⊢_{S} [M′/x]N : τ}

for contexts A′ that extend A, by induction on the structure of N. We may always assume that bound variables of N are not in the domain of A (and consequently distinct from free avriables of M and M′).

Case N is x: The terms [M/x]N and M are equal. Thus there exists a proof of A′ ⊢_{S} M : τ, and consequently there is also a derivation of A′ ⊢_{S} M′ : τ, which is a derivation of A ⊢_{S} [M′/x]N : τ.

Case N is y: The term [M/x]N and [M′/x]N are equal.

Case N is let y = [M/x]N_{1} in [M/x]N_{2}: The first non equality rule that ends the derivation of A′ ⊢_{S} [M/x]N : τ is necessarily a Gen-Let rule.

\frac{A′ ⊢_{S} [M/x]N_{1} : τ_{1} A′[y : ∀ W · τ_{1}] ⊢_{S} [M/x]N_{2} : τ_{2}}{A ⊢_{S} let y = [M/x]N_{1} in [M/x]N_{2} : τ_{2}}

such that τ_{2} is E-equal to τ. Since y is not free in M or M′, we can apply the induction hypothesis to both premises, then rule Gen-Let, and conclude with an equality rule.

Case N is N_{1} N_{2} or N is λ y. N_{1}: These cases are similar to case Let.

Corollary 9 If W is disjoint from A, and x is not free in M, then

\frac{A ⊢_{S} M : σ A[x : ∀ W · σ] ⊢_{S} N : τ}{A ⊢_{S} [M/x]N : τ}

\underline{Proof}: Since x is not free in M, we have A[x : ∀ W · σ] ⊢_{S} M : σ by context restriction. Rule Sub’ shows that A[x : ∀ W · σ] ⊢_{S} x ⊂ M. Applying the term substitution theorem 1 with context A[x : ∀ W · σ], and terms x for M and M for M′, we get A[x : ∀ W · σ] ⊢ [M/x]N : τ and the conclusion follows from the context-restriction lemma.

Corollary 10 (Subject reduction)

\frac{A ⊢_{S} (λ x. N) M : τ}{A ⊢_{S} [M/x]N : τ}  and  \frac{A ⊢_{S} let x = M in N : τ}{A ⊢_{S} [M/x]N : τ}

\underline{Proof}: In each case, the premise implies that there exist a type σ and a set of variables W taken outside of A (W is empty in the first rule) such that

A ⊢_{S} M : σ A[x : ∀ W · σ] ⊢_{S} N : τ

We conclude by previous corollary.

The reverse of subject reduction does not hold, since if x does not occur in N, then M may not be typable while N is. A slightly weaker property is term expansion.

Lemma 11 (Term expansion)

\frac{A ⊢_{S} M : σ A ⊢_{S} [M/x]N : τ}{A ⊢_{S} let x = M in N : τ}

holds in S.

\underline{Proof}: The proof assumes theorem 4 which is shown in section 4 independently of this lemma (there is also another but longer proof of the lemma that does not use theorem 4). We assume A ⊢_{S} M : σ. Theorem 4 ensures that there is a principal typing A ⊢_{S} M : σ′ for the typing problem A ▷ M : β. We write W the set of variables of σ′ that do not appear in A. We show

\frac{A′ ⊢_{S} [M/x]N : τ}{A′[x : ∀ W · σ′] ⊢_{S} N : τ}

for all context A′ that extend A, by induction on N. The lemma will follow immediately by a Let rule. We can always assume that all bound variables of N are outside the domain of A (consequently, they are disctinct from free variables of M).

Case N is x: Then [M/x]N is M. Thus A′ ⊢ M : τ, and by context-restriction, A ⊢ M : τ. Since A ⊢ M : σ′ is a principal solution of the typing problem A ▷ M : β, there exists a substitution μ of domain outside of A, that is in W, that maps σ′ to τ. The conclusion follows by applying rule Var-Inst.

Other Cases: In all other cases, [M/x]N and N have the same top structure. We apply the induction hypothesis to the premises and conclude with the same rule. This includes the case when N is y.

Let ⊢_{X} be the typing relation defined in C(∀ W · T^{ι}) × ML × T by the rules Var-Inst, Fun, App and the rule

\frac{A ⊢_{S} M : σ  A ⊢_{S} [M/x]N : τ}{A ⊢_{S} let x = M in N : τ}  (Let’)

Lemma 12 The typing relation ⊢_{S} restricted to C(T^{ι})×ML×T^{ι} and the typing relation ⊢_{X} are equivalent.

\underline{Proof}: The rule Let’ can be proved for ⊢_{S} by the subject reduction lemma. Conversely, the rule Gen-Let can be proved for ⊢_{X} by the term-expansion lemma.

The typing relation ⊢_{X} may be used to prove syntactic results of type inference, but it should not be taken as the basis for a type inference algorithm. The expansion of Letexpressions during typechecking looses the underlying sharing of the Let-bound expression which may be typed several times.

3 Unificands

A type inference algorithm is obtained in the next section by considering typing problems as unificands. In this section we recall the generalization of term equations as unificands. The results of the first two parts are well known but the presentation is new. Unificands are treated more abstractly so that we can also consider typing problems as unificands in the next section. In the last part, we consider a special case of order-sorted unification, for which we have a simple fast unification algorithm. The results of this section were first introduced in chapter 2 of [Rém90]. The formulation that we present here is much simpler. It uses existential unificands as in [KJ90].

In this section, we are given a term algebra T (S, V) and a regular equational theory on terms, whose unification is decidable and unitary unifying. Unitary unifying means that any unification problem that has a solution has a principal solution. In fact, it is not necessary that unification be unitary but only finitary unifying, then typing problems will have principal set of solutions instead of principal solutions. We will emphasize places where the difference matters. We study unification in T /E (read T modulo the E-equality). However we always work with terms of T and manipulate their E-equality explicitly. The equational theory E may be empty, of course, which includes free unification.

3.1 Set of unificands

The substitutions of T are functions from V to T equal to the identity almost everywhere. An admissible set of substitutions is a subset of substitutions S such that:

• S is stable by E-equality,

• S is stable by composition,

• S is stable by restrictions,

• For any variable α, there are infinitely many variables β such that both α ↦ β and β ↦ α are in S

The last condition is technical and ensures that there are enough renamings. It follows that an admissible set of substitutions is stable by sums of substitutions.

Admissible sets of substitutions are more general that order-sorted substitutions. If α is a variable, S(T ) does not necessarily contains all its subterms. In this part that an admissible set of substitutions is given.

Let Q be a set of objects, given with a function subst on T^{V} × Q to Q, a function vars from Q to W, and a predicate valid on Q (i.e. a subset of Q). We say that Q is a set of unificands if the following five properties hold for any unificand Q and any substitutions μ and ν:

1. D(μ) ∩ vars(Q) = ∅ ⟹ subst(μ, Q) = Q

2. subst(μ, subst(ν, Q)) = subst(μ ∘ ν, Q)),

3. vars(subst(μ, Q)) = V(μ(vars(Q))),

4. subst(μ, valid) ⊂ valid

5. μ =_{E} ν ∧ subst(μ, Q) ∈ valid ⟹ subst(ν, Q) ∈ valid

Example 1 Multi-equations are multi-sets of terms, written τ_{1} ˙= … τ_{p}. The set of variables of a multi-equation e, written V(e) is the union of the variables of all its components. The substitution of a multi-equation is the multi-equation obtained by substituting all its components. The set of multi-equations form a set of unificands when valid multi-equations are those that have all their components E-equal.

Unificands defined on the same algebra can be combined. The conjunction (respectively the disjunction) of the set of unificands (Q′, vars′, subst′, valid′) with the set of unificands (Q′′, vars′′, subst′′, valid′′) is the set of unificands (Q, vars, subst, valid), written Q′ ∧ Q′′ (respectively Q′ ∨ Q′′) defined by 1. Q = Q′ × Q′′. Elements of Q are written Q′ ∧ Q′′ (respectively Q′ ∨ Q′′),

2. vars(Q′ ∧ Q′′) = vars(Q′) ∪ vars(Q′′),

3. subst(μ, Q′ ∧ Q′′) = subst(μ, Q′) ∧ subst(μ, Q′′),

4. valid(Q′ ∧ Q′′) ⟺ valid′(Q′) and valid′′(Q′′),

(respectively valid(Q′ ∧ Q′′) ⟺ valid′(Q′) or valid′′(Q′′).)

The existential quantification of the set of unificands (Q′, vars′, subst′, valid′′) by a variable α, is the set of unificands (Q, vars, subst, valid), written ∃ α · Q, defined by

1. Q = Q′

2. vars(∃ α · Q) = vars′(Q) \ {α}

3. subst(μ, ∃ α · Q) = ∃ α · subst′(μ \ {α}, Q)

4. valid(∃ α · Q) ⟺ ∃τ, valid′((α ↦ τ)(Q))

A solution (also called a unifier) of a unificand U is a substitution that maps U to a unificand V such that valid(V). A unificand is solvable if it has at least one solution. The set of solutions of a unificand Q is written U(Q). It is stable by substitution. A solution is principal if all other solutions are instances of it. In the case of finitary theories, we may consider sets of principal solutions, such that all other solutions are instances of one solution of the set. Two unificands are equivalent if they have the same set of solutions. This operation is defined even if the two unificands are taken in two different sets of unificands. We write ⊥ for a unificand that is not solvable. The equivalence of unificands is indeed an equivalence relation.

Moreover, equivalences of unificands are compatible with the conjunctions, disjunction and existential quantification of unificands, that is, if Q′ and Q′′ are equivalent, then (we omit disjunction rules)

Q ∧ Q ≡ Q ∧ Q′′  Q′ ∧ Q ≡ Q′′ ∧ Q  ∃ α · Q′ ≡ ∃ α · Q′′

With respect to these equivalences, the conjunction of unificands (respectively the disjunction of unificands) is commutative and associative. Indeed, the existential quantifier acts as a binder for variables in unificands: existential unificands are equivalent by renaming of variables bound by ∃’s, exchange of consecutive ∃’s, and removal of vacuous ∃’s:

Q ∧ (Q′ ∧ Q′′) ≡ (Q ∧ Q′) ∧ Q′′  Q ∧ Q′ ≡ Q′ ∧ Q  Q ∧ ⊥ ≡ ⊥
∃ α · ∃ β · Q ≡ ∃ β · ∃ α · Q ∃ α · Q = ∃ β · (α ↦ β)(Q)

and, if α ∉ vars(Q),

∃ α · Q ≡ Q Q ∧ (∃ α · R) ≡ ∃ α · Q ∧ R

The above equivalences are called structural: they do not depend on the structure of unificands. We will consider unificand equality modulo structural equivalences.

Existential unificands capture the notion of garbage collection. During unification (or type inference) some variables may be introduced as auxiliary variables. However, they should be invisible at the end of the computation. In the literature, they are often called fresh variables, but rarely formalized. A possible formalization of fresh variables is to carry a finite set of variables that contains all variables that have been used and outside of which new variables have to be taken. This is a global treatment. On the opposite, existential variables are treated locally. For instance in Q ∧ R, the unificand R may be replaced by a unificand R′ introducing a variable α:

R ≡ ∃ α · R′(α)

Then, we automatically have:

Q ∧ R ≡ Q ∧ ∃ α · R′(α)

The existential quantifier can be pushed outside of Q if it does not contain α. After renaming α, we get:

Q ∧ R ≡ ∃ α′ · (Q ∧ R′(α′))

Existential unificands permit the definition and reasoning on local rules, from which global rules can trivially be deduced and used in algorithms. “Fresh variable” annotations are replaced by the usual convention that bound variables are kept distinct from all others.

An arbitrary unificand can always be written ∃ W · U where U does not contain any existential quantification, and U itself may always be written as a disjunction of conjunctions of basic unificands.

3.2 Term unification with systems of multi-equations

In this part all substitutions are admissible.

Arbitrary conjunctions of multi-equations are called systems of multi-equations. Systems of multi-equations are a good structure for describing unification on terms since they allow us to formalize sharing of terms. In case the theory is not unitary, we consider disjunction of systems of multi-equations.

We write V (e) for the set of variable terms of e, and T (e) the set of non variable terms of e. If T (e) is a singleton τ, we write ê for the substitution that maps V (e) to τ. If all terms are variables, we write ê for a substitution that maps V (e) to an arbitrary element of V. If T (e) has more than one term, then ê is undefined. When it exists ê is a trivial solution of e.

We describe a unification algorithm by rewriting rules {A \atop -⇝} ; B that transforms unificands into

equivalent unificands. Unification in the empty theory is mainly implemented by the following rules:

{α = e ∧ α = e′ \atop -------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; α = e = e′  (Fuse)

{e = f(τ_{1}, … τ_{p}) = f(σ_{1}, … σ_{p}) \atop ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ∃ α_{1}, … α_{p} · (e = f(α_{1}, … α_{p}) ∧ ⋀_{i∈[1,p]}(α_{i} = τ_{i} = σ_{i})) (Decompose)

{f(τ_{1}, … τ_{p}) = g(σ_{1}, … σ_{q}) = e \atop -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ⊥ (Collision) ; if f ≠ g,

A multi-equation is completely decomposed if it has at most one variable term per equation. A system is completely decomposed if it is fused and all multi-equations are completely decomposed. Applying them in any order the rules Fuse, Decompose and Collision always terminates (each step first decreasing the size of the system, then the number of multiequations). In the empty theory, a system to which none of the rules apply is completely decomposed.

In a non-empty theory, the rule Decompose is only an equivalence for a subset of symbols called decomposable symbols. A collision pair is a pair of symbols for which the rule Collision is an equivalence. The rules Fuse, Decompose and Collision are no longer sufficient to transform an arbitrary system into a completely decomposed system. We call Mutate a valid rule that transforms a multi-equation into an equivalent system such that applying the four rules Fuse, Decompose, Mutate and Collision always terminates with a completely decomposed system. Mutation does not necessarily exists. In particular, there is no possible mutation in a theory that is not finitary unifying. If the theory is unitary unifying, then the mutation need not to introduce any disjunction.

{e \atop --------------------------------------------------------------------------------------------------⇝} ; mutate(e)  (Mutate)

We say that a multi-equation e is directly inner the multi-equation e′ if there is at least one variable term of e′ that appears in a non variable term of e. We write < − the direct-inner relation, and ≮ − its negation. We write

Q < − R  for  ∀e′ ∈ Q, ∀e ∈ R, e < − e′

and

Q≮ − R  for  ∀e ∈ Q, ∀e′ ∈ R, e ≮ − e′

We call inner the transitive closure of the direct-inner relation on all multi-equations of Q, written as < −_{Q}^{∗}. The intuition of the inner relation is the following: if μ is a solution of Q and e and e′ are two equations of Q such that e < − e′, then μ maps all terms of the equation e to a common term τ and all terms of e′ to τ′, such that τ is a sub-term of τ′ of μ(e′).

A conjunction Q equal to e_{1} ∧ … e_{p} is said to be in the outer-first order if

∀i, ∀j ≥ i, e_{i} ≮ − e_{j}

It is said to in outer-last order if the reverse sequence is outer-first order. A system is free if no multi-equation is in inner relationship with one another.

The inner relation of a solvable completely decomposed system is strict. Checking the strictness of the inner relation is called the occur-check. If occur check fails on a completely decomposed subsystem of Q, it surely fails on the whole system. A theory is strict if any solvable completely decomposed system has a strict inner relation. That is, in a strict theory, a term is never equal to one of its sub-terms. The occur check for a strict theory is the rule

{Q \atop -⇝} ; ⊥ if e < −_{Q}^{∗} e, (Occur)

It is completed by the replacement rule.

{e ∧ Q \atop -------------------------------------------------------------------------⇝} ; e ∧ ê(Q) (Replace) if e ∧ Q≮ − e,

A principal unifier of a strict, free and completely decomposed system e_{1} ∧ … e_{p}, is the composition, in any order, of the trivial solutions of its equations: ê_{p} ∘ … ê_{1}.

A free system does not need to be computed to exhibit a principal solution. It can be directly read from a strict completely decomposed system: such a system can always be written in an outer-first order e_{1} ∧… e_{p}. Successive replacements in outer-first order produce a free system in which ê_{p} ∘ … ê_{1} is a principal unifier. It is noted Q̂.

The principal solution Q̂|` W of a completely decomposed system ∃ W · Q is defined modulo a renaming of variables in W.

Useless existential quantifiers can be eliminated at anytime:

{∃ α · (Q ∧ α ˙= e) \atop ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; e ∧ Q if α ∉ V(e ∧ Q), (Restrict)

The rule Generalize could have been used initially to transform the system into a system of small terms (of depth at most one), for which other rewriting rules will work more efficiently by more sharing.

\frac{(α ↦ τ)(e)}{∃ α · (e ∧ α = τ)} if α ∈ e \ V(τ) ∧ τ ∉ V, (Generalize)

3.3 Hierarchical unification

We describe a very simple case of sorted unification where variables are given ranks, and all substitutions are rank decreasing, as in section 2. More precisely, we assume that a mapping ϕ of V into IN is givent such that there are infinitely many variables of every rank. As in section 2, we write T^{n} the sets of terms of rank n and T_{n} the sets of terms of rank smaller or equal to n.

Rank decreasing substitutions are those for which there exists a decreasing function in IN → IN whose composition with ϕ is equal to ϕ ∘ μ. They are stable by composition, and form an admissible set of substitutions for unificands. A renaming is a raw-renaming such that ϕ ∘ μ is equal to ϕ. Its inverse is also a renaming.

We refer to non admissible substitutions as raw substitutions. Any unificand that is rawsolvable is solvable, since the unificand can be mapped to T^{0} by a raw renaming into V^{0} which is rank decreasing, then it is solvable since unification in T^{0} is isomorphic to raw-unification in T .

In the following we use the framework of unificands to show how to solve hierarchical unification problems. We add extra information to systems of multi-equations. Every multiequation e is constrained by one integer p called its rank. We write e ↓ p the constrained multi-equation and ↓(e) for p. The rank of a system is the maximum rank of its multiequations.

A substitution is solution of a hierarchical equation if it is a solution of the raw equation. The rank of an equation is only a memory for efficiency purposes. A constrained system of multi-equations Q is one such that:

∀μ ∈ U(Q), ∀e ∈ Q, ∀τ ∈ e, ϕ(μ(α)) ≤ ↓(e) ≤ ϕ(α)

The rank of a transformation {Q \atop -⇝} ; Q′ is the rank of Q. The transformation is constrained if it is an

equivalence such that if Q is constrained, then Q′ is constrained as well. It is compositional

if additionally {Q ∧ R \atop ----------------------------------------------------⇝} ; Q′ ∧ R is a constrained equivalence for all R. We associate a constrained

transformation to each raw transformation.

{α = e ↓ p ∧ α = e′ ↓ p′ \atop ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; α = e = e′ ↓ min(p, p′)  (Fuse)

{e = f(τ_{1}, … τ_{p}) = f(σ_{1}, … σ_{p}) ↓ p \atop -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ∃ α_{1}, … α_{p} · (e = f(α_{1}, … α_{p}) ∧ ⋀_{i∈[1,p]}(α_{i} = τ_{i} = σ_{i})) ↓ p If α_{i} ∈ V^{p},  (Decompose)

{f(τ_{1}, … τ_{p}) = g(σ_{1}, … σ_{q}) = e \atop -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ⊥ (Collision) ; If f ≠ g,

We call mutation at rank p, a constrained mutation of a multi-equation e ↓ p.

We add the compositional transformation

{e′ ↓ p ∧ e \atop ----------------------------------------------------------------------------------⇝} ; e′ ↓ q ∧ e If e′ < − e, ↓ (e) ≤ q < p,  (Propagate)

If ∀α ∈ T (e), (ϕ(α) ≤ q < p) ∨ (∃e′ ∈ Q, α ∈ V (e′) ∧ ↓(e′) ≤ q < p),

{e ↓ p ∧ Q \atop ------------------------------------------------------------------------------------⇝} ; e ↓ q ∧ Q  (Realize)

A constrained system Q is canonical if it is ⊥ or completely decomposed, propagated and realized and if every multi-equation e composed of variables has a variable of rank ↑(e). A completely decomposed, propagated and realized system can always be turned into a canonical system by using the following rule

{V (e) ↓ p \atop -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ∃ α · V (e) = α ↓ p if \{ \begin{matrix}∀β ∈ V (e), ϕ(β) > p, \\ α ∈ V^{p}, \end{matrix}  (Extend)

When e is reduced to variables, we always require that the arbitrary variable chosen to define ê is of lower rank. This also applies to trivial solutions of strict, completely decomposed unificands.

Theorem 2 If Q is strict, canonical and free, then Q̂ is a principal solution of Q.

\underline{Proof}: When Q is free, Q̂ is trivially a solution, since it is a raw-solution and rank-decreasing, and conversely, any solution μ is such that μ ∘ Q̂ = μ. Therefore, it suffices to see that replacement in the outer-first order keeps the system canonical, because then Q is equivalent to a free canonical system, say R, obtained by replacement in an outer-first order, whose principal solution R̂ is equal to Q̂.

Thus hierarchical unification proceeds as simple unification leading to ⊥ or a completely decomposed system, and then computes ranks of variables before a principal solution can be read. We show below that computation of ranks can be done by propagation and realization after the system has been completely decomposed. While maintaining a completely decomposed system can be done incrementally, the cost of propagation and realization dissuades from computing canonical systems incrementally. In the following, we introduce partial canonical systems, for which the cost of propagation and realization is done only on a subsystem.

A unificand Q ∧ R is a conjunction at rank n if the maximum rank of Q is strictly lower than n, then we write Q ∧_{n} R. A conjunction Q ∧_{n} R at rank n is a separation at rank n, if additionaly:

1. ∀e ∈ R, n ≤ ↓(e),

2. R is completely decomposed in Q ∧ R,

3. R≮ − Q

A separation Q ∧_{n} R at rank n is n-canonical if no Propagate, Realize or Extend rule may apply to a multi-equation of R.

Theorem 3 A solvable n-canonical conjunction ∃ W · Q ∧_{n} R has a principal solution of the form (μ ∘ R̂) |` W where μ is a principal solution of ∃ W · Q.

\underline{Proof}: Any fusion, decomposition, propagation or realization of an n-canonical system ∃ W · Q ∧ R only involves multi-equations of Q and leaves R in outer relation to the rest of the system. Thus there is an equivalent canonical system ∃ W, W′ · Q′ ∧ R such that R is in outer relation to Q′. A principal solution of ∃ W · Q∧R is (Q̂′∘R̂)|` W ∪ W′, that is (Q̂′|` W′∘R̂)|` W. Indeed, Q̂′ |` W′ is a principal solution of ∃ W · Q.

Algorithm 1 A n-canonical system can be obtained using the following steps:

1. Starting with R_{0}, apply decomposition, fusion and collision. Then apply the occur-check. This produces either ⊥, or a strict, completely decomposed system ∃ W · R_{1}. Return ⊥ in the first case, continue otherwise.

2. Apply propagation to R_{1} in an outer-first order. It terminates in at most as many steps as there are multi-equations in R_{1}, with a unificand R_{2}.

3. Apply realization to R_{2} in an inner-first order. It terminates in at most as many steps as there are multi-equations in R_{2}, with a unificand R_{3}.

4. Let Q the composition of all multi-equations of R_{3} of rank lower than n, and R_{4} of all others. Extend R_{4} to ∃ W′ · R.

The conjunction ∃ W, W′ · Q ∧_{n} R is n-canonical.

\underline{Proof}: The unificand Q is propagated (respectively realized) in R if no propagation (respectively realization) of R involves a multi-equation of R. The correction of the algorithm easily follows from:

• Let Q ∧ R be completely decomposed. If R is propagated in Q ∧ R and R is outer to Q and if R′ is a propagation of Q, then R′ is propagated in Q ∧ R′.

• Let Q ∧ R be completely decomposed. If Q is realized in Q ∧ R and R is outer to Q and if R′ is a realization of R, then Q is realized in Q ∧ R′.

• Realization of a completely decomposed and propagated system keeps the system propagated.

Lemma 13 If Q ∧ R is n-canonical, and all variables of Q′ are of ranks at most n, then (Q ∧ Q′) ∧ R is n-canonical.

\underline{Proof}: It is a conjunction at rank n. Propagation of R into Q′ cannot happen since the lower rank of R is greater than the higher rank of Q′. Realization of an equation of R by Q′ cannot happen since no equation of Q′ is not inner to R. Realization of Q by equations of Q′ cannot indirectly fire the realization of an equation of R by Q.

Algorithm 2 The algorithm 1 for computing a n-canonical form of R_{0} can be improved by initially splitting R_{0} into a conjunction at Q′ ∧ R′_{0} where Q′ is the largest sub-unificand of Q_{0} that has all its variables in V_{n}. Running the algorithm 1 on R′_{0} produces Q ∧ R. Then, (Q′ ∧ Q) ∧ R is n-canonical.

The algorithm 2 is implemented in the appendix A.

4 Type inference

The substitution lemma allows us to consider triples A▷_{n}M : τ as unificands for the admissible set of ranked substitutions and the following three definitions:

1. V(A ▷_{n} M : τ) is V(A) ∪ V(τ),

2. μ(A ▷_{n} M : τ) is μ(A) ▷_{n} M : μ(τ),

3. valid_{n} is the relation ⊢_{n}.

The closure of the disjoint union of these unificands and systems of multi-equations by conjunction and existential quantification are called typing problems.

The principal typing property is equivalent to having principal solutions to all solvable typing problems. We can formalize the algorithm that computes principal solutions as a set of simplifications of typing unificands that are equivalences.

Lemma 14 Let A be a context of level n and α be a type variable of level at most n. The following rules are equivalences:

1. If x : ∀ W · τ is in A, τ in T_{n} and W a subset of V^{n} \ {α}, then:

{A ▷_{n} x : α \atop ---------------------------------------------------------------------⇝} ; ∃ W · α = τ  (Var)

If x is not in A, then A ▷_{n} x : α is not solvable.

2. If β is in V^{n}, then

{A ▷_{n} M N : α \atop ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ∃ β · A ▷_{n} M : β ∧ A ▷_{n} N : β → α  (App)

3. If β and γ are in V_{n}, then

{A ▷_{n} λ x. M : α \atop ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ∃ βγ · A[x : β] ▷_{n} M : γ ∧ α = β → γ ↓ n  (Fun)

4. Let β be in V^{n+1} \ V(A).

If ∃ W · Q ∧_{n} R is a solvable n-canonical unificand equivalent to A ▷_{n+1} M : β (such that W is disjoint from V(A) and α), then

{A ▷_{n} let x = M in N : α \atop ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ∃ W · Q ∧ A[x : ∀ V^{n+1} · R̂(β)] ▷_{n} N : α  (Let)

If A ▷_{n} M : β is not solvable, then neither is A ▷_{n} let x = M in N : α.

\underline{Proof}: Each case of the lemma is of the form {A \atop -⇝} ; B (R). We successively show that any solution

μ of A is solution of B (R-Direct), and conversely that any solution μ of B is a solution of A (R-Inverse).

Case Var-Direct: We can choose W disjoint from μ(α) and form μ. From the hypothesis μ(A) ⊢_{n} x : μ(α) we know that there exists a substitution ν with domain W that maps μ(τ) to μ(α) modulo E. The term μ(α) is also equal to (ν ∘ μ)(α). Therefore, ν ∘ μ is a solution of α ˙= τ, and so is (ν ∘ μ) \ W.

Case Var-Inverse: We again choose W disjoint from μ(α) and from μ. We know from the hypothesis that μ is a solution of ∃ W · α ˙= τ. That is, there exists a substitution ν of domain W such that ν ∘ μ is a solution of τ ˙= α. As for the Var-Direct case, this means that ν maps μ(τ) to μ(α). Therefore, μ is a solution of A ▷_{n} x : α.

Case App, Fun: They are both immediate.

Case Let-Direct: We know from the hypothesis μ(A) ⊢_{n} let x = M in N : μ(α) that there exists τ such that μ(A) ⊢_{n+1} M : τ and μ(A)[x : ∀ V^{n+1} · τ] ⊢_{n} N : μ(α). The substitution (β ↦ τ) ∘ μ is a solution of A ⊢_{n+1} M : β and thus, it is a solution also of ∃ W · Q ∧_{n} R. Therefore, it can be extended to a solution ν of Q ∧_{n} R of domain W. By theorem 3, ν is of the form ξ ∘ R̂ where ξ is a solution of Q. Since R̂ is of domain in V^{n+1}, it leaves A and α unchanged. We have ξ(A)[x : ∀ V^{n+1} · ξ(R̂(β))] ⊢_{n} N : ξ(α) and by lemma C-Gen we get ξ(A)[x : ∀ V^{n+1} · (ξ |` V_{n})(R̂(β))] ⊢_{n} N : ξ(α), that is ξ is a solution of A[x : ∀ V^{n+1} · R̂(β)] ▷_{n} N : α. Finally, ξ is a solution of the unificand ∃ W · Q ∧ A[x : ∀ V^{n+1} · R̂(β)] ▷_{n} N : α of rank n, and so is μ, which is equal to ξ on the set V_{n} (their restrictions to V_{n} are equal).

Case Let-Inverse: We know that μ is a solution of ∃ W · Q∧A[x : ∀ V^{n+1} · R̂(β)]▷_{n} N : α. That is, μ can be extended to a solution ξ of domain W of both unificands Q and A[x : ∀ V^{n+1} · R̂(β)] ▷_{n} N : α. The substitution ξ ∘ R̂, say ν, satisfies both Q and R. Therefore, ν \ W, is a solution of A ▷_{n} M : β. So is ν since W is disjoint from both V(A) and β. The substitution ν also satisfies ν(A)[x : ∀ V^{n+1} · ν(β)] ▷_{n} N : ν(α). Using rule Let, we conclude that ν is a solution of the unificand A ▷_{n} let x = M in N : α at rank n. So are ξ and μ which are equal to ν on the set V_{n}.

Case Failure: The two unsolvable cases are immediate by showing the inverse implications.

Theorem 4 If the equational theory is unitary unifying, all solvable typing problems have principal solutions; there is an algorithm that given any typing problem, either returns a principal solution or returns failure, if the problem is unsolvable.

Algorithm 3 For any integer n, an n-canonical unificand equivalent to a typing problem A ▷_{n} M : τ is recursively computed by the two steps, starting with the unificand Q reduced to A ▷_{n} M : τ:

1. Apply rules Var, App, Fun and Let to Q in any order. Rule Let recursively calls the algorithm on smaller typing problems. This terminates with a unification problem ∃ W · R.

2. Put R in n-canonical form using algorithm 2. This produces a conjunction ∃ W′· Q′∧R′.

Then ∃ W, W′ · Q′ ∧ R′ is n-canonical and equivalent to A ▷_{n} M : τ.

The decomposition, fusion, collision and mutation of the last step may be merged with the first step. The soundness and correctness of the algorithm directly follows from lemma 14.

5 Extensions of the core language

In this section we describe a few extensions of the core language and examples of practical equational theories in ML. We first show that the language can be extended with constants. Type abbreviations in ML are nicely formalized by an equational theory on types. We briefly mention the extension of ML with extensible records and indicate other possible applications.

5.1 Term constants

For sake of simplicity, we have omitted term constants in the core language. They can be incorporated quite easily:

M ::= … | c

Constants come with principal and closed type schemes, or equivalently, with a constant context B with the set of constants ranging into closed type schemes as.

The typing relation ⊢_{B} for ML with term constants is defined with respect to the constant context B by all the rules of S plus the following:

\frac{c : ∀ W · τ ∈ B  μ : W → V,}{A ⊢_{B} c : μ(σ)}  (Const-Inst)

If the context A and the constant context B are disjoint, then the judgements A ⊢_{B} M : τ and B ∪ A ⊢_{S} M : τ are equivalent. This also includes the case of an infinite set of constants, provided they are finitely representable.

5.2 Type abbreviations

Type abbreviations are often considered as syntactic sugar. This would be correct if parsers expanded them. However, it is more efficient to keep type abbreviations during typechecking, and expand them by need, since they are a more compact representation of large types. Type abbreviations can be nicely formalized with a very simple equational theory on types.

The set of type symbols is the union of original symbols C and an ordered set of abbreviation symbols C′ composed of f′_{0}, f′_{1}, and so on. Type abbreviations are defined by a sequence of equalities:

f′_{i}(α_{1}, … α_{p}) = τ_{i}

where τ_{i} is only composed of symbols of indices lower that i and all of variables among α_{1}, … α_{p}. These equalities define the presentation of a theory E.

Types are the algebra T (V, Σ_{C∪C′})/E. Type-abbreviation theories are acyclic [Tha92] and thus syntactic^{1} [Kir85], but their presentation are not usually syntactic. Yet, there is a trivial mutation that can be deduced from the non syntactic presentation. All symbols are decomposable. All pairs of original symbols produce collision. Mutation is composed of the following rules:

{f′_{j}(σ_{1}, … σ_{p}) ˙= τ ˙= e \atop ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------⇝} ; ∃ α_{1}, … α_{p} · ∧ \{ \begin{matrix}f_{j}(α_{1}, … α_{p}) ˙= e \\ τ ˙= τ_{j} \\ α_{i} ˙= σ_{i}, i ∈ [1, p] \end{matrix} if Top (τ) = Top (τ_{i}), Mutate (f)

where Top (τ) is the symbol of τ at the empty occurrence.

The type-abbreviation theory is regular, and has a unitary unification algorithm, thus ML with abbreviations has principal typings and a type inference algorithm.

Type-abbreviation theories are very simple. Yet, they provide examples of theories that may involve the arrow symbol: for instance, the theory E reduced to the axiom:

f_{0}(α) = α → α

is a type abbreviation.

1Syntactic theories are equational theories such that any provable equality can be proved with at most one occurrence of an axiom at the root; they are theories for which there is a unification algorithm that extends the efficient unification algorithm for empty theories of [MM82].

5.3 Extensible records

An important application of the use of sorted types modulo an equational theory is type inference with extensible records [Rém91]. The equations are used to describe duplication of “row types”. Sorts are used for two different purposes: they restrict the formation of terms and the power of the equations; they also introduce a fine control of polymorphism since generic variables range only over types of a certain sort.

A. Ohori also uses sorted types for record structure [Oho90] but his sorts are ordered and our results do not directly apply to his system. Types modulo equations have also been used in [Tha91] but type reconstruction is different: it uses coercions in programs.

5.4 Other applications

Treating typing problems as unificands has two main advantages. Soundness and completeness of the type-inference algorithm with respect to the typing rules can be proved independently for each transformation, and is thus easier. It also formalizes unification on graphs, that leads to efficient algorithms.

Ranks have been used to compute variables that can be generalized incrementally. It is not so critical for the usual Damas-Milner type system, but it is for some extensions, for example with subtypes where typing are constrained by a set of inequations. Simplification of inequations is usually expensive. The control of simplification is crucial. Too many simplifications are too expensive, but too few simplifications will unnecessarily duplicate large structures through generic polymorphism. Ranks keep track of the dependencies of polymorphic binding variables and give the right boundary for simplifications.

Conclusion

The extension of ML with a regular, decidable and unitary unifying equational theory on types preserve all usual syntactic properties of ML; the formulation itself is changed so little that the extension is quite natural. Types can be sorted, provided that judgements and arrow types are of the same toplevel sort.

The language of unificands is well adapted to type inference: properties are easily stated and proofs are usually simpler since they are separated in small independent parts. The algorithm is described by transformation of unificands, which leaves the control more flexible. Unificands allows one to treat type inference and unification in a uniform manner and formalize the sharing between types in typing problems and in unification problems naturally. Benefitting from the work on unification, the use of existential unificands nicely handles the introduction of variables during resolution, avoiding the informal fresh variables or the heavy formalization of garbage collection.

Generalization in ML only applies to variables that have been recently introduced. Hierarchical types keep track of the freshness of type variables during unification; they are very simple order-sorted types, and fit well eithin the same framework of unification. They make generalization a trivial step.

This work includes the original ML language and ML with type abbreviations as a simple instance. An important application is typechecking of extensible records.

22 A TYPE INFERENCE FOR THE ORIGINAL ML LANGUAGE IN CAML-LIGHT

A Type inference for the original ML language in Caml-Light

The aim of this appendix is to give a real implementation of the type inference algorithm based on unificands and ranked unification. The language that is considered is the one of section 1 extended with integer constants. Types are unsorted and taken in the empty theory. Type declarations and type abbreviations are not allowed. The language is a toy language, but the implementation is robust, and adding more features to the language is not difficult.

We separately describe all modules with their interfaces. We give the complete implementations of most important modules, but we leave to the user the front and back end module implementations. In fact, the implementation can be used for typechecking without its front and back ends by typing in the abstract syntax of programs instead of entering the programs themselves.

The implementation runs on Caml-Light, version 0.5^{2} [LM92].

Module ml

This module defines the abstract syntax of ML programs and a parser of concrete programs.

type expr =

Var of string | Fun of string * expr | App of expr * expr | Let of string * expr * expr | Int of int;;

value parse expr : char stream → expr;;

Module multi

This module defines the deep representation of types and unificands and provides a few functions to manipulate them.

Types and completely decomposed multi-equations are represented by the same multi structure. In order to perform in-place fusion (which corresponds to applying a partial solution of an unificand to the unificand itself in non destructive unification algorithms), all multi structures are mutable objects. The nod of a variable that has been substituted is a Linto nod and points to another multi structure, but eventually ends with a Nolink nod that contains the canonical element of the multi-equation. The term field of a variable or a multi-equation that has only variable terms is Var. Otherwise it is Term (symb, args) where symb and args are the top symbol and the list of immediate subterms of the canonical element. The field rank stores the rank of the multi-equation, and the mark field is used internally by algorithms to keep track of nods that have been visited at some stage of a recursive visit of the structure. They avoid looping since multi structures are graphs.

All multi-equations are kept completely decomposed at any time. A multi-equation α ˙= β ˙= τ can be thought of as two variables α and β both substituted by the term τ.

type symbol = Arrow | Int;;

type multi = {mutable nod: nod} and nod = Nolink of desc | Linkto of multi and desc = {term: term; mutable rank: int; mutable mark : unit ref} and term = Var | Term of symbol * multi list;;

2This version is distributed by anonymous ftp at nuri.inria.fr

let rec repr u = match u.nod with Linkto v → let v = repr v in u.nod ← Linkto v;v

| → u;;

let rec desc u = match u.nod with Nolink u desc → u desc

| → desc (repr u);;

let mark() = ref();; let no mark = mark();;

let level = ref 0;; let equations = ref ([||]: multi list vect);;

let reset level() = level := 1; equations := [|[]; []|];;

let push level() =

if vect length !equations < !level + 2 then

begin let new equations = make vect (!level + 2) [] in for i = 0 to !level do new equations.(i) ← (!equations).(i) done; equations := new equations

end; level := succ !level;;

let pop level() = (!equations).(!level) ← []; level := pred !level;;

let new u = let u desc = {term = u; rank = !level; mark = no mark} in let u = {nod = Nolink u desc} in (!equations).(!level) ← u::((!equations).(!level)); u;;

The function repr computes canonical elements of multi-equations doing path compression. Its accompanying function nod return the nod of the canonical element.

Each creation of a variable or of a term is done at the current level and produces a new multi-equation that is sorted with respect to its rank and stored in the equations reference.

Module print

This module implements a printer of multi objects. It is left to the user.

#open ”multi”;;

value reset namers : unit → unit and print multi: multi → unit;;

Module generic

This module is the heart of the algorithm; it implements generalization and instantiation of types.

#open ”multi”;;

exception Cycle of multi;;

value generalize: multi → unit and instance: multi → multi;;

Generalization of a unificand at the highest rank first propagates and realizes the unificand at this rank. Then it turns variables of the highest rank into generic variables. Propagation, realization and marking of generic variables of a multi-equation are completed by the function propagate and generalize that recursively visits the unificand: propagation is executed before the recursive calls, which comes in outer-most order, and realization proceeds after returns, thus in inner-most order. Marking immediately follows the realization, since the sub-unificand cannot be affected by inner-most returns. The function generalize controls the process. It first marks fresh multi-equations and sort them according to their rank. Then it calls the propagate and realize function starting with multi-equations of lower ranks. Garbage unificands are not generalized but only checked for acyclicity.

Genericity is not a property of variables but of multi-equations. Generic multi-equations are represented by setting their rank field to a negative integer. The absolute value identifies the multi-equation locally to the unificand that is being generalized and it is used by the instance function that copies the generic part of the unificand as a graph.

#open ”multi”;;

let occur check visited = let visiting = mark() in occur check where rec occur check u = let u desc = desc u in if u desc.mark == visiting then raise (Cycle u) else if u desc.mark != visited & u desc.rank = !level then (match u desc.term

with Var → ()

| Term(C,L) →

u desc.mark ← visiting; do list occur check L; u desc.mark ← visited);;

let propagate and realize n fresh visited = let generic index = ref 0 and visiting = mark() in propagate realize where rec propagate realize k u = let u desc = desc u in if u desc.mark == visiting then raise (Cycle u); if u desc.mark != visited then begin

begin match u desc.term

with Var → u desc.rank ← min u desc.rank k

| Term(C,L) →

if u desc.mark == fresh then

begin u desc.mark ← visiting; let propagate realize = propagate realize (min u desc.rank k) in u desc.rank ← it list (fun k u → max k (propagate realize u)) 1 L

end

end;

u desc.mark ← visited;

if u desc.rank = n then (u desc.rank ← (decr generic index; !generic index)) end; if u desc.rank < 0 then n else u desc.rank;;

let generalize u =

let visited = mark() and fresh = mark() in

let generalize = propagate and realize !level fresh visited and occur check = occur check visited in let sorted = make vect (!level +1) [] in

let sort u = match u.nod with Linkto → ()

| Nolink u desc → u desc.mark ← fresh; sorted.(u desc.rank) ← u::sorted.(u desc.rank) in

do list sort !equations.(!level);

for i = 0 to !level − 1 do do list (generalize i) sorted.(i) done; generalize !level u;

let update u = let u desc = desc u in if u desc.rank = !level then occur check u else if u desc.rank < 0 then () else

(!equations).(u desc.rank) ← u::(!equations).(u desc.rank) in

for i = 0 to !level do do list update sorted.(i) done ;;

type table = None | Multi of multi;;

let instance u = let u = repr u in let u desc = desc u in if u desc.rank >= 0 then u else let table = make vect (−u desc.rank) None in instance u

where rec instance u = let u = repr u in let u desc = desc u in if u desc.rank >= 0 then u else match table.(−u desc.rank−1) with None →

let v = new Var in

table.(−u desc.rank−1) ← Multi v;

let u desc = match u desc.term with Var → Var

| Term (C, L) → Term (C, map instance L) in v.nod ← Nolink {term = u desc; rank = !level; mark = no mark}; v

| Multi v → v;;

Module unify

This module implements free unification, following the three rules Fuse, Collision and Decomposition.

#open ”multi”;;

exception Collision of symbol * symbol;;

let rec unify u v =

let u = repr u in let v = repr v in

if u == v then () else

let U = desc u in let V = desc v in

match U.term, V.term with Var, →

u.nod ← Linkto v; V.rank ← min U.rank V.rank

| , Var →

v.nod ← Linkto u; U.rank ← min U.rank V.rank

| Term(C,L), Term(D,M) → if C ≠ D then raise (Collision (C, D)); if U.rank < V.rank then v.nod ← Linkto u else u.nod ← Linkto v; do list2 unify L M;;

The algorithm for syntactic unification would be similar, but the collision case would be preceeded by other successful decomposition cases, automatically deduced from a syntactic presentation of the theory.

Module typing

This module implements algorithm 3.

#open ”multi”;; #open ”print”;; #open ”unify”;; #open ”generic”;;

exception Unbound of string;;

let rec expr A = expr A where rec expr A =

function ml Var x → instance (try assoc x A with Not found → raise (Unbound x))

| ml App (M, N) → let u = expr A N in let v = new Var in unify (expr A M) (new (Term (Arrow, [u;v]))); v

| ml Fun (x,M) → let u = new Var in let v = expr ((x,u)::A) M in new (Term (Arrow, [u; v]))

| ml Let (x, M, N) → push level (); let u = expr A M in generalize u; pop level (); expr ((x,u)::A) N

| ml Int c → new (Term (Int,[])) ;;

let type expr B M = reset level(); let u = expr B M in generalize u; u;;

Module step

The function step parses an expression, calls type expr with an empty environment and this expression, and pretty prints the result type, handling and reporting errors that may have been raised.

value step: unit → unit;;

Module batch

The batch function make step loop for ever.

value batch: unit → unit;;

This provides a stand alone typechecker.

References

[CDDK86] Dominique Clément, Joëlle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple applicative language: Mini-ML. Technical Report 529, INRIA-Rocquencourt, France, 1986.

[Dam85] Luis Damas. Type assignment in programming languages. PhD thesis, University of Edinburgh, 1985.

[DM82] Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Nineteenth Annual Symposium on Principles Of Programming Langages, pages 207–212, 1982.

[Kir85] Claude Kirchner. Méthodes et outils de conception systématique d’algorithmes d’unification dans les théories équationnelles. Thèse de doctorat d’état en informatique, Université de Nancy 1, 1985.

[KJ90] Claude Kirchner and Jean-Pierre Jouannaud. Solving equations in abstract algebras: a rule-based survey of unification. Research Report 561, Université de Paris Sud, Orsay, France, April 1990.

[LM92] Xavier Leroy and Michel Mauny. The caml light system, version 0.5. documentation and users’ guide. Logiciel 3, INRIA-Rocquencourt, BP 105, F-78 153 Le Chesnay Cedex, 1992.

[MM82] Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

[Oho90] Atsushi Ohori. Extending ML polymorphism to record structure. Technical report, University of Glasgow, 1990.

[Rém90] Didier Rémy. Algèbres Touffues. Application au Typage Polymorphe des Objects Enregistrements dans les Langages Fonctionnels. Thèse de doctorat, Université de Paris 7, 1990.

[Rém91] Didier Rémy. Type inference for records in a natural extension of ML. Technical Report 1431, INRIA-Rocquencourt, BP 105, F-78 153 Le Chesnay Cedex, May 1991.

[Tha91] Satish Thatte. coercive type isomorphism. In Functional Programming and Computer Architecture, volume 523. Springer Verlag, 1991.

[Tha92] Satish Thatte. Finite acyclic theories are unitary. Personal communication, 1992.