J. Functional Programming 1 (1): 1–000, January 1993 \begin{matrix}c \\ ◯ \end{matrix} 1993 Cambridge University Press 1

Type Reconstruction for Type Classes^{1}

Tobias Nipkow^{2} and Christian Prehofer^{3}

TU München^{4}

Abstract

We study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner’s work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This leads to simple type inference systems and algorithms which closely resemble those for ML. In particular we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.

1 Introduction

The extension of Hindley/Damas/Milner polymorphism with the notion of type classes in the functional programming language Haskell (HJW92) has attracted much attention. Type classes permit the systematic overloading of function names while retaining the advantages of the Hindley/Damas/Milner system: every typable expression has a most general type which can be inferred automatically. Although many extensions to Haskell’s type system have already been proposed (and also implemented), we believe that the essence of Haskell’s type inference algorithm has still not been presented in all its simplicity. The main purpose of this paper is to give a particularly simple algorithm, a contribution for implementors. At the same time we present a correspondingly simple type inference system, a contribution aimed at users of the language. Finally we give rigorous proofs of the soundness and completeness of the algorithm with respect to the inference system. Although both the algorithm and the inference system resemble their ML-counterparts very closely, the proofs are considerably more involved.

A type class in Haskell is essentially a set of types (which all happen to provide a certain set of functions). The classical example is equality. In the pre-standard versions of ML, the equality function = has the polymorphic type ∀α.α → α → bool,

1 This is an extended version of (NP93) 2 Research supported by ESPRIT BRA 6453, TYPES. 3 Research supported by the Deutsche Forschungsgemeinschaft (DFG) under grant Br

887/4, Deduktive Programmentwicklung. 4 Address: Institut für Informatik, Technische Universität München, 80290 München,

  Germany. Email: {nipkow,prehofer}@informatik.tu-muenchen.de

where the type variable α ranges over all types. However, = should not be applied to arguments of function type. To fix this problem, Standard ML (MTH90) introduces special type variables that range only over types where equality is defined. Equality differs from other polymorphic functions not just because of its restricted domain but also because of its mixture of polymorphism and overloading: equality on lists is implemented differently from equality on integers.

Type classes treat both issues in a systematic way: the type variable α is restricted to elements of a certain type class, say Eq, the class of all “equality types”. Then for each type τ where = should be defined, we have to declare that τ is of class Eq by providing an implementation of = of type τ → τ → bool.

To express the fact that a type τ is in some class C we introduce the judgement τ : C.^{1} The idea of viewing Haskell as a three level system of expressions, types and classes, where classes classify types, goes back to Nipkow and Snelting (NS91). However, in their system it is impossible to express that a type belongs to more than one class. To overcome this difficulty we introduce sorts as finite sets of classes. The judgement τ : {C_{1}, …, C_{n}} is a compact form of the conjunction τ : C_{1} ∧ … ∧ τ : C_{n}. Alternatively we may think of {C_{1}, …, C_{n}} as a notation for C_{1} ∩ … ∩ C_{n}, the intersection of the types belonging to the classes C_{1} to C_{n}. This leads to a simple type inference system and algorithm. The former resembles that for Mini-ML (CDDK86), the latter is very similar to algorithm I by Milner (Mil78). The main difference is that in both cases we also compute a set of constraints of the form α : {C_{1}, …, C_{n}} where α is a type variable.

2 Mini-Haskell

Since the aim of this paper is simplicity, we treat only the most essential features of Haskell relating to type classes. The resulting language is basically Mini-ML (CDDK86) plus class and instance declarations, Mini-Haskell for short. Its syntax is shown in Figure 1. Although the next paragraph provides a brief account of type classes, the reader should consult the Haskell Report (HJW92) or the original paper on type classes (WB89) for motivations and examples. Note that we do not follow the concrete names of classes etc. of Haskell in our examples.

Mini-Haskell extends ML by a restricted form of overloading. Ignoring subclasses for a moment, each class declaration introduces a new class C and a new overloaded function name x. Semantically, C represents the set of all types which support a function x. For instance

class α : Eq where eq : α → α → bool

introduces the class Eq of all those types τ which provide a function eq : τ → τ → bool. A class declaration is like a module interface: it separates declarations from implementations. In order to “prove” that a particular type, say int, is in Eq, a “witness” for the required function eq needs to be provided. This is the purpose of

1 If classes are viewed as predicates on types, this leads to the Haskell notation C(τ).

Type classes  C
Sorts  S = {C_{1}, …, C_{n}}
Type variables  α
Type constructors t
Types  τ = α | t(τ_{1}, …, τ_{n})
Type schemes  σ = τ | ∀α:S.σ
Identifiers  x
Expressions  e = x
| (e_{0} e_{1})
| λx.e
| let x = e_{0} in e_{1}
Declarations  d = class α : C ≤ S where x : σ
| inst t : (S_{1}, …, S_{n})C where x = e
Programs  p = d; p | e

Fig. 1. Syntax of Mini-Haskell types and expressions

instance declarations. In order to prove int : Eq we instantiate eq by eq int, some existing function of type int → int → bool:

inst int : Eq where eq = eq int

In general we can instantiate classes not just by ground types but also by type constructors. For example we may wish to express that a type list(τ) admits equality provided τ does:

inst list : (Eq)Eq where eq = …

The declaration list : (Eq)Eq expresses that list maps types of class Eq to types of class Eq. The implementation of eq on lists is intentionally left blank: due to the absence of pattern matching and recursion in our language, the required code would be a nest of conditionals wrapped up in a fixpoint combinator.

Classes can be arranged in hierarchies. The general class declaration

class α : C ≤ S where x : σ

introduces the new class C as a subclass of all classes in S, which must have been defined already. Type α is in C only if it is in the intersection of all the classes in S and provides a function x of type σ. For example the class Ord of ordered types can be defined as a subclass of Eq which provides an additional function le:

class α : Ord ≤ Eq where le : α → α → bool

Subclasses are mere syntactic sugar (CHO92). In the above example Ord could be defined without reference to Eq as a completely separate class. The only difference is that without subclasses the judgement τ : Ord has to be expanded to become τ : Eq ∧ τ : Ord, i.e. τ : {Eq, Ord}. However, it is almost easier to deal with subclasses directly than to eliminate them, as done in (NP93). To demonstrate this, and because subclasses are part of Haskell, we have included them in Mini-Haskell.

2.1 Sorts and Types

As motivated in the introduction, sorts are finite sets of classes. This representation is a key ingredient for the concise treatment of type inference. Yet semantically the sort {C_{1}, …, C_{n}} should be understood as C_{1} ∩ … ∩ C_{n}. Thus {C} and C are equivalent, and the empty set {} is the sort/set of all types. If S_{1} is more specialized, i.e. represents fewer types than S_{2}, we write S_{1} ⪯ S_{2}. Given a partial order ≤ on classes, the induced quasi-order ⪯ on sorts is defined by

S_{1} ⪯ S_{2} ⇔ ∀C_{2} ∈ S_{2}.∃C_{1} ∈ S_{1}. C_{1} ≤ C_{2}

It follows directly that S_{1} ⊇ S_{2} implies S_{1} ⪯ S_{2}. In the context of a non-trivial ordering ≤ on classes, the reverse implication does not hold: for example {Ord} ⪯ {Eq} although {Ord} ⊉ {Eq}. It is easy to see that any two sorts S_{1} and S_{2} possess an infimum whose representation is their union S_{1} ∪ S_{2}.

Because ⪯ is in general only a quasi-order (i.e. it is not antisymmetric), it gives rise to an equivalence

S_{1} ≈ S_{2} ⇔ S_{1} ⪯ S_{2} ∧ S_{2} ⪯ S_{1}.

Sorts which are equivalent modulo ≈, for example {Ord} and {Ord, Eq}, represent the same set of types. Although it would be mathematically more elegant to work with equivalence classes [S]_{≈}, we prefer to stay closer to an implementation and work with sorts directly. Nevertheless it should be kept in mind that an implementation is free to choose an arbitrary representative from an equivalence class [S]_{≈}, for example the one with fewest elements.

Types in Mini-Haskell are simply terms over variables and constructors of fixed arity. Note that → is just another type constructor, i.e. τ_{1} → τ_{2} is short for →(τ_{1}, τ_{2}). The set of free variables in a type scheme is denoted by FV(σ). Bound variables in type schemes range only over certain subsets of types: ∀α:S.σ abbreviates all instances {α ↦ τ}σ where τ : S, a judgment defined formally below.

In the sequel a list of syntactic objects s_{1}, …, s_{n} is abbreviated by \overline{s_{n}}. For instance, ∀\overline{α_{n}:S_{n}}.σ is equivalent with ∀α_{1}:S_{1}, …, α_{n}:S_{n}.σ. Orderings extend to lists in the componentwise manner: \overline{S_{n}} ⪯ \overline{T_{n}} ⇔ ∀i. S_{i} ⪯ T_{i}.

2.2 Declarations and Programs

As shown in Figure 1, expressions are λ-terms extended with let-definitions. A program is a sequence of declarations followed by an expression.

A Mini-Haskell class declaration class α : C ≤ {C_{1}, …, C_{m}} where x : σ corresponds to the Haskell declaration class (C_{1}α, …, C_{m}α) ⇒ Cα where x :: τ, where τ is the body of σ. Note that σ must contain no free variables except α. The translation in the opposite direction is more involved because a Haskell class can declare any number of functions. This feature is clearly not essential and could, for instance, be modeled by representing a set of functions by a single tuple of functions. Strictly speaking, we could have dropped class names altogether since there is a one to one correspondence between class names and the single function declared in that class. This would have lead us to the language of Stefan Kaes (Kae88) but would have obscured the connection with Haskell.

