Coherence for qualified types

Mark P. Jones^{∗}

All translations are equal, but some translations are more equal than others.

Misquoted, with apologies to George Orwell, from Translation Farm, 1945.

Research Report YALEU/DCS/RR-989, September 1993

Abstract

The meaning of programs in a language with implicit overloading can be described by translating them into a second language that makes the use of overloading explicit. A single program may have many distinct translations and it is important to show that any two translations are semantically equivalent to ensure that the meaning of the original program is well-defined. This property is commonly known as coherence. This paper deals with an implicitly typed language that includes support for parametric polymorphism and overloading based on a system of qualified types. Typical applications include Haskell type classes, extensible records and subtyping. In the general case, it is possible to find examples for which the coherence property does not hold. Extending the development of a type inference algorithm for this language to include the calculation of translations, we give a simple syntactic condition on the principal type scheme of a term that is sufficient to guarantee coherence for a large class of programs. One of the most interesting aspects of this work is the use of terms in the target language to provide a semantic interpretation for the ordering relation between types that is used to establish the existence of principal types. On a practical level, our results explain the importance of unambiguous type schemes in Haskell.

Introduction

Consider the task of evaluating an expression of the form x + y + z. Depending on the way that it is parsed, this expression might be treated as either (x +y)+z or x +(y+z). Fortunately, it does not matter which of these we choose since the fact that (+) is associative is both necessary and sufficient to guarantee that they are actually equivalent. We are therefore free to choose whichever is more convenient, retaining the same well-defined semantics in either case. This paper deals with a similar problem that occurs with programs in OML, a simple implicitly typed language with overloading. The meaning of such programs can be described by translating them into OP, an extended language which uses additional constructs to make the use of overloading explicit. However, different typing derivations for a given OML program can lead to distinct translations and, just as in the example above, it is important to show that any two translations have the same meaning. In the terminology of [2], we need to show that ‘the meaning of a term does not depend on the way that it was type checked’, a property that they refer to as coherence. The type system of OML is an extended form of the ML type system that includes support for qualified types [7]. The central idea is to allow the use of type expressions of the form π ⇒ σ to represent all those instances of σ which satisfy π, a predicate on types. Applications of qualified types include Haskell type classes, extensible records and subtyping. In previous work, we have described how the standard type inference algorithm for ML can be extended to calculate principal type schemes for terms in OML. In this paper, we extend these results to show how an arbitrary translation of an OML term can be written in terms of a particular principal translation determined by the type inference algorithm. Exploiting this relationship, we give conditions that can be used to guarantee that all of the translations for a given term are equivalent. The remaining sections of this paper are as follows. Section 1 outlines the use of qualified types and defines the languages OML and OP and the translation between them that is used in this paper. A simple example in Section 2 shows that a single term may have semantically distinct translations and hence that we cannot hope to establish a general coherence result for arbitrary terms. Instead, we must look for conditions which can be used to ensure coherence for as wide a class of programs as possible. As a first step, we need to specify exactly what it means for two translations to be equivalent. This is dealt with in Section 3 using a syntactic definition of (typed) equality between OP terms. One of the most important tools in the development of a type inference algorithm is the ordering relation (≤) between type schemes. Indeed, without a notion of ordering, it would not even be possible to talk about principal or most general type schemes! Motivated by this, Section 4 gives a semantic interpretation for (≤) using OP terms which we call conversions. Sections 5 and 6 extend the development of type inference for qualified types in [7] to include the calculation of translations. In particular, we show that any translation of an OML term can be written in the form C (λw.E′)v where C is a conversion of a particular kind, E′ is the principal translation and v, w are fixed collections of variables. Hence the task of establishing the equivalence of two arbitrary translations reduces to showing the equivalence of two terms of the form C_{1}(λw.E′)v and C_{2}(λw.E′)v where C_{1} and C_{2} are conversions of a particular type. One obvious way to approach this problem is to show that that these conversions are equivalent. Exploring this possibility in Section 7, we obtain sufficient conditions for the equivalence of a pair of conversions of a particular type and hence for an arbitrary pair of translations. In particular, we show that the meaning of any term with an unambiguous principal type scheme (a simple syntactic condition) is well-defined, generalizing an earlier result in [1] for the special case of a system of type classes. Section 8 concludes with a description of related work and some ideas for further research. Further details of the work described in this paper together with full proofs for the results presented here may be found in [8].

∗This paper summarizes work carried out while the author was a member of the Programming Research Group, Oxford, supported by a SERC studentship [8]. Current address: Yale University, Department of Computer Science, P.O. Box 208285, New Haven, Connecticut 06520-8285, USA. Electronic mail jones-mark@cs.yale.edu.

Supported in part by a grant from DARPA, contract number N00014-91-J-4043.

1 Basic definitions

This section outlines the principal features of a system of qualified types and of OML in particular. We refer the reader to either [7] or [8] for further details.

1.1 Predicates and evidence

A language of predicates on types is an essential component of any system of qualified types. For example, predicates of the form Eq τ that hold precisely when there is an equality operator defined for values of type τ are often used in work with type classes. Predicates are used to identify particular sets of types, so a term with type ∀t.π(t) ⇒ f (t) can be treated as having any of the types in the set

{ f (τ) | τ is a type such that π(τ) holds }.

