ML typing, explicit polymorphism and qualified types

Mark P. Jones

Yale University, Department of Computer Science, P.O. Box 208285, New Haven, CT 06520-8285.

                    jones-mark@cs.yale.edu

Abstract. The ML type system was originally introduced as a means of identifying a class of terms in a simple untyped language, often referred to as core-ML, whose evaluation could be guaranteed not to “go wrong”. In subsequent work, the terms of core-ML have also been viewed as a ‘convenient shorthand’ for programs in typed languages. Notable examples include studies of ML polymorphism and investigations of overloading, motivated by the use of type classes in Haskell. In this paper, we show how qualified types, originally developed to study type class overloading, can be used to explore the relationship between core-ML programs and their translations in an explicitly typed language. Viewing these two distinct applications as instances of a single framework has obvious advantages; many of the results that have been established for one can also be applied to the other. We concentrate particularly on the issue of coherence, establishing sufficient conditions to guarantee that all possible translations of a given core-ML term are equivalent. One of the key features of this work is the use of conversions, similar to Mitchell’s retyping functions, to provide an interpretation of the ordering between type schemes in the target language.

1 Introduction

In his seminal paper on polymorphism in programming languages [14], Milner introduced the ML type system as a means of identifying a large class of programs in an untyped λ-calculus whose execution would not “go wrong”. The language that Milner used, with only minor variations, has subsequently become known as core-ML and is widely used in studies of type inference.

A number of authors have shown how particular programming language features can be understood using type inference to guide a translation from core-ML into some suitably extended language. For example, Harper and Mitchell [5] have presented a semantics for ML polymorphism using core-XML, an explicitly typed version of core-ML that includes constructs for type abstraction and application, similar to those in the polymorphic λ-calculus.

Another example is the treatment of overloading proposed by Wadler and Blott [25] in which overloading is represented by introducing so-called dictionary abstractions and applications. This basic idea has been used in all current implementations of Haskell type classes [8] and has been widely studied [1, 9, 10, 12, 17, 18, 21, 23, 24].

This paper is motivated by the observation that both ideas can be dealt with in the same framework, allowing us to exploit the connections between the two systems so that results and ideas originally developed with one application in mind can also be applied to the other. More precisely, we show how qualified types, originally developed to to study type class overloading, can be used to investigate the translation of core-ML programs into a language that includes constructs for dealing with explicit polymorphism.

We begin with a brief review of core-ML in Section 2 and, in Section 3, show how the structure of typing derivations can be used to guide a translation from core-ML into the polymorphic λ-calculus. One particular problem is that a single term can have many different translations, each with potentially distinct semantics.

Our main aim is to give coherence conditions that can be used to identify a large class of core-ML terms for which all translations are guaranteed to be semantically equivalent. Section 4 shows how the type systems of core-ML and polymorphic λ-calculus can be extended to support qualified types and then Section 5 formalizes what it means for two translations to be equivalent. The following three sections extend the conventional type inference algorithm for core-ML to calculate principal translations. First, Section 6 extends the standard ordering between type schemes to the explicitly typed calculus. The algorithm itself is presented in Section 7 and used to establish the desired coherence results in Section 8.

Section 9 addresses another important issue, that of showing that the semantics of translated terms agrees with the intended semantics of the original programs.

2 A review of core-ML

We begin with a quick review of core-ML. This material is standard (see [4, 14] for example) but is included here to illustrate the notation used in the following sections. It also provides a summary of the most important tools used in the study of ML type inference, including in particular, the ordering on type schemes.

The terms of core-ML are those of simple untyped λ-calculus with the addition of a let construct to enable the definition and use of polymorphic terms:

E ::= x | λx.E | E F | let x = E in F .

The syntax for types distinguishes monotypes from (polymorphic) type schemes:

τ ::= b | t | τ → τ  monotypes
σ ::= ∀T .τ  type schemes

where b denotes a base type, t a type variable and T a finite set of type variables. For convenience, if σ = ∀T .τ, then we write ∀t.σ as an abbreviation for ∀(T ∪ {t}).τ. Type schemes that are equivalent up to renaming of bound variables will be considered equal. 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 typing rules will be described using type assignments, i.e. (finite) sets 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 maps x to σ. The complete typing rules for core-ML are given in Figure 1. Each judgement of the form A ⊢ E : σ is

(var)  \begin{matrix}(x :σ) ∈ A \\ A ⊢ x : σ \end{matrix}  (∀E)  \begin{matrix}A ⊢ E : ∀α.σ \\ A ⊢ E : [τ/α]σ \end{matrix}
(→E) \begin{matrix}A ⊢ E : τ′ → τ & A ⊢ F : τ′ \\ A ⊢ EF : τ \end{matrix}  (∀I ) \begin{matrix}A ⊢ E : σ & α ∉ TV (A) \\ A ⊢ E : ∀α.σ \end{matrix}
(→I )