A Mini-Haskell instance declaration inst t : (S_{1}, …, S_{n})C where x = e expresses that t(τ_{1}, … τ_{n}) is in class C provided the τ_{i} are of sort S_{i}. It corresponds to the Haskell declaration inst (con) ⇒ C(t α_{1} … α_{n}) where x = e where con is a list consisting of assumptions C′ α_{i} with C′ ∈ S_{i} for all i = 1 … n.

2.3 Classifying Types

Before we embark on type inference, the simpler problem of sort inference has to be settled. In ML and many other languages we have the judgement e : τ, expressing that e is of type τ. Similarly, we classify types by sorts with the judgement τ : S, stating that type τ is in sort S. This judgement depends on

• the sorts of the type variables in τ. This is recorded in a sort context Γ, which is a total mapping from type variables to sorts such that Dom(Γ) = {α | Γα ≠ {}} is finite. Sort contexts can be written as [α_{1}:S_{1}, …, α_{n}:S_{n}].

• the “functionality” of the type constructors. The behaviour of type constructors is specified by declarations of the form t : (\overline{S_{n}})C which are lifted directly from instance declarations. In the sequel Δ always denotes a set of such declarations.

• the subclass ordering ≤.

The pair Δ, ≤ is called a (type) signature and is denoted by Σ, i.e. Δ, ≤ and Σ are used interchangeably.

Given Γ and Σ we can infer the sort of a type τ using the judgement Σ, Γ ⊢ τ : S. The rules are shown in Figure 2. Remember that the sort {C} and the class C are equivalent.

The ordering ⪯ extends easily from sorts to contexts:

Γ ⪯ Γ′ ⇔ ∀α. Γα ⪯ Γ′α

We say that Γ′ is more general than Γ. It is easy to show that ⊢ is monotonic w.r.t. this ordering: Σ, Γ′ ⊢ τ : S implies Σ, Γ ⊢ τ : S. In the sequel this fact is often used implicitly.

Because every two sorts possess an infimum, every type τ has a most specific sort S, i.e. Σ, Γ ⊢ τ : S and if Σ, Γ ⊢ τ : S′ then S ⪯ S′. The computation of this most specific sort is straightforward and shall not concern us here because it is not relevant for our purposes.

Having seen sort inference for Mini-Haskell types we are prepared for our main goal, type inference and type reconstruction for Mini-Haskell programs.

3 Type Inference Systems

In this section we present two type inference systems for Mini-Haskell. We start with a set of inference rules which define the types of Mini-Haskell programs and

\frac{[i = 1 … n] ; ⋮ ; Σ, Γ ⊢ τ : C_{i}}{Σ, Γ ⊢ τ : \{C_{1}, …, C_{n}\}}

\frac{Σ, Γ ⊢ τ : \{C_{1}, …, C_{n}\}}{Σ, Γ ⊢ τ : C_{i}}  i = 1 … n

\frac{Γ(α) = S}{Σ, Γ ⊢ α : S}

\frac{[i = 1 … n] ; ⋮ ; t : (\overline{S_{n}})C ∈ Δ Σ, Γ ⊢ τ_{i} : S_{i}}{Σ, Γ ⊢ t(\overline{τ_{n}}) : C}

\frac{Σ, Γ ⊢ τ : C_{1} C_{1} ≤ C_{2}}{Σ, Γ ⊢ τ : C_{2}}

Fig. 2. The judgement Σ, Γ ⊢ τ : S

CLASS (Δ, (≤ ∪ {(C, D) | D ∈ S})^{∗}, Γ, E[x:∀α:C.σ] ⊢ p : σ′) / (Δ, ≤, Γ, E ⊢ (class α : C ≤ S where x : σ; p) : σ′)

INST  \frac{\begin{matrix}Δ ∪ \{t : (\overline{S_{n}})C\}, ≤, Γ, E ⊢ p : σ′ \\ E(x) = ∀α:C.σ Γ[\overline{α_{n}:S_{n}}], Δ, ≤, E ⊢ e : \{α ↦ t(\overline{α_{n}})\}σ \end{matrix}}{Δ, ≤, Γ, E ⊢ (inst t : (\overline{S_{n}})C where x = e; p) : σ′}

Fig. 3. The judgement Δ, ≤, Γ, E ⊢ p : σ

expressions. Then we proceed to a more restricted, syntax-directed set of rules, which will be the basis for the type inference algorithm.

As usual in type inference for ML-like languages, an environment is a finite mapping E = [x_{1}:σ_{1}, …, x_{n}:σ_{n}] from identifiers to types. The domain of E is Dom(E) = {x_{1}, …, x_{n}}. E[x:σ] is a new map which maps x to σ and all other x_{i} to σ_{i}. The free type variables in E are FV(E) = FV(E(x_{1})) ∪ … ∪ FV(E(x_{n})). If V is a set of type variables the restriction of Γ to variables not in V is Γ\V = [α:Γα | α ∈ Dom(Γ) − V].

A substitution is a finite mapping from type variables to types, written as {α_{1} ↦ τ_{1}, …}. Substitutions are denoted by θ and δ; {} is the empty substitution. Define Dom(θ) = {α | θα ≠ α}, Cod(θ) = ⋃_{α∈Dom(θ)} FV(θ(α)) and FV(θ) = Dom(θ) ∪ Cod(θ).

There are two judgements which are defined in Figures 3 and 4: Δ, ≤, Γ, E ⊢ p : σ and Δ, ≤, Γ, E ⊢ e : σ express that program p and expression e are of type σ in the context of Δ, ≤, Γ and E.

The rules for Δ, ≤, Γ, E ⊢ p : σ, when applied backwards, simply traverse the declarations, building up Δ, ≤ and E. Class declarations extend E and ≤, instance declarations extend Δ. Notice that it is necessary to take the transitive closure (≤ ∪ {(C, D) | D ∈ S})^{∗} of ≤ and the new subclass relations in rule CLASS.

Rule INST also type-checks the instantiation of x by e, making sure that e is of type \{α ↦ t(\overline{α_{n}})\}σ, where σ is the generic type of x and \{α ↦ t(\overline{α_{n}})\} is a type substitution with new type variables \overline{α_{n}}.

Note that there are two context conditions for declaration sequences we have chosen not to formalize:

1. class α : C ≤ S must be preceded by a declaration for each superclass in S, but not by another declaration class α : C;

2. inst t : (\overline{S_{n}})C must be preceded, for each superclass D of C, by a declaration inst t : (\overline{T_{n}})D such that \overline{S_{n}} ⪯ \overline{T_{n}}, but not by another declaration inst t(…)C.

These conditions are the result of translating the restrictions actually adopted in Haskell (HJW92, 4.3.2) to Mini-Haskell. Enforcing them is simple enough and has thus been ignored in this paper. Nevertheless we assume in the sequel that all declarations, and hence Δ and ≤, meet the above conditions.

ASM Σ, Γ, E ⊢ x : E(x)
∀E  \begin{matrix}Σ, Γ, E ⊢ e : ∀α:S.σ & Σ, Γ ⊢ τ : S \\ Σ, Γ, E ⊢ e : \{α ↦ τ\}σ \end{matrix}
∀I  \begin{matrix}Σ, Γ[α:S], E ⊢ e : σ & α ∈ FV(σ) − FV(E) \\ Σ, Γ, E ⊢ e : ∀α:S.σ \end{matrix}
APP \begin{matrix}Σ, Γ, E ⊢ e_{1} : τ_{2} → τ_{1} & Σ, Γ, E ⊢ e_{2} : τ_{2} \\ Σ, Γ, E ⊢ (e_{1} e_{2}) : τ_{1} \end{matrix}
ABS {Σ, Γ, E[x:τ_{1}] ⊢ e : τ_{2} \atop Σ, Γ, E ⊢ λx.e : τ_{1} → τ_{2}}

LET (Σ, Γ, E ⊢ e_{1} : σ_{1} Σ, Γ, E[x:σ_{1}] ⊢ e_{2} : σ_{2}) / (Σ, Γ, E ⊢ let x = e_{1} in e_{2} : σ_{2})

Fig. 4. The judgement Σ, Γ, E ⊢ e : σ

The rules for Σ, Γ, E ⊢ e : σ extend the classical system of Damas and Milner (DM82) by the notion of sorts, which are represented via Σ, Γ, and restricted quantification in type schemes. The assumption α ∈ FV(σ) in ∀I is not really essential (for soundness). Its practical significance is discussed in Section 8. In contrast to the CLASS and INST rules, Σ remains fixed.

3.1 Syntax-directed Type Inference

The next step towards a type reconstruction algorithm is a more restricted set of rules. The application of these rules is determined by the syntax of the expression whose type is to be computed. To distinguish the syntax-directed system we use ⊳ instead of ⊢ and prime the names of its rules, e.g. ASM′.

Definition 3.1 The type scheme σ′ = ∀\overline{α′_{n}:S′_{n}}.τ′ is a generic instance of σ = ∀\overline{α_{m}:S_{m}}.τ under Σ and Γ, written Σ, Γ ⊢ σ ⪰ σ′, iff there exists a substitution θ such that

θτ = τ′,
Dom(θ) ⊆ \{\overline{α_{m}}\},
Σ, Γ[\overline{α′_{n}:S′_{n}}] ⊢ θα_{i} : S_{i} [i = 1 … m],
\{\overline{α′_{n}}\} ∩ FV(σ) = \{\}.

With this relation on types we can now define the most general or principal type of an expression. We say E is closed if FV(E) = {}.