An object with a qualified type can only be used if we provide evidence that the predicates involved are satisfied. A simple choice for a predicate of the form Eq τ might be an equality function for values of type τ, but the exact form of evidence used in any particular application does not affect the work described here and we think of it purely as a semantic interpretation of predicates. Evidence values are written using a language of evidence expressions that includes a set of evidence variables v. The set of evidence variables in an expression e is denoted EV (e). The final component in a system of predicates is an entailment relation ⊢⊢ which may vary from one application to another. An expression of the form P ⊢⊢ e :π indicates that we can obtain evidence e for the predicate π from the predicate assignment P, a list of pairs of the form v : π′. For example, v : Eq τ ⊢⊢ eqList v : Eq [τ] might indicate that, if v is bound to an equality test for values of type τ, then the expression eqList v gives an equality test for lists of such values. Figure 1 lists the properties which the entailment relation is expected to satisfy. These rules make use of some simple abbreviations, blurring the distinction between sequences

(id)  v :P ⊢⊢ v :P
(term)  v :P ⊢⊢ ∅
(fst)  v :P, w :Q ⊢⊢ v :P
(snd)  v :P, w :Q ⊢⊢ w :Q

(univ)

v :P ⊢⊢ e :Q  v :P ⊢⊢ e′:R
v :P ⊢⊢ e :Q, e′:R

(trans)

v :P ⊢⊢ e :Q  v′:Q ⊢⊢ e′:R
v :P ⊢⊢ [e/v′]e′:R

(close)

v :P ⊢⊢ e :Q
v :SP ⊢⊢ e :SQ
(evars)  v :P ⊢⊢ e :Q ; EV (e) ⊆ v

Figure 1: Predicate entailment with evidence.

and individual objects. For example, if P = π_{1}, …, π_{n} is a list of predicates and v = v_{1}, …, v_{n} is a list of evidence variables then we write v : P for the predicate assignment v_{1} :π_{1}, …, v_{n} :π_{n}. The empty sequence is written ∅ and the concatenation of two sequences P and Q is written P, Q. The letter S in rule (close) denotes an arbitrary substitution of types for type variables.

1.2 Terms and types

This paper deals with the relationship between two implicitly typed λ-calculi with support for qualified types. The first of these is an extension of ML and will be referred to as OML – an abbreviation of ‘Overloaded ML’. As in [4], the terms of OML are those of simple untyped λ-calculus with the addition of a let construct to enable the definition and use of polymorphic, overloaded terms:

E ::= x  variable
| EF  application
| λx.E  abstraction
| let x = E in F local definition

Following the distinction between types and type schemes in ML, the types of terms in OML are given by:

τ ::= t  type variables
| τ → τ function types
ρ ::= P ⇒ τ qualified types
σ ::= ∀T .ρ type schemes

where t denotes a type variable, P a finite sequence of predicates and T a finite set of type variables. The → and ⇒ symbols are treated as right associative infix binary operators with → binding more tightly than ⇒. Additional type constructors such as those for lists, pairs and record types will be used as required. The set of type variables appearing (free) in an expression X is denoted TV (X ) and is defined in the obvious way. In particular, TV (∀T .ρ) = TV (ρ) \ T . The second language will be referred to as OP – an abbreviation for ‘Overloaded Polymorphic λ-calculus’. The terms of OP are the same as those for OML with additional constructs for evidence abstraction and application:

E ::= …
| Ee  evidence application
| λv.E evidence abstraction

As before, it is convenient to use some abbreviations for dealing with sequences of evidence abstractions or applications. For example, if v = v_{1}, …, v_{n} and e = e_{1}, …, e_{n}, then we write λv.E and Ee as abbreviations for λv_{1}…. λv_{n}.E and (… (Ee_{1}) …)e_{n} respectively. The language of types in OP is given by the grammar:

σ ::= t  type variables
| σ → σ function types
| ∀t.σ polymorphic types
| π ⇒ σ qualified types

An OML qualified type (π_{1}, …, π_{n}) ⇒ τ can be identified with the OP type π_{1} ⇒ … ⇒ π_{n} ⇒ τ. OP types are considerably more flexible than those of OML since there is no distinction between simple types and type schemes. In particular, OP allows functions with polymorphic and/or overloaded values as their arguments. Strictly speaking, there is no need to include the let construct in OP since we can code a polymorphic local definition let x = E in F as (λx.F )E. The most important benefit of including let is that it makes it easier to treat OML as a (proper) sublanguage of OP.

1.3 Typing rules

Reasons of space prevent us from including the full typing rules for OML and OP. Instead, we present both systems using a hybrid with judgements P | A ⊢ E ⇝ E′ : σ where E is an OML term and E′ is a corresponding OP term referred to as a translation of E. The first component P in these judgements is a predicate assignment, while A is a type assignment, i.e. a (finite) set of pairs of the form x : σ in which no term variable x appears more than once. Type assignments can be interpreted as finite functions mapping term variables to types. We write A(x) for the type assigned to x by A, A_{x} for the assignment obtained by removing x from the domain of A, and A, x :σ for the assignment which is the same as A except that it also maps x to σ. The typing rules are given in Figure 2. Note the use of the symbols τ, ρ and σ to restrict the application of certain rules to particular kinds of type expression, given by the grammar for OML types above. With these restrictions in mind, and ignoring the translation component of each judgement, Figure 2 gives the typing rules for OML. On the other hand, if we disregard the OML term in each judgement and ignore the distinction between the three classes of type in OML, we obtain the typing rules for OP. The significance of this hybrid formulation is that it enables us to deal simultaneously with OML and OP terms whose typing derivations have the same structure. The relationship between OML terms and translations given by the rules in Figure 2 is not functional – there is no unicity of type, and different derivations of the same typing in OML can result in distinct translations. On the other hand, we can always recover the original OML term corresponding to a given translation using the function:

Erase (x)  = x
Erase (EF ) = (Erase E) (Erase F )
⋮
Erase (Ee)  = Erase E
Erase (λv.E) = Erase E

1.4 Ordering type schemes

Each OML typing includes a predicate set that restricts its use to environments in which the given predicates hold. As such, it is convenient to work with a slightly more general notion of type scheme which also contains constraints on the environments in which it may be used.

