Type Inference for Parametric Type Classes

Kung Chen, Martin Odersky, Paul Hudak

Department of Computer Science Yale University Box 2158 Yale Station New Haven, CT 06520

June 11, 1992

Abstract

Haskell’s type classes permit the definition of overloaded operators in a rigorous and (fairly) general manner that integrates well with the underlying Hindley-Milner type system. As a result, operators that are monomorphic in other typed languages can be given a more general type. Most notably missing, however, are overloaded functions for data selection and construction. Such overloaded functions are quite useful, but the current Haskell type system is not expressive enough to support them.

We introduce the notion of parametric type classes as a significant generalization of Haskell’s type classes. A parametric type class is a class that has type parameters in addition to the placeholder variable which is always present in a class declaration. Haskell’s type classes are special instances of parametric type classes with just a placeholder but no parameters. We show that this generalization is essential to represent container classes with overloaded data constructor and selector operations. Furthermore, through a simple encoding scheme, we show that parametric type classes are able to capture the notion of “type constructor variables”, thus permitting the definition of overloaded operators such as map.

The underlying type system supporting our proposed generalization is an extension of Hindley-Milner type system with parametric type classes. The range of type variables are bounded by constraints. Rules for satisfiability and entailment of these constraints are given by a context-constrained instance theory that is separate from the inference rules of the type system. The decoupling of the instance theory from the type inference system makes our system more modular than previous work. We prove that the resulting type system is decidable, and provide an effective type inference algorithm to compute the principal types for well-typed expressions.

1 Introduction

Haskell’s type classes provide a structured way to introduce overloaded functions, and are perhaps the most innovative (and somewhat controversial) aspect of the language design [HJW91]. Type classes permit the definition of overloaded operators in a rigorous and (fairly) general manner that integrates well with the underlying Hindley-Milner type system. As a result, operators that are monomorphic in other typed languages can be given a more general type. Examples include the numeric operators, reading and writing of arbitrary datatypes, and comparison operators such as equality, ordering, etc.

Haskell’s type classes have proven to be quite useful. Most notably missing, however, are overloaded functions for data selection and construction. Such overloaded functions are quite useful, but the current Haskell type system is not expressive enough to support them (of course, no other language that we know if is capable of supporting them in a type-safe way either).

A Motivating Example

As a simple example, consider the concept of a sequence: a linearly ordered collection of elements, all of the same type. There are at least two reasonable implementations of sequences, linked lists and vectors. There is an efficiency tradeoff in choosing one of these representations: lists support the efficient addition of new elements, whereas vectors support efficient random (including parallel) access. Currently the choice between representations is made at the programming language level. Most functional languages provide lists as the “core” data structure (often with special syntax to support them), relegating arrays to somewhat of a second-class status. Other languages, such as Sisal and Nial, reverse this choice and provide special syntax for arrays instead of lists (this often reflects their bias toward parallel and/or scientific computation).