Definition 3.2 The type scheme σ is a principal type of an expression e w.r.t. Σ and a closed environment E, if Σ, [], E ⊢ e : σ and for every σ′ with Σ, [], E ⊢ e : σ′, the type scheme σ′ must be a generic instance of σ, i.e. Σ, [] ⊢ σ ⪰ σ′.

For the syntax-directed system, the rules APP and ABS remain unchanged, the quantifier rules are incorporated into ASM and LET, as shown in Figure 5.

ASM′  {Σ, Γ ⊢ E(x) ⪰ τ \atop Σ, Γ, E ⊳ x : τ}

LET′ (Σ, Γ[\overline{α_{k}:S_{k}}], E ⊳ e_{1} : τ_{1} Σ, Γ, E[x:∀\overline{α_{k}:S_{k}}.τ_{1}] ⊳ e_{2} : τ_{2}) / (Σ, Γ, E ⊳ let x = e_{1} in e_{2} : τ_{2})
where \{\overline{α_{k}}\} = FV(τ_{1}) − FV(E)

Fig. 5. The judgement Σ, Γ, E ⊳ e : σ

There is a straightforward correspondence between the two systems. The syntaxdirected derivations are sound

Theorem 3.3 If Σ, Γ, E ⊳ e : τ then Σ, Γ, E ⊢ e : τ.

and in a certain sense complete w.r.t. the original system:

Theorem 3.4 If Σ, Γ, E ⊢ e : ∀\overline{α_{n}:S_{n}}.τ then Σ, Γ[\overline{α_{n}:S_{n}}], E ⊳ e : τ.

The proof of the last theorem is standard, as for instance in (CDDK86, App. A.1). Theorem 3.4 clarifies in what sense ⊳ works differently from ⊢: by applying the primed rules backwards, the sort constraints for type variables are stored solely in Γ, and not in the type scheme of e. For instance, the LET′ rule explicitly extends Γ. The ⪰ operation, used in the ASM′ rule, may introduce new type variables, whose sorts must be constrained in Γ.

The syntax-directed system already has a very operational flavour. In order to make the transition from a type inference system to an algorithm we need one more ingredient: unification.

4 Unification of Types with Sort Constraints

This section deals with unification in the presence of sort constraints in the form of contexts. This problem can in principle be reduced to order-sorted unification, as done in (NS91) w.r.t. ⪯. However, we have refrained from doing so because it is contrary to our quest for simplicity: involving order-sorted unification makes the algorithm appear more complicated than it actually is. In addition, the standard theory of order-sorted unification would need to be reformulated anyway: it assumes that variables are tagged with their sort, rather than using contexts.

For the remainder of this paper we assume a fixed signature Σ = (Δ, ≤). This is simply a notational device which avoids excessive parameterization.

Since sort information is maintained in contexts, we frequently work with pairs of contexts and substitutions. A substitution θ obeys the sort constraints of Γ in the context of Γ′, written Γ′ ⊢ θ : Γ, iff Σ, Γ′ ⊢ θα : Γα for all α. Because Σ, Γ′ ⊢ θα : Γα is trivially fulfilled if Γα = {} it suffices to require Σ, Γ′ ⊢ θα : Γα for all α ∈ Dom(Γ). For instance, let Eq and list be defined as in the examples in Section 2. Then we have [β:Eq] ⊢ {α ↦ list(β)} : [α:Eq].

We define an ordering on context-substitution pairs:

(Γ, θ) ≥ (Γ′, θ′) ⇔ ∃δ. δθ = θ′ ∧ Γ′ ⊢ δ : Γ

where δθ is defined as the composition: (δθ)(s) = δ(θ(s)).

The set of unifiers of τ_{1} and τ_{2} w.r.t. Γ, written U(Γ, τ_{1}=τ_{2}), consists of the following context-substitution pairs:

U(Γ, τ_{1}=τ_{2}) = {(Γ′, θ) | θτ_{1} = θτ_{2} ∧ Γ′ ⊢ θ : Γ}

A unifier (Γ_{0}, θ_{0}) ∈ U(Γ, τ_{1}=τ_{2}) is most general if (Γ_{0}, θ_{0}) ≥ (Γ_{1}, θ_{1}) for all (Γ_{1}, θ_{1}) ∈ U(Γ, τ_{1}=τ_{2}). We say that unification modulo Σ is unitary if for all Γ and τ_{1}=τ_{2} the set U(Γ, τ_{1}=τ_{2}) is empty or contains a most general unifier.

A signature Σ is called coregular if for all type constructors t and all classes C the set

D(t, C) = \{\overline{S_{n}} | ∃D ≤ C. (t : (\overline{S_{n}})D) ∈ Δ\}

is either empty or contains a greatest element w.r.t. ⪯. If Σ is coregular let Dom(t, C) return the greatest element of D(t, C) or fail if D(t, C) is empty. For instance, Dom(list, Eq) = Eq but Dom(list, Ord) fails.

Sorted unification can be expressed as unsorted unification plus constraint solving. Given a coregular signature Σ, this has the following simple form:

unify(Γ, τ_{1}=τ_{2}) =

let θ = mgu(τ_{1}=τ_{2})

Γ_{c} = Constrain(θ, Γ)

in (Γ_{c} ∪ (Γ\Dom(θ)), θ) where

• mgu computes an unsorted mgu (in particular we assume that θ is idempotent and that Dom(θ) ∪ Cod(θ) ⊆ FV(τ_{1}=τ_{2})) or fails if none exists,

• the union of two sort contexts is defined by

Γ_{1} ∪ Γ_{2} = [α : Γ_{1}α ∪ Γ_{2}α | α ∈ Dom(Γ_{1}) ∪ Dom(Γ_{2})]

• Constrain(θ, Γ) computes the most general context Γ_{c} such that Γ_{c} ⊢ θ : Γ:

Constrain(θ, Γ) = ⋃_{α∈Dom(θ)} constrain(θα, Γα)

• constrain(τ, S) computes the most general context Γ such that Σ, Γ ⊢ τ : S:

constrain(α, S) = [α:S]
constrain(t(\overline{τ_{n}}), S) = ⋃_{C∈S} constrains(\overline{τ_{n}}, Dom(t, C))
constrains(\overline{τ_{n}}, \overline{S_{n}}) = ⋃_{i=1...n} constrain(τ_{i}, S_{i})

Thus unify fails if mgu fails or if some Dom(t, C) used in Constrain does not exist. By induction on the first argument of constrain it can be shown that

constrain(t(\overline{τ_{n}}), S) = constrains(\overline{τ_{n}}, ⋃_{C∈S} Dom(t, C))

which provides an alternative definition of constrain which is also useful in the proofs below. To see how constrain works, assume Eq and list again as in the examples in Section 2. Then constrain(list(β), Eq) = constrains(β, Dom(list, Eq)) = [β:Eq].

Soundness and completeness of Constrain are captured by the following lemmas which assume coregularity of Σ and are proved by induction on the structure of τ:

Lemma 4.1 If constrain(τ, S) is defined then Σ, constrain(τ, S) ⊢ τ : S.

Lemma 4.2 If constrain(θτ, S) is defined then constrain(τ, S) is defined as well and furthermore constrain(θτ, S) ⊢ θ : constrain(τ, S) holds.

Lemma 4.3 If Σ, Γ ⊢ τ : S then constrain(τ, S) is defined and more general than Γ.

Finally, the main theorems:

Theorem 4.4 If Σ is coregular, unify computes a most general unifier. Proof To show soundness, let unify(Γ, τ_{1}=τ_{2}) terminate with result (Γ_{0}, θ_{0}). It follows directly that θ_{0}τ_{1} = θ_{0}τ_{2}. It remains to be seen that Γ_{0} ⊢ θ_{0}α : Γα for all α. If α ∉ Dom(θ_{0}), then Γα ⊆ Γ_{0}α and the claim follows trivially. If α ∈ Dom(θ_{0}) then Γ_{0} ⪯ Γ_{c} = Constrain(θ_{0}, Γ) ⪯ constrain(θ_{0}α, Γα) and the claim follows from Lemma 4.1.

To show completeness let (Γ_{1}, θ_{1}) ∈ U(Γ, τ_{1}=τ_{2}), i.e. θ_{1}τ_{1} = θ_{1}τ_{2} and Γ_{1} ⊢ θ_{1} : Γ. Since τ_{1} and τ_{2} have an unsorted unifier θ_{1}, mgu(τ_{1}=τ_{2}) is defined and yields a substitution θ_{0} such that θ_{1} = δθ_{0} for some δ. Definedness of unify(Γ, τ_{1}=τ_{2}) also requires definedness of constrain(θ_{0}α, Γα): since Γ_{1} ⊢ θ_{1}α : Γα, Lemma 4.3 implies definedness of constrain(θ_{1}α, Γα) and Lemma 4.2 yields definedness of constrain(θ_{0}α, Γα). Thus unify(Γ, τ_{1}=τ_{2}) terminates with a result (Γ_{0}, θ_{0}).

It remains to be shown that Γ_{1} ⊢ δ : Γ_{0}. If β ∈ Dom(θ_{0}) then Γ_{0}β = {} and hence Γ_{1} ⊢ δβ : Γ_{0}β holds trivially. Now assume β ∉ Dom(θ_{0}). Thus Γ_{0}β = Γ_{c}β ∪ Γβ. From Γ_{1} ⊢ θ_{1} : Γ it follows that Γ_{1} ⊢ δβ : Γβ. Proving Γ_{1} ⊢ δ : Γ_{c} is more involved. From Lemma 4.2 it follows that constrain(θ_{1}α, Γα) ⊢ δ : constrain(θ_{0}α, Γα) for any α. Since Γ_{1} ⊢ θ_{1}α : Γα, Lemma 4.3 implies Γ_{1} ⪯ constrain(θ_{1}α, Γα) and thus by monotonicity Γ_{1} ⊢ δ : constrain(θ_{0}α, Γα). This in turn easily yields Γ_{1} ⊢ δ : Constrain(θ_{0}, Γ), i.e. Γ_{1} ⊢ δ : Γ_{c}. □