Definition 1 A constrained type scheme is an expression of the form (P |σ) where P is a set of predicates and σ is a type scheme.

Any type scheme σ may be identified with a constrained type scheme of the form (∅ | σ). Note that there is no need to use constrained type schemes in OP since we can treat (P |σ) as an abbreviation for the OP type P ⇒ σ We will write (P′ | σ′) ≤ (P | σ) to indicate that (P | σ) is more general than (P′ | σ′). A suitable ordering relation, extending the ordering between type schemes in Damas and Milner’s treatment of type inference for ML, was suggested in [7] and can be characterized as follows:

Definition 2 Suppose that σ = ∀α_{i}.Q ⇒ ν, σ′ = ∀β_{j} .Q′ ⇒ ν′ and that none of the variables β_{j} appears free in σ, P or P′. Then (P′ | σ′) ≤ (P | σ) if and only if there are types τ_{i} such that ν′ = [τ_{i}/α_{i}]ν and P′, Q′ ⊢⊢ P, [τ_{i}/α_{i}]Q.

2 The coherence problem

To justify the use of translations as a semantics for OML, we need to show that:

• For each OML term E there is an OP term E′ that is a translation of E.

• Any translation of a well-typed OML term is welltyped in OP.

• The mapping from terms to translations must be welldefined. In other words, we must show that any translations E_{1} and E_{2} of an OML term E given by derivations P | A ⊢ E ⇝ E_{1} : σ and P | A ⊢ E ⇝ E_{2} : σ are, in some precise sense, equivalent.

The first two properties follow immediately from the typing rules given above, but it is relatively simple to show that the third property does not hold in general. For example, Haskell [6] provides two standard functions:

read : ∀a.Text a ⇒ String → a
show : ∀a.Text a ⇒ a → String

for converting between values and their printable representations as strings. Now suppose that the type assumption A containing these functions and that implementations have been provided for both integers and booleans, in a predicate assignment P = {u : Text Int, v : Text Bool}. Now

(var)  \begin{matrix}(x : σ) ∈ A \\ P |A ⊢ x ⇝ x : σ \end{matrix}

(→E)

P |A ⊢ E ⇝ E′ : τ′ → τ  P |A ⊢ F ⇝ F′ : τ′

P |A ⊢ EF ⇝ E′F′ : τ

(→I )

P |A_{x} , x :τ′ ⊢ E ⇝ E′ : τ

P |A ⊢ λx.E ⇝ λx.E′ : τ′ → τ

(⇒E)

P |A ⊢ E ⇝ E′ : π ⇒ ρ  P ⊢⊢ e :π

P |A ⊢ E ⇝ E′e : ρ

(⇒I )

P, v :π, P′ |A ⊢ E ⇝ E′ : ρ

P, P′ |A ⊢ E ⇝ λv.E′ : π ⇒ ρ

(∀E)

P |A ⊢ E ⇝ E′ : ∀t.σ

P |A ⊢ E ⇝ E′ : [τ/t]σ

(∀I )

P |A ⊢ E ⇝ E′ : σ

P |A ⊢ E ⇝ E′ : ∀t.σ

t ∉ TV (A) ∧ t ∉ TV (P)

(let)

P |A ⊢ E ⇝ E′ : σ  Q |A_{x} , x :σ ⊢ F ⇝ F′ : τ

P, Q |A ⊢ (let x = E in F ) ⇝ (let x = E′ in F′) : τ

Figure 2: Hybrid typing rules for OML and OP

consider the composition of these two functions read . show converting a string to some type of values, and then back to a string. Instantiating the quantified type variable in the type of read (and hence also that of show) determines the type of intermediate values used and leads to the following derivations with translations that are clearly not equivalent:

P |A ⊢ (read . show) ⇝ (read u . show u) : String → String P |A ⊢ (read . show) ⇝ (read v . show v) : String → String

Clearly, we cannot hope to establish the general coherence result in the third item above; i.e. that all translations of an arbitrary OML term are semantically equivalent. In the rest of this paper we work towards a more modest goal – to identify a collection of OML terms for which the coherence property can be established.

3 Equality of OP terms

Before we can establish sufficient conditions to guarantee coherence, we need to specify formally what it means for two terms (specifically, two translations) to be equivalent. This section gives a syntactic characterization of (typed) equality between OP terms using judgements of the form P | A ⊢ E = F : σ (with the implicit side-condition that both P |A ⊢ E : σ and P |A ⊢ F : σ in OP).

3.1 Uniqueness of evidence

The use of predicate assignments in the definition of equality enables us to capture the ‘uniqueness of evidence’; to be precise, we require that any evidence values e and f constructed by entailments P ⊢⊢ e : Q and P ⊢⊢ f : Q are semantically equivalent, in which case we write P ⊢ e = f : Q. Since we only intend such judgements to be meaningful when both entailments hold, the definition of equality on evidence expressions can be described directly using:

P ⊢ e = f :Q ⇔ P ⊢⊢ e :Q ∧ P ⊢⊢ f :Q.

This condition is essential if any degree of coherence is to be obtained. Without it, for example, it would be possible to have semantically distinct versions of an overloaded operator that cannot be distinguished either by name or by type.

3.2 Reduction of OP terms

We will base the definition of equality on OP terms on a notion of (typed) reductions using judgements of the form P | A ⊢ E > F : σ with the implicit side condition that P |A ⊢ E : σ in OP. There is no need to include P |A ⊢ F : σ as a second side condition since this follows from the first by the subject reduction theorem – ‘reduction preserves typing’. We split the definition of reduction into three parts, the first of which appears in Figure 3. This includes the familiar definitions of β-conversion for evidence and term abstractions and let expressions and a rule of η-conversion for evidence abstractions. An unfortunate consequence of this approach is that the axiom (β) is not sound in models of the λ-calculus with call-by-value semantics and hence our results can only be applied to languages with lazy or call-by-name semantics. This limitation stems more from the difficulty of axiomatizing call-by-value equality than from anything implicit in our particular application and will be discussed in Section 8. A second collection of rules in Figure 4 is used to describe the renaming of bound variables in λ-abstractions, evidence