\begin{matrix}A_{x} , x :τ′ ⊢ E : τ \\ A ⊢ λx.E : τ′ → τ \end{matrix}

(let)

A ⊢ E : σ A_{x} , x :σ ⊢ F : τ

A ⊢ (let x = E in F ) : τ

Fig. 1. Typing rules for core-ML.

called a typing and represents the assertion that, if the types of free variables are as specified by the type assignment A, then the expression E can be treated as having type σ.

As a first step to characterizing the set of types that can be assigned to a given term, we introduce an ordering ≤ on the set of type schemes.

Definition 1 Suppose that σ = ∀α_{i}.τ, σ′ = ∀β_{j} .τ′ and that none of β_{j} appears free in τ (this last condition can always be satisfied by renaming bound variables in σ′). Then σ is less general than σ′ (written σ ≤ σ′) if there are types ν_{i} such that τ′ = [ν_{i}/α_{i}]τ.

It is easy to show that ≤ is reflexive, transitive and preserved by substitutions.

There is a standard procedure, based on Milner’s algorithm W [14], which, given a term E and a type assignment A, calculates a type scheme σ such that A ⊢ E : σ. (It is also possible for the algorithm to fail, in which case there are no derivable typings of this form). Furthermore, the inferred type scheme σ is principal (or most general) in the sense that, if A ⊢ E : σ′ for some σ′, then σ′ ≤ σ. In fact, we can strengthen this to show that σ′ ≤ σ ⇔ A ⊢ E : σ′.

3 From core-ML to polymorphic λ-calculus

As part of an attempt to describe the type structure of Standard ML, Harper and Mitchell [5] introduced an explicitly typed variant of core-ML called core-XML. Their intention was that any implicitly typed term in the former might be regarded as a convenient shorthand for an explicitly typed term in the latter.

Given a semantics for the target language, a translation process can also be used to study the meaning of programs in the source language. This section describes a similar process for translating core-ML into an explicitly typed language. Since our interest is more in the semantics of core-ML than its type structure, we will use the polymorphic λ-calculus, abbreviated here to PΛ, as the target language. The set of types in PΛ is given by:

σ ::= t | b | σ → σ | ∀t.σ.

Notice that this allows polymorphic values to be used as the arguments and results of PΛ functions. This extra flexibility will be useful in subsequent sections, particularly Section 6.

The types of core-ML correspond to a subset of PΛ types, given by σ′ ::= τ | ∀t.σ′. For any σ′ in this set, the corresponding type scheme will be written as scheme(σ′). For example, scheme(∀α.∀β.α → β) = ∀{α, β}.α → β.

The terms of PΛ are similar to those for core-ML except that λ abstractions and let constructs are annotated with types and additional constructs are included for type abstraction (λt.E) and application (E τ):

E ::= x | λx :τ.E | E F | let x :σ = E in F | λt.E | E τ

Strictly speaking, there is no need to include the let construct in the definition of PΛ because the type system is sufficiently powerful to allow us to encode any term of the form let x : σ = E in F in the form (λx : σ.F )E. On the other hand, including let makes it easier to maintain a direct correspondence between core-ML terms and their translations.

The typing rules for PΛ are given in Figure 2. Clearly, there is a strong correspondence between these rules and those in Figure 1. This can be captured formally using a function Erase mapping PΛ terms to core-ML terms:

Erase (x)  = x
Erase (λx :t.E) = λx.(Erase E)
⋮
Erase (Et)  = Erase E
Erase (λt.E) = Erase E

It is straightforward to show that, for any core-ML derivation of a typing A ⊢ E : σ, there is a PΛ term E′ such that A ⊢ E : σ′ by a PΛ derivation of the same structure, scheme(σ′) = σ and Erase E′ = E. We will describe the term E′ as a

(var)

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

(let)

A ⊢ E : σ A_{x} , x :σ ⊢ F : σ′

A ⊢ (let x :σ = E in F ) : σ′

(→I ) \begin{matrix}A_{x} , x :σ′ ⊢ E : σ \\ A ⊢ λx :σ′.E : σ′ → σ \end{matrix}  (→E) \begin{matrix}A ⊢ E : σ′ → σ & A ⊢ F : σ′ \\ A ⊢ EF : σ \end{matrix}
(∀I )

A ⊢ E : σ t ∉ TV (A)
A ⊢ λt.E : ∀t.σ

(∀E)

\begin{matrix}A ⊢ E : ∀t.σ \\ A ⊢ Eτ : [σ′/t]σ \end{matrix}

Fig. 2. Typing rules for polymorphic λ-calculus, PΛ.

translation of E and use the notation A ⊢ E ⇝ E′ : σ to refer to a translation of a term in a specific context.