Theorem 4.5 Unification modulo Σ is unitary iff Σ is coregular. Proof The “if” direction is a consequence of Theorem 4.4. For the “only if” direction let Σ not be coregular. Thus there are classes C, D ≤ E and declarations t : (\overline{S_{n}})C and t : (\overline{T_{n}})D, \overline{S_{n}} ⪯̸ \overline{T_{n}}, and \overline{T_{n}} ⪯̸ \overline{S_{n}}, such that there is no third declaration t : (\overline{U_{n}})E′, E′ ⪯ E, and \overline{S_{n}}, \overline{T_{n}} ⪯ \overline{U_{n}}. Hence the unification problem ([β:E], t(\overline{α_{n}})=β) does not have a most general unifier. Two maximal ones are ([\overline{α_{n}:S_{n}}], θ) and ([\overline{α_{n}:T_{n}}], θ) where θ = \{β → t(\overline{α_{n}})\}. □

Thus we have a precise characterization of those signatures where principal types exist.

It remains to be seen if Mini-Haskell’s CLASS and INST declarations yield coregular signatures. In fact they do if restricted by the unformalized context conditions set out in Section 3. The latter context conditions imply that every Δ and ≤ derived from valid class and instance declarations has the following strong property: D(t, C) is either the singleton \{\overline{S_{n}}\}, where t(\overline{S_{n}})C is the unique declaration for t with result C, or empty, if there is no such declaration. Therefore Dom(t, C) can be computed using Δ alone, without reference to ≤. This leads to the observation that type unification, and hence, as we shall see in the next section, type inference, can ignore the subclass hierarchy completely.

It should be pointed out that ignoring the subclass hierarchy means giving up a degree of freedom afforded by the equivalence ≈ on sorts defined in Section 2. For example unify([α : {Eq}, β : {Ord}], α = β) returns ([α : {Eq, Ord}], {β ↦ α}). Taking ≈ into account, we could just as well return ([α : {Ord}], {β ↦ α}). In order to show that the subsequent developments do not depend on which of these unifiers is computed, we assume in the sequel that unify is an arbitrary function which, provided Σ is coregular, returns a most general unifier: if U(Γ, τ_{1}=τ_{2}) ≠ {} then

• unify(Γ, τ_{1}=τ_{2}) ∈ U(Γ, τ_{1}=τ_{2}) and

• (Γ′, θ) ≤ unify(Γ, τ_{1}=τ_{2}) for all (Γ′, θ) ∈ U(Γ, τ_{1}=τ_{2}).

This implies a number of simple properties:

Fact 4.6 If unify(Γ, τ_{1}=τ_{2}) = (Γ′, θ) then

• θ is a most general unifier of τ_{1} and τ_{2},

• Dom(Γ′) ∪ FV(θ) ⊆ Dom(Γ) ∪ FV(τ_{1}) ∪ FV(τ_{2}),

• Dom(Γ′) ∩ Dom(θ) = {}.

The second fact states that unify does not introduce new variables, and the last expresses that Γ′ does not constrain variables instantiated by θ. It is easy to see that the Γ′ is determined only up to ≈. Hence the unification algorithm could always ensure that Γ′ is “minimized” by removing redundant elements from each sort.

Finally one may wonder if the fact that coregularity is strictly weaker than Haskell’s context conditions means the latter could be relaxed. We believe that there are no non-trivial relaxations but do not want to enlarge on this subject because it requires going beyond the type system to take semantics and pragmatics into account.

5 Algorithm W

The syntax-directed rule system in Figure 5 is non-deterministic, since rule ASM′ can choose any instance of the type of x. To obtain a deterministic algorithm, we refine the syntax directed system such that it keeps types as general as possible. The result is algorithm W in Figure 6. In this section we assume that Σ is coregular — otherwise unify is not well-defined.

W(V, Γ, E, e) = case e of

x ⇒  \begin{matrix}let & \begin{matrix}∀\overline{α_{n}:S_{n}}.τ & = & E(x) \\ β_{i} & ∉ & V [i = 1 … n] \end{matrix} \\ in (V′ ∪ \{\overline{β_{n}}\}, Γ[\overline{β_{n}:S_{n}}], \{\}, \{\overline{α_{n} ↦ β_{n}}\}τ) \end{matrix}

λx.e ⇒ let \begin{matrix}α & ∉ & V \\ (V′, Γ′, θ′, τ) & = & W(V ∪ \{α\}, Γ, E[x:α], e) \end{matrix}

in (V′, Γ′, θ′, α → τ)

(e_{1} e_{2}) ⇒ let (V_{1}, Γ_{1}, θ_{1}, τ_{1}) = W(V, Γ, E, e_{1})

(V_{2}, Γ_{2}, θ_{2}, τ_{2}) = W(V_{1}, Γ_{1}, θ_{1}E, e_{2})
α ∉ V_{2}
(Γ′, θ′) = unify(Γ_{2}, θ_{2}θ_{1}τ_{1} = θ_{2}τ_{2} → α)
in (V_{2} ∪ {α}, Γ′, θ′θ_{2}θ_{1}, α)

let x = e_{1} in e_{2} ⇒ let \begin{aligned}(V_{1}, Γ_{1}, θ_{1}, τ_{1}) & = & W(V, Γ, E, e_{1}) \\ \{\overline{α_{n}}\} & = & FV(θ_{1}τ_{1}) − FV(θ_{1}E) \\ (V_{2}, Γ_{2}, θ_{2}, τ_{2}) & = & W(V_{1}, Γ_{1}\\{\overline{α_{n}}\}, \\ & & (θ_{1}E)[x : ∀\overline{α_{n}:Γ_{1}α_{n}}.θ_{1}τ_{1}], e_{2}) \end{aligned}

in (V_{2}, Γ_{2}, θ_{2}θ_{1}, τ_{2})

Fig. 6. Algorithm W

Algorithm W follows the same pattern as Milner’s original algorithm of the same name (Mil78): the type of an expression e is computed by traversing e in a top-down manner. W(V, Γ, E, e) returns a quadruple (V′, Γ′, θ, τ), where θτ is the type of e in the context of Γ′ and θE. The top level call is W ({}, [], E, e), where E is closed. Observe the different let-constructs: the one on the left hand side is in the object language, the ones on the right are part of the type inference algorithm.

The parameter V contains all “used” variables, i.e. variables that occur in Γ or in E. Thus a type variable α ∉ V is a “new” variable. For our algorithm to be truly functional, a linear ordering on variables may be used, such that the “next” new variable α ∉ V can be computed deterministically. We will assume in general that W is invoked with V, Γ and E such that FV(E) ∪ Dom(Γ) ⊆ V.

Algorithm W is not meant to be implemented directly but merely serves as a mathematically tractable stepping stone towards an efficient implementation. Its principal weakness is the fact that substitutions are computed from scratch and composed later on. This problem is addressed and solved with algorithm I in the next section. In contrast to substitutions, contexts are computed incrementally, i.e. the result context Γ′ is an extension of the input context Γ.

A formal analysis of W requires some more notation. For an environment E and a substitution θ, define θE = [x : θ(E(x)) | x ∈ Dom(E)]. Two substitutions are equal on a set of variables W, written as θ =_{W} θ′, if θα = θ′α for all α ∈ W. The restriction of a substitution to a set of variables W is defined as θ|_{W} α = θα if α ∈ W and θ|_{W} α = α otherwise. Given a list of syntactic objects \overline{C_{n}} we write FV(\overline{C_{n}}) instead of FV(C_{1}) ∪ … ∪ FV(C_{n}).

We first show that the algorithm is invariant under α-conversion. The free variables of an expression e, i.e. FV(e), and the application of a substitution to e are defined as usually in λ-calculus.

Lemma 5.1 If W(V, Γ, E[x:τ], e) = (V′, Γ′, θ′, τ′) and y ∉ Dom(E) then W(V, Γ, E[y:τ], {x ↦ y}e) = (V′, Γ′, θ′, τ′). Proof by induction on e. □

With this lemma, we can easily show the desired theorem for α-conversion.

Theorem 5.2 Let e be λx.e_{2} or let y = e_{1} in e_{2}. If W(V, Γ, E, e) is defined, y ∉ Dom(E), and y ∉ FV(e), then W(V, Γ, E, e′) = W(V, Γ, E, e), where e′ is λy.{x ↦ y}e_{2} or let y = e_{1} in {x ↦ y}e_{2} respectively. Proof by induction, using Lemma 5.1. □

The following correctness and completeness results for W do not depend on the particular unification algorithm, as discussed towards the end of Section 4.

Theorem 5.3 (Correctness of W) If W(V, Γ, E, e) = (V′, Γ′, θ, τ) then Σ, Γ′, θE ⊳ e : θτ.

Before we can prove the correctness theorem, we need to supply a series of lemmas. The following lemma shows the basic relations between the variables of the objects used by W. The first item states that all used variables are recorded in V′. Next, all new variables occuring in the computed objects are in V′ but not in V, i.e. there is no “reuse” of names. The third item states that if some type variables of the computed type are not new, they must have been in the environment E. The last item requires the computed context to be free of assumptions about old variables (which are in Dom(θ′)), i.e. no “litter”.

Lemma 5.4 Assume W(V, Γ, E, e) = (V′, Γ′, θ′, τ) and FV(E) ∪ Dom(Γ) ⊆ V. Then

1. V ⊆ V′ and Dom(Γ′) ∪ FV(θ′, E, τ) ⊆ V′