(β)  P |A ⊢ (λx.E)F > [F /x]E : σ
(β_{e})  P |A ⊢ (λv.E)e > [e/v]E : σ
(β-let) P |A ⊢ (let x = E in F ) > [E/x]F : σ

(η_{e})

v ∉ EV (E)
P |A ⊢ (λv.Ev) > E : σ

Figure 3: Rules of computation

(α)

x ∉ FV (λy.E)
P |A ⊢ (λy.E) > (λx.[x/y]E) : σ

(α_{e})

v ∉ EV (λw.E)
P |A ⊢ (λw.E) > (λv.[v/w]E) : σ

(α-let)

x ∉ FV (λy.E)

P |A ⊢ (let y = E in F ) > (let x = E in [x/y]F ) : σ Figure 4: Rules for renaming bound variables

\begin{matrix}(x :σ) ∈ A \\ P |A ⊢ x > x : σ \end{matrix}

P |A ⊢ E > E′ : σ′ → σ  P |A ⊢ F > F′ : σ′

P |A ⊢ EF > E′F′ : σ

P |A_{x} , x :σ′ ⊢ E > E′ : σ
P |A ⊢ λx.E > λx.E′ : σ′ → σ
P |A ⊢ E > E′ : π ⇒ σ  P ⊢ e = e′:π

P |A ⊢ Ee = E′e′ : σ

P, v :π, P′ |A ⊢ E > E′ : σ
P, P′ |A ⊢ λv.E > λv.E′ : π ⇒ σ

P |A ⊢ E > E′ : ∀t.σ P |A ⊢ E > E′ : [τ/t]σ

P |A ⊢ E > E′ : σ  t ∉ TV (A) ∪ TV (P)

P |A ⊢ E > E′ : ∀t.σ

P |A ⊢ E > E′ : σ  P |A_{x} , x :σ ⊢ F > F′ : τ

P |A ⊢ (let x = E in F ) > (let x = E′ in F′) : τ Figure 5: Structural laws for reductions between terms. abstractions and let expressions. Any such renaming is permitted so long as we avoid clashes with free variables. The final group of structural rules in Figure 5 is closely modeled on the typing rules for OP and can be used to describe the reduction of subterms within a given term.

3.3 Equalities between terms

The rules in Figure 6 define the equality relation for terms in OP as the transitive, symmetric closure of the reduction relation described above. The first two rules ensure that

P |A ⊢ E = F : σ

P |A ⊢ F = E : σ

P |A ⊢ E = E′ : σ  P |A ⊢ E′ = E′′ : σ

P |A ⊢ E = E′′ : σ

P |A ⊢ E > F : σ

P |A ⊢ E = F : σ

Figure 6: Definition of equality between terms.

equality is an equivalence relation. There is no need to include reflexivity here since this is a direct consequence of the structural rules in Figure 5. The last rule shows how reductions give rise to equalities. In practice, many of the rules used in the definition of equality above will be used implicitly in the proof of equalities between terms. The following example uses all three of the rules in Figure 6 (as well as subject reduction to justify the fact that the intermediate steps are well-typed):

P |A ⊢ let x = E in [F /x]F′

= [E/x]([F /x]F′)  (β-let)
= [[E/x]F /x]F′
= let x = [E/x]F in F′ : σ (β-let)

The context in which this equality is established (given by P, A and σ) does not play a part in the calculation. Examples like this are quite common and we will often avoid mentioning the context altogether in such situations, writing ⊢ E = F to indicate that P | A ⊢ E = F : σ for any choice of P, A and σ for which the required side conditions hold. The above property of let expressions may seem unfamiliar, and it is worth illustrating why it is useful in our work. Suppose that ∅ ⊢⊢ e : Eq Int and that (==) denotes an equality function of type ∀a.Eq a ⇒ a → a → Bool. Now consider the OML term:

let f = (λx.λy.x == y) in f 2 3.

Since the function f is only ever applied to integer values, it is sufficient to treat f as having type Int → Int → Bool, with translation:

let f = (λx.λy.(==) e x y) in f 2 3 However, the type inference algorithm calculates the type of f as ∀a.Eq a ⇒ a → a → Bool and results in a translation of the form:

let f = (λv.λx.λy.(==) v x y) in f e 2 3.

The following calculation shows that these translations are equal and hence that it is possible to eliminate the evidence abstraction used in the second case. The second step is justified by the result above.

⊢ let f = (λv.λx.λy.(==) v x y) in f e 2 3 =

let f = (λv.λx.λy.(==) v x y)
in [f e/f ](f 2 3)
= let f = [λv.λx.λy.(==) v x y/f ](f e) in f 2 3
= let f = (λv.λx.λy.(==) v x y) e in f 2 3
= let f = (λx.λy.(==) e x y) in f 2 3

As in the last step here, many equalities between terms can be obtained by replacing one subterm with an equivalent term. These steps are justified by the structural rules in Figure 5 and are often used implicitly in proofs.

4 Conversions

One of the most important tools in the treatment of type inference is the ordering relation ≤ used to describe when one (constrained) type scheme is more general than another. For example, assuming that ∅ ⊢⊢ e :Eq Int, the ordering:

(∀a.Eq a ⇒ a → a → Bool) ≥ (Int → Int → Bool)