Of course, it is possible to design a language which places equal emphasis on both “container structures”. However, a naive approach faces the problem that every function on sequences has to be implemented twice, once for lists and once for arrays. The obvious cure for this name-space pollution and duplicated code is overloading. In our context, that means specifying the notion of a sequence as a type class with (at least) lists and vectors as instance types. Using Haskell-like notation, this would amount to the following declarations:

         class Sequence a s
         where cons :: a -> s -> s
               nth  :: s -> Int -> a
               len  :: s -> Int
         instance Sequence a (List a)
         where cons  =  (:)
               nth   =  (!)
               len   =  (#)
         instance Sequence a (Vector a)
         where cons  =  vecCons
               nth   =  vecNth
               len   =  vecLen

This defines the overloaded constructor cons, overloaded indexing selector nth, and a length function len. (Note the resemblance to a “container class” in object-oriented programming.)

The only problem with this code is that it is not valid Haskell, since Haskell’s type classes are permitted to constrain only one type, thus ruling out a declaration such as “class Sequence a s”. In essence, this restriction forces overloaded constructors and selectors to be monomorphic (which makes them fairly useless).

Even if this restriction did not exist, there is another problem with the current type class mechanism, which can be demonstrated through the typing of len:

         Sequence a s => s -> Int

Even if multi-argument type classes were allowed, this qualified type would still not be valid Haskell since it is ambiguous: Type variable a occurs in the context (Sequence a s), but not in the typepart proper (s->Int). ^{1} Ambiguous types need to be rejected, since they have several, possibly conflicting, implementations.

A related, but harder, problem arises if we extend our example to include an overloaded map function. Having such a function is attractive, since together with join and filter, it allows us to generalize (i.e. overload) the notion of a “list comprehension” to include all instances of Sequence, not just lists. In [CHO92], we elaborate on this, extending it further to comprehensions for arbitrary instances of class monad, such as bags and lists. This seems quite natural since, after all, the domain of sets is where the “comprehension” notation came from. However, a problem becomes evident as soon as we attempt to give a type for map.

    map: (Sequence a sa, Sequence b sb) => (a -> b) -> sa -> sb.

This type is too general, since it would admit also implementations that take one sequence type (e.g. a list) and return another (e.g. a vector). Generality is costly in this context since it again leads to ambiguity. For instance, the function composition (map f . map g) would be ambiguous; the type of map g, which does not appear in the type of the enclosing expression, can be either a list or a vector.

What is needed is some way to specify that map returns the same kind of sequence as its argument, but with a possibly different element type. A nice way to notate this type would be:

    map: Sequence (s a) => (a -> b) -> s a -> s b

where s is a variable which ranges over type constructors instead of types. To accommodate this, Sequence should now be viewed as a type constructor class instead of a type class. However, because the instance relationships are now expressed at the functor-level, there is the danger (as has been conjectured in [Lil91]) that second order unification is needed to reconstruct types, thus rendering the system undecidable.

To solve these problems, we introduce the notion of parametric type classes as a significant generalization of Haskell’s type classes. Parametric type classes can have type arguments in addition to the constrained type variable, and thus are able to express classes such as Sequence defined earlier. Moreover, through a simple encoding scheme, we show that parametric type classes are able to capture the notion of “type constructor variables,” thus permitting the definition of overloaded operators such as map. As a matter of fact, parametric type classes are a conservative extension of Haskell’s type system: If all classes are parameterless, the two systems are equivalent. Most importantly, we prove that the resulting type system is decidable, and provide an effective type inference algorithm to compute the principal types for well-typed expressions.

1Satish Thatte has pointed out that the ambiguity problem can be circumvented in this case by having the len operation in a different class from the cons and nth operations. This is true in principle, but it would severely restrict the way operators can be grouped.

The rest of this report is organized as follows: Section 2 introduces parametric type classes. Section 3 presents them formally, in a non-deterministic type system. Section 4 presents an equivalent syntax-directed system that bridges the gap between the non-deterministic system and a type reconstruction algorithm. Section 5 introduces context-preserving unification and presents such a unification algorithm to be used in the type inference algorithm. Section 6 presents a simple algorithm to compute principal types for our type system and proves its soundness and completeness. Section 7 explains when a type scheme is ambiguous and how operators such as map can be typed in our system. Section 8 describes related work. Section 9 concludes.

2 Parametric Type Classes

A parametric type class is a class that has type parameters in addition to the placeholder variable which is always present in a class declaration. To distinguish between placeholder and type parameters, we write the placeholder in front of the class, separated by an infix (::). For instance:

         class t :: Eq where
         class s :: Sequence a where

The first definition introduces a class without parameters; in Haskell this would be written class Eq t. The second definition defines a type class Sequence with one parameter; this cannot be expressed in standard Haskell. The infix (::) notation is also used in instance declarations and contexts. The two instance declarations of Sequence presented in the last section would now be written:

         inst List a   :: Sequence a where ...
         inst Vector a :: Sequence a where ...

In an instance declaration, of form T :: Sequence a, say, the type T must not be a variable. Furthermore, if two types T1 and T2 are both declared to be instances of Sequence, then their top-level type constructors must be different. Thus, the instance declarations given above are both valid. On the other hand,

         inst a :: Sequence (List a)

would violate the first restriction, and

         inst List Int  :: Sequence Int
         inst List Char :: Sequence Char

Type variables  α
Type constructors κ
Class constructors c
Types  τ ::= () | κ τ | α | τ_{1} × τ_{2} | τ_{1} → τ_{2}
Type schemes  σ ::= ∀α::Γ.σ | τ
Type classes  γ ::= c τ
Class sets  Γ ::= {c_{1} τ_{1}, ..., c_{n} τ_{n}}  (n ≥ 0, c_{i} pairwise disjoint)
Contexts  C ::= {α_{1} ::Γ_{1}, …, α_{n} ::Γ_{n}}  (n ≥ 0)

Expressions  e ::= x | e e′ | λx.e | let x = e′ in e
Programs  p ::= class α::γ where x :σ in p
| inst C ⇒ τ::γ where x = e in p
| e

Figure 1: Abstract Syntax of Mini-Haskell+

would violate the second restriction. Effectively, these restrictions ensure that in a proof of an instance relationship every step is determined by the class name and the type in placeholder position. The class parameter types, on the other hand, depend on the placeholder type.

One consequence of these restrictions is that there is at most one way to deduce that a type is an instance of a class. This is necessary to guarantee coherence. It is not sufficient, since types might be ambiguous; see Section 7 for a discussion. Another consequence is that sets of instance predicates are now subject to a consistency criterion: If we have both T :: Sequence a and T :: Sequence b then we must have a = b. That is, a = b is a logical consequence of the two instance predicates and the restrictions on instance declarations. The type reconstruction algorithm enforces consistency in this situation by unifying a and b.

Enforcing consistency early helps in keeping types small. Otherwise, we could get many superfluous instance constraints in types. As an example, consider the composition (tl . tl), where tl is typed (s :: Sequence a) => s -> s. Without the consistency requirement, the most general

type for the composition would be (s ::  Sequence a, s ::  Sequence b) => s -> s. Com-

posing tl n times would yield a type with n Sequence constraints, all but one being superfluous.

3 The Type System of Parametric Classes

This section presents our type system formally. We first define the abstract syntax of classes and types in the context of a small example language. We then explain formally what it means for a type to be an instance of a class. Based on these definitions, we define a non-deterministic type system with the same six rules as in [DM82], but with parametric type classes added. We claim that, in spite of its added generality, the system is actually simpler than previously published type systems for standard Haskell.

C ⊢⊢ α::γ (α::{… γ …} ∈ C )

\frac{C ⊢⊢ C′}{C ⊢⊢ τ::γ} ( inst C′ ⇒ τ::γ ∈ Ds)

\frac{C ⊢⊢ τ::γ_{1} … C ⊢⊢ τ::γ_{n}}{C ⊢⊢ τ::\{γ_{1}, ..., γ_{n}\}} (n ≥ 0)

\frac{C ⊢⊢ τ_{1} ::Γ_{1} … C ⊢⊢ τ_{n} ::Γ_{n}}{C ⊢⊢ \{τ_{1} ::Γ_{1}, …, τ_{n} ::Γ_{n}\}} (n ≥ 0)

Figure 2: Inference Rules for Entailment

Syntax

The example language is a variant of Mini-Haskell [NS91], augmented with parameterized type classes. Its abstract syntax and types are shown in Figure 1. A parametric type class γ in this syntax has the form c τ, where c is a class constructor, corresponding to a class in Haskell, and τ is a type. Classes with several parameters are encoded using tuple types, e.g. c (α, β). Parameterless classes are encoded using the unit type, e.g. Eq ().

The instance relationship between a type and a type class is denoted by an infix (::); the predicate τ′:: c τ reads τ′ is an instance of c τ. We use the same infix notation to stipulate that a type be an instance of each member of a set of classes. In particular, bound variables in a type scheme are constrained by a (possibly empty) set of classes. The informal meaning of this is that, in ∀α::Γ.σ, α may only be instantiated to types that are instances of every class in Γ.

One simplification with respect to standard Haskell concerns the absence of a hierarchy on classes. The subclass/superclass relationship is instead modeled by class sets Γ. Consider for instance the class Eq () of equality types in Haskell and its subclass Ord () of ordered types. We can always represent Ord () as a set of two classes, {Eq (), Ord′ ()}, where Ord′ contains only operations (<, ≤), which are defined in Ord but not in Eq. Translating all classes in a program in this way, we end up with sets over a flat domain of classes. This shows that we can without loss of generality disregard class hierarchy in the abstract syntax.

Instance Theories

In this subsection, we make precise when a type τ is an instance of a class set Γ, a fact which we will express τ :: Γ. Clearly, the instance relation depends on the instance declarations Ds in a program. We let these declarations generate a theory whose sentences are instance judgments of the form C ⊢⊢ τ :: γ. An instance judgment is true in the theory iff it can be deduced using the inference rules in Figure 2.

Context

In these rules the context C is a set of instance assumptions α::Γ (all α’s in C are disjoint), where the class set Γ is subject to the consistency criterion mentioned in the previous section. When convenient, we will also regard a context as a finite mapping from type variables to class sets, i.e. C α = Γ iff α:: Γ ∈ C . Thus the domain of C , dom(C ) , is defined as the set of type variables α such that α::Γ ∈ C . As type classes can now contain parameters, we define the region of a context C ,

reg(C ) = ⋃_{α∈dom(C )} fv(C α)

and the closure of C over a set of type variables, Δ, written C^{∗}(Δ), as the least fixpoint of the equation

C^{∗}(Δ) = Δ ∪ C^{∗}(reg(C |_{Δ})).

Here fv is the standard function that maps every type (scheme) to the set of free type variables that occur in it. By natural extension, it can be applied to class and set of classes.

We say C_{1} is contained in C_{2}, written C_{1} ⪯ C_{2}, if dom(C_{1}) ⊆ dom(C_{2}) and C_{1}α ⊆ C_{2}α for each α ∈ dom(C_{1}). We write C_{1} ⊎ C_{2} for the disjoint union of two contexts and C\_{α} for restriction of a context C to all type variables in its domain other than α. As a consequence of the consistency criterion, the set union of two contexts is not well-defined but for compatible contexs. Two contexts C_{1} and C_{2} are called compatible, written C_{1} ⋈ C_{2}, if for any class constructor c and type variable α, α ∈ dom(C_{1}) ∩ dom(C_{2}), we have τ = τ′ whenever c τ ∈ C_{1}α and c τ′ ∈ C_{2}α.

A context C is called closed if C^{∗}(dom(C )) = dom(C ), or, equivalently, reg(C ) ⊆ dom(C ). A context C is called acyclic if all the type variables α, α ∈ dom(C ), can be topologically sorted according to the order: α < β if α ∈ fv(C β). We shall restrict our discussion to only closed acyclic contexts in the remainder of the report.

Finally, we shall say that an object Π is covered by a context C if fv(Π) ⊆ dom(C ).

Constrained Substitution

A substitution is a map from type variables to types. The domain of a substitution S, dom(S), is the set of type variables α such that Sα ≠ α. The region of a substitution can be defined just as the region of a context. As usual, the composition of substitutions S and R is denoted by S ∘ R, or simply by juxtaposition SR.

In the following, we shall apply substitutions not only to types, but also to (sets of) classes and (sets of) instance predicates. On all of these, substitution is defined pointwise, i.e. it is a homomorphism on sets, class constructor application and (::). Since a context is a special form of an instance predicate set, substitutions can be applied to contexts. However, the result of such a substitution is in general not a context, as the left hand side α of an instance predicate α:: Γ can be mapped to a non-variable type. Our typing rules, on the other hand, require contexts instead of general predicate sets. Thus, we need a means to find a context that is a conservative approximation to a predicate set. We use the following definitions:

Definition. A constrained substitution is a pair (S, C ) where S is a substitution and C is a closed context such that C = SC .

Definition. A constrained substitution (S, C ) preserves a constrained substitution (S_{0}, C_{0}) if there is a substitution R such that S = R ∘ S_{0}, C covers RC_{0}, and C ⊢⊢ RC_{0}. We write in this case (S, C ) ⪯ (S_{0}, C_{0}).

It is easy to show that ⪯ is a preorder.

Definition. A constrained substitution (S, C ) is most general among those constrained substitutions that satisfy some requirement R if (S, C ) satisfies R, and, for any (S′, C′) that satisfies R, (S′, C′) ⪯ (S, C ).

Definition. A constrained substitution (S, C ) is a normalizer of an instance predicate set P if C ⊢⊢ SP.

To ensure the principal type property of our type system with parametric classes, we have to place the following requirements on the entailment relation ⊢⊢:

• monotonicity: for any contexts C and C′, if C′ ⪯ C then C ⊢⊢ C′.

• transitivity under substitution: for any substitution S, contexts C and C′, predicate set P, if C ⊢⊢ SC′ and C′ ⊢⊢ P then C ⊢⊢ SP.

• most general normalizers: If a predicate set P has a normalizer then it has a most general normalizer.

From the viewpoint of type reconstruction, the first two requirements are needed to ensure that once established entailments are not falsified by later substitutions or additions to contexts. They follow directly from the inference rules in Figure 2. The last requirement ensures that there is a most general solution to an entailment constraint. To establish existence of most general normalizers, we have to place two restrictions on the instance declarations in a program:

(a) There is no instance declaration of the form inst C ⇒ α::c τ .

(b) For every pair of type and class constructor (κ, c), there is at most one instance declaration of the form inst C ⇒ κ τ′::c τ . Furthermore, τ′ must be the unit type, or a possible empty tuple of distinct type variables and both dom(C ) and fv(τ) are contained in fv(τ′).

Restriction (a) is part of current Haskell, and restriction (b) is a direct generalization of current Haskell’s restriction to incorporate parametric type classes.

Theorem 3.1 If the instance declarations Ds of a program satisfy the restrictions (a) and (b), then ⊢⊢ admits most general normalizers.

Proof: See Section 5.

Typing Rules

Given an entailment relation ⊢⊢ between contexts and instance predicates, we now formalize a theory of typing judgments. Typing judgments are of the form A, C ⊢ e : σ, where A is an assumption set of type predicates x : σ (all x disjoint), C is a context, and e is an expression or a program. A typing judgment A, C ⊢ e : σ holds in the theory iff it can be deduced using the inference rules in Figures 3 and 4.

The rules in Figure 3 form a non-deterministic type system for expressions, along the lines of of the standard Hindley/Milner system [DM82]. One notable difference between this system and the

(var)  A, C ⊢ x : σ (x : σ ∈ A)
(∀−elim)  \frac{A, C ⊢ e : ∀α::Γ.σ  C ⊢⊢ τ::Γ}{A, C ⊢ e : [α ↦ τ] σ}

(∀−intro)  \frac{A, C .α::Γ ⊢ e : σ}{A, C ⊢ e : ∀α::Γ.σ} (α ∉ fv A ∪ reg C )

(λ−elim)  \frac{A, C ⊢ e : τ′ → τ  A, C ⊢ e′ : τ′}{A, C ⊢ e e′ : τ}

(λ−intro)  \frac{A.x :τ′, C ⊢ e : τ}{A, C ⊢ λx.e : τ′ → τ}

(let)  \frac{A, C ⊢ e′ : σ  A.x :σ, C ⊢ e : τ}{A, C ⊢ let x = e′ in e : τ}

Figure 3: Typing Rules for Expressions

(class)  \frac{A.x :∀_{fv γ}∀α::\{γ\}.σ, C ⊢ p : τ}{A, C ⊢ class α::γ where x :σ in p : τ}

(inst)  \frac{A, C ⊢ x :∀α::\{γ\}.σ  A, C ⊢ e :[α ↦ τ′]σ  A, C ⊢ p : τ}{A, C ⊢ inst C′ ⇒ τ′::γ where x = e in p : τ}

Figure 4: Typing Rules for Declarations

standard Hindley/Milner system is that the bound variable in a type scheme ∀α :: Γ.σ can be instantiated to a type τ only if we know from the context that τ :: Γ (rule ∀−elim). The second difference concerns rule (∀−intro), where the instance predicate on the generalized variable α is “discharged” from the context to form the type scheme ∀α:: Γ.σ. Here fv(A) is the set of type variables that occur free in A, i.e., ⋃ fv(σ) for each (x :σ) ∈ A.

One may obsevre that a signle context C is used in deriving both the type scheme for the letdefinition and the type for the let-body. We could use two different contexts, but the following lemma justifies our use of a single context C in deriving the type for a let-expression. Let bv(σ) be the set of bounded variables that occur in σ. We have:

Lemma 3.2 Given a typing judgement A, C′ ⊢ e : σ and a context C such that C′ ⪯ C and dom(C ) ∩ bv(σ) = ∅, we can construct another derivation for A, C ⊢ e : σ.

Proof: By induction on the structure of A, C′ ⊢ e : σ. The only nontrivial case is when the last rule applied is (∀−intro).

We have a derivation of the form :

\frac{A, C′.α::Γ ⊢ e : σ′}{A, C′ ⊢ e : ∀α::Γ.σ′} (α ∉ fv A ∪ reg C′)

Let σ = ∀α::Γ.σ′. It is clear that dom(C .α::Γ) ∩ bv(σ′) = ∅ given dom(C ) ∩ bv(σ) = ∅. Moreover, since C′ ⪯ C , we have C′.α:: Γ ⪯ C .α:: Γ. Hence by induction we can constrcut the following derivation:

\frac{\frac{A, C′.α::Γ ⊢ e : σ′}{A, C .α::Γ ⊢ e : σ′}}{A, C ⊢ e : ∀α::Γ.σ′} (induction) (let)

The rules in Figure 4 extend this system from expressions to programs. In rule (class), the overloaded identifier x is added to the assumption set. Rule (inst) expresses a compatibility requirement between an overloaded identifier and its instance expressions. These rules have to be taken in conjunction with the requirements (a), (b) on instance declarations listed in the last subsection. We say a program p = Ds e has type scheme σ, iff Ds satisfies these requirements and generates an entailment relation ⊢⊢, and A_{0}, {} ⊢ p : σ, for some given closed initial assumption set A_{0}.

The Instance Relation and Principal Type Schemes

A useful fact about Hindley/Milner type system is that when an expression e has a type, there is a principal type scheme which captures the set of all other types derivable for e thruogh the notion of generic instances. The remainder of this section introduces the definitions of generic instance and principal type schemes in our system.

Definition. A type scheme σ′ = ∀α′_{j} :: Γ′_{j} .τ′ is a generic instance of a type scheme σ = ∀α_{i} :: Γ_{i}.τ under a context C , if there exists a substitution S on {α_{i}} such that

1. α′_{j} is not free in σ,

2. Sτ = τ′, and

3. C ⊎ {α′_{j} ::Γ′_{j} } ⊢⊢ Sα_{i} ::SΓ_{i}.

We write in this case, σ′ ⪯_{C} σ, and we drop the subscript in ⪯_{C} if C = {}.

The definiton of ⪯_{C} is an extension of the ordering relation defined in [DM82]. The only new requirement on instance entailment is needed for the extension with parametric type classes. It is easy to see that ⪯_{C} defines a preorder on the set of type schemes.

We obtain a decision procedure for ⪯_{C} by performing a match to establish (2), followed by a test of the validity of (3). We shall see in Section 5 how the latter can be done using the normalization function defined there.

Two type schemes σ and σ′ are called syntactically equivalent, written σ = σ′, iff they are instances of each other, i.e., σ ⪯ σ′ and σ′ ⪯ σ.

The following properties of (⪯_{C} ) are easily established:

Lemma 3.3 Let (σ, C_{1}) = gen(τ, A, C ) and (σ′, C_{1}) = gen(τ, A, C ⊎ C′). Then σ′ ⪯ σ and σ ⪯_{C′} σ′. Proof: Follows immediately from the definition. Lemma 3.4 If σ′ ⪯_{C} σ and C ⪯ C′ then σ′ ⪯_{C′} σ. Proof: Follows immediately from the definition, and noting that ⊢⊢ is monotonic. The next lemma shows that the ordering on type schemes is preserved by constrained substitutions. Lemma 3.5 If σ′ ⪯_{C} σ and C′ ⊢⊢ SC then Sσ′ ⪯_{C′} Sσ. Proof: Let σ = ∀α_{i} :: Γ_{i}.τ and σ′ = ∀β_{j} :: Γ′_{j} .τ′. By definition, there are types τ_{i} forming a substitution R, R = [α_{i} ↦ τ_{i}], such that

1. β_{j} are not free in σ,

2. Rτ = τ′, and

3. C ⊎ {β_{j} ::Γ′_{j} } ⊢⊢ R{α_{i} ::Γ_{i}}. Without loss of generality we can assume that neither α_{i} nor β_{j} are involved in S. Hence

Sσ = ∀α_{i} ::SΓ_{i}.Sτ and Sσ′ = ∀β_{j} ::SΓ′_{j} .Sτ′.

Now let R′ = [α_{i} ↦ Sτ_{i}]. We show that Sσ′ ⪯_{C′} Sσ through R′.

R′(Sτ) = [α_{i} ↦ Sτ_{i}]Sτ
= S([α_{i} ↦ τ_{i}]τ)
= Sτ′.

Moreover, since C′ ⊢⊢ SC and β_{j} are not involved in S, we have

C′ ⊎ {β_{j} ::SΓ′_{j} } ⊢⊢ S(C ⊎ {β_{j} ::Γ′_{j} }).

By the transitivity under substitution of ⊢⊢ on (3), we get

C′ ⊎ {β_{j} ::SΓ′_{j} } ⊢⊢ S(R{α_{i} ::Γ_{i}}).

Using a similar argument, we have

R′({α_{i} ::SΓ_{i}}) = S(R{α_{i} ::Γ_{i}}),

so

C′ ⊎ {β_{j} ::SΓ′_{j} } ⊢⊢ R′({α_{i} ::SΓ_{i}}).

Finally, since β_{j} are not involved in S and do not occur free in σ, neither will they occur free in Sσ. This completes the proof.

(var′)  A, C ⊢′ x : τ (x : σ ∈ A, τ ⪯_{C} σ)
(λ−elim′)  \frac{A, C ⊢′ e : τ′ → τ  A, C ⊢′ e′ : τ′}{A, C ⊢′ e e′ : τ}

(λ−intro′)  \frac{A.x :τ′, C ⊢′ e : τ}{A, C ⊢′ λx.e : τ′ → τ}

(let′)  \frac{A, C′ ⊢′ e′ : τ′  A.x :σ, C ⊢′ e : τ}{A, C ⊢′ let x = e′ in e : τ} (σ, C′′) = gen(τ′, A, C′), C′′ ⪯ C

Figure 5: Determinstic Typing Rules for Expressions

We can easily extend the definition of instance relation to type asumption sets: For type assumption sets A′ and A, A′ ⪯_{C} A if dom(A′) = dom(A) and A′(x) ⪯_{C} A(x) for all x, x ∈ dom(A).

With the definiton of ordering on type schemes, we can define the notion of principal type schemes in our system.

Definition. Given A, C , and e, we call σ a principal type scheme for e under A and C iff A, C ⊢ e : σ , and for every σ′, if A, C ⊢ e : σ′ then σ′ ⪯_{C} σ.

We shall develop an algorithm to compute principal type schemes in the following sections.

4 A Deterministic Type Inference System

We present a deterministic type inference system in this section. Compared to the typing rules in Section 3, the rules here are so formulated that the typing derivation for a given term e is uniquely detrmined by the syntactic structure of e, and hence are better suited to use in a type inference algorithm. We show that the system is equivalent to the previous one in terms of expressiveness and, in addition, has all the nice properties toward the construction of a type reconstruction algorithm.

Deterministic Typing Rules

The typings rules for the deterministic system are given in Figure 5. The rules ∀−intro and ∀−elim have been removed and typing judgements are now of the form A, C ⊢′ e : τ where τ ranges over the set of type expressions as opposed to type schemes in the typing judgements of Section 3. Other major differences are that rule (var′) instantiates a type scheme to a type according to the definition of generic instance and rule (let′) use the generalization function, gen, to introduce type schemes.

The function gen takes as arguments a type scheme, an assumption set, and a context, and returns a generalized type scheme and a discharged context. It is defined by gen (σ, A, C ) =

if ∃α ∈ dom(C )\(fv A ∪ reg C ) then

gen (∀α::C α.σ, A, C\_{α}) else (σ, C )

In other words, instance assumptions in the given context, except those constraining type variables in the assumption set, are discharged and moved to form a more general type scheme in an order so that type variables are properly quantified. This is formalized in the following lemma:

Lemma 4.1 Let C be a closed and acyclic context that covers both type τ and type assumption set A. If gen(τ, A, C ) = (σ, C′) where σ = ∀α_{i} ::C α_{i}.τ, then {α_{i}} ⊎ C^{∗}(fv A) = dom(C ). In other words, dom(C′) = C^{∗}(fv A).

Proof: Follows immediately from gen’s definition.

It is clear that the gen function is derived from the rule (∀−intro) used in the non-deterministic typing system. Hence we have the follwoing lemma:

Lemma 4.2 If A, C ⊢ e :τ and (σ, C′) = gen(τ, A, C ) then A, C′ ⊢ e : σ.

Proof: By applying (∀−intro) repeatedly on A, C ⊢ e :τ.

Note that both the (∀−intro) rule and the gen function generalize a type scheme by discharging the instance assumptions contained in the context. Clearly, to derive a more genral typing, one would presume the context to constrain as many type variables as used in the inference process. This can always be achieved by assuming an empty class set for those unconstrained type variables and thus making them part of the context. Consequently, as a convention, in writing A, C ⊢′ e : τ, we shall assume that both A and τ are covered by C .

The following lemma shows that the set of free type variables in the assumption set is, roughly speaking, preserved under constrained substitution.

Lemma 4.3 Given a type assumption set A, contexts C and D, and a substitution S such that A is covered by C and SC is covered by D, if D ⊢⊢ SC then ⋃{fv(Sα) | α ∈ C^{∗}(fv A)} = D^{∗}(fv SA).

Proof: We prove ⋃{fv(Sα) | α ∈ C^{∗}(fv A)} ⊆ D^{∗}(fv SA) only; the proof for the other direction is quite similar and thus omitted.

If α ∈ (C )^{∗}(fv A) then α ∈ C^{k}(fv A) for some k, k ≥ 0. Thus an induction on k suffices:

k = 0 : Clearly, if α ∈ fv(A) then fv(Sα) ⊆ fv(SA) ⊆ D^{∗}(fv SA).

k = n + 1 : Suppose that β ∈ fv(C α) for some α ∈ C^{n}(fv A). By induction, fv(Sα) ⊆ D^{∗}(fv SA). There are four possibile cases depending on the effects of S on α and β:

• If α ∉ dom(S) and β ∉ dom(S), then clearly β ∈ fv(Dα) since D ⊢⊢ SC . So, by induction, we have α ∈ D^{∗}(fv SA) and hence fv(Sβ) ⊆ D^{∗}(fv SA).

• If α ∉ dom(S) and β ∈ dom(S), then clearly Dα = S(C α) since D ⊢⊢ SC . So, fv(Sβ) ⊆ fv(Dα). By induction, we have α ∈ D^{∗}(fv SA) and hence fv(Sβ) ⊆ D^{∗}(fv SA).

• If α ∈ dom(S) and β ∉ dom(S), then there are two possibile cases according to the structure of Sα:

– If Sα = ρ, i.e. fv(Sα) = {ρ}, then β ∈ fv(Dρ) since D ⊢⊢ SC . By induction, ρ ∈ D^{∗}(fv SA) and hence fv(Sβ) ⊆ D^{∗}(fv SA).

– If Sα = (κ τ), then from D ⊢⊢ SC and our requirement on instance declaration, we have β ∈ fv(τ). But, since fv(Sα) = fv(τ), we have fv(τ) ⊆ D^{∗}(fv SA) by induction and hence fv(Sβ) ∈ D^{∗}(fv SA).

• If α ∈ dom(S) and β ∈ dom(S), then the four possible cases based on the structures of Sα and Sβ can be similarly reasoned as the previous case.

The next two lemmas describe the interaction between the gen function and constrained substitution. They are evry useful in later proofs.

Lemma 4.4 Let (σ, C′) = gen(τ, A, C ) and (σ′, D′) = gen(Sτ, SA, D). If D ⊢⊢ SC then σ′ ⪯_{D′} Sσ.

Proof: Let σ = ∀α_{i} ::Γ_{i}.τ and σ′ = ∀α′_{j} ::Γ′_{j} .Sτ. Now let β_{i} be new type variables, then

Sσ = ∀β_{i} ::S[α_{i} ↦ β_{i}]Γ_{i}.S[α_{i} ↦ β_{i}]τ.

To show that σ′ ⪯_{D′} Sσ, we choose the substitution R = [β_{i} ↦ Sα_{i}]. Thus,

R(S[α_{i} ↦ β_{i}]τ) = [β_{i} ↦ Sα_{i}]S([α_{i} ↦ β_{i}]τ)
= S[β_{i} ↦ α_{i}][α_{i} ↦ β_{i}]τ
= Sτ

and similarly R(S[α_{i} ↦ β_{i}]Γ_{i}) = SΓ_{i}.

Now, the next thing to show is that D′ ⊎ {α′_{j} ::Γ′_{j} } ⊢⊢ R({β_{i} ::S[α_{i} ↦ β_{i}]Γ_{i}}). But since

R({β_{i} ::S[α_{i} ↦ β_{i}]Γ_{i}}) = {Sα_{i} ::SΓ_{i}}
= S{α_{i} ::Γ_{i}},

and D = D′ ⊎ {α′_{j} ::Γ′_{j} } by Lemma 4.1, what we need to show is that D ⊢⊢ S{α_{i} ::Γ_{i}}. This follows directly from the given facts that {α_{i} ::Γ_{i}} ⪯ C and D ⊢⊢ SC .

Finally, since β_{i} are not free in σ′, we have σ′ ⪯_{D′} Sσ.

The following lemma shows that, under certain conditions, the composition of generalization and constrained substitution can be commutative.

Lemma 4.5 Let (σ, C′) = gen(τ, A, C ). For any context C′′ and substitution S such that C′′ covers SC′ and C′′ ⊢⊢ SC′, there exist a substitution R and a context D such that

RA = SA, D ⊢⊢ RC , Sσ = σ′, and D′ ⪯ C′′

where (σ′, D′) = gen(Rτ, RA, D).

Proof: Let σ = ∀α_{i} ::Γ_{i}.τ and R = S[α_{i} ↦ β_{i}] where β_{i} are new type variables. From Lemma 4.1, none of α_{i} occurs in A, so we have RA = SA.

Next, let D = R{α_{i} ::Γ_{i}} ⊎ C′′|_{fv(SC′)}. From Lemma 4.1, C = {α_{i} ::Γ_{i}} ⊎ C′ and hence RC′ = SC′. Now, since C′′ ⊢⊢ SC′, it follows that D ⊢⊢ RC .

Third, we shall show that Sσ = σ′. As β_{i} are new, we have Sσ = ∀β_{i} :: RΓ_{i}.Rτ. Suppose that σ′ = ∀ρ_{j} :: Γ′_{j} .Rτ, we need to show that {β_{i}} = {ρ_{j} } to complete the proof. Given D’s definition and the fact that β_{i} are new, it suffices to show that D′ = C′′|_{fv(SC′)}. This we prove by considering fv(Sα) for α ∈ dom(C′).

From Lemma 4.1, we know that dom(C′) = C^{∗}(fv A). Moreover, since D ⊢⊢ RC and RA = SA, we have fv(Sα) ⊆ D^{∗}(fv SA) for all α ∈ dom(C′) by Lemma 4.3. In other words, none of the type variables in fv(SC′) can be generalized in gen(Rτ, RA, D). Thus, D′ = C′′|_{fv(SC′)} and hence we have Sσ = σ′ and D′ ⪯ C′′. This completes the proof.

Equivalence of the two Systems

We now present a number of useful properties of the deterministic type system. They are useful not only in establishing the congruence of the two type systems, but also in investigating the relation between the type system and the type reconstruction algorithm.

We begin with the substitution lemma, which assures us that typing derivations are preserved under constrained substitution.

Lemma 4.6 (Substitution lemma) If A, C ⊢′ e :τ and C′ ⊢⊢ SC then SA, C′ ⊢′ e :Sτ.

Proof: By induction on the structure of the proof A, C ⊢′ e : τ. The only nontrivial cases are (var′) and (let′).

Case(var′) : We have a derivation of the form

A, C ⊢′ x : τ (x : σ ∈ A, τ ⪯_{C} σ).

Without the loss of generality, we assume that S is safe for σ. Hence if σ = ∀α_{i} :: Γ_{i}.τ′ then Sσ = ∀α_{i} ::SΓ_{i}.Sτ′. Our goal is to find a instantiation substitution J such that J (Sτ′) = Sτ and C′ ⊢⊢ J {α_{i} ::SΓ_{i}}.

Let I = [α_{i} ↦ τ_{i}] be the instantiation substitution such that τ = I τ′ and C ⊢⊢ I {α_{i} :: Γ_{i}}. Now define J = S ∘ I . We first show that J (Sτ′) = S(I τ′). This we prove by showing that for each α occuring τ′, J (Sα) = S(I α).

If α is bound in σ, i.e., α = α_{j} for some j , then

J (Sα_{j} ) = J α_{j} = S(I α_{j} ).

Otherwise α is free in σ, so

J (Sα) = S(I (Sα)) = S(Sα) = Sα = S(I α),

since S is safe for α_{i} and α is not in {α_{i}}. Hence J (Sτ′) = Sτ follows from τ = I τ′.

By a similar argument we can show that J (SΓ_{i}) = S(I Γ_{i}). So

J {α_{i} ::SΓ_{i}} = {S(I α_{i})::S(I Γ_{i})} = S(I {α_{i} ::Γ_{i}}).

Then from C ⊢⊢ I {α_{i} :: Γ_{i}} and C′ ⊢⊢ SC , we can infer that C′ ⊢⊢ S(I {α_{i} :: Γ_{i}}). Therefore, Sτ ⪯_{C′} Sσ through J and hence SA, C′ ⊢′ x : Sτ.

Case(let′) : We have a derivation of the form

\frac{A, C_{0} ⊢′ e′:τ A.x :σ, C ⊢′ e :τ′}{A, C ⊢′ let x = e′ in e : τ′} (σ, C_{1}) = gen(τ, A, C_{0}), C_{1} ⪯ C

and C′ ⊢⊢ SC .

Clearly, we have C′ ⊢⊢ SC_{1}, since C_{1} ⪯ C . Now, applying Lemma 4.5 to (σ, C_{1}) = gen(τ, A, C_{0}), C′ and S, we get a substitution R and a context C′′ such that

RA = SA, C′′ ⊢⊢ RC_{0}, Sσ = σ′ and C̄ ⪯ C′

where (σ′, C̄ ) = gen(Rτ, SA, C′′).

Thus we can construct the derivation

\frac{A, C_{0} ⊢′ e′:τ}{\frac{RA, C′′ ⊢′ e′ : Rτ}{SA, C′′ ⊢′ e′ : Rτ}}  (induction) (SA = RA)  \frac{A.x :σ, C ⊢′ e : τ′}{\frac{SA.x :Sσ, C′ ⊢′ e :Sτ′}{SA.x :σ′, C′ ⊢′ e :Sτ′}}

SA, C′ ⊢′ let x = e′ in e : Sτ′

(induction) (Sσ = σ′) (let′)

The next two lemmas express a form of monotonicity of typing derivations with respect to the context and the assumption set.

Lemma 4.7 If A, C ⊢′ e :τ and C ⪯ C′ then A, C′ ⊢′ e :τ.

Proof: A straightforward induction on the structure of A, C ⊢′ e :τ.

Lemma 4.8 If A′, C ⊢′ e :τ and A′ ⪯_{C} A then A, C ⊢′ e :τ.

Proof: By induction on the structure of A, C ⊢′ e :τ. The only nontrivial case is (let′):

We have a derivation of the form:

\frac{A′, C′ ⊢′ e′:τ′ A′.x :σ′, C ⊢′ e : τ}{A′, C ⊢′ let x = e′ in e : τ} (σ′, C′′) = gen(τ′, A′, C′), C′′ ⪯ C

Let σ′ = ∀α_{i} :: Γ_{i}.τ and S = [α_{i} ↦ β_{i}] where β_{i} are new type variables. Now applying S to A′, C′ ⊢′ e′:τ′, we get SA′, C̄ ⊢′ e′:Sτ′ where C̄ = SC′. Since none of the α_{i} occurs in A′, this isequivalent to A′, C̄ ⊢′ e′:Sτ′.

Next, let D = C \C′′. From Lemma 4.1 we know that C′ = C′′ ⊎ {α_{i} ::Γ_{i}}. So, D ⊎ C̄ = C ⊎ {β_{i} :: SΓ_{i}} and hence A′ ⪯_{D⊎C̄} A by Lemma 3.4. Furthermore, let (σ, C̃ ) = gen(Sτ′, A, D ⊎ C̄ ). Then, since none of the β_{i} appear free in A, we have σ = ∀β_{i} ::SΓ_{i}.∀ρ_{j} ::Γ′_{j} .Sτ′ where {ρ_{j} ::Γ′_{j} } ⊆ C . So, clearly we have σ′ ⪯_{C} σ and C̃ ⪯ C . Thus we can construct the following derivation

\frac{A′, C′ ⊢′ e′ : τ′}{\frac{A′, D ⊎ C̄ ⊢′ e′ : Sτ′}{A, D ⊎ C̄ ⊢′ e′ : Sτ′}}  (Lemma 4.7) ; (induction)  \frac{A′.x :σ′, C ⊢′ e :τ}{A.x :σ, C ⊢′ e :τ}

A, C ⊢′ let x = e′ in e : τ

(induction) (let′)

Now we can show that the deterministic system ⊢′ is equivalent to the non-deterministic system ⊢ in the following sense.

First, the deterministic system is sound with respect to the non-deterministic one.

Theorem 4.9 If A, C ⊢′ e :τ then A, C ⊢ e :τ.

Proof: By induction on the structure of the proof A, C ⊢′ e :τ. The only interesting case is (let′):

We have a derivation of the form

\frac{A, C′ ⊢′ e′:τ′ A.x :σ, C ⊢′ e : τ}{A, C ⊢′ let x = e′ in e : τ} (σ, C′′) = gen(τ′, A, C′), C′′ ⪯ C

Without loss of generality, we can assume that dom(C′) ∩ dom(C ) = dom(C′′), which can be achieved by a suitable renaming of variables in dom(C ). Hence, dom(C ) ∩ bv(σ) = ∅ and we can thus construct the following derivation

A, C′ ⊢′ e′ : τ′

\frac{A, C′ ⊢ e′ : τ′}{\frac{A, C′′ ⊢ e′ : σ}{A, C ⊢ e′ : σ}}

(induction) (Lemma 4.2) (Lemma 3.2)

\frac{A.x :σ, C ⊢′ e :τ}{A.x :σ, C ⊢ e :τ}

A, C ⊢ let x = e′ in e : τ

(induction) (let)

Second, for each typing derivation in the non-deterministic system we can always find a derivation in the deterministic system such that the inferred type scheme, after generalized by the gen function, is more general than the type scheme determined by the non-deterministic one.

Theorem 4.10 If A, C ⊢ e : σ then there is a context C′, and a type τ such that C ⪯ C′, A, C′ ⊢′ e :τ and σ ⪯_{C} σ′ where (σ′, C′′) = gen(τ, A, C′).

Proof: By induction on the structure of A, P ⊢ e :σ.

Case(var) : We have a derivation of the form :

A, C ⊢ x : σ (x : σ ∈ A).

Let σ = ∀α_{i} ::Γ_{i}.τ′. Define C′ and τ as follows:

C′ = C ⊎ S{α_{i} ::Γ_{i}}, τ = Sτ′

with S of the form [α_{i} ↦ β_{i}] where β_{i} are new type variables. So, by definition, C ⪯ C′ and τ ⪯_{C′} σ. Thus

A, C′ ⊢′ x : τ (x : σ ∈ A, τ ⪯_{C′} σ)

Finally, since C ⪯ C′, it is clear that σ ⪯_{C} σ′ where (σ′, C′′) = gen(τ, A, C′).

Case(∀−elim) : We have a derivation of the form :

\frac{A, C ⊢ e : ∀α::Γ.σ C ⊢⊢ τ::Γ}{A, C ⊢ e : [α ↦ τ]σ}

By induction,

A, C′ ⊢′ e : τ′

for some τ′ and C′, with C ⪯ C′, and ∀α:: Γ.σ ⪯_{C} σ′ where (σ′, C′′) = gen(τ′, A, C′). Using the hypothesis C ⊢⊢ τ::Γ and transitivity of ⪯_{C} , we have

[α ↦ τ]σ ⪯_{C} ∀α::Γ.σ ⪯_{C} σ′.

Case(∀−intro) : We have a derivation of the form :

\frac{A, C .α::Γ ⊢ e : σ}{A, C ⊢ e : ∀α::Γ.σ} (α ∉ fv(A) ∪ reg(C ))

By induction,

A, C′ ⊢′ e : τ

for some τ and C′, with (C .α::Γ) ⪯ C′ and σ ⪯_{C .α::Γ} σ′ where (σ′, C′′) = gen(τ, A, C′).

Since α ∉ fv(A)∪reg(C ) and (α::Γ) ∈ C′, we know that (α::Γ) will be generalized in gen(τ, A, C′). It then follows that ∀α::Γ.σ ⪯_{C} σ′.

Case(λ−elim) : We have a derivation of the form :

\frac{A, C ⊢ e : τ′ → τ A, C ⊢ e′ : τ′}{A, C ⊢ ee′ : τ}

By induction,

A, C_{1} ⊢′ e : ν

for some ν and C_{1}, with C ⪯ C_{1} and τ′ → τ ⪯_{C} ∀α_{i} :: Γ_{i}.ν where (∀α_{i} :: Γ_{i}.ν, C_{0}) = gen(ν, A, C_{1}). Therefore there is a substitution R, R = [α_{i} ↦ τ_{i}], such that

C ⊢⊢ R{α_{i} ::Γ_{i}} and Rν = τ′ → τ.

From Lemma 4.1, we know that dom(C_{0}) = (C_{1})^{∗}(fv A) = C^{∗}(fv A). So, C_{0} ⪯ C and hence C ⊢⊢ RC_{1}. Then using Lemma 4.6 on R, we can get a derivation

RA, C ⊢′ e : Rν.

Since none of α_{i} appear in A this is equivalent to

A, C ⊢′ e : τ′ → τ.

By a similar argument, we get C ⊢⊢ SD_{1} and

A, C ⊢′ e′ : τ′

for some context D_{1} and substitution S, S = [β_{i} ↦ ν_{i}]. Therefore, we have A, C ⊢′ ee′ : τ. Finally, if gen(τ, A, C ) = (σ′, C′) then obviously τ ⪯_{C} σ′. Case(λ−intro) : We have a derivation of the form :

\frac{A.x :τ′, C ⊢ e : τ}{A, C ⊢ λx.e : τ′ → τ}

By induction,

A.x :τ′, C_{1} ⊢′ e : ν

for some ν and C′, with C ⪯ C_{1} and τ ⪯_{C} ∀α_{i} :: Γ_{i}.ν where (∀α_{i} :: Γ_{i}.ν, C_{0}) = gen(ν, A.x : τ′, C_{1}). Therefore, there is a substitution S, S = [α_{i} ↦ τ_{i}], such that

C ⊢⊢ S{α_{i} ::Γ_{i}} and Sν = τ.

From C ⪯ C_{1}, we know that C ⋈ C_{0}. Furthermore, as C_{1} = {α_{i} ::Γ_{i}} ⊎ C_{0} by Lemma 4.1, we have C ∪ C_{0} ⊢⊢ SC_{1}. Then, using Lemma 4.6 on S, we get a derivation

S(A.x :τ′), C ∪ C_{0} ⊢′ e : Sν.

Since none of α_{i} appears in A.x :τ′ this is equivalent to

A.x :τ′, C ∪ C_{0} ⊢′ e : τ.

Hence

A, C ∪ C_{0} ⊢′ λx.e : τ′ → τ.

Finally, if gen(τ′ → τ, A, C ∪ C_{0}) = (σ′, C′) then obviously τ′ → τ ⪯_{C} σ′. Case(let) : We have a derivation of the form :

\frac{A, C ⊢ e′ : σ A.x :σ, C ⊢ e : τ}{A, C ⊢ let x = e′ in e : τ}

We shall assume that A, σ, and τ are all covered by C , for we can always place an empty class set on unconstrained type variables. By induction,

A, C_{1} ⊢′ e′ : τ_{1}

for some τ_{1} and C_{1} with C ⪯ C_{1} and σ ⪯_{C} σ_{1} where (σ_{1}, C′_{1}) = gen(τ_{1}, A, C_{1}). Again, by induction,

A.x :σ, C_{2} ⊢′ e : τ_{2}

for some τ_{2} and C_{2} with C ⪯ C_{2} and τ ⪯_{C} σ_{2} where (σ_{2}, C′_{2}) = gen(τ_{2}, A.x :σ, C_{2}).

Without loss of generality, we can assume that dom(C_{1}) ∩ dom(C_{2}) = dom(C ). This can always be achieved by a suitable renaming of the variables in C_{2}. Now, from Lemma 4.1, we have dom(C′_{1}) = (C_{1})^{∗}(fv A). But obviously (C_{1})^{∗}(fv A) = C^{∗}(fv A). Hence C′_{1} ⪯ C_{2}. So we can construct the following derivation

\frac{A, C_{1} ⊢′ e : τ_{1}  \frac{A.x :σ, C_{2} ⊢′ e : τ_{2}}{A.x :σ_{1}, C_{2} ⊢′ e : τ_{2}}}{A, C_{2} ⊢′ let x = e′ in e : τ_{2}} (Lemma 4.8) ; (let′)

Finally, we need to show that if gen(τ_{2}, A, C_{2}) = (σ_{3}, C′_{3}) then τ ⪯_{C} σ_{3}. Note that since fv(σ) ⊆ dom(C ) and C ⪯ C_{2}, we have fv(σ) ⊆ dom(C_{2}) and hence σ_{2} ⪯_{C} σ_{3} by Lemma 3.3. Thus, τ ⪯_{C} σ_{3} follows immediately.

This completes the proof.

5 Context-Preserving Unification

Type reconstruction usually relies on unification to compute most general types. One consequence of rule (∀−elim) is that the well-known syntactic unification algorithm of Robinson [Rob65] cannot be used since not every substitution of variables to types satisfies the given instance constraints. Nipkow and Snelting have shown that order-sorted unification can be used for reconstructing of types in Haskell [NS91], but it is not clear how to extend their result to parametric type classes. We show in this section that algorithm mgu, shown in Figure 6, yields the most general contextpreserving unifier of two types.

Function mgu takes two types and returns a transformer on constrained substitutions. The application mgu τ_{1} τ_{2} (S_{0}, C_{0}) returns a most general constrained substitution that unifies the types τ_{1} and τ_{2} and preserves (S_{0}, C_{0}), if such a substitution exists. The algorithm is similar to the one of Robinson, except for the case mgu α τ (S_{0}, C_{0}), where α may be substituted to τ only if τ can be shown to be an instance of C_{0}α. This constraint translates to an application of the subsidary function mgn to τ and C α.

The call mgn τ Γ (S, C ) computes a most general (S, C )−preserving normalizer of {τ::Γ}, provided one exists. This is accomplished by normalizing τ :: γ for each γ ∈ Γ through mgn′. In mgn′, it may in turn call mgu τ τ′ to solve a subproblem of the form C .α:: ({c τ′} ∪ Γ′) ⊢⊢ α:: c τ. The unification is required since all class constructors in a class set are pairwise disjoint. Thus, the above entailment has τ = τ′ as a logical consequence. The other call to mgu is made when solving the entailment C ⊢⊢ κ τ′ :: c τ. Since there is at most one instance declaration for each (κ, c) pair, it either fails or finds the proper instance declaration. To instantiate the instance declaration C′ ⇒ κ τ̃′:: c τ̃ , the standard pattern matching operation match is first called. It takes the pair of types (τ̃′, τ′) and returns a most general substitution S′ such that S′τ̃′ = τ′. Then, due to the at-most-one restriction, it calls mgu to unify τ and S′τ̃. Finally, it instantiates the declared context C′ and recursively normalize it.

Note that in an instance declaration, C′ ⇒ κ τ̃′::c τ̃ , the type τ̃′ is either a unit type or a tuple of distinct type variables. Besides, both fv(τ̃) and dom(C′) are contained in fv(τ̃′). Thus, it suffices to use the standard matching operation to instantiate an instance declaration, and no new type variables will be introduced in the normalization process. mgu : τ → τ → S × C → S × C mgn : τ → Γ → S × C → S × C

mgu τ_{1} τ_{2} (S, C )  = mgu′ (Sτ_{1}) (Sτ_{2}) (S, C )
mgu′ α α  = id_{S×C}
mgu′ α τ (S, C ) | α ∉ fv(τ) = mgn τ (C α) ([α ↦ τ] ∘ S, [α ↦ τ]C\_{α})
mgu′ τ α (S, C )  = mgu α τ (S, C )
mgu′ () ()  = id_{S×C}
mgu′ κ τ κ τ′ (S, C )  = mgu τ τ′ (S, C )
mgu′ (τ_{1} × τ_{2}) (τ′_{1} × τ′_{2})  = (mgu τ_{1} τ′_{1}) ∘ (mgu τ_{2} τ′_{2})
mgu′ (τ_{1} → τ_{2}) (τ′_{1} → τ′_{2})  = (mgu τ_{1} τ′_{1}) ∘ (mgu τ_{2} τ′_{2})
mgn τ {}  = id_{S×C}
mgn τ {γ} (S, C )  = mgn′ (Sτ) (Sγ) (S, C )
mgn τ (Γ_{1} ∪ Γ_{2})  = (mgn τ Γ_{1}) ∘ (mgn τ Γ_{2})
mgn′ α c τ (S, C )  = if ∃τ′.(c τ′ ∈ C α) then mgu τ τ′ (S, C )
else (S, C [α ↦ C α ∪ {c τ}])

mgn′ κ τ′ c τ (S, C ) | ∃ inst C′ ⇒ κ τ̃′::c τ̃ ∈ Ds

= let S′ = match τ̃′ τ′
(S′′, C′′) = mgu τ (S′τ̃) (S, C )
{τ_{1} ::Γ_{1}, …, τ_{n} ::Γ_{n}} = S′C′
in (mgn τ_{1} Γ_{1} ( … (mgn τ_{n} Γ_{n} (S′′, C′′))))

(and similarly for →, ×, ())

Figure 6: Unification and Normalization Algorithms

Consequently, we have the following lemma:

Lemma 5.1 Given a constrained substitution (S, C ) and types τ_{1}, τ_{2} such that both Sτ_{1} and Sτ_{2} are covered by C , if mgu τ_{1} τ_{2} (S, C ) = (S′, C′), then there exists a substitution R such that S′ = R ∘ S and both dom(R) and reg(R) are contained in C^{∗}(fv(Sτ_{1}) ∪ fv(Sτ_{2})).

Moreover, in the course of computing the unifier, whenever the substitution is extended with [α ↦ τ] in mgu′, the context constraints on α are discharged from C and all occurrences of α in C are replaced by τ. By doing so we obtain the following lemma:

Lemma 5.2 Given a constrained substitution (S, C ) and types τ_{1}, τ_{2} such that both Sτ_{1} and Sτ_{2} are covered by C , if mgu τ_{1} τ_{2} (S, C ) = (S′, C′), then (S′, C′) is a constrained substitution and dom(S′) \ dom(S) = dom(C ) \ dom(C′).

In order to prove the termination of the unification algorithm, we need to define some metric functions on sets and types. We write |s| for the number of elements in set s, and, overloading the | | operation, define |τ| to be the number of symbols in τ :

|α| = 1
|()| = 1
|κ τ| = 1 + |τ|
|(τ × τ′)| = 1 + |τ | + | τ′|
|(τ → τ′)| = 1 + |τ | + | τ′|

We now proceed to prove that call to mgu with proper arguments will always terminate.

Lemma 5.3 (Termination of mgu) Given a constrained substitution (S, C ), types τ̄_{1} and τ̄_{2} such that both Sτ̄_{1} and Sτ̄_{2} are covered by C , then mgu τ̄_{1} τ̄_{2} (S, C ) either fails or terminates.

Proof: We can think of the four functions, mgu, mgu′, mgn, mgn′, as mutually recursively defined over the tuple (τ̄_{1}, τ̄_{2}, τ̄_{3}, γ, Γ, (S, C )), where τ̄_{1} and τ̄_{2} are paired with mgu and mgu′, τ̄_{3} and Γ with mgn, and τ̄_{3} and γ with mgn′. The termination of them can be proved by defining a degree over the tuple:

(|dom(C )|, |τ̄_{3}|, |Γ|, |τ̄_{2}|, |τ̄_{1}|).

We order degrees lexicographically and argue that each recursive call reduces the degree.

From Lemma 5.2, we know that C is never enlarged by these functions and whenever S is extended, C will be correspondingly diminished. This fact explains why we put |dom(C )| as the first component of the degree and is crucial to the following argument.

Calls to mgu are unfolded to calls to mgu′. In mgu′, the recursive call to mgn diminishes |dom(C )| and the recursive calls to mgu are supplied with subcomponents of τ̄_{1}, τ̄_{2} and a possibly diminished C . For instance, the call mgu′ (τ_{1} × τ_{2}) (τ′_{1} × τ′_{2}) will be expanded to (mgu τ_{1} τ′_{1}) ∘ (mgu τ_{2} τ′_{2}). Then, we could get from mgu τ_{2} τ′_{2} (S, C ) some (S′, C′) such that |S′τ_{1}| > |(τ_{1}×τ_{2})| when unfolding mgu τ_{1} τ′_{1} (S′, C′). In that case, however, we would have |dom(C′)| < |dom(C )| by Lemma 5.2 and hence the degree would still be reduced. So we know that the degree is reduced in each case.

Function mgn recursively calls itself with a smaller class set and calls mgn′ only when a singleton class set is reached. In mgn′, the calls to mgu are unfolded, and, from the above argument for mgu′, we know that the degree will be reduced. Moreover, in recursively normailzing the context of an instance declaration, the series of recursive calls to mgn are passed the subcomponents of τ̄_{3} and a possibly diminished C , thus the degree will be reduced as the normalization process proceeds.

Since there is no infinite decreasing sequence of tuples of natural number, it follows that mgu τ̄_{1} τ̄_{2} (S, C ) either terminates or fails.

Lemma 5.4 (Soundness of mgu and mgn)

1. If mgn τ̄_{3} Γ (S, C ) = (S′, C′) then (S′, C′) ⪯ (S, C ) and C′ ⊢⊢ S′(τ̄_{3} ::Γ).

2. If mgu τ̄_{1} τ̄_{2} (S, C ) = (S′, C′) then S′τ_{1} = S′τ_{2} and (S′, C′) ⪯ (S, C ).

Proof: We use induction on the degree of the parameters.

If |dom(C )| = 0 then there is no type variable involved and so the lemma is vacuously true.

We now proceed to show that the lemma is also true for |dom(C )| = n + 1.

1. mgn τ̄_{3} Γ (S, C ) :

Induction base (Sτ̄_{3} = α), consider mgn α Γ (S, C ), α ∈ dom(C ) :

(a) Γ = {} : Obvious.

(b) Consider mgn′ α (c τ) (S, C ). There are two possibilities:

i. ∃τ′.(c τ′ ∈ C α) : We unfold the call mgu τ τ′ (S, C ). The interesting cases are: A. τ = β :

Let (S′, C′) = mgn τ′ (C β) ([β ↦ τ′] ∘ S, [β ↦ τ′]C\_{β}). Then, by induction on |dom(C\_{β})| we get

C′ ⊢⊢ (R′ ∘ ([β ↦ τ′])C\_{β}, and C′ ⊢⊢ S′(τ′::(C β))

where S′ = R′ ∘ ([β ↦ τ′] ∘ S). But, since S′β = R′τ′ and S′(C β) = R′(C β), by combining the above two entailments, we get C′ ⊢⊢ (R′ ∘ [β ↦ τ′])C and hence (S′, C′) ⪯ (S, C ). Moreover, since α ∈ dom(C ), we have C′ ⊢⊢ S′(α :: C α). Hence from (c τ′) ∈ C α and S′(c τ) = S′(c τ′) it is clear that C′ ⊢⊢ S′(τ̄_{3} :: c τ).

B. τ = τ_{1} × τ_{2} and τ′ = τ′_{1} × τ′_{2} : Let (S′, C′) = mgu τ_{2} τ′_{2} (S, C ). Then, by induction on |τ| and |τ′| using (2), we get

C′ ⊢⊢ R′C and S′τ_{2} = S′τ′_{2}

where S′ = R′ ∘ S. Now consider the second recursive call mgu τ_{1} τ′_{1} (S′, C′): If S′ = S then C′ = C by Lemma 5.2. So, again, by induction on |τ| and |τ′| using (2), let (S′′, C′′) = mgu τ_{1} τ′_{1} (S′, C′), then

C′′ ⊢⊢ R′′(R′C ) and S′′(τ_{1} × τ_{2}) = S′′(τ_{2} × τ′_{2})

where S′′ = R′′ ∘ S′, then By an argument similar to the one used in the previous case, we can easily show that C′′ ⊢⊢ S′′(τ̄_{3} :: c τ). Otherwise, we have |dom(C′)| < |dom(C )| by Lemma 5.2 and hence we can get the same result by induction on |dom(C )| using (2).

ii. Otherwise it is clear that (S, C [α ↦ C α ∪ {c τ}]) satisfies the requirement.

(c) Γ = Γ_{1} ∪ Γ_{2} : By a straightforward induction on Γ and possibly |dom(C )|.

Induction step (Sτ̄_{3} = κ τ′), Consider mgn′ (κ τ′) Γ (S, C ).

(a) Γ = {} : Obvious.

(b) Γ = {(c τ)}: Consider mgn′ (κ τ′) (c τ) (S, C ). Unfolding the call to mgu, and by a similar inductive argument used in the above, we have (S′′, C′′) ⪯ (S, C ) and S′′τ = S′′(S′τ̃). Then, since for all i, |τ′_{i}| < |κ τ′| and |dom(C′′)| ≤ |dom(C )|, we can get the result by a series of straightforward induction.

(c) Γ = Γ_{1} ∪ Γ_{2} : By a straightforward induction on Γ and possibly |dom(C )|.

2. mgu τ_{1} τ_{2} (S, C ) : By a similar induction, and using (1).

Lemma 5.5 (Completeness of mgu and mgn)

1. Given any constrained substitution (S̄, C̄ ), if (S̄, C̄ ) ⪯ (S, C ) and S̄τ̄_{1} = S̄τ̄_{2}, then mgu τ̄_{1} τ̄_{2} (S, C ) computes a constrained substitution (S′, C′), with S′τ̄_{1} = S′τ̄_{2} and (S̄, C̄ ) ⪯ (S′, C′) ⪯ (S, C ).

2. Given any constrained substitution (S̄, C ), if (S̄, C̄ ) ⪯ (S, C ) and C̄ ⊢⊢ S̄(τ̄_{3} :: Γ), then mgn τ̄_{3} Γ (S, C ) computes a constrained substitution (S′, C′), with C′ ⊢⊢ S′(τ̄_{3} :: Γ) and (S̄, C̄ ) ⪯ (S′, C′) ⪯ (S, C ).

Proof: We use induction on the degree of the parameters.

If |dom(C )| = 0, then there is no type variable involved and so the lemma is vacuously true.

We now proceed to to show that the lemma is also true for |dom(C )| = n + 1.

1. mgu τ̄_{1} τ̄_{2} (S, C ) : By induction on |Sτ̄_{1}| and |Sτ̄_{2}|.

(a) mgu′ α τ (S, C ) : Since S̄ unifies α and τ, we can write S̄ = R̄ ∘ ([α ↦ τ] ∘ S). Also, from the assumption (S̄, C̄ ) ⪯ (S, C ), we know that

C̄ ⊢⊢ R̄(τ::C α) and C̄ ⊢⊢ R̄([α ↦ τ]C\α).

Now let (S′, C′) = mgn τ (C α) ([α ↦ τ] ∘ S, [α ↦ τ]C\_{α}). Then, by induction on |dom(C )| using (2), we get

(S̄, C̄ ) ⪯ (S′, C′) ⪯ ([α ↦ τ] ∘ S, [α ↦ τ]C\_{α})

where S′ = R′ ∘ ([α ↦ τ] ∘ S). To complete the proof in this case, we need to show that C′ ⊢⊢ R′(τ :: C α). But this follows directly from (1) of Lemma 5.4. So, we have C′ ⊢⊢ (R′ ∘ [α ↦ τ])C and hence (S̄, C̄ ) ⪯ (S′, C′) ⪯ (S, C ).

(b) mgu′ (κ τ_{1}) (κ τ_{2}) (S, C ) : By a straightforward induction.

(c) mgu′ (τ_{1} × τ_{2}) (τ′_{1} × τ′_{2}) (S, C ) : By a straightforward induction.

2. mgn τ̄_{3} Γ (S, C ) :

Induction base (Sτ̄_{3} = α): Consider mgn α Γ (S, C ) :

(a) Γ = {} : Obvious.

(b) Consider mgn′ α (c τ) (S, C ). There are two possibilities:

i. ∃τ′.(c τ′ ∈ C α) : We unfold the call mgu τ τ′ (S, C ). The interesting cases are:

• τ = β : In order to induction on |dom(C )|, we need to verify that

(S̄, C̄ ) ⪯ ([β ↦ τ′] ∘ S, [β ↦ τ′]C\_{β}) and C̄ ⊢⊢ S̄(τ′::C β).

Suppose that S̄ = R̄ ∘ S, then, from the assumptions, we have

C̄ ⊢⊢ R̄(α::c β) and C̄ ⊢⊢ R̄C .

Now, since we know that (c τ′) ∈ C α and C̄ ⊢⊢ R̄(α :: c τ′), then, due to our requirements on instance declarations, we have R̄β = R̄τ′. Moreover, as β ∈ dom(C ), we have C̄ ⊢⊢ R̄(β::C β). It then follows that C̄ ⊢⊢ S̄(τ′::C β). Now let R̄ = R̃ ∘ [β ↦ τ′]. Then

S̄ = R̃ ∘ ([β ↦ τ′] ∘ S) and C̄ ⊢⊢ R̃([β ↦ τ′]C\_{β}).

In other words,

(S̄, C̄ ) ⪯ ([β ↦ τ′] ∘ S, [β ↦ τ′]C\_{β}).

Next, let (S′, C′) = mgn τ′ (C β) ([β ↦ τ′]∘S, [β ↦ τ′]C\_{β}). and S′ = R′∘([β ↦ τ′] ∘ S). Then by induction on |dom(C )|, we get

(S̄, C̄ ) ⪯ (S′, C′), C′ ⊢⊢ (R′ ∘ [β ↦ τ′])C\_{β}, and C′ ⊢⊢ S′(τ′::C β).

But S′β = S′τ′, so

C′ ⊢⊢ (R′ ∘ [β ↦ τ′])C .

Hence (S′, C′) ⪯ (S, C ) and C′ ⊢⊢ R′(α::(c β)).

• τ = τ_{1} × τ_{2} and τ′ = τ′_{1} × τ′_{2} : Note that if S̄ = R̄ ∘ S then R̄τ = R̄τ′, since C̄ ⊢⊢ R̄(α::(c τ)) and (c τ′) ∈ C α. Hence the result follows from a straightforward induction using 1.

ii. Otherwise it is clear that (S, C [α ↦ C α ∪ {c τ}]) satisfies the requirement.

(c) Γ = Γ_{1} ∪ Γ_{2} : By a straightforward induction on |Γ| and possibly |dom(C )|.

Induction step (Sτ̄_{3} = κ τ′): Consider mgn′ (κ τ′) Γ (S, C ).

(a) Γ = {} : Obvious.

(b) Γ = {(c τ)}: Consider mgn′ (κ τ′) (c τ) (S, C ). Note that if S̄ = R̄ ∘ S then R̄τ = R̄(S′τ̃) since C̄ ⊢⊢ R̄((κ τ′) :: (c τ)), inst C′ ⇒ κ τ̃′ :: c τ̃ ∈ Ds, and S′ = match τ̃′ τ′. Thus, by a similar inductive argument for mgu τ (S′τ̃) (S, C ) using 1, we get (S̄, C̄ ) ⪯ (S′′, C′′) ⪯ (S, C ) and S′′τ = S′′(S′τ̃). Then since for all i, |τ′_{i}| < |κ τ′| and |dom(C′′)| ≤ |dom(C )|, we can get the result by a straightforward induction.

(c) Γ = Γ_{1} ∪ Γ_{2} : By a straightforward induction.

Based on these lemmas, we have the following theorem for our unification algorithm.

Theorem 5.6 Given a constrained substitution (S_{0}, C_{0}) and types τ_{1}, τ_{2}, if there is a (S_{0}, C_{0})- preserving unifier of τ_{1} and τ_{2} then mgu τ_{1} τ_{2} (S_{0}, C_{0}) returns a most general such unifier. If there is no such unifier then mgu τ_{1} τ_{2} (S_{0}, C_{0}) fails in a finite number of steps.

tp (x, A, S, C )  = inst (S(Ax), S, C )
tp (e_{1} e_{2}, A, S, C )  = let (τ_{1}, S_{1}, C_{1}) = tp (e_{1}, A, S, C )

(τ_{2}, S_{2}, C_{2}) = tp (e_{2}, A, S_{1}, C_{1})

α a fresh type variable

(S_{3}, C_{3}) = mgu τ_{1} (τ_{2} → α) (S_{2}, C_{2}.α::{}) in (S_{3}α, S_{3}, C_{3})

tp (λx.e, A, S, C )  = let α a fresh type variable

(τ_{1}, S_{1}, C_{1}) = tp (e_{1}, A.x :α, S, C .α::{}) in (S_{1}α → τ_{1}, S_{1}, C_{1})

tp (let x = e_{1} in e_{2}, A, S, C ) = let (τ_{1}, S_{1}, C_{1}) = tp (e_{1}, A, S, C )

(σ, C_{2}) = tpgen (τ_{1}, S_{1}A, C_{1}, C ) in tp (e_{2}, A.x :σ, S_{1}, C_{2})

where

inst (∀α::Γ.σ, S, C )  = let β a fresh type variable
in inst ([α ↦ β] σ, S, C .β::Γ)
inst (τ, S, C )  = (τ, S, C )
tpgen (σ, A, C , C′)  = if ∃α ∈ dom(C )\(fv(A) ∪ reg(C ) ∪ dom(C′))then
tpgen (∀α::C α.σ, A, C\_{α}, C′)
else (σ, C )

Figure 7: Type Reconstruction Algorithm

6 Type Reconstruction

This section discusses type reconstruction. Having developed the unification algorithm needed for parametric type classes, we can proceed to present a type reconstruction algorithm, and state its soundness and completeness with respect to the inference rules given in Section 3 using those rules in Section 4 and the equivalence result established therein. As a corollary of these results, we obtain a prinicpal type scheme property of our system analogous to the one in [DM82]. The type reconstruction algorithm has been implemented in the Yale Haskell compiler. Its size and complexity compare favorably to the type reconstruction parts of our prior Haskell compiler.

An algorithm for type reconstruction is shown in Figure 7.^{2} Function tp takes as arguments an expression, an assumption set, and an initial constrained substitution, and returns a type and a final constrained substitution. The function is straightforwardly extended to programs. The remainder of this section establishes the correspondence between tp and the type system of Section 4 and, thereby, that of Section 3.

We need the following lemmas to establish the soundness and completeness of our algorithm. We begin by showing that tp is indeed a constrained substitution transformer.

2This is actually a simplification of the real algorithm becuase we can get a cyclic context after the call to unification function and thus violate our restriction on contexts. So what is missing here is a clique-detection algorithm, which is simply a variant of occur checking. We omit it here for simplicity.

Lemma 6.1 Given a constrained substitution (S, C ), an expression e, and type assumption set A such that SA is covered by C , if tp(e, A, S, C ) = (τ, S′, C′), then (S′, C′) is a constrained substitution and S′ = R ∘ S for some substitution R.

Proof: By a straightforward induction, and using Lemma 5.1 and Lemma 5.2.

Hence we shall often omit the requirement of constrained substitution from now on when writing tp(e, A, S, C ).

One may notice that we have used a new generalization function in dealing with let-expression. The reason for doing so can be stated as follows. Recall the typing rule (let′) presented in Section 4. There are two contexts used in the antecedent part of that rule : one for deriving the type of the let-definition and one for the type of the let-body. But only the second one appears in the conclusion part and it is those instance assumptions contained in the first one that are generalized by the gen function. While in tp, we maintain a single context and pass it through the whole algorithm. If we were to use the gen function in the let-expression in tp we would overgeneralize those instance assumptions generated in the previous stages and passed to tp as part of the initial context.

To avoid such overgeneralization, we need to confine the domain of generalization to only those instance assumptions generated while reconstructing the type of the let-definition. The new generalization function, tpgen, compared to gen, takes an extra context parameter, C′, whose instance assumptions will be excluded from generalization. Then, in the algorithm, when doing generalization, we pass the initial context to tpgen as the second context argument to restrict the domain of generalization. Hence only those newly generated instance assumptions will be generalized.

The following lemma shows that the context is preserved during the type reconstruction process and thus justifies our scheme.

Lemma 6.2 Given a constrained substitution (S, C ), an expression e, and type assumption set A such that SA is covered by C , if tp(e, A, S, C ) = (τ, S′, C′) then (S′, C′) ⪯ (S, C ).

Proof: By induction on the structure of e, but we need some stronger induction hypothesis. Let S′ = R ∘ S. The induction hypothesis is:

1. dom(C ) ⊆ dom(S′) ⊎ dom(C′).

2. fv(τ) ⊆ dom(C′) and hence (C′)^{∗}(fv τ) ⊆ dom(C′).

3. fv(S′A) ⊆ dom(C′) and hence (C′)^{∗}(fv S′A) ⊆ dom(C′).

4. RC is covered by C′.

5. If ρ ∈ dom(C )\C^{∗}(fv SA) then ρ ∈ dom(C′)\(C′)^{∗}(fv S′A), but ρ ∉ dom(R), ρ ∉ (C′)^{∗}(fv τ) and ρ ∉ (C′)^{∗}(reg R).

6. (S′, C′) ⪯ (S, C ).

Case e = x : Suppose that x : σ ∈ A and S is safe for σ. Let σ = ∀α_{i} :: Γ_{i} τ′ and β_{i} be new type variables. We have

tp(x, A, S, C ) = inst(S(Ax), S, C )
= inst(∀α_{i} ::SΓ_{i}.Sτ′, S, C )
= (J (Sτ′), S, C ⊎ C_{0})

where J = [α_{i} ↦ β_{i}] and C_{0} = {β_{i} ::J (SΓ_{i})}

So, τ = J (Sτ′), S′ = S, C′ = C ⊎ C_{0}, and R = id. Therefore

1. Obvious.

2.

fv(τ) ⊆ fv(Sσ) ∪ {β_{i}}
⊆ fv(SA) ∪ {β_{i}}
⊆ dom(C′).

3. Obvious.

4. Obvious.

5. Obvious.

6. Obvious.

Case e = λx.e′ : By a straightforward induction.

Case e = e_{1}e_{2} : We have

tp (e_{1} e_{2}, A, S, C ) = let (τ_{1}, S_{1}, C_{1}) = tp (e_{1}, A, S, C )

(τ_{2}, S_{2}, C_{2}) = tp (e_{2}, A, S_{1}, C_{1})

α a fresh type variable

(S_{3}, C_{3}) = mgu τ_{1} (τ_{2} → α) (S_{2}, C_{2}.α::{}) in (S_{3}α, S_{3}, C_{3})

Now in order to use the lemmas for the unification algorithm, we need to show that fv(S_{2}τ_{1}) ∪ fv(S_{2}τ_{2}) ⊆ dom(C_{2}). From the induction hypothesis of (2), we have fv(τ_{1}) ⊆ dom(C_{1}) and fv(τ_{2}) ⊆ dom(C_{2}). But, since both (S_{1}, C_{1}) and (S_{2}, C_{2}) are constrained substitution, we know that S_{1}τ_{1} = τ_{1} and S_{2}τ_{2} = τ_{2}, and hence it suffices to look into fv(R_{2}τ_{1}) only where S_{2} = R_{2} ∘ S_{1}.

Consider type variable β, β ∈ fv(τ_{1}). By the induction hypothesis of (6), we know that C_{2} ⊢⊢ R_{2}C_{1}. Thus, if β ∈ (C_{1})^{∗}(fv S_{1}A) then fv(R_{2}β) ⊆ (C_{2})^{∗}(fv S_{2}A) according to Lemma 4.3, and hence fv(R_{2}β) ⊆ dom(C_{2}) by the induction hypothesis of (3). Otherwise, we have β ∉ dom(R_{2}) according to the induction hypothesis of (5) and hence β ∈ dom(C_{2}) by the induction hypothesis of 1. Therefore fv(S_{2}τ_{1}) ∪ fv(S_{2}τ_{2}) ⊆ dom(C_{2}) and hence (C_{2})^{∗}(fv(S_{2}τ_{1}) ∪ fv(S_{2}τ_{2})) ⊆ dom(C_{2}) since C_{2} is closed.

Let S_{1} = R_{1} ∘ S, S_{2} = R_{2} ∘ S_{1}, and S_{3} = R_{3} ∘ S_{2}. We continue our proof:

1. By induction,

dom(C ) ⊆ dom S_{1} ⊎ dom C_{1} ⊆ dom S_{2} ⊎ dom C_{2}

From Lemma 5.2, dom(C_{2}.α :: {}) \ dom(C_{3}) = dom(R_{3}). Thus, dom(S_{2}) ⊎ dom(C_{2}) ⊆ dom(S_{3}) ⊎ dom(C_{3}), and hence dom(C ) ⊆ dom(S_{3}) ⊎ dom(C_{3}).

2. We know that τ = S_{3}α. If α ∈ dom(R_{3}) then, from Lemma 5.1, we know that reg(R_{3}) ⊆ dom(C_{2}), so fv(S_{3}α) ⊆ dom(C_{2}). Moreover, from Lemma 5.2, dom(C_{2}.α:: {}) \ dom(C_{3}) = dom(R_{3}). But, since dom(R_{3}) ∩ reg(R_{3}) = ∅, so we have fv(S_{3}α) ⊆ dom(C_{3}). Otherwise, α ∉ dom(R_{3}) and fv(S_{3}α) = α. Hence α ∈ dom(C_{3}) as dom(C_{2}.α::{})\dom(C_{3}) = dom(R_{3}).

3. By induction, (C_{2}^{∗})(fv S_{2}A) ⊆ dom(C_{2}). From Lemma 5.1, reg(R_{3}) ⊆ dom(C_{2}.α:: {}), and hence fv(S_{3}A) ⊆ dom(C_{2}.α :: {}). Moreover, from Lemma 5.2, we know that dom(C_{2} α :: {}) \ dom(R_{3}) = dom(C_{3}). But, since none of the variable in dom(R_{3}) occurs in fv(S_{3}A), we have fv(S_{3}A) ⊆ dom(C_{3}) and hence (C_{3})^{∗}(fv S_{3}A) ⊆ dom(C_{3}) as C_{3} is closed.

4. By induction,

fv(R_{1}C ) ⊆ dom(C_{1}) and fv(R_{2}C_{1}) ⊆ dom(C_{2}).

So we have fv(R_{2}R_{1}C ) ⊆ dom(C_{2}). Moreover, from Lemma 5.1 and Lemma 5.2, we know that

dom(R_{3}), reg(R_{3}) ⊆ dom(C_{2}.α::{}) and dom(C_{2}.α::{}) \ dom(C_{3}) = dom(R_{3}).

But since dom(R_{3}) ∩ reg(R_{3}) = ∅, it then follows that fv(R_{3}R_{2}R_{1}C ) ⊆ dom(C_{3}).

5. For any ρ, ρ ∈ dom(C ) \ C^{∗}(fv SA), we have, by induction, ρ ∈ dom(C_{2}) \ (C_{2})^{∗}(fv S_{2}A), but ρ ∉ dom(R_{1}) ∪ (C_{1})^{∗}(fv τ_{1}) ∪ (C_{1})^{∗}(reg R_{1}) and ρ ∉ dom(R_{2}) ∪ (C_{2})^{∗}(fv τ_{2}) ∪ (C_{2})^{∗}(reg R_{2}).

Next, from Lemma 5.1, dom(R_{3}) ∪ reg(R_{3}) ⊆ (C_{2})^{∗}(fv R_{2}τ_{1}) ∪ (C_{2}^{∗})(fv τ_{2}) ∪ {α}. So, we have ρ ∉ dom(R_{3}) ∪ fv(τ) ∪ reg(R_{3}) where τ = S_{3}α. Moreover, from Lemma 5.2, dom(C_{2}.α:: {}) \ dom(C_{3}) = dom(R_{3}). In other words, ρ ∈ dom(C_{3}), but ρ ∉ fv(S_{3}A). Now, since dom(C_{3}) ⊆ dom(C_{2}), clearly we have ρ ∈ dom(C_{3}) \ (C_{3})^{∗}(fv S_{3}A), but ρ ∉ dom(R_{3}) ∪ (C_{3})^{∗}(fv τ) ∪ (C_{3})^{∗}(reg R_{3}).

Finally, R = R_{3} ∘R_{2} ∘R_{1}. It follows from the argument above that ρ ∉ dom(R)∪(C_{3})^{∗}(fv τ)∪ (C_{3})^{∗}(reg R).

6. By a straightforward induction, and using Lemma 5.4.

Case e = (let x = e_{1} in e_{2}) : we have

tp (let x = e_{1} in e_{2}, A, S, C ) = let (τ_{1}, S_{1}, C_{1}) = tp (e_{1}, A, S, C )
(σ, C_{2}) = tpgen (τ_{1}, S_{1}A, C_{1}, C )
(τ_{2}, S_{2}, C_{3}) = tp (e_{2}, A.x :σ, S_{1}, C_{2})
in (τ_{2}, S_{2}, C_{3})

By the induction hypothesis of (3), (C_{1})^{∗}(fv S_{1}A) ⊆ dom(C_{1}). To do induction on the second recursive call, we need to show that (C_{2})^{∗}(fv S_{1}(A.x : σ)) ⊆ dom(C_{2}). Suppose that σ = ∀α_{i} :: Γ_{i}.τ_{1}. Then we have dom(C_{1}) \ dom(C_{2}) = {α_{i}}, fv(σ) ⊆ (C_{1}^{∗})(fv S_{1}A), and none of the α_{i} can occur in (C_{1})^{∗}(fv S_{1}A) according to tpgen’s definition. So, fv(S_{1}(A.x : σ)) ⊆ dom(C_{2}) and hence (C_{2}^{∗})(fv S_{1}(A.x :σ)) ⊆ dom(C_{2}).

Let S_{1} = R_{1} ∘ S and S_{2} = R_{2} ∘ S_{1}. We continue the proof:

1. By induction, dom(C ) ⊆ dom(S_{1}) ⊎ dom(C_{1}) and dom(C_{2}) ⊆ dom(S_{2}) ⊎ dom(C_{3}). To complete the proof, it suffices to show that dom(C ) ⊆ dom(S_{1}) ⊎ dom(C_{2}). But, since none of the α_{i} occurs in dom(C ), this is obviously true. Hence dom(C ) ⊆ dom(S_{2}) ⊎ dom(C_{3}) follows directly by induction on the second recursive call.

2. By a straightforward induction.

3. By a straightforward induction.

4. By induction, fv(R_{1}C ) ⊆ dom(C_{1}) and fv(R_{2}C_{2}) ⊆ dom(C_{3}). To completethe proof, it suffices to show that none of the α_{i} occurs in fv(R_{1}C ); this in turn can be shown by considering fv(R_{1}α) for α ∈ dom(C ): If α ∈ C^{∗}(fv SA), then, from Lemma 4.3, fv(R_{1}α) ⊆ (C_{1})^{∗}(fv S_{1}A) and hence none of the α_{i} occurs in fv(R_{1}α) in this case. Otherwise, α ∉ dom(R_{1}) according to the induction hypothesis of (5) and hence R_{1}α = α. But, since none of the α_{i} occurs in dom(C ), we know that α ≠ α_{i}, for all i. Therefore, fv(R_{1}C ) ⊆ dom(C_{2}), and hence fv(R_{2}R_{1}C ) ⊆ dom(C_{3}).

5. For any ρ, ρ ∈ dom(C ) \ C^{∗}(fv SA), we have, by induction, ρ ∈ dom(C_{1}) \ (C_{1})^{∗}(fv S_{1}A), but ρ ∉ dom(R_{1}) ∪ (C_{1})^{∗}(fv τ_{1}) ∪ (C_{1})^{∗}(reg R_{1}). By the definition of tpgen, we have ρ ∈ dom(C_{2}) and dom(C_{2}) ⊆ dom(C_{1}). Thus, ρ ∈ dom(C_{2}) \ (C_{2})^{∗}(fv S_{1}A) and the result follows directly by induction on the second recursive call.

6. By induction, (S_{1}, C_{1}) ⪯ (S, C ) and (S_{2}, C_{3}) ⪯ S_{1}, C_{2}). To complete the proof we need to show (S_{1}, C_{2}) ⪯ (S, C ). By an argument similar to the one used in (4), we know that none of the α_{i} occurs in R_{1}C . So, (S_{1}, C_{2}) ⪯ (S, C ) and C_{3} covers R_{2}R_{1}C . It then follows immediately that (S_{2}, C_{3}) ⪯ (S, C ).

Now we can proceed to prove the soundness of our algorithm.

Theorem 6.3 If tp(e, A, S, C ) = (τ, S′, C′) then S′A, C′ ⊢′ e : τ.

Proof: By induction on the structure of e.

Case e = x : Suppose that x : σ ∈ A and S is safe for σ. Let σ = ∀α_{i} :: Γ_{i} τ′ and β_{i} be new type variables. We have

tp(x, A, S, C ) = inst(S(Ax), S, C )
= inst(∀α_{i} ::SΓ_{i}.Sτ′, S, C )
= (J (Sτ′), S, C ⊎ C_{0})

where J = [α_{i} ↦ β_{i}] and C_{0} = {β_{i} ::J (SΓ_{i})} So, τ = J (Sτ′), S′ = S, and C′ = C ⊎ C_{0}. Clearly, τ ⪯_{C′} S′σ and hence

S′A, C′ ⊢′ x : τ

using (var′) rule.

Case e = e_{1}e_{2} : We have

tp (e_{1} e_{2}, A, S, C ) = let (τ_{1}, S_{1}, C_{1}) = tp (e_{1}, A, S, C )

(τ_{2}, S_{2}, C_{2}) = tp (e_{2}, A, S_{1}, C_{1})

α a fresh type variable

(S_{3}, C_{3}) = mgu τ_{1} (τ_{2} → α) (S_{2}, C_{2}.α::{}) in (S_{3}α, S_{3}, C_{3})

By induction,

S_{1}A, C_{1} ⊢′ e_{1} : τ_{1} and S_{2}A, C_{2} ⊢′ e_{2} : τ_{2}.

Let S_{1} = R_{1} ∘ S, S_{2} = R_{2} ∘ S_{1}, S_{3} = R_{2} ∘ S_{2}. From Lemma 6.2, we have C_{1} ⊢⊢ R_{1}C , C_{2} ⊢⊢ R_{2}C_{1}. Furthermore, we know that S_{3}τ_{1} = S_{3}(τ_{2} → α) and C_{3} ⊢⊢ R_{3}(C_{2}.α:: {}) from Lemma 5.4. Hence C_{3} ⊢⊢ R_{3}(R_{2}C_{1}) and we can construct the following derivation

\frac{S_{1}A, C_{1} ⊢′ e_{1} : τ_{1}}{\frac{S_{3}A, C_{3} ⊢′ e_{1} : S_{3}τ_{1}}{S_{3}A, C_{3} ⊢′ e_{1} : S_{3}τ_{2} → S_{3}α}}  (Lemma 4.6) ; (Lemma 5.4)  \frac{S_{2}A, C_{2} ⊢′ e_{2} : τ_{2}}{S_{3}A, C_{3} ⊢′ e_{2} : S_{3}τ_{2}}

S_{3}A, C_{3} ⊢′ e_{1}e_{2} : S_{3}α

(Lemma 4.6) (λ−elim′)

Case e = λx.e′ : By a straightforward induction.

Case e = (let x = e_{1} in e_{2}) : We have

tp (let x = e_{1} in e_{2}, A, S, C ) = let (τ_{1}, S_{1}, C_{1}) = tp (e_{1}, A, S, C )
(σ, C_{2}) = tpgen (τ_{1}, S_{1}A, C_{1}, C )
(τ_{2}, S_{2}, C_{3}) = tp (e_{2}, A.x :σ, S_{1}, C_{2})
in (τ_{2}, S_{2}, C_{3})

By induction

S_{1}A, C_{1} ⊢′ e_{1} : τ_{1} and S_{2}A.x :S_{2}σ, C_{3} ⊢′ e_{2} : τ_{2}

We shall combine these two derivations using Lemma 4.5 to complete the proof.

First, let (σ̄, C̄ ) = gen(τ_{1}, S_{1}A, C_{1}). Then, σ̄ = ∀α_{i} :: Γ_{i}.σ for some i, i ≥ 0, and {α_{i} :: Γ_{i}} ⊆ C_{2} according to the definitions of gen and tpgen. Next, let S_{2} = R_{2} ∘S_{1}. From Lemma 6.2, C_{3} ⊢⊢ R_{2}C_{2}. Hence C_{3} ⊢⊢ R_{2}C̄ , since C̄ ⪯ C_{2}. Now, applying Lemma 4.5 to σ̄, R_{2}, and C_{3}, we get a substitution R and a context C′ such that

R(S_{1}A) = R_{2}(S_{1}A), C′ ⊢⊢ RC_{1}, R_{2}σ̄ = σ′ and C′′ ⪯ C_{3}

where (σ′, C′′) = gen(Rτ_{1}, R_{2}(S_{1}A), C′).

Finally, it is clear that σ ⪯_{C_{2}} σ̄ by Lemma 3.3 and Lemma 3.4. Then, from C_{3} ⊢⊢ R_{2}C_{2}, we have, by Lemma 3.5, R_{2}σ ⪯_{C_{3}} R_{2}σ̄. But S_{2}σ = R_{2}σ, hence S_{2}σ ⪯_{C_{3}} σ′. Therefore, we can construct the following derivation

\frac{S_{1}A, C_{1} ⊢′ e_{1} : τ_{1}}{\frac{R(S_{1}A), C′ ⊢′ e_{1} : Rτ_{1}}{S_{2}A, C′ ⊢′ e_{1} : Rτ_{1}}}  (Lemma 4.6) ; (Lemma 4.5)  \frac{S_{2}A.x :S_{2}σ, C_{3} ⊢′ e_{2} : τ_{2}}{S_{2}A.x :σ′, C_{3} ⊢′ e_{2} : τ_{2}}

S_{2}A, C_{3} ⊢′ let x = e_{1} in e_{2} : τ_{2}

(Lemma 4.8) (let′)

This completes the proof.

Together with Theorem 4.9, we have the following soundness result.

Corollary 6.4 (Soundness of tp) If tp(e, A, S, C ) = (τ, S′, C′) then S′A, C′ ⊢ e : τ.

Ultimately, we will state and prove that tp is able to compute the most general derivable typing for a given term.

Theorem 6.5 Suppose that S′A, C′ ⊢′ e : τ′ and (S′, C′) ⪯ (S_{0}, C_{0}). Then tp(e, A, S_{0}, C_{0}) succeeds with (τ, S, C ), and there is a substitution R such that

1. S′ = RS, except on new type variables of tp(e, A, S_{0}, C_{0}),

2. C′ ⊢⊢ RC , and

3. τ′ = Rτ.

Proof: Let R_{0} be the substitution such that S′ = R_{0} ∘ S_{0} and C′ ⊢⊢ R_{0}C_{0}. We prove this theorem, again, by induction on the structure of S′A, C′ ⊢′ e : τ′.

Case(var′) : We have a derivation of the form :

S′A, C′ ⊢′ x : τ′ (x : σ ∈ A, τ′ ⪯_{C′} S′σ).

Without loss of generality, we can assume that variables in σ have been suitably renamed so that no name clash will occur in the following proof. Let σ = ∀α_{i} ::Γ_{i}.ν. Then S′σ = ∀α_{i} ::S′Γ_{i}.S′ν.

As τ′ ⪯_{C′} S′σ, there are types τ_{i} such that

[α_{i} ↦ τ_{i}](S′ν) = τ′ and C′ ⊢⊢ {τ_{i} ::[α_{i} ↦ τ_{i}](S′Γ_{i})}.

On the other hand, let β_{i} be new type variables, we have

tp(x, A, S_{0}, C_{0}) = ([α_{i} ↦ β_{i}](S_{0}ν), S_{0}, C_{0} ⊎ C_{1})

where C_{1} = {β_{i} ::[α_{i} ↦ β_{i}](S_{0}Γ_{i})}. In other words, τ = [α_{i} ↦ β_{i}](S_{0}ν), S = S_{0}, and C = C_{0} ⊎ C_{1}.

Now let R = [β_{i} ↦ τ_{i}]R_{0}. Then, clearly S′ = RS except on the new type variables β_{i}. Moreover, we have

Rτ = ([β_{i} ↦ τ_{i}]R_{0})[α_{i} ↦ β_{i}]S_{0}ν
= ([β_{i} ↦ τ_{i}][α_{i} ↦ β_{i}])(R_{0}S_{0})ν (R_{0} safe for α_{i})
= [α_{i} ↦ τ_{i}]S′ν
= τ′

and RC = R_{0}C_{0} ⊎ RC_{1}. But, since

RC_{1} = [β_{i} ↦ τ_{i}]R_{0}({β_{i} ::[α_{i} ↦ β_{i}]S_{0}Γ_{i}})
= {τ_{i} ::[α_{i} ↦ τ_{i}]R_{0}S_{0}Γ_{i}}
= {τ_{i} ::[α_{i} ↦ τ_{i}](S′Γ_{i})},

so we have C′ ⊢⊢ RC as well. Case(λ−elim′) : We have a derivation of the form :

\frac{S′A, C′ ⊢′ e_{1} : τ_{1} → τ_{2} S′A, C′ ⊢′ e_{2} : τ_{1}}{S′A, C′ ⊢′ e_{1}e_{2} : τ_{2}}

By induction, tp(e_{1}, A, S_{0}, C_{0}) = (ν_{1}, S_{1}, C_{1}) succeeds and there is a substitution R_{1} such that 1. S′ = R_{1}S_{1}, except on Δ_{1},

2. C′ ⊢⊢ R_{1}C_{1}, and

3. R_{1}ν_{1} = τ_{1} → τ_{2}. where Δ_{1} is the set of new type variables of tp(e_{1}, A, S_{0}, C_{0}). Clearly, S′A = (R_{1}S_{1})A and hence (R_{1}S_{1})A, C′ ⊢′ e_{2} : τ_{1}. So, by induction , tp(e_{2}, A, S_{1}, C_{1}) = (ν_{2}, S_{2}, C_{2}) succeeds and there is a substitution R_{2} such that

1. R_{1}S_{1} = R_{2}S_{2}, except on Δ_{2},

2. C′ ⊢⊢ R_{2}C_{2}, and

3. R_{2}ν_{2} = τ_{1}. where Δ_{2} is the set new type variables of tp(e_{2}, A, S_{1}, C_{1}). Now let α be a new variable and R′ = [α ↦ τ_{2}]R_{2}S_{2}. Then, clearly

S′ = R′ except on Δ_{1} ∪ Δ_{2} ∪ {α}

and

C′ ⊢⊢ [α ↦ τ_{2}]R_{2}(C_{2}.α::{}).

In addition, we show that (R′, C′) is indeed a (S_{2}, C_{2}.α::{})−preserving unifier of ν_{1} and ν_{2} → α:

R′ν_{1} = (R_{2}S_{2})ν_{1}  (α new)
= (R_{1}S_{1})ν_{1}  (R_{1}S_{1} = R_{2}S_{2} except on Δ_{2})
= R_{1}ν_{1}  (S_{1}C_{1} = C_{1})
= τ_{1} → τ_{2}
= R_{2}ν_{2} → R′α
= R_{2}(S_{2}ν_{2}) → R′α (S_{2}C_{2} = C_{2})
= R′ν_{2} → R′α  (α new)
= R′(ν_{2} → α)

Thus, from Theorem 5.6, mgu ν_{1} (ν_{2} → α) (S_{2}, C_{2}.α::{}) succeeds with (S_{3}, C_{3}) such that S_{3}ν_{1} = S_{3}(ν_{2} → α), R′ = R ∘ S_{3} and C′ ⊢⊢ RC_{3} for some substitution R.

Since mgu does not introduce any new type variables, we know that Δ_{1} ∪ Δ_{2} ∪ {α} is the set of new type variables of tp(e_{1}e_{2}, A, S_{0}, C_{0}). Therefore, tp(e_{1}e_{2}, A, S_{0}, C_{0}) succeeds with (S_{3}α, S_{3}, C_{3}) and R is the required substitution:

1. S′ = RS_{3}, except on new type variables of tp(e_{1}e_{2}, A, S_{0}, C_{0}),

2. C′ ⊢⊢ RC_{3}, and

3. τ_{2} = R′α = R(S_{3}α).

Case(λ−intro′) : We have a derivation of the form :

\frac{S′A.x :τ′, C′ ⊢′ e : τ}{S′A, C′ ⊢′ λx.e : τ′ → τ}

Let α be a new type variable and S′′ = [α ↦ τ′] ∘ S′. Then, S′′(A.x : α), C′ ⊢′ e : τ and (S′′, C′) ⪯ (S_{0}, C_{0}.α:: {}). So, by induction, tp(e, A.x : α, S_{0}, C_{0}.α:: {}) = (τ_{1}, S, C ) succeeds and there is a substitution R such that

1. S′′ = RS except on the new type variables of tp(e, A.x :α, S_{0}, C_{0}.α::{}),

2. C′ ⊢⊢ RC , and

3. Rτ_{1} = τ.

Therefore, tp(λx.e, A, S_{0}, C_{0}) succeeds with (Sα → τ_{1}, S, C ) and R is the required substitution :

1. S′ = RS except on new type variables of tp(λx.e, A, S_{0}, C_{0})

2. C′ ⊢⊢ RC , and

3. R(Sα → τ_{1}) = S′′α → τ = τ′ → τ.

Case(let′) : We have a derivation of the form:

\frac{S′A, D ⊢′ e_{1} : τ_{1} S′A.x :σ′, C′ ⊢′ e_{2} : τ_{2}}{S′A, C′ ⊢′ let x = e_{1} in e_{2} : τ_{2}}

where (σ′, C′′) = gen(τ_{1}, S′A, D) and C′′ ⪯ C′.

We cannot do a direct induction on S′A, D ⊢′ e_{1} : τ_{1}, since this would require (S′, D) ⪯ (S_{0}, C_{0}), which is not true in general. But, we note that (S, D∪C′) can suit our purpose here. Without loss of generality, we can assume that dom(D) ∩ dom(C′) = dom(C′′). So, D ⋈ C′, and if σ′ = ∀α_{i} ::Γ_{i}.τ_{1} then D ∪ C′ = {α_{i} ::Γ_{i}} ⊎ C′ and hence (S′, D ∪ C′) ⪯ (S_{0}, C_{0}).

Moreover, S′A, D ∪ C′ ⊢′ e_{1} : τ_{1} by Lemma 4.7. So, by indution, tp(e_{1}, A, S_{0}, C_{0}) = (ν_{1}, S_{1}, C_{1}) succeeds and there is a substitution R_{1} such that

1. S′ = R_{1}S_{1} except on new type variables of tp(e_{1}, A, S_{0}, C_{0}), 2. D ∪ C′ ⊢⊢ R_{1}C_{1}, and

3. R_{1}ν_{1} = τ_{1}.

Hence S′A = (R_{1}S_{1})A and (R_{1}S_{1})A.x : σ′, C′ ⊢′ e_{2} : τ_{2}. Now, in order to apply the induction hypothesis to the second recursive call, we need to show that

C′ ⊢⊢ R_{1}C_{2} and σ′ ⪯_{C′} R_{1}σ

where (σ, C_{2}) = tpgen(ν_{1}, S_{1}A, C_{1}, C_{0}).

Since (D ∪ C′) \ C′ = {α_{i} ::Γ_{i}}, we can prove C′ ⊢⊢ R_{1}C_{2} by showing that none of the α_{i} occurs in R_{1}C_{2}; this in turn can be proved by analyzing fv(R_{1}α) for α ∈ dom(C_{2}). There are two possibie cases according to tpgen’s definition:

• α ∈ (C_{1})^{∗}(fv S_{1}A) : As D ∪ C′ ⊢⊢ R_{1}C_{1}, we have fv(R_{1}α) ⊆ (D ∪ C′)^{∗}(fv R_{1}S_{1}A) by Lemma 4.3. But, since R_{1}S_{1}A = S′A and (D ∪ C′)^{∗}(fv S′A) = D^{∗}(fv S′A), so we have fv(R_{1}α) ⊆ D^{∗}(fv S′A) and hence none of the α_{i} occurs in fv(R_{1}α) in this case.

• α ∈ (dom(C_{1})∩dom(C_{0}))\(C_{1})^{∗}(fv S_{1}A) : Since α is not a new type variable of tp(e_{1}, A, S_{0}, C_{0}), R_{1}S_{1}α = S′α. Moreover, as α ∈ dom(C_{1}), from (1) of Lemma 6.2, we have α ∉ dom(S_{1}). But, S′ = R_{0}S_{0}, so fv(R_{1}α) = fv(R_{1}S_{1}α) = fv(R_{0}α). Finally, from C′ covers R_{0}C_{0} and C′ ⊢⊢ R_{0}C_{0}, it follows that fv(R_{1}α) ⊆ dom(C′) and hence none of the α_{i} occurs in fv(R_{1}α) in this case, either.

To show that σ′ ⪯_{C′} R_{1}σ, we first define (σ̃, C̃ ) = gen(τ_{1}, S′A, D ∪ C′). Then, clearly σ′ ⪯_{C′} σ̃ and C̃ ⪯ C′. Next, let (σ̄, C̄ ) = gen(ν_{1}, S_{1}A, C_{1}). We observe that R_{1} is the substitution that relates these two generalization. So, from Lemma 4.4, we have σ̃ ⪯C̃ R_{1}σ̄ and hence σ̃ ⪯_{C′} R_{1}σ̄. Finally, note that σ̄ ⪯_{C_{2}} σ according to their definitions. So, from C′ ⊢⊢ R_{1}C_{2}, we have R_{1}σ̄ ⪯_{C′} R_{1}σ by Lemma 3.5, and hence σ′ ⪯_{C′} R_{1}σ by the transitivity of ⪯_{C′}.

Now we can proceed to the second recursive call to tp. By hypothesis, S′A.x :σ′, C′ ⊢′ e_{2} : τ_{2}, but

S′A.x :σ′ = R_{1}S_{1}A.x :σ′ ⪯_{C′} R_{1}S_{1}A.x :R_{1}σ = R_{1}S_{1}(A.x :σ),

so R_{1}S_{1}(A.x : σ), C′ ⊢′ e_{2} : τ_{2} by Lemma 4.8. Hence by induction, tp(e_{2}, A.x : σ, S_{1}, C_{2}) = (ν_{2}, S_{2}, C_{3}) succeeds and there is a substitution R_{2} such that

1. R_{1}S_{1} = R_{2}S_{2} except on new type variables of tp(e_{2}, A, S_{1}, C_{2}),

2. C′ ⊢⊢ R_{2}C_{3}, and

3. τ_{2} = R_{2}ν_{2}.

Therefore, tp(let x = e_{1}in e_{2}, A, S_{0}, C_{0}) succeeds with (ν_{2}, S_{2}, C_{3}) and R_{2} is the required substitution since S′ = R_{2}S_{2} except on new type variables of tp(let x = e_{1}in e_{2}, A, S_{0}, C_{0}).

This completes the proof.

Together with Theorem 4.10, we have the completeness result.

Corollary 6.6 (Completeness of tp) Suppose that S′A, C′ ⊢ e : σ′ and (S′, C′) ⪯ (S_{0}, C_{0}). Then tp(e, A, S_{0}, C_{0}) succeeds with (τ, S, C ), and there is a substitution R such that

1. S′ = RS except on the new type variables of tp(e, A, S_{0}, C_{0}), and

2. σ′ ⪯_{C′} Rσ

where (σ, C̃ ) = gen(τ, SA, C ).

Proof: By Theorem 4.10, S′A, C_{1} ⊢′ e : ν for some context C_{1} that C′ ⪯ C_{1} and some type ν such that σ′ ⪯_{C′} σ_{1} where (σ_{1}, C′_{1}) = gen(ν, S′A, C_{1}). Now, since (S′, C′) ⪯ (S_{0}, C_{0}), we have (S′, C_{1}) ⪯ (S_{0}, C_{0}). Therefore, by Theorem 6.5, if tp(e, A, S_{0}, C_{0}) = (τ, S, C ), then there is a substitution R such that

1. S′ = RS except on new type variables of tp(e, A, S_{0}, C_{0}),

2. C_{1} ⊢⊢ RC , and

3. ν = Rτ.

Clearly, S′A = SA. Now let (σ, C̃ ) = gen(τ, SA, C ). Then, applying Lemma 4.4 on R, we get σ_{1} ⪯_{C′_{1}} Rσ. But C′_{1} ⪯ C′, so σ′ ⪯_{C′} Rσ by Lemma 3.4.

As a corollary, we have the following result for principal type schemes.

Corollary 6.7 Suppose that dom(C_{0}) = (C_{0})^{∗}(fv S_{0}A) and tp(e, A, S_{0}, C_{0}) = (τ, S, C ). Then σ is a principal type scheme for e under SA and C′ where (σ, C′) = gen(τ, SA, C )

Proof: If tp(e, A, S_{0}, C_{0}) = (τ, S, C ) then SA, C ⊢ e : τ by Theorem 6.3 and Theorem 4.9. Now, since (σ, C′) = gen(τ, SA, C ), we have SA, C′ ⊢ e : σ by Lemma 4.2. Moreover, from Lemma 6.2, we have (S, C ) ⪯ (S_{0}, C_{0}). In other words, S = R_{0}S_{0} and C ⊢⊢ R_{0}C_{0} for some substitution R_{0}. So, in order to apply Corollary 6.6, we need to show that (S, C′) ⪯ (S_{0}, C_{0}). From Lemma 4.1, we have dom(C′) = C^{∗}(fv SA). So, by Lemma 4.3, we have fv(R_{0}α) ⊆ dom(C′) for all α ∈ dom(C_{0}), and hence C′ ⊢⊢ R_{0}C_{0}. Therefore, (S, C′) ⪯ (S_{0}, C_{0}).

Now, suppose that SA, C′ ⊢ e : σ′ for some type scheme σ′. By Corollary 6.6, there is a substitution R such that

1. S = RS except on new type variables of tp(e, A, S_{0}, C_{0}) and

2. σ′ ⪯_{C′} Rσ.

Furthermore, from Lemma 4.3, we know that ⋃{fv(Sα) | α ∈ (C_{0})^{∗}(fv S_{0}A)} = C^{∗}(fv SA). Hence type variables in C^{∗}(fv SA) are unchanged by R because of (1). Now, since fv(σ) ⊆ C^{∗}(fv SA), we have Rσ = σ. It then follows that σ is a principal type scheme for e under SA and C′.

7 Ambiguity Revisited

As we have seen in the introduction, parametric type classes share with standard type classes the problem that type schemes might be ambiguous.

Definition. Given a type scheme σ = ∀α_{i} :: Γ_{i}.τ, let C_{σ} = {α_{i} :: Γ_{i}} be the generic context of σ and τ_{σ} = τ be the type proper of σ. Conversely, if C = {α_{i} :: Γ_{i}} and C covers τ then we shall write < C , τ > for the type scheme ∀α_{i} ::Γ_{i}.τ formed from C and τ.

Definition. A generic type variable α in a type scheme σ = ∀α_{i} :: Γ_{i}.τ is (weakly) ambiguous if (1) C_{σ} α ≠ ∅, and (2) α ∉ C_{σ}^{∗}(fv τ).

Ambiguous type variables pose an implementation problem. The usual approach to implement overloading polymorphism is to pass extra dictionary arguments for every type class in the context of a function signature. Since the constraints on ambiguous variables are non-empty (1), dictionaries need to be passed. But since the ambiguous variable does not occur free in the type (2), it is never instantiated, hence we do not know which dictionaries to pass. Seen from another perspective, any dictionary of an appropriate instance type would do, but we have a problem of coherence: There are several implementations of an expression with possibly different semantics [Jon92a].

The problem is avoided by requiring that the programmer disambiguate expressions if needed, by using explicit type signatures. Conceptually, the ambiguity check takes place after type reconstruction; would it be part of type reconstruction then the principal type property would be lost. In a way, the ambiguity problem shows that sometimes reconstructed types are too general. Every ambiguous type has a substitution instance which is unambiguous (just instantiate ambiguous variables). The trouble is that there is not always a most general, unambiguous type.

Compared to multi-argument type classes, our type system often produces types with less ambiguity. Consider:

               len :: (sa :: Sequence a) => sa -> Int

Seen as a multi-argument type class, a would be ambiguous, since it occurs in a predicate but not in the type itself. Seen as a parametric type class, however, a is not ambiguous: Although it does not occur in the type, it both unconstrained and dependent on sa through (sa :: Sequence a). Hence both (1) and (2) fail.

Ambiguity problems can be further reduced by making use of the following observation: Because of restriction (b) in Section 3, the top-level type constructor of a type uniquely determines the dictionary that needs to be passed. Hence, if two types have the same top-level type constructor (but possibly different type arguments), their dictionaries share the same data constructor (but have possibly different parameters). We can recognize equality of top-level type constructors statically, using the following technique:

We introduce a special “root” class TC , with one type parameter but no operations. Every type is an instance of TC by virtue of the following instance declaration (which can be thought of being implicitly generated for every type κ τ).

inst κ τ::TC (κ ())

Effectively, TC is used to “isolate” the top-level type constructor of a type. That is, if two types are related by a TC constraint, we know that they have the same top-level type constructor. The two types are then called similar:

Definition. Given a context C , let similarity in C , (∼_{C} ), be the smallest transitive and symmetric relation such that C ⊢⊢ τ_{1} ::TC τ_{2} implies τ_{1} ∼_{C} τ_{2}.

TC is treated like every other type class during type reconstruction. It is treated specially in the ambiguity check, allowing us to strengthen the ambiguity criterion:

Definition. A generic type variable α in a type scheme σ is strongly ambiguous if α is weakly ambiguous in σ, and, for every type τ, α ∼_{C_{σ}} τ implies that τ is a strongly ambiguous type variable in σ.

The TC technique enables us to type map precisely^{3}

map : ∀a.∀b.∀t.∀sa ::{Sequence a, TC t}.∀sb ::{Sequence b, TC t}.(a → b) → sa → sb

This states that sa and sb are instance types of Sequence with element types a and b, and that sa and sb share the same type constructor.

The knowledge that sa and sb have the same type constructor is initially on the meta-level, derived from the form of the compiler-generated instance declarations. We can formalize it in the type system as follows:

Definition. A type scheme σ = ∀α_{i} :: Γ_{i}.τ′ is in reduced form if none of the Γ_{i} contains a class TC (κ τ), for arbitrary constructor κ and type τ. We use σ_{R} for type schemes in reduced form.

Definition. Two type schemes σ_{1}, σ_{2} are equivalent under a context C , σ_{1} ≃_{C} σ_{2}, iff for all reduced type schemes σ_{R},

σ_{R} ⪯_{C} σ_{1} ⇔ σ_{R} ⪯_{C} σ_{2}.

We extend the definition of generic instance to include equivalence: A type scheme σ_{1} is a generic instance of a type scheme σ_{2} under a context C if there is a type scheme σ′ s.t. σ_{1} ≃_{C} σ′, and σ′ ⪯_{C} σ_{2} according to the definition of ⪯_{C} in Section 3. This stronger notion of generic instance is important to check user-defined type signatures.

Example: After substituting List a for sa, the type signature of map would become:

∀sb ::{Sequence b, TC (List ())}.(a → b) → List a → sb

The usual definition of map for lists, on the other hand, would have type:

(a → b) → List a → List b

Equivalence is necessesary to verify that the first type is an instance of the second.

Without loss of generality, we shall assume that all type schemes are closed and thus drop the subscript in ≃_{C} in the following discussion.

In order to handle the extended notion of generic instance, we introduce the function r to rewrite a type scheme into a more ’reduced’, but equivalent one. r (σ) = let (S, C ) = reduce(C_{σ}) in < C , S(τ_{σ}) > where reduce (C ) =

3Previously, it has been conjectured that this required second-order unification.

if ∃(α::{TC (κ ())} ∪ Γ) ∈ C then let β a fresh type variable in mgu α (κ β) (id, C\_{α}.α::Γ.β::{})

else (id, C )

As might be expected, the convention on class TC enables us to reduce σ by properly instantiating σ and normalizing its generic context. Furthermore, the set of reduced generic instances of σ is preserved by r, as formalized in the following lemma:

Lemma 7.1 σ ≃ r(σ).

Proof: Let σ′ = r(σ). We prove that for all reduced type schemes σ_{R}, if σ_{R} ⪯ σ then σ_{R} ⪯ σ′. The converse part follows immediately from the definition of ⪯.

By the definition of ⪯, C_{σ_{R}} ⊢⊢ S_{0}C_{σ} and τ_{σ_{R}} = S_{0}τ_{σ} for some substitution S_{0}. In particular, for (α:: {TC (κ ())} ∪ Γ) ∈ C_{σ}, we have C_{σ_{R}} ⊢⊢ S_{0}(α:: {TC (κ ())} ∪ Γ). So, S_{0} = S′ ∘ [α ↦ κ ν] for some type ν and substitution S′ according to our convention on class TC .

Next, let β be a new type variable and S = S′[β ↦ ν][α ↦ κ β]. Then S = S_{0} except on β. Moreover, we have Sα = S(κ β) and (S, C_{σ_{R}}) ⪯ (id, C_{σ}\_{α}.α::Γ.β::{}). So, if mgu α (κ β) (id, C_{σ}\_{α}.α:: Γ.β :: {}) = (S̄, C̄ ), then, by Lemma 5.5, S = S′′ ∘ S̄ and C_{σ_{R}} ⊢⊢ S′′C̄ for some substitution S′′. But C_{σ′} = C̄ and τ_{σ′} = S̄τ_{σ}. So, τ_{σ_{R}} = Sτ_{σ} = S′′τ_{σ′} and hence σ_{R} ⪯ σ′.

Moreover, the two notions of equivalent coincide for reduced type schemes:

Lemma 7.2 For any two reduced type schemes σ_{R} and σ′_{R}, σ_{R} = σ′_{R} iff σ_{R} ≃ σ′_{R}.

Proof: Follows immediately from their definitions.

Now, let r^{∗}(σ) be the reduced type scheme obtained by repeatedly applying r to σ. With the above two lemmas, we can easily prove the following theorem:

Theorem 7.3 For any two type schemes σ_{1} and σ_{2}, σ_{1} ≃ σ_{2} iff r^{∗}(σ_{1}) = r^{∗}(σ_{2}).

Proof: We prove the “if” part; the proof for the converse part is similar and thus omitted.

By Lemma 7.1, r^{∗}(σ_{1}) ≃ σ_{1} and σ_{2} ≃ r^{∗}(σ_{2}). So, r^{∗}(σ_{1}) ≃ r^{∗}(σ_{2}) and hence r^{∗}(σ_{1}) = r^{∗}(σ_{2}) by Lemma 7.2.

Consequently, by repeatedly applying r to rewrite type schemes to their reduced forms, we get a decision procedure for the extended generic instance relation.

8 Related Work

Wadler and Blott [WB89] introduced type classes and presented an extension of the Hindley-Milner type system that incorporates them. They proposed a new form of type, called a predicated type, to specify the types of overloaded functions. A quite similar notion was used under the name of category in the Scratchpad II system for symbolic computation [JT81]. Also related are Kaes’ work on parametric overloading [Kae88], F-bounded polymorphism in object-oriented programming [CCH^{+}89], and [Rou90]. The type class idea was quickly taken up in the design of Haskell. Its theoretical foundation, however, took some time to develop. The initial approach of [WB89] encoded Haskell’s source-level syntax in a type system that was more powerful than Haskell itself, since it could accommodate classes over multiple types. This increased expressiveness can, however, lead to undecidability, as has been investigated by Volpano and Smith [VS91]. Indeed, the system published in [WB89] is apparently undecidable.

The source-level syntax of Haskell, on the other hand, has a sufficient number of static constraints to guarantee decidability. This was shown in [NS91], where Nipkow and Snelting modeled type classes in a three-level system of values, types, and partially ordered sorts. In their system, classes correspond to sorts and types are sorted according the class hierarchy. Order-sorted unification [MGS89] is used to resolve overloading in type reconstruction. The use of an order-sorted approach is mathematically elegant, yet we argue that the ordering relation between classes is a syntactic mechanism and thus not necessary for developing a type system for type classes. Furthermore, it is not obvious how to extend their system to incorporate our proposed extensions.

Work was also done to extend the type class concept to predicates over multiple types. Volpano and Smith [VS91] looked into modifications of the original system in [WB89] to ensure decidability of type reconstruction and to get a sharper notion of well-typed expressions. Jones [Jon91, Jon92b] gave a general framework for qualified types. His use of predicate sets is at first sight quite similar to our context-constrained instance theory. The main difference between the two approaches lies in our use of normal forms (Jones does not address this issue) and our distinction between constrained and dependent variables. This distinction allows us to solve the ambiguity problems previously encountered in definitions of container classes. Recently, based on the notion of constrained types, Kaes [Kae92] presented a generic inference system of which overloading and subtyping are special instances.

9 Conclusion

We have proposed a generalization of Haskell’s type classes to support container classes with overloaded data constructors and selectors. The underlying type system is an extension of the Hindley-Milner type system with parametric type classes. This extension preserves two important properties of the original system, namely decidable typability and principal types. Its type scheme uses bounded quantification whose introduction and elimination depend on a separate contextconstrained instance theory. The decoupling of the instance theory from the type inference system makes our system more modular than previous work. We believe that the gained modularity can also be a great aid to implementors.

Compared to other approaches, our type system follows closest in spirit to the design of Haskell’s type classes. Indeed, the use of normalized context has its root in the source-level syntax of Haskell. The instant normalization of context constraints matches well with the C −T rule stated in the Haskell report, which requires that a C −T instance declaration for class C and type T appear either in the module in which C is declared or in the module in which T is declared. From a pragmatic viewpoint, the C −T rule is a reasonable requirement for systems supporting separate compilation to handle globally overloaded operators. But for type systems with general predicate sets like qualified types or constrained types, it seems difficult to find such a proper rule for them without being overly restrictive.

On the other hand, we associate context constraints with individual quantified type variables in forming a type scheme. By doing so, we have restricted the expressiveness of our system. For instance, we exclude cylic contexts from our discussion. Therefore, in the future, we plan to investigate the feasibility of having a context set in our type scheme.

Acknowledgement

We wish to thank Mark Jones, Stefan Kaes, Tobias Nipkow, and Satish Thatte for their critical comments and helpful discussions.

References

[CCH^{+}89] P. Canning, W. Cook, W. Hill, W. Olthoff, and J. Mitchell. F-bounded polymorphism for object-oriented programming. In Proc. ACM Conf. Functional Programming Languages and Computer Architecture, pages 273–280, 1989.

[CHO92] Kung Chen, Paul Hudak, and Martin Odersky. Parametric type classes. In Proc. ACM Conf. on Lisp and Functional Programming. ACM, June 1992.

[DM82] L. Damas and R. Milner. Principal type schemes for functional programs. In Proc. 9th ACM Symp. on Principles of Programming Languages, pages 207–212, Jan. 1982.

[HJW91] Paul Hudak, Simon Peyton Jones, and Philip L. Wadler. Report on the programming language Haskell: a non-strict, purely functional language, version 1.1. Technical Report YALEU/DCS/RR-777, Dept. of Computer Science, Yale University, New Haven, Conn., August 1991.

[Jon91] Mark P. Jones. Type inference for qualified types. Technical Report PRG-TR-10-91, Oxford University Computing Laboratory, Oxford, UK, 1991.

[Jon92a] Mark P. Jones. Coherence for qualified types. Private communication, March 1992.

[Jon92b] Mark P. Jones. A theory of qualified types. In B. Krieg-Brückner, editor, Proc. European Sysposium on Programming, pages 287–306. Springer Verlag, Feburary 1992. LNCS 582.

[JT81] R.D. Jenks and B.M. Trager. A language for computational algebra. In Proc. ACM Symposium on Symbolic and Algebraic Manipulation, pages 22–29, 1981.

[Kae88] S. Kaes. Parametric overloading in polymorphic programming languages. In H. Ganzinger, editor, Proc. 2nd European Symosium on Programming, Lecture Notes in Computer Science, Vol. 300, pages 131–144, Nancy, France, March 1988. Springer-Verlag.

[Kae92] Stefan Kaes. Type inference in the presence of overloading, subtyping abd recursive types. In Proc. ACM Conf. on Lisp and Functional Programming. ACM, June 1992.

[Lil91] Mark D. Lilibridge. A generalization of type classes. distributed to Haskell mailing list, June 1991.

[MGS89] J. Meseguer, J. Goguen, and G. Smolka. Order-sorted unification. J. Symbolic Computation, 8:383–413, 1989.

[NS91] T. Nipkow and G. Snelting. Type classes and overloading resolution via order-sorted unification. In J. Hughes, editor, Proc. Conf. on Functional Programming and Computer Architecture, pages 15–28. Springer-Verlag, 1991. LNCS 523.

[Rob65] J. Robinson. A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach., 12(1):23–41, 1965.

[Rou90] Francois Rouaix. Safe run-time overloading. In Seventeenth Annual ACM Symp. on Principles of Programming Languages, pages 355–366, San Franscico, CA, January 1990.

[VS91] Dennis M. Volpano and Geoffery S. Smith. On the complexity of ML typability and overloading. In J. Hughes, editor, Proceedings of Functional Programming and Computer Architecture, pages 15–28. Springer-Verlag, 1991. LNCS 523.

[WB89] Phil Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In Sixteenth Annual ACM Symp. on Principles of Programming Languages, pages 60–76. ACM, 1989.