2. (Dom(Γ′) ∪ FV(θ′, τ)) − (Dom(Γ) ∪ FV(E)) ⊆ V′ − V.

3. FV(θ′, τ) ∩ V ⊆ FV(E)

4. Dom(Γ′) ∩ Dom(θ′) = {}

Proof The first claim follows easily since all new variables are recorded in V′ and since the unification algorithm does not introduce new variables (see Fact 4.6). For the same reason and since all variables in Dom(Γ′) ∪ FV(θ′, τ) are either new or in Dom(Γ) ∪ FV(E), we obtain the second claim from FV(E) ∪ Dom(Γ) ⊆ V.

The remaining two items are shown by induction on the term structure:

x : trivial since all β_{i} are new variables, i.e. β_{i} ∉ V. λx.e : by induction hypothesis and since α is a new variable. (e_{1} e_{2}) : We first show

(FV(θ′) ∪ {α}) ∩ V ⊆ FV(E).

Since the unification algorithm does not introduce new variables, it follows that FV(θ′) ⊆ FV(θ_{2}θ_{1}, τ_{1}, τ_{2}) ∪ {α}. Because α ∉ V, it suffices to show

FV(θ_{2}θ_{1}, τ_{2}, τ_{1}) ∩ V ⊆ FV(E).  (1)

The induction hypothesis for e_{2} yields FV(θ_{2}, τ_{2}) ∩ V_{1} ⊆ FV(θ_{1}E). Using FV(θ_{1}E) ⊆ FV(E, θ_{1}) and V ⊆ V_{1} we obtain FV(θ_{2}, τ_{2}) ∩ V ⊆ FV(E, θ_{1}). By induction hypothesis for e_{1}, i.e. FV(θ_{1}, τ_{1})∩V ⊆ FV(E), we easily get (1). Next we show that Dom(Γ′) ∩ Dom(θ′θ_{2}θ_{1}) = {}. We obtain Dom(Γ_{1}) ∩ Dom(θ_{1}) = {} from the induction hypothesis. Then from Dom(θ_{1}) ⊆ V_{1} and Dom(θ_{1}) ∩ FV(θ_{1}E) = {} (idempotence of θ_{1}) we obtain Dom(Γ_{2}) ∩ Dom(θ_{1}) = {}, as Dom(Γ_{2}) − (Dom(Γ_{1}) ∪ FV(θ_{1}E)) ⊆ V_{2} − V_{1} (item 2 of Lemma 5.4). Next, from Dom(Γ_{2}) ∩ Dom(θ_{2}) = {} (induction hypothesis) and since Dom(θ_{2}θ_{1}) = Dom(θ_{1}) ∪ Dom(θ_{2}), Dom(Γ_{2}) ∩ Dom(θ_{2}θ_{1}) = {} follows. Then Dom(Γ′) ∩ Dom(θ′θ_{2}θ_{1}) = {} follows from the properties of the unification algorithm, i.e. it may not constrain variables from Dom(θ′) (see Fact 4.6).

let x = e_{1} in e_{2}: We first show

FV(θ_{2}θ_{1}, τ_{2}) ∩ V ⊆ FV(E).

The induction hypothesis for e_{2} yields

FV(θ_{2}, τ_{2}) ∩ V_{1} ⊆ FV(θ_{1}E[x : ∀\overline{α_{n}:Γ_{1}α_{n}}.θ_{1}τ_{1}])

Since FV(∀\overline{α_{n}:Γ_{1}α_{n}}.θ_{1}τ_{1}) ⊆ FV(θ_{1}E), we get

FV(θ_{2}, τ_{2}) ∩ V_{1} ⊆ FV(θ_{1}E).

Then the rest of the proof proceeds as for (e_{1} e_{2}).

The proof of Dom(Γ_{2}) ∩ Dom(θ_{2}θ_{1}) = {} also works as in the (e_{1} e_{2}) case; the only difference (apart from the additional θ′) is that we have Dom(Γ_{2}) ∩ \{\overline{α_{n}}\} = \{\}, which only simplifies the proof. □

The next lemma shows that the relation Γ ⊢ θ : Γ′ enjoys a kind of transitivity property w.r.t. substitutions.

Lemma 5.5 If Γ_{2} ⊢ θ_{2} : Γ_{1} and Γ_{1} ⊢ θ_{1} : Γ then Γ_{2} ⊢ θ_{2}θ_{1} : Γ Proof We have to show ∀α ∈ Dom(Γ).Γ_{2} ⊢ θ_{2}θ_{1}α : Γα. Consider the derivation of Γ_{1} ⊢ θ_{1}α : Γα (by premise). It is easy to construct a derivation of Γ_{2} ⊢ θ_{2}θ_{1}α : Γα, since ∀β ∈ FV(θ_{1}α).Γ_{2} ⊢ θ_{2}β : Γ_{1}β and Γ_{1} ⊢ β : Γβ (as θ_{1}β = β follows from the idempotence of θ_{1}). □

The fact that W specializes contexts is shown in the next result.

Lemma 5.6 If W(V, Γ, E, e) = (V′, Γ′, θ′, τ) then Γ′ ⊢ θ′ : Γ.

Proof by induction on the structure of e:

x: Γ[β_{n}:S_{n}] ⊢ {} : Γ trivial. λx.e: Since the induction hypothesis holds for any E, including E[x:α], Γ′ ⊢ θ′ : Γ

follows directly. (e_{1} e_{2}): By induction hypothesis we get Γ_{1} ⊢ θ_{1} : Γ and Γ_{2} ⊢ θ_{2} : Γ_{1} and by

transitivity (Lemma 5.5) and by correctness of the unification algorithm we get Γ′ ⊢ θ′θ_{2}θ_{1} : Γ.

let x = e_{1} in e_{2}: By induction hypothesis we get

Γ_{1} ⊢ θ_{1} : Γ  (2)
Γ_{2} ⊢ θ_{2} : Γ_{1}\{α_{n}}  (3)

Now we show

Γ_{1}\{α_{n}} ⊢ θ_{1} : Γ  (4)

That is, we have to show Γ_{1}\\{\overline{α_{n}}\} ⊢ θ_{1}β : Γβ for all β ∈ Dom(Γ). First we prove FV(θ_{1}(Dom(Γ))) ∩ \{\overline{α_{n}}\} = \{\}. From Lemma 5.4, item 3, it follows that FV(θ_{1}τ_{1}) ∩ Dom(Γ) ⊆ FV(E). Idempotence of θ_{1} yields FV(θ_{1}τ_{1}) ∩ FV(θ_{1}(Dom(Γ))) ⊆ FV(θ_{1}E). Simple set theory yields FV(θ_{1}(Dom(Γ))) ∩ (FV(θ_{1}τ_{1}) − FV(θ_{1}E)) = {} as claimed above. Now (4) follows. Combining (4) and (3) by transitivity (Lemma 5.5) yields Γ_{2} ⊢ θ_{2}θ_{1} : Γ □

The next lemma states that ⊳ is preserved under instantiation assuming a context that obeys the constraints.

Lemma 5.7 If Σ, Γ, E ⊳ e : τ and Γ′ ⊢ θ′ : Γ, then Σ, Γ′, θ′E ⊳ e : θ′τ.

Proof simple by adding proofs of the form Γ′ ⊢ θ′α : Γα in the proof tree of Σ, Γ, E ⊳ e : τ to obtain a proof of Σ, Γ′, θ′E ⊳ e : θ′τ. □

At last we are able to prove the correctness theorem:

Proof of Theorem 5.3 by induction on the structure of e. We have the following cases:

x: Correctness follows easily from

ASM′  {Σ, Γ[\overline{β_{n}:S_{n}}] ⊢ E(x) ⪰ \{\overline{α_{n} ↦ β_{n}}\}τ \atop Σ, Γ[\overline{β_{n}:S_{n}}], E ⊳ x : \{\overline{α_{n} ↦ β_{n}}\}τ}

λx.e: By induction hypothesis we get Σ, Γ′, (θ′E)[x:θ′α] ⊳ e : θτ. Then ABS applies:

ABS {Σ, Γ, (θ′E)[x:θ′α] ⊳ e : θ′τ′ \atop Σ, Γ, θ′E ⊳ λx.e : θ′α → θτ′}

(e_{1} e_{2}): We get

Σ, Γ_{1}, θ_{1}E ⊳ e_{1} : θ_{1}τ_{1}
Σ, Γ_{2}, θ_{2}θ_{1}E ⊳ e_{2} : θ_{2}τ_{2}

from the induction hypotheses for e_{1} and e_{2}. The correctness of the unification algorithm yields Γ′ ⊢ θ′ : Γ_{2} and then with Γ_{2} ⊢ θ_{2} : Γ_{1} (from Lemma 5.6) and Lemma 5.5 we obtain Γ′ ⊢ θ′θ_{2} : Γ_{1}. From Lemma 5.7 we now get the two premises for the AP P rule, since θ′θ_{2}θ_{1}τ_{1} = θ′θ_{2}τ_{2} → θ′α. Furthermore, θ_{2}θ_{1}α = α, since α is a new variable (i.e. α ∉ V_{2} and Dom(θ_{2}) ∪ Dom(θ_{1}) ⊆ V_{2} by Lemma 5.4).

APP \begin{matrix}Σ, Γ′, θ′θ_{2}θ_{1}E ⊳ e_{1} : θ′θ_{2}θ_{1}τ_{1} & Σ, Γ′, θ′θ_{2}θ_{1}E ⊳ e_{2} : θ′θ_{2}τ_{2} \\ Σ, Γ′, θ′θ_{2}θ_{1}E ⊳ (e_{1} e_{2}) : θ′α \end{matrix}