might be used to justify replacing an integer equality function, say primEqInt :: Int →Int →Bool with a generic equality function with the more general type ∀a.Eq a ⇒a →a → Bool as in the previous section. This breaks down in OP due to the presence of evidence abstraction and application: simply replacing primEqInt with (==) in primEqInt 2 3 does not even give a well-typed expression! The correct approach is to replace primEqInt by (==) e. More generally, we will deal with examples like this using OP terms as an interpretation of the ordering between type schemes. For each σ ≥ σ′ we identify a particular collection of terms that we call conversions from σ to σ′. Each such conversion is a closed OP term C : σ → σ′ and hence any term of type σ can be treated as having type σ′ by applying the conversion C to it. One possible conversion for the example above is:

(λx.xe) : (∀a.Eq a ⇒a →a →Bool)→(Int →Int →Bool).

Note that the type of this conversion (as in the general case) cannot be expressed as an OML type scheme since it uses the richer structure of OP types. For the purposes of type inference it would be sufficient to take any term C of type σ → σ′ as a conversion for σ′ ≤ σ but this is clearly inadequate if we are also concerned with the semantics of the terms involved; we can only replace E with CE if we can guarantee that these terms are equivalent, except perhaps in their use of evidence abstraction and application. More formally, we need to ensure that ⊢ Erase (CE) = Erase E for all OP terms E (or at least, all those occurring as translations of OML terms). Since Erase (CE) = (Erase C ) (Erase E), the obvious way to ensure that this condition holds is to require that Erase C is equivalent to the identity term id = λx.x. These ideas extend to conversions between arbitrary constrained type schemes. It is tempting to define the set of conversions from (P′ | σ′) to (P | σ) as the set of all closed OP terms C : (P | σ) → (P′ | σ′) for which Erase C is equivalent to id. In practice it is more convenient to choose a more conservative definition that gives more information about the structure of conversions:

Definition 3 Suppose σ = (∀α_{i}.Q ⇒ τ), σ′ = (∀β_{j} .Q′ ⇒ τ′) and none of β_{j} appear free in σ, P or P′. A conversion C from (P |σ) to (P′ |σ′), written C :(P |σ) ≥ (P′ |σ′), is a closed OP term of type (P |σ) → (P′ |σ′) such that:

• Erase C = id,

• v :P′, w :Q′ ⊢⊢ e :P, f :[τ_{i}/α_{i}]Q,

• τ′ = [τ_{i}/α_{i}]τ,

• and ⊢ C = λx.λv.λw.xef

for some types τ_{i}, evidence variables v and evidence e.

It is straightforward to verify that the term λx.λv.λw.xef mentioned in this definition is a conversion from (P | σ) to (P′ |σ′) and it follows that any equivalent OP term with the same type will also be a conversion of the same kind. On the other hand, we cannot assume that all such conversions will be equivalent to this particular term since there may be more than one choice for the types τ_{i} and hence for the evidence expressions f in the definition above. It is immediate from the definitions above that (P | σ) ≥ (P′ | σ′) if and only if there is a conversion C : (P | σ) ≥ (P′ | σ′) (this may require renaming the bound variables of σ′ to apply the definition of conversions). As a result, all of the properties of the (≤) ordering described in [7] can be extended to analogous results for conversions. For example, the following proposition shows that reflexivity of (≤) corresponds to the identity conversion while transitivity of (≤) corresponds to composition of conversions.

Proposition 1 For any (P | σ) there is a conversion id : (P | σ) ≥ (P | σ). Furthermore, if C : (P | σ) ≥ (P′ | σ′) and C′: (P′ | σ′) ≥ (P′′ | σ′′), then (C′ ∘ C ) : (P | σ) ≥ (P′′ | σ′′) where (C′ ∘ C ) ≡ λx.C′(Cx).

From a categorical perspective, this proposition can be used to show that there is a category whose objects are type schemes and whose arrows are (equivalence classes of) conversions. The only additional properties needed to justify this are that the composition of equivalence classes is welldefined and associative, both of which are easily verified. The ordering relation (≤) is preserved by substitutions and the corresponding result for conversions is:

Proposition 2 If C :(P |σ) ≥ (P′ |σ′) and S is a substitution of types for type variables, then C :S(P |σ) ≥ S(P′ |σ′).

The ordering between type schemes extends to an ordering between (constrained) type assignments, writing (P | A) ≥ (P′ | A′) to indicate that (P | A(x)) ≥ (P′ | A′(x)) for each x ∈ dom A = dom A′. It is useful to extend the definition of conversions to orderings between type assignments. For the purposes of this work, it is sufficient to consider only the case of orderings of the form A ≥ A′ and A ≥ (P | A′), the first of which is just a special case of the second with P = ∅. One simple approach would be to define a conversion for an ordering A ≥ (P | A′) as a function that gives a conversion from A(x) to (P | A′(x)) for each x ∈ dom A. However, whereas we might use a conversion C :σ ≥ (P |σ′) to treat a term of type σ as having type σ′, we will typically use a conversion between type assignments to simultaneously replace each occurrence of a variables mentioned in the type assignment with an appropriate new term. From this perspective it seems more sensible to think of a conversion between type assignments as a term substitution. Furthermore, the translations of a term are calculated with respect to a particular predicate assignment (the first component in a derivation v : P | A ⊢ E ⇝ E′ : σ) and may involve the evidence variables in the domain of that assignment. It is therefore necessary to specify these variables explicitly as part of the type of the conversion.

Definition 4 A conversion C from a type assignment A to a constrained type assignment (v : P | A′) with the same domain, written C : A ≥ (v : P | A′), is a substitution such that:

• dom C ⊆ dom A = dom A′. In particular, if x ∉ dom A, then Cx ≡ x.

• (λx.λv.Cx):A(x) ≥ (P |A′(x)) for each x ∈ dom A.