The relationship between the two type systems can be pictured by the following diagram.

[figure: core-ML derivations; PΛ ; derivations; ϕ; ψ; core-ML typings; PΛ ; typings]

The two vertical arrows, ϕ and ψ, are functions mapping derivations to the typings that appears as their conclusion. As a result of the explicit type annotations, the structure of any PΛ derivation of a typing A ⊢ E′ : σ is uniquely determined by the syntactic structure of E′ and hence ψ is injective. However, a single core-ML typing can have many distinct derivations, so ϕ is certainly not injective. It follows that a core-ML term may have many distinct translations in a given context.

There are a number of conditions that need to be established to justify the use of translations as a semantics for core-ML terms:

– Existence of translations: For every derivable core-ML typing A ⊢ E : σ, there is a translation E′ such that A ⊢ E ⇝ E′ : σ. This follows directly from the definition of translations given above. Moreover, there is an effective way of calculating a translation using the structure of the typing derivation.

– Soundness of translation: Every translation of a well-typed core-ML term is well-typed in PΛ. This again follows directly from the definition of translations.

– Agreement with expected semantics: The semantics of translated terms should agree with the intended semantics of the original core-ML programs.

Of course, the ‘intended’ semantics may vary depending on the language in question. We discuss this further in Section 9.

– Coherence of translation: The mapping from terms to translations must be well-defined. More accurately, we must show that any translations E_{1} and E_{2} of a core-ML term E given by derivations A ⊢ E ⇝ E_{1} : σ and A ⊢ E ⇝ E_{2} : σ are semantically equivalent. Our use of the term coherence follows [2]; the meaning of a term should not depend on the way that it is type checked.

Unfortunately, it is relatively easy to find core-ML terms for which the coherence property does not hold. For example, consider the structure of the typing derivation for the term foo bar using the type assignment A = {foo : ∀t.t → b, bar : ∀t.t} that would be constructed by an implementation of core-ML type inference:

(foo :∀t.t → b) ∈ A

(var)

A ⊢ foo : ∀t.t → b

(∀E)

A ⊢ foo : t′ → b

(bar :∀t.t) ∈ A

(var)

A ⊢ bar : ∀t.t (∀E)

A ⊢ bar : t′ (→E)

A ⊢ foo bar : b

From this derivation we obtain A ⊢ foo bar ⇝ (foo t′) (bar t′) : b. Clearly, by replacing t′ with distinct base types b_{1} and b_{2}, we can obtain distinct translations (foo b_{1}) (bar b_{1}) and (foo b_{2}) (bar b_{2}) that are not equivalent.

There is a second reason for loss of coherence. In core-ML, we chose to use a set of variables in the syntax for type schemes, capturing the intuition that the ordering of the quantified variables is not significant. However, the ordering of quantified variables in PΛ is significant because it determines the ordering of type parameters and we would not expect two arbitrary terms of the form λα.λβ.E and λβ.λα.E to be equivalent.

Perhaps the coherence property is too strong? Is it really necessary to ensure that all translations of a term are equivalent? One alternative would be to choose a particular type-inference algorithm for core-ML that attempts to construct a derivation for a given typing and fails only if no such derivation exists. If, on the other hand, the algorithm succeeds then we can treat the PΛ term corresponding to the constructed derivation as a ‘canonical’ translation of the input term. We will not consider this approach any further here; it seems unnatural to base a definition of the semantics of a language on the almost arbitrary choice of a particular version of the type checking algorithm.

With the examples above, it is clear that we cannot establish a coherence property for all core-ML typings and translations. The best we can hope for is to identify a large class of terms for which coherence can be guaranteed. There are two reasons why the type systems of core-ML and PΛ are not suitable for this task:

– The typing rules do not provide enough information about the way that polymorphic types are instantiated within a derivation. For the example above, we might have expected the translation of foo bar to be λt′.(foo t′) (bar t′), capturing the free variable t′. However, the standard definition of ML type inference uses only the type of a term (not its translation) to determine when universal quantification (and hence, type abstraction in the translation) should be used. Since t′ does not appear free in the inferred type b, no attempt will be made to quantify over this variable. (This is consistent with the logical interpretation of type schemes where we would expect ∀t′.b to be equivalent to just b.)

– The typing rules do not provide enough of a distinction between quantification and type abstraction. This is particularly noticeable in the example above illustrating the importance of the ordering of type parameters.

In the following sections, we will present modified versions of core-ML and PΛ that include the additional information needed to avoid these problems.

As a reference to related work, we should mention that the coherence problem for the translation from core-ML to core-XML was first noted by Ohori [19] and the significance of free type variables in translated terms was commented on by Harper and Mitchell [5].

4 Translations using qualified types