let x = e_{1} in e_{2} : Using Γ′_{1} = Γ_{1}\\{\overline{α_{n}}\}, \overline{S_{n} = Γ_{1}α_{n}}, and E′ = E[x : ∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1}] the induction hypotheses are

Σ, Γ′_{1}[\overline{α_{n}:S_{n}}], θ_{1}E ⊳ e_{1} : θ_{1}τ_{1}  (5)
Σ, Γ_{2}, θ_{2}θ_{1}E′ ⊳ e_{2} : θ_{2}τ_{2}  (6)

Notice that FV(θ_{1}E′) ∩ \{\overline{α_{n}}\} = \{\}. To apply LET′, we show

Σ, Γ_{2}[\overline{α_{n}:S_{n}}], θ_{2}θ_{1}E ⊳ e_{1} : θ_{2}θ_{1}τ_{1}  (7)

As we get Γ_{2} ⊢ θ_{2} : Γ′_{1} from Lemma 5.6 and FV(θ_{2}) ∩ \{\overline{α_{n}}\} = \{\} from Lemma 5.4 (recall that \{\overline{α_{n}}\} ⊆ V_{1} and \{\overline{α_{n}}\} ∩ FV(θ_{1}E′) = \{\}), we obtain

Γ_{2}[\overline{α_{n}:S_{n}}] ⊢ θ_{2} : Γ′_{1}[\overline{α_{n}:S_{n}}].

Then (7) follows from Lemma 5.7 and (5). As Dom(θ_{1})∩FV(τ_{2}) = {} is a consequence of Lemma 5.4 (as above, Dom(θ_{1}) ⊆ V_{1} and Dom(θ_{1}) ∩ FV(θ_{1}E′) = {} as θ_{1} is idempotent), we obtain

Σ, Γ_{2}, θ_{2}θ_{1}E′ ⊳ e_{2} : θ_{2}θ_{1}τ_{2}  (8)

Now LET′ applies to

\begin{matrix}(7) & (8) & \{\overline{α_{n}}\} = FV(θ_{1}τ_{1}) − FV(θ_{1}E) \\ Γ_{2}, Σ, θ_{2}θ_{1}E ⊳ let x = e_{1} in e_{2} : θ_{2}θ_{1}τ_{2} \end{matrix}

□

The following lemma is crucial for establishing the principal type theorem.

Lemma 5.8 (Completeness of W) If Σ, Γ^{∗}, θ^{∗}E ⊳ e : τ^{∗}, Dom(Γ) ∪ FV(E) ⊆ V, and Γ^{∗} ⊢ θ^{∗} : Γ then there exists a substitution δ such that

W(V, Γ, E, e) = (V_{1}, Γ_{1}, θ_{1}, τ_{1}),
θ^{∗}E = δθ_{1}E,
τ^{∗} = δθ_{1}τ_{1},
Γ^{∗} ⊢ δ : Γ_{1}.

Proof by induction on the structure of e. We assume w.l.o.g. a derivation for Σ, Γ^{∗}, θ^{∗}E ⊳ e : τ^{∗} that has no variable overlap with the new variables V_{1} − V used by algorithm W.

x: We have

ASM′  {Σ, Γ^{∗} ⊢ θ^{∗}E(x) ⪰ τ^{∗} \atop Σ, Γ^{∗}, θ^{∗}E ⊳ x : τ^{∗}}

Observe that we can write θE(x) = θ^{∗}∀\overline{α_{n}:S_{n}}.τ as ∀\overline{α_{n}:S_{n}}.θ̂^{∗}τ, where θ̂^{∗} = θ^{∗}|_{Dom(θ^{∗})−\{\overline{α_{n}}\}}, possibly by renaming some \overline{α_{n}}. Assuming Σ, Γ^{∗} ⊢ θ^{∗}E(x) ⪰ τ^{∗}, let θ be the corresponding substitution as in Definition 3.1 with Dom(θ) ⊆ \{\overline{α_{n}}\}, and τ^{∗} = θθ̂^{∗}τ. Let δ = θ^{∗} ∪ \{\overline{β_{n} ↦ θα_{n}}\}. As \overline{β_{n}} are new variables, θ^{∗}E = δE holds. Next, τ^{∗} = δ(\{\overline{α_{n} ↦ β_{n}}\}τ) = θθ̂^{∗}τ follows easily. Finally, Γ^{∗} ⊢ δ : Γ[\overline{β_{n}:S_{n}}] follows from Γ^{∗} ⊢ θ^{∗} : Γ (by premise) and from Σ, Γ^{∗} ⊢ θ′α_{i} : S_{i}, [i = 1, …, n] (see Definition 3.1).

λx.e: The derivation ends with

ABS {Σ, Γ^{∗}, (θ^{∗}E)[x:τ_{1}^{∗}] ⊳ e : τ_{2}^{∗} \atop Σ, Γ^{∗}, θ^{∗}E ⊳ λx.e : τ_{1}^{∗} → τ_{2}^{∗}}

As the algorithm is invariant under α-conversion (Lemma 5.2), we can safely assume that x ∉ Dom(E). To apply the induction hypotheses, we define θ_{0} = θ^{∗} ∪ {α ↦ τ_{1}^{∗}}. Then Σ, Γ^{∗}, θ_{0}(E[x:α]) ⊳ e : τ_{2}^{∗} and Γ^{∗} ⊢ θ_{0} : Γ are easy to verify. By induction hypothesis there exists δ_{1} such that

W(V ∪ {α}, Γ, E[x:α], e) = (V′, Γ′, θ′, τ′),  (9)
(θ_{0}E)[x:τ_{1}^{∗}] = δ_{1}θ′E[x:α],  (10)
τ_{2}^{∗} = δ_{1}θ′τ′,  (11)
Γ^{∗} ⊢ δ_{1} : Γ′  (12)

and hence W(V, Γ, E, λx.e) = (V′, Γ′, θ′, α → τ′). Now θ_{0}E = δ_{1}θ′E follows from (10). Furthermore, from (10) we obtain τ_{1}^{∗} = δ_{1}θ′α and hence τ_{1}^{∗} → τ_{2}^{∗} = δ_{1}θ′(α → τ′) from (11).

(e_{1} e_{2}): We assume

APP {Σ, Γ^{∗}, θ^{∗}E ⊳ e_{1} : τ_{2}^{∗} → τ_{1}^{∗} Σ, Γ^{∗}, θ^{∗}E ⊳ e_{2} : τ_{2}^{∗} \atop Σ, Γ^{∗}, θ^{∗}E ⊳ (e_{1} e_{2}) : τ_{1}^{∗}}

Applying the induction hypothesis to e_{1} yields δ_{1} such that

W(V, Γ, E, e) = (V_{1}, Γ_{1}, θ_{1}, τ_{1}),  (13)
θ^{∗}E = δ_{1}θ_{1}E,  (14)
τ_{2}^{∗} → τ_{1}^{∗} = δ_{1}θ_{1}τ_{1},  (15)
Γ^{∗} ⊢ δ_{1} : Γ_{1}.  (16)

The induction hypothesis with e_{2} with Γ_{1}, where Γ^{∗} ⊢ δ_{1} : Γ_{1}, and θ_{1}E yields δ_{2} such that

W(V_{1}, Γ_{1}, θ_{1}E, e_{2}) = (V_{2}, Γ_{2}, θ_{2}, τ_{2}),  (17)
θ^{∗}E = δ_{2}θ_{2}θ_{1}E,  (18)
τ_{2}^{∗} = δ_{2}θ_{2}τ_{2},  (19)
Γ^{∗} ⊢ δ_{2} : Γ_{2}.  (20)

Let δ^{∗} be defined as

δ^{∗}β = \begin{cases}δ_{1}β & if β ∈ FV(θ_{1}τ_{1}) − Cod(θ_{2}) \\ τ_{1}^{∗} & if β = α \\ δ_{2}β & otherwise \end{cases}

We show that δ^{∗} is a unifier of θ_{2}θ_{1}τ_{1} = θ_{2}τ_{2} → α. Notice that FV(θ_{2}, τ_{2}) ∩ FV(θ_{1}τ_{1}) ⊆ FV(θ_{1}E) follows from Lemma 5.4 and that the two substitutions δ_{2}θ_{2} and δ_{1} coincide on FV(θ_{1}E): combining (14) with (18) yields

δ_{2}θ_{2} =_{FV(θ_{1}E)} δ_{1}  (21)

This overlap simplifies the following proofs by case analysis, in which the case β = α is immaterial. First, to show δ^{∗}θ_{2}τ_{2} = δ_{2}θ_{2}τ_{2} = τ_{2}^{∗}, assume β ∈ FV(τ_{2}). Then in case β ∉ FV(θ_{2}), δ^{∗}τ_{2} = δ_{2}τ_{2} follows from (21) if β ∈ FV(θ_{1}τ_{1}) as FV(θ_{2}, τ_{2}) ∩ FV(θ_{1}τ_{1}) ⊆ FV(θ_{1}E), and is trivial otherwise. If β ∈ FV(θ_{2}), then δ^{∗}θ_{2}τ_{2} = δ_{2}θ_{2}τ_{2} is trivial. To show δ^{∗}θ_{2}θ_{1}τ_{1} = δ_{1}θ_{1}τ_{1}, assume β ∈ FV(θ_{1}τ_{1}). If β ∈ Dom(θ_{2}), (21) gives the desired result as Dom(θ_{2}) ∩ FV(θ_{1}τ_{1}) ⊆ FV(θ_{1}E). In case β ∉ Dom(θ_{2}), δ^{∗}θ_{1}τ_{1} = δ_{1}τ_{1} follows easily. Hence δ^{∗} is the desired unifier:

δ^{∗}θ_{2}θ_{1}τ_{1} = τ_{2}^{∗} → τ_{1}^{∗} = δ^{∗}(θ_{2}τ_{2} → α).

We obtain Γ^{∗} ⊢ δ^{∗} : Γ_{2} from (16) and (20) by case analysis: we have to show Σ, Γ^{∗} ⊢ δ^{∗}β : Γ_{2}β for all β ∈ Dom(Γ_{2}). First recall that Dom(Γ_{2}) ∩ Dom(θ_{2}) = {} by Lemma 5.4. If β ∈ FV(θ_{1}τ_{1}) − Cod(θ_{2}), then we have another case distinction: if β ∈ Dom(θ_{2}), then Γ_{2}β = {}, otherwise θ_{2}β = β and from Γ_{2} ⊢ θ_{2} : Γ_{1} (Lemma 5.6), we have Γ_{1}β ⊆ Γ_{2}β and the claim follows from (16). The case β = α is trivial because Γ_{2}α = {}. The remaining case, Σ, Γ^{∗} ⊢ δ_{2}θ_{2}β : Γ_{2}β, follows easily from (20) since Dom(Γ_{2}) ∩ Dom(θ_{2}) = {}.

Then by completeness of unification, θ′ is a most general unifier computed in unify, and there exists δ′ such that δ^{∗} = δ′θ′. Hence we get

W(V, Γ, E, (e_{1} e_{2})) = (V_{2} ∪ α, Γ′, θ′θ_{2}θ_{1}, α),
θ^{∗}E = δ′θ′θ_{2}θ_{1}E,
τ^{∗} = δ′θ′θ_{2}τ_{2},
Γ^{∗} ⊢ δ′ : Γ′,

where the last statement follows from the completeness of unification. let x = e_{1} in e_{2}: We assume Γ^{∗} ⊢ θ^{∗} : Γ and, by LET′,

Σ, Γ^{∗}[\overline{α_{k}^{∗}:S_{k}^{∗}}], θ^{∗}E ⊳ e_{1} : τ_{1}^{∗} Σ, Γ^{∗}, (θ^{∗}E)[x:∀\overline{α_{k}^{∗}:S_{k}^{∗}}.τ_{1}^{∗}] ⊳ e_{2} : τ_{2}^{∗}
Σ, Γ^{∗}, θ^{∗}E ⊳ let x = e_{1} in e_{2} : τ_{2}^{∗}

where \{\overline{α_{k}^{∗}}\} = FV(τ_{1}^{∗}) − FV(θ^{∗}E). As the algorithm is invariant under αconversion (Lemma 5.2), we can safely assume that x ∉ Dom(E). As \{\overline{α_{k}^{∗}}\} ∩ FV(θ^{∗}E) = \{\} we can w.l.o.g. rename \overline{α_{k}^{∗}} in the premises of the above rule (not in Γ′) in order to assume that \{\overline{α_{k}^{∗}}\}∩Dom(Γ^{∗}) = \{\}. Formally, this can be done by Lemma 5.5. Then we can apply the induction hypothesis to e_{1} with Γ^{∗}[\overline{α_{k}^{∗}:S_{k}^{∗}}] ⊢ θ^{∗} : Γ and obtain δ_{1} such that

W(V, Γ, E, e_{1}) = (V_{1}, Γ_{1}, θ_{1}, τ_{1}),  (22)
θ^{∗}E = δ_{1}θ_{1}E,  (23)
τ_{1}^{∗} = δ_{1}θ_{1}τ_{1},  (24)
Γ^{∗}[\overline{α_{k}^{∗}:S_{k}^{∗}}] ⊢ δ_{1} : Γ′_{1}[\overline{α_{n}:S_{n}}],  (25)

where Γ′_{1} = Γ_{1}\\{\overline{α_{n}}\} and \overline{S_{n}} = \overline{Γ_{1}α_{n}}. From \{\overline{α_{n}}\} = FV(θ_{1}τ_{1}) − FV(θ_{1}E) we infer FV(\{\overline{δ_{1}α_{n}}\}) = FV(δ_{1}θ_{1}τ_{1}) − FV(δ_{1}θ_{1}E) = \{\overline{α_{k}^{∗}}\}. Hence Γ^{∗} ⊢ δ_{1} : Γ′_{1} follows from (25). Notice that δ_{1}∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1} = ∀\overline{α_{n}:S_{n}}.δ̂_{1}θ_{1}τ_{1}, where δ̂_{1} = δ_{1}|_{Dom(δ_{1})−\{\overline{α_{n}}\}}, follows from the assumption that new variables used by W do not occur in the chosen derivation, i.e. in Cod(δ_{1}). Then we obtain Σ, Γ^{∗} ⊢ δ_{1}∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1} ⪰ ∀\overline{α_{k}^{∗}:S_{k}^{∗}}.τ^{∗} by using δ_{1}|_{\{\overline{α_{n}}\}} as the substitution in Definition 3.1 and because Σ, Γ^{∗}[\overline{α_{k}^{∗}:S_{k}^{∗}}] ⊢ δ_{1}α_{i} : S_{i}, [i = 1 … n] follows from (25). Now the problem is that the induction hypothesis cannot be applied directly to e_{2} with Γ^{∗} ⊢ δ_{1} : Γ′_{1} and θ_{1}E[…], since in general (θ^{∗}E)[x:∀\overline{α_{k}^{∗}:S_{k}^{∗}}.τ_{1}^{∗}] ≠ (δ_{1}θ_{1}E)[x:δ_{1}∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1}]. Thus we have to find a different basis in order to apply the induction hypothesis for e_{2}. From

Σ, Γ^{∗}(θ^{∗}E)[x:∀\overline{α_{k}^{∗}:S_{k}^{∗}}.τ_{1}^{∗}] ⊳ e_{2} : τ_{2}^{∗}  (26)

we can infer

Σ, Γ^{∗}, (θ^{∗}E)[x:δ_{1}∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1}] ⊳ e_{2} : τ_{2}^{∗},

since at each application of ASM′ to x in the proof of (26), we can use the more general [x:δ_{1}∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1}] instead of [x:∀\overline{α_{k}^{∗}:S_{k}^{∗}}.τ_{1}^{∗}]. Then the induction hypothesis applies to e_{2} with Γ^{∗} ⊢ δ_{1} : Γ′_{1} and the environment θ_{1}E[x:∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1}]. We get δ_{2} such that

W(V_{1}, Γ′_{1}, E, e_{2}) = (V_{2}, Γ_{2}, θ_{2}, τ_{2}),  (27)
(θ^{∗}E)[x:δ_{1}∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1}] = δ_{2}θ_{2}(θ_{1}E[x:∀\overline{α_{n}:S_{n}}.θ_{1}τ_{1}]),  (28)
τ_{2}^{∗} = δ_{2}θ_{2}τ_{2},  (29)
Γ^{∗} ⊢ δ_{2} : Γ_{2}.  (30)

Hence W(V, Γ, E, let x = e_{1} in e_{2}) = (V_{2}, Γ_{2}, θ_{2}, τ_{2}). We obtain τ_{2}^{∗} = δ_{2}θ_{2}θ_{1}τ_{2} from τ_{2}^{∗} = δ_{2}θ_{2}τ_{2} and Dom(θ_{1}) ∩ FV(τ_{2}) = {} (as in Theorem 5.3). It only remains to show θ^{∗}E = δ_{2}θ_{2}θ_{1}E, which is a consequence of (28), as x ∉ Dom(E). □

Now we can finally show the desired principal type theorem.

Theorem 5.9 If e has type σ_{0} under a closed environment E, i.e. Σ, [], E ⊢ e : σ_{0} and FV(E) ⊆ V_{0}, then W(V_{0}, [], \{\}, E, e) = (V, Γ, θ, τ) and ∀\overline{α_{n}:Γα_{n}}.θτ is a principal type of e w.r.t. Σ and E, where \{\overline{α_{n}}\} = FV(θτ). Proof Assume some typing Σ, [], E ⊢ e : ∀\overline{α′_{m}:S′_{m}}.τ′. We infer Σ, [α′_{m}:S′_{m}], E ⊢ e : τ′ by ∀E and then obtain a syntax-directed derivation Σ, [α′_{m}:S′_{m}], E ⊳ e : τ′ by Theorem 3.4. Then Lemma 5.8 applies with Γ^{∗} = [α′_{m}:S′_{m}] and θ^{∗} = {}. We thus get δ such that

E = δE,
τ′ = δθτ,
Γ^{∗} ⊢ δ : Γ.

Then ∀\overline{α_{n}:Γα_{n}}.θτ is a principal type of e w.r.t. E, since ∀\overline{α_{n}:Γα_{n}}.θτ ⪰ ∀\overline{α′_{m}:S′_{m}}.τ′ follows from τ′ = δθτ, \{\overline{α_{n}}\} = FV(θτ), and Γ^{∗} ⊢ δ : Γ. □

6 Algorithm I

As in the original work by Milner (Mil78), we now present a more efficient refinment of algorithm W. Compared to W, algorithm I^{2} takes an extra argument, the substitution computed so far. This substitution is extended incrementally instead of computing new subtitutions and composing them later.

The equivalence of W and I is an easy matter. A renaming is an injective substitution that maps variables to variables only.

Theorem 6.1 (Equivalence of W and I) Assume θ_{0} is an idempotent substitution such that θ_{0}E_{0} = E. If W(V, Γ, E, e) = (V′, Γ′, θ′, τ′) then I(V, Γ, θ_{0}, E_{0}, e) = (V′′, Γ′′, θ′′, τ′′) and there exists a renaming σ such that V′′ = σV′, ∀α.Γ′′α = Γ′(σα), θ′′τ′′ = σθ′τ′ and θ′′E = σθ′E. Proof by simple induction on the structure of e. □