Note that the expression Cx in this definition denotes an application of a (meta-language) substitution to a particular variable; C is not an OP term. Continuing with the previous example and assuming that ∅ ⊢⊢ e : Eq Int, one possible conversion for the type assignment ordering

{(==) : Int → Int → Bool} ≤

{(==) : ∀a.Eq a ⇒ a → a → Bool}

would be the substitution that maps (==) to (==) e and fixes every other variable. To see how this might be used, consider an OP term in which the (==) has been treated as having type Int → Int → Bool. If we replace this with a generic equality function with the more general type, then we need to include the evidence e for Eq Int with every use of (==). This is precisely the effect obtained by applying the conversion to the original term.

5 Syntax-directed translation

The next two sections follow the development of [7] to describe the relationship between an arbitrary translation of an OML term and a particular translation determined by the type inference algorithm. For reasons of space, we will only sketch the details here and refer the reader to [8] for further explanation and motivation. The rules in Figure 2 are not well-suited to use in a type inference algorithm since it is not always clear which (if any) should be used to obtain an optimal (i.e. principal) typing for a given term. Our solution is to work with the set of typing rules in Figure 7 in which the structure of a derivation P |A ⊢^{s} E ⇝ E′ : τ is uniquely determined by the syntactic structure of the OML term E and to show that this syntaxdirected approach is equivalent to the original type system.

(var)^{s}

(x :(∀α_{i}.Q ⇒ ν)) ∈ A  P ⊢⊢ e :[τ_{i}/α_{i}]Q

P |A ⊢^{s} x ⇝ xe : [τ_{i}/α_{i}]ν

(→E)^{s}

P |A ⊢^{s} E ⇝ E′ : τ′ → τ  P |A ⊢^{s} F ⇝ F′ : τ′

P |A ⊢^{s} EF ⇝ E′F′ : τ

(→I )^{s}

P |A_{x} , x :τ′ ⊢^{s} E ⇝ E′ : τ

P |A ⊢^{s} λx.E ⇝ λx.E′ : τ′ → τ

(let)^{s}

v′:P′ |A ⊢^{s} E ⇝ E′ : τ′  P |A_{x} , x :σ′ ⊢^{s} F ⇝ F′ : τ  σ′ = Gen(A, P′ ⇒ τ′)

P |A ⊢^{s} (let x = E in F ) ⇝ (let x = λv′.E′ in F′) : τ

Figure 7: Syntax-directed typing rules with translation

Note that the OP translation for a given OML term need not be uniquely determined since there may be distinct choices for the evidence values e introduced in (var)^{s}. This, of course, is the source of the incoherence in the translation semantics of OML. A simple proof by induction establishes the soundness of the syntax-directed rules with respect to those in Figure 2.

Theorem 1 If P |A⊢^{s} E ⇝E′:τ, then P |A⊢E ⇝E′:τ.

The reverse process, to establish a form of completeness property by showing that every translation and typing obtained using the general rules in Figure 2 can, in some sense, be described by a syntax-directed derivation is less obvious. For example, if P | A ⊢ E ⇝ F : σ, then it will not in general be possible to derive the same typing in the syntaxdirected system because σ is a type scheme, not a simple type. However, for any v′: P′ | A ⊢^{s} E ⇝ F′ : τ, Theorem 1 shows that v′ : P′ | A ⊢ E ⇝ F′ : τ, and the most general typing that can be obtained from this using (⇒I ) and (∀I ) is ∅|A ⊢ E ⇝ λv′.F′ : Gen(A, P′ ⇒ τ) where:

Gen(A, ρ) = ∀(TV (ρ) \ TV (A)).ρ.

The following theorem shows that it is always possible to find a derivation in this way such that the inferred type scheme Gen(A, P′ ⇒ τ′) is more general than the constrained type scheme (P | σ) in the original derivation and that the translations are related by the corresponding conversion.

Theorem 2 If v : P | A ⊢ E ⇝ E′ : σ, then there is a predicate assignment v′: P′, a type τ′ and a term E′′ such that v′: P′ | A ⊢^{s} E ⇝ E′′ : τ′ and v : P | A ⊢ C (λv′.E′′)v = E′ : σ for some conversion C :Gen(A, P′ ⇒ τ′) ≥ (P |σ).

The proof (by structural induction) is quite complicated and makes use of several results which are of interest in their own right. In particular, if we assume that v :P |A ⊢^{s} E ⇝ E′ : τ, then:

• SP |SA ⊢^{s} E ⇝ E′ : Sτ for any substitution S.

• If Q ⊢⊢ e :P, then Q |A ⊢^{s} E ⇝ [e/v]E′ : τ.

• If C : A′ ≥ (v : P | A), then v : P | A′ ⊢^{s} E ⇝ E′′ : τ and v :P |A′ ⊢ CE′ = E′′ : τ.

Each of these extends earlier results described in [7].

6 Type inference and translation

Figure 8 gives the rules necessary to extend the type inference algorithm from [7] to include the calculation of a translation. These rules can be interpreted as an attribute grammar in which the type assignment A and OML term E in a judgement of the form P | TA ⊢^{W} E ⇝ E′ : τ are inherited attributes, while the predicate assignment P, substitution T , OP translation E′ and type τ are synthesized. Any typing and translation that is obtained using the type inference algorithm can be derived in the syntax-directed system:

Theorem 3 If P |TA⊢^{W} E ⇝E′:τ, then P |TA⊢^{s} E ⇝E′:τ.

Combining this with Theorem 1 we obtain:

Corollary 1 If P |TA⊢^{W} E ⇝E′:τ, then P |TA⊢E ⇝E′:τ.