A qualified type is a type of the form π ⇒ σ denoting those instances of type σ which satisfy the predicate π. In previous work [9, 10], we have concentrated on the use of qualified types to explore the combination of overloading and polymorphism, with applications to Haskell type classes, extensible records and subtyping. In the following sections, we will show that they can also be used to establish sufficient conditions that guarantee coherence for a large class of core-ML terms.

4.1 Predicate systems

Different systems of predicates can be used to describe different applications. In each case, the properties of predicates can be captured by an entailment relation ⊢⊢ between finite sets of predicates. In fact, for the purposes of this work, we need to extend the definition of entailment to describe not only what is entailed, but also how. The basic idea is to require that a value of type π ⇒ σ can only be used if we are supplied with evidence that the predicate π holds. We will assume that the definition of a system of predicates includes a language of evidence expressions e and evidence variables v. The entailment relation is expressed by judgements of the form:

v_{1} :π_{1}, …, v_{n} :π_{n} ⊢⊢ e_{1} :π′_{1}, …, e_{m} :π′_{m}.

indicating that, if the variables v_{i} are bound to evidence values for the predicates π_{i}, then the evidence expressions e_{j} give evidence for the corresponding predicates π′_{j} . We will often abbreviate such entailments, writing them in the form v :P ⊢⊢ e :Q where v, e and P, Q are the appropriate sequences of evidence variables, evidence expressions and predicates respectively.

We refer to expressions of the form v :P on the right of an entailment as predicate assignments. The empty predicate assignment is denoted ∅. For any predicate system, the definition of entailment is required to satisfy the rules in Figure 3. The variable S in rule (close) denotes an arbitrary substitution of types for type