2 Although the typography in (Mil78) is ambiguous, Milner has confirmed by email that he intended it to be I, not J: it is an imperative implementation of W. Milner’s I is imperative because he maintains a single global copy of θ which is updated by sideeffects. In a purely functional style this requires an additional argument and result.

I(V, Γ, θ, E, e) = case e of

x ⇒  \begin{matrix}let & \begin{matrix}∀\overline{α_{n}:S_{n}}.τ & = & E(x) \\ β_{i} & ∉ & V [i = 1 … n] \end{matrix} \\ in (V ∪ \{\overline{β_{n}}\}, Γ[\overline{β_{n}:S_{n}}], θ, \{\overline{α_{n} ↦ β_{n}}\}τ) \end{matrix}

λx.e ⇒ let \begin{matrix}α & ∉ & V \\ (V′, Γ′, θ′, τ) & = & I(V ∪ \{α\}, Γ, θ, E[x:α], e) \end{matrix}

in (V′, Γ′, θ′, α → τ)

(e_{1} e_{2}) ⇒ let (V_{1}, Γ_{1}, θ_{1}, τ_{1}) = I(V, Γ, θ, E, e_{1})

(V_{2}, Γ_{2}, θ_{2}, τ_{2}) = I(V_{1}, Γ_{1}, θ_{1}, E, e_{2})
α ∉ V_{2}
(Γ′, θ′) = unify(Γ_{2}, θ_{2}τ_{1} = θ_{2}τ_{2} → α)
in (V_{2} ∪ {α}, Γ′, θ′θ_{2}, α)

let x = e_{1} in e_{2} ⇒ let \begin{aligned}(V_{1}, Γ_{1}, θ_{1}, τ_{1}) & = & I(Γ, θ, E, e_{1}) \\ \{\overline{α_{n}}\} & = & FV(θ_{1}τ_{1}) − FV(θ_{1}E) \end{aligned}

in I(V_{1}, Γ_{1}\\{\overline{α_{n}}\}, θ_{1}, E[x : ∀\overline{α_{n}:Γ_{1}α_{n}}.θ_{1}τ_{1}], e_{2})

Fig. 7. Algorithm I

7 Related Work

The structure of algorithms W and I is very close to that of Milner’s algorithms of the same name (Mil78). Apart from the fact that our version of I is purely applicative (hence we carry the substitution and the set of used variables around explicitly), the main difference is that we also have to maintain a set of constraints Γ. In fact, this is the only real difference to Milner’s algorithms.

Probably the first combination of ML-style polymorphism and parametric overloading (as opposed to finite overloading as in Hope (BMS80)) was presented by Kaes (Kae88). His language is in fact very close to our Mini-Haskell, except that he does not introduce classes explicitly. More importantly, he does not use contexts to record information about type variables but tags type variables directly.

The original version of type classes as presented by Wadler and Blott (WB89) was significantly more powerful than what went into Haskell, the reason being that the original system was undecidable, as shown later by Volpano and Smith (VS91). The relationship to Haskell proper is discussed in Section 2.

Nipkow and Snelting (NS91) realized that type inference for type classes can be formulated as an extension of ordinary ML-style type inference with order-sorted unification, i.e. simply by changing the algebra of types and the corresponding unification algorithm. Although this was an interesting theoretical insight, it only lead to a simple algorithm for a restricted version of Haskell where each type variable is constrained by exactly one class. In addition it was not possible to identify ambiguous typings like Σ, [α:C], E ⊢ e : int because there was no notion of contexts and type variables were tagged with their sort. Both problems have been eliminated in the present paper.

An interesting extension of Haskell using the notion of “qualified types” was designed and implemented by Mark Jones (Jon92b). The main difference is that he allows arbitrary predicates P (τ_{1}, …, τ_{n}) over types as opposed to our membership constraints α : S. On the other hand he does not solve constraints of the form τ : S to obtain atomic constraints of the form α : S′ as is done in our function constrain. Instead he accumulates the unsolved constraints.

Independently of our own work Chen, Hudak and Odersky (CHO92) developed an extension of type classes using similar techniques and arriving at a similar type reconstruction algorithm. Since their type system is more general, they use different and more involved formalisms, in particular for unification. In contrast, we reduce unification to its essence by splitting it into standard unification plus constraint solving. This enables us to give a sufficient and necessary criterion for unitary unification, which is required for principal types. As discussed in Section 4, the restrictions in Haskell guarantee unitary unification.

Kaes (Kae92) presents an extension of Hindley/Milner polymorphism with overloading, subtypes and recursive types. Due to the overall complexity of the resulting system, the simplicity of the pure system for overloading is lost.

The pragmatics of implementing type classes are discussed by Peterson and Jones (PJ83). In particular they give hints on how to implement a truly imperative version of algorithm I using mutable variables. This is of significant importance because a naïve functional implementation of algorithm I, in particular one representing substitutions as association lists, performs quite poorly.

8 Ambiguity

We would like to conclude this paper with a discussion of the ambiguity problem which affects most type systems with overloading. It is caused by the fact that although a program may have a unique type, its semantics is not well-defined. According to our rules, the program

class α : C where f : α → int; class α : D where c : α; (f c)

has type int in any context containing an assumption α : {C, D}. Yet the program has no semantics because there are no instances of f and c at all. If there were multiple instances of both C and D, it would be impossible to determine which one to use in the expression (f c).

Motivated by such examples, a typing Σ, Γ, E ⊢ e : σ is usually defined to be ambiguous if there is a type variable in Γ which does not occur free in σ or E.

Ideally one would like to have that every well-typed expression has a well-defined semantics. However, ambiguous terms may have more than one semantics, as the above example suggests. Fortunately, Blott (Blo92) and Jones (Jon92a) have shown that in type systems closely related to the one studied in this paper, the semantics of unambiguous terms is indeed well-defined.

As we have not provided a semantics for our language, we have not introduced ambiguity formally. Nevertheless there is one place in our inference system where we anticipate a particular treatment of ambiguity. In rule ∀I, the proviso α ∈ FV(σ) is intended to propagate ambiguity problems: with this restriction, the expression

Type Reconstruction for Type Classes 23

let x = (f c) in 5 (preceded by classes C and D as declared above) has type int only in a context containing an assumption α : {C, D}. If the proviso is dropped, the expression also has type int in the empty context, thus disguising the local ambiguity. The reason is that x can be given the ambiguous type ∀α:{C, D}.int, but since x does not occur in 5, this does not matter. Although in a lazy language x need not be evaluated and hence the semantics of the whole let is indeed unambiguous, we would argue that for pragmatic reasons it is advisable to flag ambiguities whenever they arise.

From this discussion it is obvious that a semantics and a coherence proof for the type system w.r.t. a semantics are urgently needed.

Acknowledgements. The authors wish to thank the anonymous referees for their critical reading and their helpful comments.

References

Stephen Blott. An approach to overloading with polymorphism. PhD thesis, Dept. of

Computing Science, University of Glasgow, 1992. Rod Burstall, Dave MacQueen, and Don Sannella. Hope: an experimental applicative

language. In Proc. 1980 LISP Conference, pages 136–143, 1980. Dominique Clément, Joëlle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple

applicative language: Mini-ML. In Proc. ACM Conf. Lisp and Functional Programming, pages 13–27, 1986.

Kung Chen, Paul Hudak, and Martin Odersky. Parametric type classes. In Proc. ACM

Conf. on LISP and Functional Programming, pages 170–181. ACM Press, June 1992. Luis Damas and Robin Milner. Principal type schemes for functional programs. In Proc.

9th ACM Symp. Principles of Programming Languages, pages 207–212, 1982. Paul Hudak, Simon Peyton Jones, and Philip Wadler. Report on the programming lan-

guage Haskell: A non-strict, purely functional language. ACM SIGPLAN Notices, 27(5), May 1992. Version 1.2.

Mark P. Jones. Qualified types: Theory and practice. D.Phil. Thesis, Programming

Research Group, Oxford University Computing Laboratory, July 1992. Mark P. Jones. A theory of qualified types. In Bernd Krieg-Brückner, editor, Proc.

European Symposium on Programming, pages 287–306. LNCS 582, 1992. Stefan Kaes. Parametric overloading in polymorphic programming languages. In Proc.

2nd European Symposium on Programming, pages 131–144. LNCS 300, 1988. Stefan Kaes. Type inference in the presence of overloading, subtyping and recursive types.

In Proc. ACM Conf. LISP and Functional Programming, pages 193–204. ACM Press, June 1992.

Robin Milner. A theory of type polymorphism in programming. J. Comp. Sys. Sci.,

17:348–375, 1978. Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT

Press, 1990. Tobias Nipkow and Christian Prehofer. Type checking type classes. In Proc. 20th ACM

Symp. Principles of Programming Languages, pages 409–418. ACM Press, 1993. Tobias Nipkow and Gregor Snelting. Type classes and overloading resolution via order-

sorted unification. In Proc. 5th ACM Conf. Functional Programming Languages and Computer Architecture, pages 1–14. LNCS 523, 1991.

John Peterson and Mark Jones. Implementing type classes. In Proc. SIGPLAN ’93 Symp. Programming Language Design and Implementation, pages 227–236. ACM Press, 1983.

24 Tobias Nipkow and Christian Prehofer

Dennis M. Volpano and Geoffrey S. Smith. On the complexity of ML typability with overloading. In Proc. 5th ACM Conf. Functional Programming Languages and Computer Architecture, pages 15–28. LNCS 523, 1991.

Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In Proc. 16th ACM Symp. Principles of Programming Languages, pages 60–76, 1989.