This is important because it shows that the ‘translation’ E′ of an OML term E produced by the algorithm above is a valid translation of E and, in particular, that it is a welltyped OP term. We will refer to the translations produced by this algorithm as principal translations. The following theorem provides strong motivation for this terminology, showing that every translation obtained using the syntaxdirected system can be expressed in terms of a principal translation.

Theorem 4 If v:P|SA⊢^{s} E⇝E′:τ, then w:Q|TA⊢^{W}E ⇝E′′:ν and there is a substitution R such that τ = Rν, v:P ⊢⊢e:RQ, v :P |SA ⊢ E′ = [e/w]E′′ : τ and S ≈ RT .

The notation S ≈ RT used here means that Sα = RT α for all but a finite number of new type variables α. Theorem 4 can now be used to describe the relationship between arbitrary translations of an OML term and a principal translation:

Corollary 2 Ifv:P|SA⊢E ⇝E′:σ, thenw:Q|TA⊢^{W} E ⇝E′′: ν for some w :Q, T , E′′ and σ and there is a substitution R and a conversion C : RGen(TA, Q ⇒ ν) ≥ (P | σ) such that S ≈ RT and v :P |SA ⊢ C (λw.E′′)v = E′ : σ.

(var)^{W}

(x :∀α_{i}.P ⇒ τ) ∈ A  β_{i} and v new

v :[β_{i}/α_{i}]P |A ⊢^{W} x ⇝ xv : [β_{i}/α_{i}]τ

(→E)^{W}

P |TA ⊢^{W} E ⇝ E′ : τ  Q |T′TA ⊢^{W} F ⇝ F′ : τ′  T′τ ∼^{U} τ′ → α  α new

U (T′P, Q)|UT′TA ⊢^{W} EF ⇝ E′F′ : U α

(→I )^{W}

P |T (A_{x} , x :α) ⊢^{W} E ⇝ E′ : τ  α new

P |TA ⊢^{W} λx.E ⇝ λx.E′ : T α → τ

(let)^{W}

v :P |TA ⊢^{W} E ⇝ E′ : τ  P′ |T′(TA_{x} , x :σ) ⊢^{W} F ⇝ F′ : τ′  σ = Gen(TA, P ⇒ τ)

P′ |T′TA ⊢^{W} (let x = E in F ) ⇝ (let x = λv.E′ in F ) : τ′

Figure 8: Type inference algorithm with translation

7 Coherence results

Corollary 2 is important because it shows that any translation of an OML term E in a particular context can be written in the form C (λw.E′)v where E′ is a principal translation and C is the corresponding conversion. Applied to two arbitrary derivations v : P | A ⊢ E ⇝ E′_{1} : σ and v :P |A ⊢ E ⇝ E′_{2} : σ, it follows that:

v :P |A ⊢ E′_{1} = C_{1}(λw.E′)v : σ and

v :P |A ⊢ E′_{2} = C_{2}(λw.E′)v : σ

where C_{1} and C_{2} are conversions from the principal type scheme to (P | σ). One obvious way to ensure that these translations are equal is to show that C_{1} = C_{2}.

7.1 Equality of conversions

Taking a slightly more general view, suppose that C_{1}, C_{2} are conversions from σ to (P′ |σ′). Without loss of generality, we can assume that σ = (∀α_{i}.Q ⇒ ν) and σ′ = (∀αj^{′} .Q′ ⇒ ν′) where the variables αj^{′} only appear in (Q′ ⇒ ν′). Using the definition of conversions, it follows that there are types τ_{i} such that ν′ = [τ_{i}/α_{i}]ν, C_{1} = λx.λv′.λw′.xef and

v′:P′, w′:Q′ ⊢⊢ e :P, f :[τ_{i}/α_{i}]Q.

Similarly for C_{2} there are types τi^{′} such that ν′ = [τi^{′}/α_{i}]ν, C_{2} = λx.λv′.λw′.xe′f′ and

v′:P′, w′:Q′ ⊢⊢ e′:P, f′:[τi^{′}/α_{i}]Q.

Clearly, it is sufficient to show e = e′ and f = f′ to prove that the these two conversions are equivalent. The first equality is an immediate consequence of the uniqueness of evidence; both e and e′ are evidence for the predicates P under the evidence assignment v′ : P′, w′ : Q′ and so must be equal. The same argument cannot applied to the second equality since the predicates [τ_{i}/α_{i}]Q may not be the same as those in [τi^{′}/α_{i}]Q due to differences between τ_{i} and τi^{′}. Nevertheless, [τ_{i}/α_{i}]ν = ν′ = [τi^{′}/α_{i}]ν, and so τ_{i} = τi^{′} for all α_{i} ∈ TV (ν). Hence if {α_{i}} ∩ TV (Q) ⊆ TV (ν), then the two predicate sets [τ_{i}/α_{i}]Q and [τi^{′}/α_{i}]Q will be equal and f = f′ as required. We will give a special name to type schemes with this property:

Definition 5 A type scheme σ = ∀α_{i}.Q ⇒ ν is unambiguous if {α_{i}} ∩ TV (Q) ⊆ TV (ν).

The same concept of unambiguous type schemes is used in Haskell, motivating our use of the term here. The discussion above shows that all conversions from an unambiguous type scheme are equivalent:

Proposition 3 If C_{1}, C_{2} :σ ≥ (P′ |σ′) are conversions and σ is an unambiguous type scheme then C_{1} = C_{2}.

7.2 Equality of translations

As an immediate corollary, it follows that, if the principal type scheme for a term E is unambiguous, then any two translations of E must be equivalent:

Theorem 5 If v : P | A ⊢ E ⇝ E′_{1} : σ and v : P | A ⊢ E ⇝ E′_{2} : σ and the principal type scheme of E in A is unambiguous, then v :P |A ⊢ E′_{1} = E′_{2} : σ.