(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

Fig. 3. Predicate entailment with evidence.

variables, while the expression EV (e) in rule (evars) denotes the collection of evidence variables appearing in the evidence expression e.

For the purposes of this paper, we will use the set of types τ as predicates with a collection of evidence expressions given by:

e ::= v | b | e → e

together with the entailment relation given by extending the rules in Figure 3 with the axioms:

∅ ⊢⊢ b :b v :τ, w :τ′ ⊢⊢ (v → w):(τ → τ′).

These are just the standard rules for type formation with evidence variables in place of type variables. We have used the same syntax for types and evidence expressions; in a practical implementation, evidence expressions would be used to construct and manipulate the concrete representations of types.

4.2 Extending core-ML and PΛ with predicates

In the following we will work with extensions of core-ML and PΛ that make use of a system of predicates. We refer to these languages as core-MLP and PΛP respectively (corresponding to OML and OP in [10]).

The terms of core-MLP are the same as those of core-ML, but the set of types includes not only types and type schemes, but also qualified types:

τ ::= b | t | τ → τ  monotypes
ρ ::= τ | π ⇒ ρ  qualified types
σ ::= ∀T .ρ  type schemes

It follows from this grammar that function arguments and results in core-MLP cannot be polymorphic or qualified (in much the same way that the language of types in core-ML makes it impossible to use polymorphic functions as first-class values).

The language of terms in PΛP is essentially the same as those of PΛ except that we omit the type annotations for λ- and let-bound variables and replace the constructs for type abstraction and application with equivalent constructs for evidence values:

E ::= x | λx.E | E F | let x = E in F | λv.E | E e.

The set of PΛP types is a direct extension of the types in PΛ to include qualified types:

σ ::= t | b | σ → σ | π ⇒ σ | ∀t.σ.

Rather than giving separate definitions for the type systems of core-MLP, PΛP, and the translation between them, the rules in Figure 4 define all three using judgements of the form P | A ⊢ E ⇝ E′ : σ. The first component, P, is a predicate assignment, E is a core-MLP term and E′ is the corresponding PΛP translation. Ignoring the translations E′, these rules describe the type system of core-MLP. Note the use of the symbols τ, ρ and σ to restrict the application of certain rules to particular kinds of type, according to the grammar for core-MLP types given above. On the other hand, if we disregard the core-MLP term in each judgement and ignore the distinction between different kinds of type expression, then the same rules define the type system of PΛP. Finally, since the rules identify terms in each language with typing derivations of the same structure, it follows that P | A ⊢ E ⇝ E′ : σ is derivable if and only if E′ is a translation of E in the sense of Section 3.

4.3 From core-ML to core-MLP

The rules in Figure 4 break the direct connection between universal quantification and type abstraction since there are different introduction and elimination rules for each. To understand how core-ML typing can be studied using the type system of core-MLP, we need to be able to map core-ML type schemes ∀α_{i}.τ to core-MLP type schemes of the form ∀α_{i}.α_{1} ⇒ … ⇒ α_{n} ⇒ τ, forcing us to arrange the type parameters in some specific order. If these annotations are included in the types assigned to all free variables in a given term, then the typing rules in Figure 4 will ensure that information about the way that polymorphic types are instantiated will be propagated throughout the typing derivation.

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

(let)

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

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

(→I )

P |A_{x} , x :τ′ ⊢ E ⇝ E′ : τ
P |A ⊢ λx.E ⇝ λx.E′ : τ′ → τ
(→E)

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

Qualified types: (⇒I )

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

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

Polymorphism: (∀I )

P |A ⊢ E ⇝ E′ : σ t ∉ TV (A) ∧ t ∉ TV (P)
P |A ⊢ E ⇝ E′ : ∀t.σ
(∀E)

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

Fig. 4. Typing and translation rules for core-MLP and PΛP.

As an aside, we mention that there may be some situations where it may be useful to be able to omit some quantified variables from the list of qualifying predicates. For example, we might use the type scheme ∀t.t → t for an implementation of the identity function that can be used for all types of values, while ∀t.t ⇒ t → t would be more appropriate in a system where different representations are used for different types of values and the implementation of the identity function truly does depend on the value that is assigned to t. We can capture this formally by requiring that any expression E whose type should unconditionally be reflected in the predicate assignment of a typing be replaced by id E where id is a predefined identifier representing the identity function with polymorphic type ∀t.t ⇒ t → t.

5 A definition of equality for PΛP 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 PΛP terms using judgements of the form P | A ⊢ E = F : σ (with the implicit side-condition that both P | A ⊢ E : σ and P | A ⊢ F : σ). Our task for establishing coherence can then be described formally as:

Given derivations P | A ⊢ E ⇝ E_{1} : σ and P | A ⊢ E ⇝ E_{2} : σ, determine sufficient conditions to guarantee that P |A ⊢ E_{1} = E_{2} : σ.

One reason for including type information as part of the definition of equality is to avoid making unnecessary constraints on the choice of semantic model. Given a judgement P | A ⊢ E = F : σ we require only that E and F have the same meaning (which must be an element of the type denoted by σ) in environments that satisfy P and A.

5.1 Uniqueness of evidence

Another reason for using predicate assignments in the definition is to enable 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 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 and is central to establishing the coherence criteria given in Section 8. Defining the equality of evidence expressions and proving uniqueness of evidence is straightforward for the current application and we omit further details here.

5.2 Reduction of PΛP terms

In common with many treatments of typed λ-calculi, we will define the equality relation between terms using a notion of reduction between terms. More precisely, we use a judgement of the form P |A ⊢ E >F : σ to describe a (typed) reduction from E to F with the implicit side condition that P | A ⊢ E : σ. There is no need to include P | A ⊢ F : σ as a second side condition since it can be shown that this condition is implied by the first. This is a consequence of the subject reduction theorem – ‘reduction preserves typing’ – which is proved using standard techniques as in [7].

The most important rules in the definition of reduction are given in Figure 5, including definitions of β-conversion for both kinds of λ-abstractions and let expressions and a rule of η-conversion for evidence abstractions. One unfortunate consequence of our 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

(β)  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 : σ

Fig. 5. Rules of computation

from the difficulty of axiomatizing call-by-value equality than from anything implicit in our particular application; for example, Ohori [19] mentions similar problems in his work to describe a simple semantics for ML Polymorphism.

Additional rules are needed to describe the renaming of bound variables (αreduction) and structural properties (to allow reduction of subterms within a given term). These are standard and will be omitted from the presentation here.

5.3 Equalities between PΛP terms

As we have already mentioned, equalities between PΛP terms will be represented by judgements of the the form P |A ⊢ E = F : σ with the implicit side condition that both P | A ⊢ E : σ and P | A ⊢ F : σ. Figure 6 gives the definition of the equality between terms as the transitive, symmetric closure of the reduction relation described in the previous section. The first two rules ensure that equality

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 : σ

Fig. 6. Definition of equality between terms

is an equivalence relation. (There is no need to include reflexivity here since this is a direct consequence of the structural rules.) The last rule shows how reductions give rise to equalities. Note that in this case there is no need to establish that both P | A ⊢ E : σ and P | A ⊢ F : σ since the latter follows from the former by the subject reduction theorem mentioned above.

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′  (substitution)
= let x = [E/x]F in F′ : σ (β-let)

Notice that the context in which this equality is established (given by P, A and σ) is not significant. Examples like this are quite common and we will often avoid mentioning the context altogether in such situations, writing ⊢ E = F to indicate that E and F are equivalent in the sense that P |A ⊢ E = F : σ for any choice of P, A and σ for which the implicit side conditions hold.

The above property of let expressions may seem a little unfamiliar, so it is worth illustrating how it can be useful in the work described here. Suppose that g :∀t.t → t → t and consider the core-MLP term:

let f = λx.g x x in f 1

Since the local definition for function f is only ever applied to integer values, it is sufficient to treat f as having type Int → Int → Int, with a corresponding translation:

let f = λx :Int.g Int x x in f 1

However, the type inference algorithm uses ∀t.t → t as the type for f and leads to a translation of the form:

let f = λt.λx :t.g t x x in f Int 1

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.

⊢ let f = λt.λx :t.g t x x in f Int 1

= let f = λt.λx :t.g t x x in [f Int/f ](f 1) (substitution)
= let f = [λt.λx :t.g t x x/f ](f Int) in (f 1) (by result above)
= let f = (λt.λx :t.g t x x) Int in (f 1)  (substitution)
= let f = λx :Int.g Int x x in (f 1)  (β)

6 Ordering and conversion functions

The ordering ≤ is a central part of the treatment of core-ML type inference described in Section 2. used to express when one type is more general than another. For example, an ordering of the form (b → b) ≤ (∀t.t → t) might be used to argue that, for the purposes of type inference, any term of type b → b can be replaced by a term with type ∀t.t → t. This property does not extend to the explicitly typed language PΛ; if f :b → b, f′:∀t.t → t and x :b, then f x has type b, but f′ x is not even well-typed! Of course, the correct approach is to replace f with f′ b.

To understand the role of the ≤ ordering in the explicitly typed calculus, we will define a collection of terms for each σ′ ≤ σ, referred to as conversions from σ to σ′. Each conversion is a closed PΛP 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.xb) : (∀t.t → t) → (b → b).