This generalizes an earlier result by Blott [1] for the special case of the type system in [13]. Theorem 5 is easy to work with in concrete implementations. The first step in type-checking an OML program is to use the type inference algorithm to calculate its principal type and translation. If the program does not have a principal type, then it cannot be well-typed and will be rejected. If the principal type is not unambiguous, then we cannot guarantee a well-defined semantics and the program must again be rejected. For example, the principal type scheme of the term out (in x) in the example in Section 2 is ∀a.C a ⇒ Int which is ambiguous and hence the program will not be accepted. Note that Theorem 5 gives a condition that is sufficient, but not necessary, to guarantee coherence. For example, any attempt to compare the empty list with itself in Haskell by evaluating [] == [] leads to an error since this term has an ambiguous principal type Eq [a] => Bool, even though it should evaluate to True for any choice of the type variable a. On the other hand, this cannot be established using the definition of equality in Section 3 and we might conjecture that the restriction to terms with unambiguous principal types is both necessary and sufficient to guarantee coherence with respect to that formulation of provable equality.

8 Related work

A number of researchers have investigated the coherence properties of particular type systems using a process of normalization of typing derivations. Examples of this include systems with explicit subtyping [2, 3], a form of implicit subtyping called scaling [12] and an earlier treatment of type classes [1]. The basic idea in each case is to give a collection of reduction rules and prove that they are confluent, that they preserve meaning and that any reduction sequence terminates (and hence, that the rules are strongly normalizing). The confluence property guarantees the existence of a unique normal form and the fact that meaning is preserved by reduction is then sufficient to guarantee coherence. In the work described in this paper, the rules for reductions between terms in Section 3.2 correspond to reductions between derivations and the formulation of the syntax-directed system can be thought of as a means of identifying the ‘normal forms’ of a derivation. From this perspective, Theorem 2 can be interpreted as a proof that the reduction process terminates and that it preserves meaning. However, having shown that the coherence property does not hold in the general case (Section 2) we do not guarantee the existence of unique normal forms or confluence. The most important and novel feature of our work is the use of conversions to give a semantic interpretation to to ordering between constrained type schemes. In effect, a conversion acts as a record of the way in which one derivation is reduced to another. Some of this information is lost because we do not distinguish between conversions that are provably equal but, as we have seen, we retain sufficient detail to establish useful conditions that guarantee coherence. Our use of conversions is closely related to Mitchell’s use of retyping functions in [9] to give minimal typings for a restricted set of terms in a version of the pure polymorphic λ-calculus. The flexibility of the language of types in the systems considered by Mitchell (essentially the same as those in OP but without qualified types) is largely responsible for the difficulty of extending this to a larger collection of terms. These problems have been avoided here by working with the OML type system which is based on a more restricted collection of type schemes. One of the biggest limitations of our work is caused by the decision to include β-reduction in the definition of equality (Section 3.2). As an immediate consequence, the results in this paper cannot be applied to languages with call-by-value semantics. The same problem occurs in other work, including the coherence proof in [1]. One possibility would be to rework these results using an axiomatization of equality for call-by-value semantics such as that given by Riecke [11], but it would clearly be preferable to find a single formulation that can be used for both cases. Another promising approach would be to use ideas from category theory as in [10] for a language with intersection types and subtyping, and in [5] for a system of type classes. One of the main attractions of the categorical approach from the theoretical standpoint is the increased generality resulting from a higher level of abstraction. The main benefit for practical work is likely to be the ‘variable-free’ approach which avoids some of the messy technical details involving free and bound variables. As mentioned in Section 4, our treatment of conversions has a strong categorical flavour and we would hope to be able to extend the techniques developed here to provide a more general treatment of coherence for qualified types.

References

[1] S.M. Blott. An approach to overloading with polymorphism. Ph.D. thesis, Department of computing science, University of Glasgow, July 1991 (draft version).

[2] V. Breazu-Tannen, T. Coquand, C.A. Gunter and A. Scedrov. Inheritance and coercion. In IEEE Symposium on Logic in Computer Science, 1989.

[3] P.-L. Curien and G. Ghelli. Coherence of subsumption. In Fifteenth Colloquium on Trees in Algebra and Programming. Springer Verlag LNCS 431, 1990.

[4] L. Damas and R. Milner. Principal type schemes for functional programs. In 8th Annual ACM Symposium on Principles of Programming languages, 1982.

[5] B. Hilken and D. Rhydeheard. Towards a categorical semantics of type classes. In Theoretical aspects of computer software. Springer Verlag LNCS 526, 1991.

[6] P. Hudak, S.L. Peyton Jones and P. Wadler (eds.). Report on the programming language Haskell, version 1.2. ACM SIGPLAN notices, 27, 5, May 1992.

[7] M.P. Jones. A theory of qualified types. In European symposium on programming. Springer Verlag LNCS 582, 1992.

[8] M.P. Jones. Qualified types: Theory and Practice. D. Phil. Thesis. Programming Research Group, Oxford University Computing Laboratory. July 1992.

[9] J.C. Mitchell, Polymorphic type inference and containment. In G. Huet (ed.), Logical Foundations of Functional Programming, Addison Wesley, 1990.

[10] J.C. Reynolds. The coherence of languages with intersection types. In Theoretical aspects of computer software. Springer Verlag LNCS 526, 1991.

[11] J.G. Riecke. A complete and decidable proof system for call-by-value equalities (preliminary report). In 17th International Colloquium on Automata, Languages and Programming. Springer Verlag LNCS 443, 1990.

[12] S. Thatte. Type inference and implicit scaling. In European Symposium on Programming. Springer Verlag LNCS 432, 1990.

[13] P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad-hoc. In ACM Principles of Programming Languages, 1989.