Note that the type of this conversion (as in the general case) cannot be expressed as an core-MLP type scheme since it uses the richer structure of PΛP types.

For the purposes of type inference it would be sufficient to take any term C of type σ → σ′ as a conversion for σ′ ≤ σ since CE has type σ′ for any term E of type σ. 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 PΛP terms E (or at least, all those occurring as translations of core-MLP 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.

In previous work with qualified types, we have used the concept of a constrained type scheme, written as a pair (P |σ), that captures both the type scheme σ for a term and the constraints P on the environments in which that typing can be used. In PΛP, the constrained type scheme (P | σ) corresponds to the qualified type P ⇒ σ. The following definition can be used to describe 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 PΛP 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 a little more insight into the structure of conversions. The following definition is closely based on the syntactic characterization of the ordering between constrained type schemes given in [10] and based, in turn, on the definition of the ordering on core-ML type schemes presented in Section 2:

Definition 2 Suppose that σ = (∀α_{i}.Q ⇒ τ) and σ′ = (∀β_{j} .Q′ ⇒ τ′) and that none of the variables β_{j} appear free in σ, P or P′. A closed PΛP term C of type (P | σ) → (P′ | σ′) such that Erase C is equivalent to id is called a conversion from (P | σ) to (P′ | σ′), written C : (P | σ) ≥ (P′ | σ′), if there are types τ_{i}, evidence variables v and w and evidence expressions e and f such that:

v :P′, w :Q′ ⊢⊢ e :P, f :[τ_{i}/α_{i}]Q, τ′ = [τ_{i}/α_{i}]τ and ⊢ C = λx.λv.λw.xef .

As stated in Section 2, the ordering relation between core-ML type schemes is reflexive, transitive and preserved by substitutions. The corresponding results for conversions are given by the following proposition:

Proposition 3 For all appropriate constrained type schemes:

– id :(P |σ) ≥ (P |σ).

– If C :(P |σ) ≥ (P′ |σ′) and C′:(P′ |σ′) ≥ (P′′ |σ′′), then (C′ ∘ C ):(P |σ) ≥ (P′′ |σ′′) where C′ ∘ C = λx.C′(Cx).

– If C : (P | σ) ≥ (P′ | σ′), then C : S(P | σ) ≥ S(P′ | σ′) for any substitution S of types for type variables.

Note that the concept of a conversion is closely related to that of Mitchell’s retyping functions, as used in [16] to obtain minimal typings for a restricted set of terms in a version of the pure polymorphic λ-calculus.

7 Type inference and translation

The development of a type inference algorithm that can be used to calculate a principal type scheme for every core-MLP term was presented in [9]. In this section, we show that this can be extended to allow the calculation of translations, as described by the rules in Figure 7. These rules can be interpreted as an attribute grammar. The type assignment A and core-MLP term E in a judgement of the form P | TA ⊢^{W} E ⇝ E′ : τ are inherited attributes, while the predicate assignment P, substitution T , translation E′ and type τ are synthesized. The notation Gen(A, ρ) used in rule (let)^{W} represents the generalization of ρ with respect to A and is defined by: Gen(A, ρ) = ∀(TV (ρ) \ TV (A)).ρ.

The following theorem shows that any typing and translation that is obtained using the type inference algorithm can also be derived using the rules in Figure 4.

Theorem 4 (Soundness) If P |TA ⊢^{W} E ⇝ E′ : τ, then P |TA ⊢ E ⇝ E′ : τ.

Given that the algorithm described here calculates a principal type scheme for each well-typed core-MLP term, we will refer to the translations that it produces as principal translations. The following theorem provides further motivation for this terminology, showing that every translation can be expressed in terms of a principal translation.

Theorem 5 (Completeness) If v : P | SA ⊢ E ⇝ E′ : σ, then there are w : Q, T , E′′ and ν such that w : Q | TA ⊢^{W} E ⇝ E′′ : ν and there is a substitution R and a conversion C : RGen(TA, Q ⇒ ν) ≥ (P | σ) such that S = RT (except perhaps for new variables) and

v :P |SA ⊢ C (λw.E′′)v = E′ : σ.

A detailed presentation of the type inference algorithm described in this section, with full proofs of Theorems 4 and 5, is included in [10].

(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} τ′ → α
U (T′P, Q)|UT′TA ⊢^{W} EF ⇝ E′F′ : U α

where α is a new variable

(→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′ : τ′
P′ |T′TA ⊢^{W} (let x = E in F ) ⇝ (let x = λv.E′ in F ) : τ′

where σ = Gen(TA, P ⇒ τ)

Fig. 7. Type inference algorithm with translation

8 Coherence results

Theorem 5 is important because it shows that any translation of an core-MLP 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. For 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 way to ensure that these translations are equal is to show that the two conversions are equal.

8.1 Equality of conversions and translations

Taking a more slightly more general view, suppose that C_{1}, C_{2} are conversions from (P′ | σ′) to (P | σ). Without loss of generality, we can assume that σ = (∀α_{i}.Q ⇒ ν) and σ′ = (∀α′_{j} .Q′ ⇒ ν′) where the variables α_{i} only appear in (Q ⇒ ν). Using the definition of conversions, it follows that:

ν = [τ_{j} /α′_{j} ]ν′ and v :P, w :Q ⊢⊢ e :P′, f :[τ_{j} /α′_{j} ]Q′

for some types τ_{j} and that ⊢ C_{1} = λx.λv.λw.xef . Similarly for C_{2} there are types τ′_{j} such that:

ν = [τ′_{j}/α′_{j} ]ν′ and v :P, w :Q ⊢⊢ e′:P′, f′:[τ′_{j}/α′_{j} ]Q′

and ⊢ C_{2} = λx.λv.λw.xe′f′. 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 hence must be equivalent. The same argument cannot be applied to the second equality since the predicates [τ_{j} /α′_{j} ]Q′ may not be the same as those in [τ′_{j}/α′_{j} ]Q′ due to differences between the types τ_{j} and τ′_{j}. Nevertheless, since [τ_{j} /α′_{j} ]ν = ν′ = [τ′_{j}/α′_{j} ]ν, it follows that τ_{j} = τ′_{j} for all α′_{j} ∈ TV (ν). Notice then that, if {α′_{j} } ∩ TV (Q′) ⊆ TV (ν), the two predicate sets [τ_{j} /α′_{j} ]Q′ and [τ′_{j}/α′_{j} ]Q′ must be equal and hence f = f′ as required. We will give a special name to type schemes with this property:

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

This definition coincides with that of an unambiguous type scheme in the treatment of type classes in Haskell, motivating our use of the same term here. Using this terminology, the discussion above shows that all conversions from an unambiguous type scheme to an arbitrary constrained type scheme are equivalent:

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

As an immediate corollary, we obtain:

Theorem 8 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 system of type classes in [25]. To illustrate how this result can be used to detect incoherence in the translation from core-ML to PΛ, we recast the example from Section 3 in the type system of core-MLP, using the type assignment A = {foo :∀t.t ⇒ t → b, bar :∀t.t ⇒ t}. The principal type of foo bar with respect to A is ∀t.t ⇒ b, which is ambiguous in the sense described above.

The restriction to unambiguous principal types is sufficient, but not necessary, to guarantee coherence. Thus we may be forced to reject some terms that have a well-defined meaning, despite the fact that they have an ambiguous principal type. For example, if we define foo = λt.λx.b_{0} for some constant b_{0} : b, then evaluating the two translations (foo b_{1}) (bar b_{1}) and (foo b_{2}) (bar b_{2}) will in fact produce the same result, b_{0}. Of course, this requires additional information about foo, not included in the original typing derivation. We conjecture that Theorem 8 might also be used as a necessary condition to establish coherence with respect to the definition of provable equality in Section 5 but we have not attempted to prove this.

8.2 Related work on coherence

Coherence results have been established for a number of different systems including those with subtyping [2, 3], intersection types [20], scaling [22] and type classes [1, 6, 10]. One standard approach used to establish results of this kind is to define a system of reduction rules on typing derivations. The required coherence property can then be established by showing that the reduction rules are strongly normalizing and preserve meaning, and that normal forms of derivations are uniquely determined by their conclusions.

Much of this could have been applied to the type systems described in this paper, but this would not have yielded a proof of coherence. The examples of incoherence show that there are typings that do not yield unique normal forms. 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.

9 Agreement with expected semantics

Consider the core-ML expression let x = E in F and suppose that E has a polymorphic type. It follows that this term will have a translation of the form let x = λt.E′ in F′. Assuming the semantics of Standard ML [15], these two programs may not have the same meaning. For example, if the evaluation of E diverges then the original term will also diverge but the translation may still converge if x is not used in F because the additional type abstraction for t is sufficient to delay the evaluation of E′. Alternatively, with a lazy evaluation strategy as in Haskell [8], the two terms will have the same denotational semantics, but the extra type parameter may cause a loss of sharing if x appears multiple times in F . These problems occur because the let construct, intended from the type theoretic perspective purely as a way of defining polymorphic values, is also used in practice for describing shared computation, sequencing (in a call-by-value language) and creating cyclic structures (in a call-by-name language). When extra parameters are required we must either compromise sharing (as in the translation above) or polymorphism (by using a translation of the form let x :σ = [τ/t]E′ in F′, restricting the opportunities for polymorphism).

Sharing is also important in languages where computations can cause side-effects. Motivated in particular by the desire to support references and first-class continuations in a language with a polymorphic type system, Leroy [13] has suggested a modification to the core-ML language that provides two distinct forms of the let construct, one for polymorphic definitions and one for shared (but monomorphic) definitions. In fact, there is no real need to extend the language since a monomorphic let expression can be treated as syntactic sugar for an expression of the form (λx.E)F . The essence of Leroy’s proposal is a change to the semantics of polymorphic let expressions, adding an extra (dummy) parameter in the definition of polymorphic values. This agrees with the semantics of core-ML given by the translations described in this paper.

The same ideas are already used in Haskell [8] as part of the infamous ‘monomorphism restriction’ (but the relationship between the two does not appear to be well-known). This again provides two syntactically distinct forms of let bindings, one of which allows overloading while the other does not, motivated by the desire to avoid a loss of sharing. The rules for distinguishing between the two are rather subtle, depending on the number of function arguments supplied and the presence of an explicit type signature. It may be preferable to make the distinction between the two forms of binding more explicit, making it easier for the programmer to anticipate where additional parameters may be inserted.

10 Conclusions

By viewing the translation from core-ML to PΛ as an application of qualified types we have been able to combine the results of previous work in each of these areas, recognizing related concepts such as the importance of coherence, and the similarity between Leroy’s proposals for polymorphism by name and the monomorphism restriction in Haskell. The same unified view has already proved useful for other work, for example, in [11] where techniques from partial evaluation are suggested as an implementation of both polymorphism and overloading. We anticipate that this will also bring several other benefits and useful insights in future work.

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. R. Harper and J.C. Mitchell. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15, 2, April 1993.

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

7. J.R. Hindley and J.P. Seldin. Introduction to combinators and λ-calculus. London mathematical society student texts 1. Cambridge University Press, 1986.

8. 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.

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

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

11. M.P. Jones. From polymorphism to monomorphism by partial evaluation. Yale University, Department of Computer Science. Submitted for publication, July 1993.

12. S. Kaes. Type inference in the presence of overloading, subtyping and recursive types. In ACM Conference on LISP and functional programming San Francisco, California, June 1992.

13. X. Leroy. Polymorphism by name for references and continuations. In 20th Annual Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993.

14. R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17, 3, 1978.

15. R. Milner, M. Tofte and R. Harper. The definition of Standard ML. The MIT Press, 1990.

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

17. T. Nipkow and G. Snelting. Type classes and overloading resolution via ordersorted unification. In 5th ACM conference on Functional Programming Languages and Computer Architecture, Cambridge, MA, August 1991. Lecture notes in computer science 523, Springer Verlag.

18. T. Nipkow and C. Prehofer. Type checking type classes. In 20th Annual Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993.

19. A. Ohori. A simple semantics for ML polymorphism. In 4th International Conference on Functional Programming Languages and Computer Architecture, Imperial College, London, September 1989. ACM Press.

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

21. G. Smith. Polymorphic type inference for languages with overloading and subtyping. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York. August 1991.

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

23. S. Thatte. Typechecking with ad hoc polymorphism.Manuscript, Department of mathematics and computer science, Clarkson University, Potsdam, NY. May 1992.

24. D. Volpano and G. Smith. On the complexity of ML typability with overloading. In 5th ACM conference on Functional Programming Languages and Computer Architecture. Lecture notes in computer science 523. Springer Verlag. 1991.

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

This article was processed using the LaTEX macro package with LLNCS style