Minimal Typing Derivations

Nikolaj Skallerud Bjørner DIKU, Department of Computer Science University of Copenhagen

January 1, 1993

Abstract

This paper presents a typing algorithm that for languages with polymorphic typings (e.g. ML), finds a typing derivation, which prevents polymorphic abstraction where it is not needed. Consequently unnecessary boxing can be avoided, allowing a more effective implementation of these languages.

It turns out that typeable expressions conveniently can be divided into two classes. One of the classes corresponds to intuitionisitic proofs containing cuts that can be pruned away. This is what we can characterize as programs containing dead code, i.e. code that is redundant for the final result. For this class we can unfortunately not always find a derivation, that prevents unnecessary polymorphic abstraction. However for the other class, containing all programs that do not have dead code, we show that there is a unique minimal derivation, i.e. a derivation such that (i) polymorphic abstraction is only introduced, where it really is needed, and (ii) there is no other derivation that at any point avoids abstraction where the minimal did not.

1 Introduction

1.1 Motivation

The current work has been inspired by unboxing analysis for polymorphic typeable programs as for instance found in [Xavier]. Based on a typing derivation of a program, unboxing analysis inserts suitable coercions such that boxed value passing to a great extent is avoided.

The programming language ML is a polymorphic programming language and algorithm W [MilDam82] can be used to find a typing derivation for an ML program. However it happens that the typings obtained by W introduce type abstraction for let bound variables where they are not always necessary. For instance in

\underline{let} mkpair = λx.(x, x) \underline{in} mkpair 3.14

Algorithm W would type mkpair : ∀α.α → α × α, instead of real → real × real.

The claim made in this paper is that in typical programs a great extent of polymorphic constructs such as mkpair are only used monomorphically and it could therefore be of interest to find the monomorphic type to avoid unnecessary boxing and unboxing.

We therefore focus on the possibilities of finding the more specific type-schemes associated with the let bound variables. By investigating this problem we gain some insight in the class of typing derivations for typeable expressions. But we remember that the only reason for doing this work is that there is a potential practical use for it.

1.2 Summary of obtained results

In this paper we investigate how typing derivations, or equivalently expressions with explicitly annotated types, can be compared via a subsumption ordering based on substitutions of type-variables. The subsumption ordering captures to which extent type schemes in a typing derivation have been instantiated. We show that:

• The classical algorithm W can be modified also to return a typing annotation i.e. a representation of a typing derivation in an expression. This annotation is shown to be most general with respect to our defined subsumption ordering.

• It is possible to find a most specific generalization (MSG) of any pair of first order terms. By a generalization of the terms t_{1}, t_{2} we understand a term t and substitutions θ_{1}, θ_{2} such that θ_{1} t = t_{1} and θ_{2} t = t_{2}. The term t is a most specific generalization (of t_{1} and t_{2}) if there for any other generalization t′ is a substitution S, such that S t′ = t.

• For a well defined class of expressions it is possible to to find a minimal annotation w.r.t. the subsumption ordering introduced. We devise an algorithm for this purpose and prove its soundness and completeness on the restricted class.

• We cannot in the general case find a unique minimal annotation. We investigate what goes wrong and how in general to find a least annotation, that subsumes all minimal incomparable annotations.

We should emphasize that there is nothing new in the first two points on this program (as opposed to the last two). This is why the report is called Minimal Typing Derivations, and not Typing Derivation Subsumption. We have included the two first points to make the report selfcontained.

The precise classification of the problem of finding least elements in the subsumption ordering leads to a result, which is of interest in itself. To say it loosely: if none of the possible typing derivations for an expression introduce type variables, not used in the derived type-scheme of the expression, then, disregarding the expressions that are used inside a let expression, there is only one way to build a derivation. We will later be much more precise about this statement, and (hopefully) be able to state it in a way somewhat more comprehensive, but it will take a number of definitions.

1.3 Outline of the paper

This paper is organized as follows: In Section 2 we introduce the object language: the types, expressions and typing derivations. We define basic operations (such as substitutions) on this language. In Section 3 we define and motivate our subsumption ordering on typing derivations. From this section one can go straight on to Section 6 to read the main results of this paper. In Section 4 we restate algorithm W, its soundness and completeness, but we go one step further by showing that W can find a typing derivation subsuming all others by the subsumption ordering defined. The proof is more or less copied from [Dam84]. As a brief interlude before we investigate minimal typing derivations, we define an algorithm that finds the most specific generalization of two first order terms. This section (Section 5) can be read independently. In Section 6 we finally introduce the algorithm that finds minimal derivations for some expressions. We prove its soundness and relative completeness. We also introduce the concept of cut-type variables, and show some central properties about these. In Section 7 we see what happens when typing derivations introduce cut-type variables. We will see that in these cases there might not be minimal typing derivations. Furthermore we will see how expressions can fail to have minimal derivations. Section 8 is the conclusion.

The paper also has 3 appendices. Appendix A sketches an algorithm, that finds more specific derivations than the original one given, in presence of cut type variables. Appendix B discusses an alternative way to formulate the main algorithm given in this paper, and appendix C introduces a sample implementation.

1.4 Notation

The metalanguage used to define types and algorithms borrows many constructs from the programming language ML. The few constructs not normally associated to Standard ML are explained briefly:

• Maps: The symbol →^{fin} is used to denote a finite map. It is written between its domain and range types. There are two ways to represent map expressions. One is as an explicit map of the form [d_{1} ↦ r_{1}, …, d_{n} ↦ r_{n}], where the domain elements are the d’s and range elements are to the right of the arrow (the r’s); the other is as a comprehended map expression of the form [d ↦ r|P (d, r)], where the predicate P determines the elements d’s and r’s (of course such that only one range element is associated to a domain element). dom is used to select the domain of a map, and rng is used to select the range of a map. Map deletion is written m \ s, where domain elements in the set s are deleted. Deletion of a single domain element x can be written m_{x}.

• Lists: Angle brackets ⟨ ⟩ are used to delimit lists. Like maps one may write explicit as well as comprehended lists. The comprehended lists are of the form ⟨x_{i}|P (x_{i})⟩ with P the predicate that holds for only the x_{i}’s and i indicates the position of x in the list. Lists are appended with .

2 Types and Expressions

For the purpose of presenting algorithms and their proofs as concisely as possible, we confine ourselves to a minimalistic approach regarding the language.

2.1 Types

Types and type-schemes are hereby of the following (standard) form:

α  ∈ TyVar
π  ∈ TyConst
θ  ∈ Substitution  = TyVar →^{fin} Type
τ  ∈ Type  = TyVar | TyConst | FunctionType
τ → τ ∈ FunctionType = Type × Type
σ  ∈ TypeScheme = Type | Quantification
∀α.σ ∈ Quantification = TyVar × TypeScheme

For notational convenience the abbreviation ∀α⃗.τ, where α⃗ is an ordered set of the variables {α_{1}, …, α_{n}}, is used for ∀α_{1} … ∀α_{n}.τ. Hereby is understood that quantification ranges over all variables in α⃗.

Substitutions are defined to be maps from type variables to types. Application of substitutions can thus be defined on type-schemes (and types) in the usual way, as we recall that we have to rename variables bound in the type-scheme to avoid conflicts with variables in the domain and range of the substitution. Substitution application is written prefix: θ σ.

We notice that the empty map [ ] is an identity substitution also referred to as id.

2.2 Expressions

The functional programming language we will consider has the following basic syntax:

\overline{e} ::= x | \overline{e} \overline{e}′ | λx.\overline{e} | \underline{let} x = \overline{e} \underline{in} \overline{e}′

We will refer to these as base expressions. Expressions of this syntax do not provide any information about which types are assigned to the variables. A typing derivation can provide this kind of information, however we will introduce the notion of annotated expressions to provide a simple way to represent typing information in the very expression.

In the literature a variant of annotated expressions is known as “explicitly typed terms of Core-XML” [MitHarp88]. We present our version as follows:

x  ∈ Var
ι  ∈ Instantiation  = Type^{∗}
Λα  ∈ TypeAbstr  = TyVar
e  ∈ Expr  = Variable | Abstraction | Application | Let
x ι  ∈ Variable  = Var × Instantiation
ee′  ∈ Application  = Expr × Expr
λx : τ.e  ∈ Abstraction  = Var × Type × Expr
\underline{let} x : σ = Λα⃗ e \underline{in} e′ ∈ Let  = Var × TypeScheme × TypeAbstr^{∗} × Expr × Expr
TE  ∈ TypeEnvironment = Var →^{fin} TypeScheme

Constants such as integers and reals can be represented as variables whose types are bound in the type environment.

The notation is inspired by higher order polymorphic λ−calculus [Girard], where type abstractions and instantiations are explicit in the expressions. However for our purpose it suffices to limit instantiations to let bound variables. This has led to the form x ι for x [τ_{1}, …, τ_{n}] instead of (… (x[τ_{1}]) … [τ_{n}]), where x has the associated type-scheme ∀α_{1}, …, α_{n}.τ. Since the position of τ_{i} in the instantiation is in a unique correspondence with a bound variable α_{i} in the associated type-scheme, an equivalent way to represent an instantiation is as a substitution from the bound variables to the instantiated types: [α_{1} ↦ τ_{1}, …, α_{n} ↦ τ_{n}]. We will later make frequent use of this correspondence.

A main difference between the annotated expressions defined here and those found in the reference [MitHarp88] is that we do not allow type abstraction at the outermost level, i.e. there can be no Λα preceding an expression e. It implies that the type annotations will always produce a monomorphic type (as opposed to a type-scheme). This “restriction” only serves the purpose of simplifying the presentation in this paper, and does not impose a fundamental restriction of the results. Indeed it is an easy (but tedious) exercise to go through the paper once it has been read and supplement definitions and algorithms with terms of the full core.

The last line in the definition of annotated expressions introduces type environments. It is essential that there is always associated a type environment with any annotated expression. The associated type environment is used to retrieve type information on free variables.

2.2.1 Annotation erasure

The correspondence between base expressions and annotated expressions should be obvious. Erasure of type annotations results in the base expressions. We will take the liberty to denote this erasure on an expression e by \overline{e}, thus at one and the same time stating that (i) \overline{e} has resulted from e by erasure of type annotations and that (ii) \overline{e} is a syntactic object defined above as a base expression.

Although formally inappropriate we hope that this hack will prevent us from being bugged down in too many tedious details.

2.2.2 Substitution on expressions

On basis of the definitions for substitution on variables in types or free variables in type-schemes, we can define substitution on expressions:

θe =^{def} case e of e_{1} e_{2} ⇒ θe_{1} θe_{2}

λx : τ.e_{1} ⇒ λx : θτ.θe_{1}
x [τ_{1}, …, τ_{n}] ⇒ x [θτ_{1}, …, θτ_{n}]
\underline{let} x : σ = Λα⃗ e_{1} \underline{in} e_{2} ⇒ \underline{let} x : θσ = Λα⃗ θe_{1} \underline{in} θe_{2}

Again we rename variables in α⃗ to avoid conflicts with variables used in the substitution.

Application of instantiations on type-schemes is written postfix not to confuse it with application of substitutions to type-schemes. Thus we write σ ι, where σ is of the form ∀α⃗.τ and ι is a map from variables in α⃗ to types. The result of the instantiation is ι τ, i.e. the result of applying the substitution ι to τ.

2.2.3 Typing derivations

Annotated expressions are introduced to abbreviate the notion of typing derivations. To recall what a typing derivation is, we restate the inference system given in [MilDam82]:

(VAR)  TE_{x} ∪ {x : σ} ⊢ x : σ

(INST)  \frac{TE ⊢ \overline{e} : ∀α.σ}{TE ⊢ \overline{e} : [α ↦ τ]σ}

(GEN)  \frac{TE ⊢ \overline{e} : σ}{TE ⊢ \overline{e} : ∀α.σ} if α is not free in TE

(COMB)  \frac{TE ⊢ \overline{e} : τ′ → τ TE ⊢ \overline{e}′ : τ′}{TE ⊢ \overline{e} \overline{e}′ : τ}

(ABS)  \frac{TE_{x} ∪ \{x : τ′\} ⊢ \overline{e} : τ}{TE ⊢ λx.\overline{e} : τ′ → τ}

(LET)  \frac{TE ⊢ \overline{e} : σ TE_{x} ∪ \{x : σ\} ⊢ \overline{e}′ : τ}{TE ⊢ \underline{let} x = \overline{e} \underline{in} \overline{e}′ : τ}

The way a typing derivation determines an annotation is illustrated by the set of rules given below:

A(TE ∪ {x : σ} ⊢ x : ∀α_{1}, …, α_{n}.τ) = Λβ⃗ x [β_{1}, …, β_{n}], β_{i} new

A ( \frac{∇}{TE ⊢ \overline{e} : [α ↦ τ]σ} )  = let Λβ.e = A(∇) in [β ↦ τ] e

A ( \frac{∇}{TE ⊢ \overline{e} : ∀α.σ} )  = Λα A(∇)

A ( \frac{∇_{1} ∇_{2}}{TE ⊢ \overline{e} \overline{e}′ : τ} )  = A(∇_{1}) A(∇_{2})

A ( \frac{∇}{TE ⊢ λx.\overline{e} : τ′ → τ} )  = λx : τ′.A(∇)

A ( \frac{∇_{1} ∇_{2}}{TE ⊢ \underline{let} x = \overline{e} \underline{in} \overline{e}′ : τ} )  = \underline{let} x : typeof(TE, A(∇_{1})) = A(∇_{1}) \underline{in} A(∇_{2})

Note: we have introduced a function typeof : TypeEnvironment × Expr → TypeScheme, that retrieves the type scheme determined by the annotation in the expression and type environment. The definition of typeof is straight forward.

Notice also that a typing derivation, as presented before, may result in a type abstraction. The function A is therefore only partial into the set of annotated expressions. As we noticed in the discussion about our notation, this limitation only serves the purpose of simplification and is of no greater significance.

The function A enables us to define what it means for an (annotated) expression to be well formed. The definition reads: An (annotated) expression e is well formed, if (i) there is a typing derivation ∇ such that A(∇) = e, (ii) every type variable is bound at most once, and (iii) the sets of bound an free type variables are disjoint. Condition (ii) and (iii) are not essential, but ease the design of the algorithms introduced in this paper.

The type environment associated with the annotated expression is implicit in this definition. It occurs in the conclusion of the inference ∇. We can make it explicit by defining the predicate: TE ⊢ e : τ. It states that e is well-formed, and there is a derivation ∇, such that A(∇) = e, and ∇ ends in the conclusion TE ⊢ \overline{e} : τ. The type τ will be called the external type of e (under TE).

We conclude this section by noticing that standard structural induction yields a generalization of the standard substitution theorem:

TE ⊢ e : τ ⇒ θTE ⊢ θe : θτ

3 Annotation subsumption

In the following section we generalize the concept of principal type-schemes of expressions to principal typing derivations. To come that far we first (in this section) recapture what a generic instance of a type-scheme is. Then we will define an ordering on annotated expressions and discuss its motivation.

What will be shown is that the annotated expression computed by W subsumes every other annotation with respect to this ordering. This result can be regarded as a generalization of the principal typing property of W, since we now compare entire typing derivations and not only the resulting type-scheme computed by W. Also the principal typing property is a consequence of the result. To find the least element in the ordering (if there are any) we will later develop an algorithm M that finds these for a broad class of expressions.

3.1 Ordering type-schemes

A type-scheme σ is a generic instance of σ′, in our notation written as σ < σ′ (where σ = ∀α⃗.τ and σ′ = ∀β⃗.τ′) iff there is a substitution θ of the variables in β⃗ to types, such that τ = θτ′ and that α⃗ does not contain variables free in σ′. To keep the substitution explicit we write σ <_{θ} σ′ for the above used type-schemes and substitution. Originally Damas defines subsumption for type-schemes via the instantiation relation: σ < σ′ iff all types instiantiable from σ are also instantiable from σ′. It is not difficult to see that this definition is equivalent to the one given above, see [Dam84, pp. 49] for further reference.

3.2 The ordering relation ⪯ on expressions

We compare two expressions e and e′ with their respective type environments TE and TE′. The type environments are used to retrieve the type-schemes bound to free variables in the expressions.

We write TE ⊢ e ⪯_{θ} TE′ ⊢ e′ to state that e is smaller that e′, realized by the substitution θ. What this formally means is stated below:

• TE ⊢ x ι  ⪯_{θ} TE′ ⊢ x ι′  iff TE(x)ι = θ (TE′(x)ι′)
• TE ⊢ e_{1} e_{2} ⪯_{θ} TE′ ⊢ e′_{1} e′_{2}  iff TE ⊢ e_{1} ⪯_{θ} TE′ ⊢ e′_{1} ∧ TE ⊢ e_{2} ⪯_{θ} TE′ ⊢ e′_{2}
• TE ⊢ λx : τ.e ⪯_{θ} TE′ ⊢ λx : τ′.e′ iff TE_{x} ∪ {x : τ} ⊢ e ⪯_{θ} TE′_{x} ∪ {x : τ′} ⊢ e′ ∧ τ = θ τ′
• TE ⊢ \underline{let} x : σ = Λα⃗ e_{1} \underline{in} e_{2} ⪯_{θ} TE′ ⊢ \underline{let} x : σ′ = Λα′ e′_{1} \underline{in} e′_{2}
iff TE_{x} ∪ {x : σ} ⊢ e_{2} ⪯_{θ} TE′_{x} ∪ {x : σ′} ⊢ e′_{2} ∧
∃θ′ · TE ⊢ e_{1} ⪯_{θ′} θTE′ ⊢ θe′_{1} ∧
σ <_{θ′} θσ′

The first three definitions ensure that the type annotations of e are obtainable from the type annotations of e′ via the substitution θ. Encountering a let-construction is a bit more complicated. We first require that the bodies compare with θ and their updated type environments, secondly since θ applies only to the free type variables in e′, we need another substitution, called θ′, which can have bound variables from σ′ in the domain and bound variables from σ in the range. We furthermore require σ to be a generic instance of θσ′; a redundant requirement, since the annotation uniquely determines the derivable type.

If two expressions e and e′ are annotations of the same base expression \overline{e} but TE ⊢ e ⪯ TE′ ⊢ e′, then loosely speaking the annotations in e′ are more abstract than those in e. An example given below illustrates the ordering:

\{x : int\} ⊢ \underline{let} id : int → int = λx : int.x \underline{in} id x

⪯_{[α↦int]}

\{x : α\} ⊢ \underline{let} id : ∀β.β → β = Λβλx : β.x \underline{in} id [α] x

The substitution θ′ introduced in the rule for let-expressions is of course [β ↦ int].

The ordering should thus reflect the degreee of type abstraction in typing derivations. The smaller an annotation is in the ordering ⪯, the more specific are the types. Ideally the least annotations would favor type constants like real, int etc. with a fixed lengthed storage requirement and only introduce type-abstraction where it really is needed.

4 Algorithm W modified to produce annotations

In this section we will present a version of W which finds an annotation. Later on we will prove that this annotation is most general with respect to the ordering defined in the last section.

4.1 Algorithm W

The version of algorithm W presented below is borrowed from [MilDam82], but modified also to return an annotated expression (i.e. a typing derivation). Gen(TE,τ) results in a type-scheme obtained by generalization over variables free in τ, but not free in TE.

W : TypeEnvironment × \overline{Expr} →^{∼} Substitution × Expr × Type W(\overline{e}) =^{def} case \overline{e} of

x ⇒ let ∀α_{1}, …, α_{n}.τ′ = TE(x) β_{1}, …, β_{n} be new type variables

in

(id, x [β_{1}, …, β_{n}], [α_{i} ↦ β_{i}|i ∈ {1, …, n}]τ′)

λx.\overline{e}_{1} ⇒ let

(S_{1}, e_{1}, τ_{1}) = W(TE_{x} ∪ \{x : β\}, \overline{e}_{1}), β is new in

(S_{1}, λx : S_{1}β.e_{1}, S_{1} β → τ_{1})

\overline{e}_{1}\overline{e}_{2} ⇒ let

(S_{1}, e_{1}, τ_{1}) = W(TE, \overline{e}_{1}) (S_{2}, e_{2}, τ_{2}) = W(S_{1}TE, \overline{e}_{2}) V = unify(S_{2}τ_{1}, τ_{2} → β), β is new

in

(V S_{2}S_{1}, (V S_{2}e_{1}) (V e_{2}), V β)

\underline{let} x = \overline{e}_{1} \underline{in} \overline{e}_{2} ⇒

let (S_{1}, e_{1}, τ_{1}) = W(TE, \overline{e}_{1}) ∀α⃗.τ_{1} = Gen(S_{1}TE, τ_{1}) (S_{2}, e_{2}, τ_{2}) = W(S_{1}TE_{x} ∪ \{x : ∀α⃗.τ_{1}\}, \overline{e}_{2})

in (S_{2} S_{1}, \underline{let} x : (S_{2}∀α⃗.τ_{1}) = (S_{2}Λα⃗ e_{1}) \underline{in} e_{2}, τ_{2})

Note: If unification fails, then the entire algorithm fails.

The classical properties of W are phrased in the following theorems, whose proofs can be found in [Dam84].

Theorem 1 (Soundness of W) If W(TE,\overline{e}) succeeds with (S,e,τ) then there exists a typing derivation for S TE ⊢ \overline{e} : τ. □

We note that the classical soundness theorem does not talk about annotated expressions, we therefore do not say anything about e here.

The next theorem talks about a type environment being an instance of another. Hereby we understand that there is a substitution, when applied to a type environment it yields its instantiation.

Theorem 2 (Completeness of W) Given TE’ and e, let TE be an instance of rm TE’ and σ a type-scheme such that there is a typing derivation for

TE ⊢ \overline{e} : σ

Then (i) W(TE,\overline{e}) succeeds (ii) If W(TE,\overline{e})= (S, e′, τ) then, for some substitution R, TE = RSTE′ and R Gen(STE′, τ) > σ. □

A direct corollary of this theorem is that if there is a typing derivation for \overline{e} under TE, then W computes a principal type scheme for \overline{e} under TE.

4.2 Generalized Completeness of W

These were almost literally the statements found in [MilDam84]. The soundness of the modified W can also be stated as: If W(TE,\overline{e}) succeeds with (S, e, τ) then STE ⊢ e : τ is well formed. The proof hereof is trivial. We will state and prove a generalization of the completeness theorem tailored for the version of W given above and the ordering on expressions defined earlier.

The theorem implies that the annotation found by W is a maximal element for well formed annotations w.r.t. the ordering ⪯. It also implies the classical completeness theorem, since the external types are uniquely determined by the annotations. This result should come as no surprise when the proof is seen: it is a simple rephrasing of Damas original proof from [Dam84] tailored for this form. We have chosen to follow Damas proof so close by that certain passages are simply copied.

The theorem reads:

Theorem 3 (Derivation Completeness) Given TE and \overline{e}, let TE′ be an instance of TE and e′ be an annotation of \overline{e} such that

TE′ ⊢ e′ : τ′

is a well formed annotation (with external type τ′). Then (i) W(TE,\overline{e}) succeeds (ii) If W(TE,\overline{e})= (S, e, τ) then, for some substitution R, TE′ = RSTE and

TE′ ⊢ e′ ⪯_{R} S TE ⊢ e

Proof The proof is carried through by structural induction over \overline{e}, as we compare the annotation obtained by W with another arbitrary annotation e′, valid under the type environment TE′.

• \overline{e} = x and e′ = xι′ = x [τ_{1}, …, τ_{n}]. Since TE′ is an instance of TE we can let R be the minimal substitution such that TE′ = R TE, in particular ∀γ⃗.τ′ = TE′(x) = R TE(x) = R ∀α⃗.τ. W(TE,x) succeeds with (id, x [β_{1}, …, β_{n}], [α_{i} ↦ β_{i}]τ). Because β_{i} are new, the substitution R′ = R ∪ [β_{i} ↦ τ_{i}|i = 1, …, n] is well defined and also satisfies:

TE′ ⊢ x ι′ ⪯_{R′} TE ⊢ x [β_{1}, …, β_{n}]

and TE′ = R′ TE

• \overline{e} = λx.\overline{e}_{1}, and e′ = λx : τ′_{1}.e′_{1}. If TE′ is an instance of TE then TE′_{x} ∪ \{x : τ′_{1}\} is an instance of TE_{x} ∪ {x : β}, β is new. It is therefore possible to use the induction hypothesis to assume that W succeeds with (S_{1}, e_{1}, τ) = W(TE_{x} ∪ \{x : β\}, \overline{e}_{1}), and:

TE′_{x} ∪ {x : τ′_{1}} ⊢ e′_{1} ⪯_{R′} S(TE_{x} ∪ {x : β}) ⊢ e_{1}

for some minimal substitution R′ also satisfying TE′_{x} ∪ {x : τ′_{1}} = R′ S(TE_{x} ∪ {x : β}). We will now show that

TE′ ⊢ λx : τ′_{1}.e′_{1} ⪯_{R} STE ⊢ λx : Sβ.e_{1}

and R S TE = TE′, for some R.

Since TE′ was assumed to be an instance of TE, there exists a substitution P from TE to TE′. Let P_{0} be the restriction of P to those type variables free in TE but not in TE_{x}. It will become clear that R = R′ ∪ P_{0}.

First of all we note that R is well defined because R′ is minimal and β, since it is new, does not occur free in TE. Further for every type variable α occurring free in TE_{x} we have P α = R′ S α. Also if α occurs free in TE but not in TE_{x} we must have Sα = α since

domS ⊆ FV(TE_{x} ∪ {x : β}) ∪ New

where New is the set of new type variables introduced in the recursive call. Thus for any type variable α occurring free in TE but not in TE_{x}, we have

P S α = P α = P_{0} α

and so we have proved

R S TE = (R′ ∪ P_{0}) S TE = P TE = TE′

and since R extends R′ the ordering ⪯ on expressions is satisfied by R.

• \overline{e} = \overline{e}_{1} \overline{e}_{2} and e′ = e′_{1} e′_{2}. By the induction hypothesis W(TE,\overline{e}_{1}) succeeds with (S_{1}, e_{1}, τ_{1}) = W(TE, \overline{e}_{1})

and

TE′ ⊢ e′_{1} ⪯_{R_{1}} S_{1}TE ⊢ e_{1}

for some R_{1}, also satisfying TE′ = R_{1} S_{1} TE. Split R_{1} up into two parts R_{1} = R_{1}^{1} ∪ R_{1}^{2} such that domR_{1}^{1} ⊆FV(S_{1} TE) and domR_{1}^{2} ⊆ (FV(TE) ∪New_{1})\FV(S_{1} TE).

Obviously, since the annotation uniquely determines the resulting type of an expression, if e′_{1} has the type τ′_{1} → τ′_{2}, then τ′_{1} → τ′_{2} = R_{1} τ_{1}.

By R_{1}, TE′ is an instance of S_{1} TE, so inductively we have that W(S_{1} TE,\overline{e}_{2}) succeeds with (S_{2}, e_{2}, τ_{2}) and

TE′ ⊢ e′_{2} ⪯_{R_{2}} S_{2} S_{1}TE ⊢ e_{2}

As before TE′ = R_{2} S_{2} S_{1} TE, τ′_{1} = R_{2} τ_{2} and we split R_{2} like we split R_{1}, such that domR_{2}^{1} ⊆FV(S_{2} S_{1} TE) and domR_{2}^{2} ⊆ (FV(S_{1} TE) ∪New_{2})\FV(S_{2} S_{1} TE).

To prove that W(TE,\overline{e}) succeeds all we have left to do is to prove that, if β is a new type variable, unify(S_{2}τ_{1}, τ_{2} → β) succeeds. we will do this by showing that

V_{0} = R_{1}^{2} ∪ R_{2}^{2} ∪ [β ↦ τ′_{2}] ∪ R_{2}^{1}

is a unifying substitution.

First of all we note that V_{0} is well defined since it is composed by maps whose domains are disjoint. Now

V_{0}(τ_{2} → β) = (V_{0}τ_{2}) → τ′_{2}

but since β and dom R_{1}^{2} is disjoint from FV(τ_{2}) (⊆ FV(S_{2}S_{1} TE) ∪ New_{2}) we have

V_{0}τ_{2} = R_{2}τ_{2} = τ′_{1}

and so V_{0}(τ_{2} → β) = τ′_{1} → τ′_{2}. Now, to see that we also have V_{0}S_{2}τ_{1} = τ′_{1} → τ′_{2}, we first note that, since

TE′ = R_{2}^{1} S_{2} S_{1} TE = R_{1}^{1} S_{1} TE

we have R_{1}^{1}α = R_{2}^{1} S_{2}α for any type variable α occurring free in S_{1}TE. But then, since FV(S_{2} τ_{1}) ⊆ dom R_{1}^{2} ∪ FV(S_{2}S_{1} TE), we have

V_{0}S_{2}τ_{1} = (R_{1}^{2} ∪ R_{2}^{2} ∪ [β ↦ τ] ∪ R_{2}^{1})S_{2}τ_{1}
= (R_{1}^{2} ∪ R_{2}^{1})S_{2}τ_{1}
= (R_{1}^{2} ∪ R_{1}^{1})τ_{1}
= τ′_{1} → τ′_{2}

Since V_{0} unifies S_{2}τ_{1} and τ_{2} → β, unify(S_{2}τ_{1}, τ_{2} → β) succeeds with some substitution V and thus W(TE,\overline{e}) also succeeds, with (V S_{2} S_{1}, e, V β) as we wanted. To prove clause (ii) of the theorem let R be a substitution such that V_{0} = R V. Then

R V S_{2} S_{1} TE = V_{0} S_{2} S_{1} TE
= R_{2} S_{2} S_{1} TE = TE′

and surely

TE′ ⊢ e′_{1} e′_{2} ⪯_{R} V S_{2} S_{1}TE ⊢ (V S_{2}e_{1}) (V e_{2})

because as we saw, for variables in e_{1}, R V S_{2} behaves like R_{1}, and for variables in e_{2}, R V behaves like R_{2}.

• \overline{e} = \underline{let} x = \overline{e}_{1} \underline{in} \overline{e}_{2}, e′ = \underline{let} x : σ′ = Λβ⃗ e′_{1} \underline{in} e′_{2} and σ′ = ∀β⃗.τ′_{1}. By the induction hypothesis the first recursive call of W succeeds with W(TE,\overline{e}_{1}) = (S_{1}, e_{1}, τ_{1}) and there is a minimal substitution R_{1} such that

TE′ = R_{1} S_{1} TE
TE′ ⊢ e′_{1} ⪯_{R_{1}} S_{1} TE ⊢ e_{1}

As we did before, we split R_{1} into two parts R_{1}^{1} ∪ R_{1}^{2}, such that dom R_{1}^{1} ⊆ FV(S_{1} TE) and dom R_{1}^{2} ⊆ (FV(TE) ∪ New_{1}) \ FV(S_{1} TE). Then σ′ <_{R_{1}^{2}} R_{1}^{1}Gen(S_{1} TE, τ_{1}), since τ′_{1} = R_{1} τ_{1} and by splitting the substitution R_{1} into the two parts it is possible to handle all type variables in Gen(S_{1} TE, τ_{1}) (= σ for future abbreviation).

Since the type scheme used for x in e′_{2} is a generic instance of R_{1}^{1}σ it is possible to modify e′_{2} to e′′_{2} such that it can be typed with the type environment TE′_{x} ∪ {x : R_{1}^{1}σ} = R_{1}(S_{1} TE_{x} ∪ {x : σ}). (This is a trivial property proved in [Dam84] as lemma 3, p. 70.) The way e′_{2} is modified is by replacing each occurrence of x ι′ in e′_{2} by x ι′′, such that σ′ ι′ = (R_{1}^{1}σ) ι′′.

Now by the induction hypothesis W(S_{1}TE_{x} ∪ \{x : σ\}, \overline{e}_{2}) succeeds with (S_{2}, e_{2}, τ_{2}) and

TE′_{x} ∪ {x : R_{1}^{1}σ} ⊢ e′′_{2} ⪯_{R_{2}} S_{2} S_{1} TE_{x} ∪ {x : S_{2}σ} ⊢ e_{2}
TE′_{x} = R_{2} S_{2} S_{1} TE_{x}
R_{1}^{1}σ = R_{2} S_{2}σ

The last two lines are obtained by splitting the type environment.

We will now prove that there is an R such that

TE′ = R S_{2} S_{1} TE

and

TE′ ⊢ \underline{let} x : σ′ = Λβ⃗e′_{1} \underline{in} e′_{2} ⪯_{R} S_{2}S_{1}TE ⊢ \underline{let} x : S_{2}σ = S_{2}Λα⃗e_{1} \underline{in} e_{2}

i.e. realizing the ordering.

Let R_{1}^{0} be the restriction of R_{1}^{1} to those type variables which occur free in S_{1}TE but not in S_{1}TE_{x}. We will show that

R = R_{2} ∪ R_{1}^{0}

satisfies the above requirements. First let α be a type variable. If α occurs free in S_{1}TE_{x} then RS_{2}α = R_{2}S_{2}α = R_{1}α. Similarly if α occurs free in S_{1}TE but not in S_{1}TE_{x} then S_{2}α = α and thus RS_{2}α = Rα = R_{1}^{0}α = R_{1}α. So we have proved RS_{2}S_{1}TE = TE′. And that R_{1}^{1} and R_{2}S_{2} coincide on common domain elements.

Secondly note that the domain of R_{1}^{0} is disjoint from FV(S_{2} S_{1} TE_{x})∪New_{2} and for every instantiation ι, in connection with x:

σ′ ι′ = (R_{1}^{1}σ) ι′′ = R_{2} (S_{2}σ)(S_{2}S_{1} ι)
= R_{2} (S_{2}S_{1}σ)(S_{2}S_{1} ι) since S_{1}σ = σ
= R_{2}S_{2}S_{1}(σ ι)
= RS_{2}S_{1}(σ ι)

This allows us to replace e′′_{2} by e′_{2} to get:

TE′_{x} ∪ {x : σ′} ⊢ e′_{2} ⪯_{R} S_{2} S_{1}(TE_{x} ∪ {x : σ}) ⊢ e_{2}

Also the domain of R_{1}^{2} is disjoint from dom R_{2}S_{2} ⊆ FV(S_{1}TE_{x}) ∪ New_{2}, so it makes sense to write

TE′ ⊢ e′_{1} ⪯_{R_{2}S_{2}∪R_{1}^{2}∪R_{1}^{0}} S_{1} TE ⊢ e_{1}

or equivalently

TE′ ⊢ e′_{1} ⪯_{R_{1}^{2}} RS_{2}S_{1} TE ⊢ RS_{2}e_{1}

because R = R_{2} ∪ R_{1}^{0} and FV(rng S_{2}) is disjoint from dom R_{1}^{0}.

Finally σ′ <_{R_{1}^{2}} R(S_{2}S_{1}σ) because RS_{2}S_{1}σ = RS_{2}σ = R_{2}S_{2}σ = R_{1}^{1}σ, and R_{1}^{2} takes care of the bound type variables in σ.

We have now proved that W(TE,\overline{e}) succeeds with (S_{2}S_{1}TE, e, τ_{2}), and that TE′ ⊢ e′ really is smaller than S_{2}S_{1}TE ⊢ e because all the conditions in the definition of ⪯ for let-expressions have been satisfied.

□

5 First Order Generalization

In this section we develop an algorithm that for a pair of types finds their most specific generalizer. The section can be read independently, so readers who are willing to accept the results can skip it. Standard references in the literature to term-generalization are [Reynolds70] and [Plotkin70].

The most specific genralization (MSG) for a pair of types can be found by an algorithm resembling unification. In contrast to unification it is always possible to find an generalization, as every type can be formed by a trivial substitution from a type-variable. The matter of finding a least general upper bound, can roughly be said to fall into two parts, the first is to find a type which preserves as much structure from the types generalized; secondly to find the least number of variables necessary to fill out the gaps where the structures diverge.

When formalized as an algorithm for a pair of types, this becomes:

PairSubst = TyVar →^{fin} Type × Type AntiUnify : Type × Type → PairSubst → Type × PairSubst AntiUnify(τ, τ′) m =^{def} case (τ, τ′) of

(τ_{1} → τ_{2}, τ′_{1} → τ′_{2}) ⇒ let (ν_{1}, m_{1}) =AntiUnify(τ_{1}, τ′_{1}) m (ν_{2}, m_{2}) =AntiUnify(τ_{2}, τ′_{2}) m_{1}

in

(ν_{1} → ν_{2}, m_{2})

⇒ if τ = τ′ then (τ, m) else

if (τ, τ′) ∈ rng m then let

α be such, that m(α) = (τ, τ′) in

(α, m) else let

α be a fresh type variable in

(α, m ∪ [α ↦ (τ, τ′)])

The above stated algorithm takes a pair of types as argument, together with an injective map from type variables to pairs of types it produces a least general type. As a side effect the map produced keeps track of the substitutions yielding the respective types. By passing the map as an argument it is ensured that variables introduced in the antiunification are reused whenever possible.

That the algorithm really gives an MSG is stated an proven in the next lemma:

Lemma 1 Let m be an injective map from type variables to pairs of different types. Let τ_{1} and τ_{2} be types such that the domain of m is disjoint from the free type variables in rng m, τ_{1} and τ_{2}. Then:

(i) AntiUnify(τ_{1}, τ_{2}) m succeeds with (τ, m′), such that the first projection of m′ is a substitution when applied to τ gives τ_{1} and the second projection of m′, when applied to τ gives τ_{2}, i.e. τ is a generalization of τ_{1} and τ_{2}. (ii) For any other generalization τ′ of τ_{1} and τ_{2}, there is a substitution from τ′ to τ, i.e. the algorithm finds the most specific generalization.

Proof By induction on Σ(τ_{1}) + Σ(τ_{2}), where

Σ(τ) =^{def} case τ of π, α ⇒ 0

τ_{1} → τ_{2} ⇒ 1 + Σ(τ_{1}) + Σ(τ_{2})

We call the first projection of m θ_{1} and the second θ_{2}.

If at least one of τ_{1} and τ_{2} is a variable or a constant, the second branch of the algorithm is chosen. We also see that the sum (Σ) for one of τ_{1} or τ_{2} is zero. There are now three cases:

• τ_{1} = τ_{2}, i.e. both are the same constant or variable type. The algorithm returns (τ_{1}, m), and since dom m only consists of new variables θ_{1} τ_{1} = τ_{1} and θ_{2} τ_{2} = τ_{2}. Another generalization τ′, when different from τ_{1}, must be a type variable, and trivially, there is a substitution from τ′ to τ_{1}.

• τ_{1} ≠ τ_{2} and (τ_{1}, τ_{2}) ∈ rng m. The algorithm picks the variable α in the domain of m such that m(α) = (τ_{1}, τ_{2}), and returns (α, m). Clearly α is an upper bound, the projections of m reconstruct τ_{1} and τ_{2}, and it is also the least upper bound, since every other upper bound has to be a variable.

• τ_{1} ≠ τ_{2} and (τ_{1}, τ_{2}) ∉ rng m. A new type variable β is introduced and (β, [β ↦ (τ_{1}, τ_{2})] ∪ m) is returned. Clearly the returned map is well defined, injective on different elements and application of it on the returned type retrieves τ_{1} and τ_{2}. Like in the previous case β is the least upper bound for both types treated.

If both types are function types, then the first branch of the case split in the algorithm is used. In the decomposition of τ_{1} and τ_{2}, Σ gets smaller so we can use the induction hypothesis to assume that for τ_{1} = τ_{1}^{1} → τ_{1}^{2}, τ_{2} = τ_{2}^{1} → τ_{2}^{2}, AntiUnify(τ_{1}^{1}, τ_{2}^{1}) m = (ν_{1}, m′) and the projections of m′ on ν_{1} retrieve τ_{1}^{1} and τ_{2}^{1}. As m′ is still injective, again AntiUnify(τ_{1}^{2}, τ_{2}^{2}) m′ = (ν_{2}, m′′) and the projections θ_{1} and θ_{2} of m′′ on ν_{2} retrieve τ_{1}^{2} and τ_{2}^{2}. We will now show that ν_{1} → ν_{2} is a most specific generalization of τ_{1} and τ_{2}.

Since τ_{1} and τ_{2} are both function types a generalization has either to be a type variable α, in which case the trivial substitution [α ↦ ν_{1} → ν_{2}], shows that the returned type is more specific; or it is a function type ν′_{1} → ν′_{2}, with ψ_{1}(ν′_{1} → ν′_{2}) = τ_{1} and ψ_{2}(ν′_{1} → ν′_{2}) = τ_{2}. In this case we know that there are substitutions θ′_{1} when applied to ν′_{1} gives ν_{1} and θ′_{2} from ν′_{2} to ν_{2}. The substitutions will have to coincide on shared elements in the domains, otherwise suppose θ′_{1}(γ) ≠ θ′_{2}(γ) for some γ ∈ dom θ′_{1} ∩ dom θ′_{2}; we will see that this leads to a contradiction. In this case θ′_{i}(γ) at some place contains a variable α in the domain of (θ_{1}, θ_{2}), where θ′_{3−i}(γ) has a different term ν (i = 1 or i = 2). Since

(θ_{1}, θ_{2})θ′_{1}(γ) = (ψ_{1}, ψ_{2})(γ) = (θ_{1}, θ_{2})θ′_{2}(γ)

it must also hold that (θ_{1}, θ_{2})(α) = (θ_{1}, θ_{2})(ν).

• ν and α cannot both be variables in the domain of (θ_{1}, θ_{2}), since ν ≠ α and (θ_{1}, θ_{2}) is injective.

• If ν is a constant type or a variable not in the domain of (θ_{1}, θ_{2}), then (θ_{1}, θ_{2})ν = (ν, ν) so θ_{1}α = θ_{2}α a contradiction.

• If ν is ν_{1} → ν_{2}, θ_{i}α = θ_{i}ν_{1} → θ_{i}ν_{2} (i = 1, 2), suggesting that both τ_{1} and τ_{2} contained functiontypes where α was introduced, a contradiction.

It has hereby been shown that θ′_{1} and θ′_{2} can be joined to form a substitution from τ′ to τ. □ The lemma easily generalizes when the algorithm antiunifies type-schemes and even nonempty lists of types/type-schemes. And in the consequent we will write AntiUnify⟨τ_{1}, …, τ_{n}⟩ for the MSG of τ_{1} to τ_{n}.

6 Algorithm M

The algorithm described in this section takes an explicitly typed expression, annotated by for instance W, and returns another annotation with the same type. It is proved that the annotation found gives a least element in the ordering ⪯ for expressions, if there are no typing derivations for the expression that introduce cut-type variables. This means that any other well formed annotation or typing derivation resulting in the same type subsumes the annotation found by M.

In the presence of cut-type variables the matter is very different and takes a separate treatment in the next section.

6.1 The algorithm

The underlying idea of M is quite simple: A recursive descent through the expression collects for each let bound variable all of its type instantiations (the ι’s). When these instantiations are applied to the type scheme a list of types is formed. Using antiunification on this list makes it is possible to extract a least general type scheme for the let bound variable.

There is however a more subtle part to the algorithm. We also have to keep track of otherwise bound type variables, which is done by the set BV. This is done to handle the situation where all instatiations ι of a given type scheme σ at the same location contain the same type variable β from BV. If we performed antiunification on all these instantiations, we would end up with a generalizer containing β, and only the set BV can indicate that we have to perform type-abstraction over β. If type abstraction is ignored, the resulting type annotation will not be well-formed. Furthermore, due to our special requirements for well formedness, we also rename the variable β to ensure that variables are bound at most at one place. We also here see the reason for doing this, since it avoids confusion about where the bound variabels in BV belong. The following example illustrates the situation described:

\underline{let} id_{1} = λx.x \underline{in}
\underline{let} id_{2} = id_{1} \underline{in}
(id_{2} 3, id_{2} 3.14)

The variable id_{2} will need a polymorphic type ∀β.β → β, but id_{1} will only be instantiated to one type variable, namely β. If we did not record that β was bound otherwise, id_{1} would be given the monomorphic type β → β and β would be free in the type environment surrounding id_{2}, obviously illegal w.r.t. our inference rules.

A collection of instances can be represented as a map from variables to lists of instantiations. An asymmetrical union is defined on these:

A ∈ InstEnvironment = Var →^{fin} Instantiation^{∗}

A + A′ =^{def} [x ↦ A(x) A′(x)]

where is list appending and, A(x) is defined to be the empty list, if x ∉ dom A. The main algorithm is presented in the following figure:

M : Expr → Expr × InstEnvironment ×TyVar−set M(e) =^{def} case e of

x ι ⇒ (e, [x ↦ ⟨ι⟩], { })

λx : τ.e_{1}⇒ let (e′_{1}, A, BV) = M(e_{1}) in (λx : τ.e′_{1}, A \ {x}, BV)
e_{1} e_{2} ⇒ let

(e′_{1}, A_{1}, BV_{1}) = M(e_{1}) (e′_{2}, A_{2}, BV_{2}) = M(e_{2})

in

(e′_{1} e′_{2}, A_{1} + A_{2}, BV_{1} ∪ BV_{2})

\underline{let} x : ∀α⃗.τ = Λα⃗ e_{1} \underline{in} e_{2} ⇒

let (e′_{2}, A_{2}, BV_{2}) = M(e_{2}) ⟨τ_{1}, …, τ_{n}⟩ = if x ∈ dom A_{2} then map (λi.(∀α⃗.τ) i) A_{2}(x) else ⟨τ⟩ (τ′, m) = AntiUnify⟨τ_{1}, …, τ_{n}⟩ {γ_{1}, …, γ_{m}} = FV(τ′) ∩ BV_{2} γ′_{1}, …, γ′_{m} be new variables. τ′′ = [γ_{i} ↦ γ′_{i}]τ′ θ = unifyα⃗(τ, τ′′) β⃗ = if x ∈ dom A_{2} then dom m ∪ {γ′_{1}, …, γ′_{m}} else α⃗ (e′_{1}, A_{1}, BV_{1}) = M(θ e_{1})

in (\underline{let} x : ∀β⃗.θτ = Λβ⃗ e′_{1} \underline{in} subst(x, θ, β⃗, e′_{2}), A_{1} + (A_{2} \ \{x\}), BV_{1} ∪ BV_{2} ∪ β⃗)

The function subst returns the updated instantiations for the new type-scheme of x. We introduce a special notation in connection with the use of standard first order unification. A subscript β⃗ denotes the set of the only type variables which can be treated as variables during unification. The function subst can now be defined as follows:

subst : Var × Substitution × TyVar-set × Expr → Expr subst(x, θ, β⃗, e) =^{def} case e of

x′ ι′ ⇒ if x = x′

then x ⋃{unifyβ⃗(θ α, ι′ α)| α ∈ dom θ}
else e

λx′ : τ.e_{1} ⇒ if x = x′

then λx′ : τ.e_{1}
else λx′ : τ.subst(x, θ, β⃗, e_{1})

e_{1} e_{2} ⇒ subst(x, θ, β⃗, e_{1}) subst(x, θ, β⃗, e_{2})

\underline{let} x′ : σ = Λα⃗ e_{1} \underline{in} e_{2} ⇒ if x = x′

then \underline{let} x′ : σ = Λα⃗ subst(x, θ, β⃗, e_{1}) \underline{in} e_{2}
else \underline{let} x′ : σ = Λα⃗ subst(x, θ, β⃗, e_{1}) \underline{in} subst(x, θ, β⃗, e_{2})

In the comming sections we show that M is correct, in the sense that it returns a well formed expression with the same type, and when all type variables used in the annotation of the expression are visible in its type or type environment, the algorithm really produces the least annotation possible.

6.2 Soundness of M

In the following lemmas we will refer to what we call: internal and external types: The external type τ of an expression e w.r.t. a type-environment TE is its type (i.e. TE ⊢ e : τ holds). The internal types of an expression are the external types of the subexpressions.

We furthermore write M(e) to denote the expression returned by the algorithm M.

The first lemma shows that subst works appropriately. It states that when M reaches a let-expression and computes θ and β⃗ then (i) the new expression subst(x, θ, β⃗, e_{2}) is well formed under the type environment TE_{x} ∪ {x : ∀β⃗.τ′′}, (ii) the new expression has the same internal types as e_{2} under TE_{x} ∪ {x : ∀α⃗.τ}.

This is phrased a bit more general in the formulation of the lemma:

Lemma 2 Let σ = ∀α⃗.τ, σ′ = ∀β⃗.τ′ and BV be the set of bound type variables in the expression e. Furthermore let ι_{1}, …, ι_{n} be the instantiations of the type-scheme σ of the variable x in e. If

1. TE_{x} ∪ {x : σ} ⊢ e : ν

2. FV(σ′) is disjoint from BV

3. σ′ <_{θ} σ and each of ι_{1}τ to ι_{n}τ is an instance of σ′

then

1. TE_{x} ∪ {x : σ′} ⊢ subst(x, θ, β⃗, e) : ν

2. The internal types of subst(x, θ, β⃗, e) under TE_{x}∪{x : σ′} are the same as those of e under TE_{x}∪{x : σ}.

Proof by induction on the structure of \overline{e}.

• e = x′ ι, if x ≠ x′, subst leaves the expression unchanged, so the result is trivial. If x = x′ we have:

ι = [α_{1} ↦ τ_{1}, …, α_{n} ↦ τ_{n}]

Since ιθ is an instance of ∀β⃗.θτ there is a unifier ψ of ιθ and θτ such that ψτ′ = ψθτ = ιτ.

The domain of the unifier is β⃗. Therefore ψ = unifyβ⃗(θτ, ιτ) = ⋃{unifyβ⃗(θα, ια)| α ∈ dom θ}. The last equality sign is justified as the unified types θτ and ιτ only differ with respect to the range of θ and ι: since ιτ = ψθτ it must also be the case that ια = ψθα for each α ∈ dom ι (= dom θ) and that the unifiers unifyβ⃗(θα, ια) coincide with ψ on common domain elements.

• e = λx′ : ν_{1}.e_{1}, if x = x′ then x does not occur free in e and the expression is left unchanged so there is nothing to prove; if x ≠ x′ then as we let ν = ν_{1} → ν_{2}, by the induction hypothesis:

TE_{x} ∪ {x : ∀β⃗.τ′, x′ : ν_{1}} ⊢ subst(x, θ, β⃗, e_{1}) : ν_{2}

holds, besides that the internal types are preserved, so it must also be the case that

TE_{x} ∪ {x : ∀β⃗.τ′} ⊢ λx′ : ν_{1}.subst(x, θ, β⃗, e_{1}) : ν

• e = e_{1} e_{2}, two trivial applications of the induction hypothesis give the result.

• e = \underline{let} x′ : σ′′ = Λγ⃗ e_{1} \underline{in} e_{2}. If x = x′ then σ′ is only used as type-scheme for x in e_{1} (σ′′ is used in e_{2}), subst should therefore only be applied to e_{1}. If x ≠ x′ we have to apply subst two places.

In both cases we have to convince ourselves that the expressions are well formed (internal type equality is evident by simple induction). Before application of subst the variables in γ⃗ were not free in the surrounding type environment TE_{x} ∪ {x : ∀α⃗.τ}, we shall see that they are not free in the updated TE_{x} ∪ {x : σ′} either. This allows type abstraction on the variables in γ⃗.

But the variables from γ⃗ is a subset of the set BV of variables bound inside e, and since these are not free in σ′ we have assured that no variable from γ⃗ is free in the new type environment. It is therefore still legal to perform the type abstraction done.

□ It is easy to see that ∀α⃗.τ together with the type-scheme ∀β⃗.θτ computed in M satisfies the requirements in the lemma. Also ∀β⃗.θτ is the most specific type-scheme that will meet these requirements, because it is found by anti-unification of all the instantiations used, followed by only necessary renaming and binding of variables in BV.

Lemma 2 enables us to prove the soundness of M:

Theorem 4 (Soundness of M)

If TE ⊢ e : τ then TE ⊢ M(e) : τ

Proof by structural induction on \overline{e}, where the only nontrivial case is for let-expressions, thus e is of the form \underline{let} x : ∀α⃗.ν = Λα⃗ e_{1} \underline{in} e_{2} and we have the assumption TE ⊢ e : τ. Recursive calls of M produces the expressions e′_{1} and e′_{2}, the set β⃗ = dom m or α⃗ and the substitution θ.

By the standard substitution theorem and, the fact that dom θ ∩ FV(TE) = { }, (since dom θ = α⃗ and generalization upon free variables in the type environment is excluded) we have:

TE ⊢ θe_{1} : θν

which by the induction hypothesis gives

TE ⊢ e′_{1} : θν

The induction hypothesis furthermore ensures

TE_{x} ∪ {x : ∀α⃗.ν} ⊢ e′_{2} : τ

which by lemma 2, ensures that:

TE_{x} ∪ {x : ∀β⃗.θν} ⊢ subst(x, θ, β⃗, e′_{2}) : τ

implying that the final result is well typed with type τ:

TE ⊢ \underline{let} x : ∀β⃗.θν = e′_{1} \underline{in} subst(x, θ, β⃗, e′_{2}) : τ

□

6.3 Cut-type variables and internal equality

For the next result we need to capture the notion of cut-type variables and internal type equality not in between \underline{let} and \underline{in}. We will treat these two concepts in each their subsections before we state and prove a result connecting these.

6.3.1 cut-type variables

Informally a cut-type variable is a type variable which occurs as a free variable in one of the internal types, but not in the external type or type environment. To make this definition a bit more precise we first define the (free) type variables of an expression with respect to a type environment:

TV(TE,e) =^{def} case e of x ι ⇒ FV(TE(x)ι)

e_{1} e_{2} ⇒ TV(TE,e_{1}) ∪ TV(TE, e_{2})
λx : τ.e′ ⇒ FV(τ) ∪ TV(TE_{x} ∪ {x : τ}, e′)
\underline{let} x : ∀α⃗.τ = Λα⃗ e_{1} \underline{in} e_{2} ⇒ TV(TE,e_{1})\α⃗ ∪ TV(TE_{x} ∪ \{x : ∀α⃗.τ\}, e_{2})

It is trivial to verify that if TE ⊢ e : τ then FV(τ) ⊆ TV(TE, e). The subset relationship cannot in general be extended to equality: FV(τ) = TV(TE, e), since there are expressions for which TV(TE,e)\FV(τ) is nonmenpty (consider { } ⊢ (λx : α → α.1) (λx : α.x) : int ). Some elements in TV(TE,e)\FV(τ) may be free in the type environment, so these cannot be replaced by substitution without affecting the type environment. This leads to the notion of cut-type variables. For the expression e, typed under TE, resulting in the external type τ (i.e. TE ⊢ e : τ holds), the set of cut-type variables is:

TV(TE, e) \ (FV(τ) ∪ FV(TE))

If for all annotations (under the same type environment TE) for an expression \overline{e} resulting in the same external type τ the set of cuttype variables is empty, or restated:

TV(TE, e) ⊆ FV(τ) ∪ FV(TE)

(where e ranges over all annotations of \overline{e}) then this really limits the possibilities for annotations as theorem 6 states.

First we notice that if this property holds for all expressions at the outermost level it will hold for all subexpressions (with updated type environments): To see this consider for a contradiction a typing derivation for TE ⊢ \overline{e} : τ, where there at some point is a cut-type variable. Give this cut-type variable a new name (γ_{new}) not found free in TE or τ and redo the derivation, where we avoid Λ abstraction over γ_{new}. Clearly this new derivation determines an annotated expression e with the external type τ, containing the cut-type variable γ_{new} ∈ TV(TE,e) but γ_{new} ∉ FV(TE) ∪ FV(τ); contradicting that no annotations had cut-type variables.

Now when do cut-type variables occur? For ML with let expressions it is not so straightforward to give a simple classification of expressions with or without cut-type variables, but for monomorphically typeable expressions of the λ-calculus, without let-constructions, it is easy to find sufficient criteria for excluding cut-type variables: expressions in strong normal form are not typeable with cut-type variables. This (in light of Gentzen’s Hauptsatz trivial) fact is proven in the next theorem. But first let us remind ourselves of the syntax of expressions (here called se) in strong normal form:

\begin{aligned}se & ::= & λx : τ.se | es \\ es & ::= & es se | x \end{aligned}

notice that x has no associated instantiation since the type environment only contains pure types.

Theorem 5 We make the stronger statement:

1. If e is of the form es typeable under TE, then TV(TE, e) ⊆ FV(TE)

2. If e is of the form se typeable under TE, resulting in the external type τ (i.e. TE ⊢ e : τ), then TV(TE, e) ⊆ FV(TE) ∪ FV(τ)

Proof By induction over \overline{e}.

• e = x. The variable x must then be in the domain of the type environment, and its type, and therefore its type variables, is found in the environment.

• e = es se. TE ⊢ e : τ i.e. TE ⊢ es : τ_{1} → τ and TE ⊢ se : τ_{1}. By the induction hypothesis TV(TE,es) ⊆ FV(TE) and TV(TE,se) ⊆ FV(TE) ∪ FV(τ_{1}). But since FV(τ_{1}) ⊆ TV(TE, es) also TV(se) ⊆ FV(TE), hence TV(TE, e) ⊆ FV(TE).

• e = λx : τ_{1}.se. We therefore have TE ⊢ e : τ_{1} → τ_{2}, by applying the induction hypothesis to TE_{x} ∪ {x : τ_{1}} ⊢ se : τ_{2}, which states that TV(TE_{x} ∪ {x : τ_{1}}, se) ⊆ FV(TE_{x} ∪ {x : τ_{1}}) ∪ FV(τ_{2}), we can conclude TV(TE, e) ⊆ FV(TE) ∪ FV(τ_{1} → τ_{2})

□

The theorem suggests that cut-type variables come in connection with β−redexes. Moreover, because a cut-type is freely instantiable to any type without affecting the resulting type of a program, one may say that presence of cut-types represent dead code.

Since let constructions introduce type-schemes and a kind of β−redexes we cannot apply the results of this theorem to full ML, but only use the theorem as a hint that cut-type variables come from dead code.

Although it is not so easy to give a simple characterization of a generic class of ground expressions, that do not have derivations with cut-type variables, it is possible to decide whether a given ground expression allows cut-type variables. By the generalized completeness theorem, the annotation obtained from W subsumes any other annotation by substitutions. It therefore happens to be enough to investigate W(TE,\overline{e}) for two things to see whether there are cut-type variables. 1: Cut-type variables may be in the resulting expression obtained from W(TE,\overline{e}). 2: If there are unused let bound variables that have associated type-schemes involving quantified variables one can skip quantification and get a cut-type variable. Hence it is an easy decision whether a ground expression has derivations with cut-type variables.

6.3.2 Internal equality ≈

To capture what we mean by that internal types of subsexpressions not in between \underline{let} and \underline{in} coincide, we introduce the equivalence relation ≈ for annotated expressions (with associated type environments):

• TE ⊢ x ι  ≈ TE′ ⊢ x ι′  iff TE(x)ι = TE′(x)ι′
• TE ⊢ e_{1} e_{2} ≈ TE′ ⊢ e′_{1} e′_{2}  iff TE ⊢ e_{1} ≈ TE′ ⊢ e′_{1} ∧ TE ⊢ e_{2} ≈ TE′ ⊢ e′_{2}
• TE ⊢ λx : τ.e ≈ TE′ ⊢ λx : τ′.e′ iff TE_{x} ∪ {x : τ} ⊢ e ≈ TE′_{x} ∪ {x : τ′} ⊢ e′ ∧ τ = τ′
• TE ⊢ \underline{let} x : σ = Λα⃗ e_{1} \underline{in} e_{2} ≈ TE′ ⊢ \underline{let} x : σ′ = Λα⃗′ e′_{1} \underline{in} e′_{2}
iff TE_{x} ∪ {x : σ} ⊢ e_{2} ≈ TE′_{x} ∪ {x : σ′} ⊢ e′_{2}

It is easy to see that if TE ⊢ e ≈ TE′ ⊢ e′, then the external type of e under TE is the same as the external type of e′ under TE′.

6.3.3 Equivalence of cut-type variable free expressions

We are now ready to state the next theorem. We assume that no annotation for \overline{e} (in a given type environment TE resulting in the type τ) have cut-type variables. By this assumption it is proven that all these annotations are equivalent under ≈.

Theorem 6 Let an expression e, a type τ and a type environment TE be given. If for all annotations e of \overline{e} under TE, such that TE ⊢ e : τ, it is the case that:

TV(TE, e) ⊆ FV(τ) ∪ FV(TE)

then for an arbitrary pair of annotations e, e′ of \overline{e}, such that TE ⊢ e : τ and TE ⊢ e′ : τ, the internal annotations will coincide:

TE ⊢ e ≈ TE ⊢ e′

Proof The proof is carried through by structural induction on \overline{e}. We recall that for e and e′ we have:

TE ⊢ e : τ  TE ⊢ e′ : τ
TV(TE, e) ⊆ FV(τ) ∪ FV(TE) TV(TE, e′) ⊆ FV(τ) ∪ FV(TE)

The cases are treated as follows:

• e is a variable. In which case the internal type is the external type, and there is nothing to prove.

• e = λx : τ_{1}.e_{1}, e′ = λx : τ′_{1}.e′_{1}. As they have the same external type τ = τ_{1} → τ_{2} = τ′_{1} → τ′_{2}, it must hold that τ_{1} = τ′_{1} and τ_{2} = τ′_{2}, hence we can apply the induction hypothesis on TE_{x} ∪ {x : τ_{1}} ⊢ e_{1} : τ_{2} and TE_{x} ∪ {x : τ_{1}} ⊢ e′_{1} : τ_{2}, which says that TE_{x} ∪ {x : τ_{1}} ⊢ e_{1} ≈ TE_{x} ∪ {x : τ_{1}} ⊢ e′_{1}, to obtain the result.

• e = \underline{let} x : σ = Λα⃗ e_{1} \underline{in} e_{2}, e′ = \underline{let} x : σ′ = Λβ⃗ e′_{1} \underline{in} e′_{2}. By the principal typing property of W there is a type-scheme σ_{p} = ∀α⃗_{p}.ν_{p} for \overline{e}_{1} under TE more general than σ = ∀α⃗.ν and σ′ = ∀β⃗.ν′. There are therefore substitutions ψ_{1} and ψ_{2}, such that ν = ψ_{1}ν_{p} and ν′ = ψ_{2}ν_{p}.

Now ν_{p} is a generalization of all the instantiations of x in e_{2} respectively e′_{2}, also no bound type variables from e_{2} or e′_{2} are free in ∀α⃗_{p}.ν_{p}. (why? if a variable is free in ∀α⃗_{p}.ν_{p}, it will also be free in all of its generic instances, in particular in σ and σ′, a contradiction.)

We can therefore assume the existence of expressions e_{3} and e′_{3}, where e_{3} is equal to e_{2} except for the instantiations of x which are changed to suit ∀α⃗_{p}.ν_{p} instead of σ. The relation between e′_{2} and e′_{3} is similar. We therefore have: subst(x, ψ_{1}, α⃗, e_{3}) = e_{2} and subst(x, ψ_{2}, β⃗, e′_{3}) = e′_{2}.

It is now possible to reason as follows:

TE_{x} ∪ {x : σ} ⊢ e_{2}

is by lemma 2 ≈ to:

TE_{x} ∪ {x : σ_{p}} ⊢ e_{3}

which by the induction hypothesis is ≈ to:

TE_{x} ∪ {x : σ_{p}} ⊢ e′_{3}

which as again by lemma 2 is ≈ to:

TE_{x} ∪ {x : σ′} ⊢ e′_{2}

• e = e_{1} e_{2}, e′ = e′_{1} e′_{2} i.e. TE ⊢ e_{1} : τ_{1} → τ, TE ⊢ e_{2} : τ_{1}, TE ⊢ e′_{1} : τ′_{1} → τ and TE ⊢ e′_{2} : τ′_{1}. By the principal typing property of W \overline{e}_{1} and \overline{e}_{2} have principal annotation resulting in external types τ_{1p} and τ_{2p}, i.e. there are derivations justifying TE ⊢ \overline{e}_{1} : τ_{1p} and TE ⊢ \overline{e}_{2} : τ_{2p}, and there are substitutions from τ_{1p} to τ_{1} → τ and τ′_{1} → τ respectively from τ_{2p} to τ_{1} and τ′_{1}, that do not involve variables from TE in their domains.

Let τ_{c} = AntiUnify(τ_{1}, τ′_{1}), then clearly there are substitutions θ, θ′ and ψ_{2} such that ψ_{2}τ_{2p} = τ_{c}, θψ_{2}τ_{2p} = θτ_{c} = τ_{1} and θ′ψ_{2}τ_{2p} = θ′τ_{c} = τ′_{1}, since τ_{2p} is an upper bound and τ_{c} is the least upper bound. Note also that the variables in the domains of θ and θ′ is the set of new variables introduced by anti-unification, they can therefore only affect variables in τ_{c}. Moreover τ_{c} → τ is the least upper bound for τ_{1} → τ and τ′_{1} → τ so there must be a substitution ψ_{1} from τ_{1p} to τ_{c} → τ. All these substitutions are by the principal typing property the identity on TE.

We have now justified the existence of derivations for TE ⊢ \overline{e}_{1} : τ_{c} → τ and TE ⊢ \overline{e}_{2} : τ_{c}. (This is a consequence of the substitution theorem.) For reference call the associated annotated expressions e_{1c} and e_{2c}.

Now FV(τ_{c}) ⊆ TV(TE, e_{2c}) ⊆ TV(TE, e_{1c} e_{2c}) ⊆ FV(TE) ∪ FV(τ), as the last inclusion is obtained by our global assumption about all annotations resulting in the type τ. So θ and θ′ such that θ(τ_{c} → τ) = τ_{1} → τ and θ′(τ_{c} → τ) = τ′_{1} → τ have to be the identity on FV(TE) ∪ FV(τ) and thus also on the variables in τ_{c}. Hence τ_{1} = τ_{c} = τ′_{1}.

We can now apply the induction hypothesis to e_{1} and e_{2} and draw the desired conclusion.

□

6.4 Relative Completeness of M

We are now ready to state and prove the main theorem about algorithm M. It states that the annotation obtained by M is indeed the smallest possible, when there are no cut type variables.

Theorem 7 (Relative completeness of M) Let \overline{e} be typeable with external type τ in a given type environment TE. If there are no annotations for \overline{e} (resulting in the external type τ) with cut-type variables, then M finds the minimal annotation w.r.t. the ordering ⪯, that preserves the external type τ.

Like in the previous theorem we compare two arbitrary annotations e and e′ of \overline{e} satisfying:

TE ⊢ e : τ, TE ⊢ e′ : τ

and show that:

TE ⊢ M(e) ⪯_{id} TE ⊢ e′

The theorem is proven in this setting. Proof by structural induction on \overline{e}.

The case where e and e′ are variables is a trivial base case, and abstractions are equally trivial to verify using the induction hypothesis.

When e is e_{1} e_{2} and e′ is e′_{1} e′_{2}, we observe by the previous theorem, that e_{1} and e′_{1} have the same external type τ_{1} → τ, as well as e_{2} and e′_{2} both have type τ_{1}. It is therefore possible to employ straight forward induction.

The only real nontrivial case is of no surprise where e and e′ are let constructions, i.e. we have TE ⊢ \underline{let} x : σ = Λα⃗ e_{1} \underline{in} e_{2} : τ and TE ⊢ \underline{let} x : σ′ = Λγ⃗ e′_{1} \underline{in} e′_{2} : τ, where σ = ∀α⃗.ν and σ′ = ∀γ⃗.ν′. By the principal typing property a principal type-scheme, say σ_{p} = ∀α⃗_{p}.ν_{p}, is associated with \overline{e}_{1} under TE. On this type-scheme there are two substitutions ψ_{1} and ψ_{2} with the properties: ν = ψ_{1}ν_{p} and ν′ = ψ_{2}ν_{p}. Instead of using σ and σ′ to type e_{2} and e′_{2}, one could use σ_{p} on expressions e_{3} and e′_{3} in which only the instantiation of x had been changed from e_{2} and e′_{2} (like done in the proof of the previous theorem). More precisely the expressions would be interrelated as:

subst(x, ψ_{1}, α⃗, e_{3}) = e_{2}
subst(x, ψ_{2}, γ⃗, e′_{3}) = e′_{2}

moreover:

TE_{x} ∪ {x : σ_{p}} ⊢ M(e_{3}) = TE_{x} ∪ {x : σ} ⊢ subst(x, ψ_{1}, α⃗, M(e_{3})) = TE_{x} ∪ {x : σ} ⊢ M(e_{2}) (∗)

as we use lemma 2 for the first equality and since e_{2} and e_{3} only differ with respect to the type-scheme of x, we can justify the second equality.

Recursive calls of M on e_{2} also result in the substitution θ and the set of typevariables β⃗, used in the resulting expression, where we can reason:

TE_{x} ∪ {x : ∀β⃗.θν} ⊢ subst(x, θ, β⃗, M(e_{2})) =  by lemma 2
TE_{x} ∪ {x : σ} ⊢ M(e_{2}) = by (∗)
TE_{x} ∪ {x : σ_{p}} ⊢ M(e_{3})  ⪯_{id} by the induction hypothesis
TE_{x} ∪ {x : σ_{p}} ⊢ e′_{3} = by lemma 2
TE_{x} ∪ {x : σ′} ⊢ e′_{2}

The subscript id on ⪯ is justified as M(e_{3}) and e′_{3} are typeable under the same type environment TE∪{x : σ_{p}} resulting in the same type τ. For since TV(TE_{x} ∪ {x : σ_{p}}, e′_{3}) ⊆FV(TE_{x} ∪ {x : σ_{p}}) ∪ FV(τ) (there are no cut-type variables) it is not possible to substitute on free variables in e′_{3} without affecting the type environment or external type, i.e. the substitution has to be id.

Consequently every type τ_{i} associated with x in subst(x, θ, β⃗, M(e_{2})) is an instance of the corresponding type τ′_{i} in e′_{2}. As we noted in connection with the justification of ⪯_{id}, all variables in TV(TE∪{x : σ′}, e′_{2}) ⊆ FV(TE_{x} ∪ {x : σ′}) ∪ FV(τ) are left unchanged. So the substitutions ψ_{i} from τ′_{i} to τ_{i} (ψ_{i}τ′_{i} = τ_{i}) do not contain variables from FV(TE_{x} ∪ {x : σ′}) ∪ FV(τ). Hence, since every τ′_{i} is an instance of σ′, also every τ_{i} must be an instance of σ′.

From ∀β⃗.θν = σ′′ there were instantiations to τ_{1}, …, τ_{n}, and recall that σ′′ was the most specific typescheme one could use for τ_{1}, …, τ_{n}. As we have just shown that we also could use σ′ as type-scheme, we have σ′′ < σ′.

Since ∀β⃗.θν = σ′′ < σ′ = ∀γ⃗.ν′, there is a substitution θ′ with domain a subset of γ⃗ such that θν = θ′ν′, i.e. realizing σ′′ <_{θ′} σ′. We can therefore reason as follows:

TE ⊢ M(θe_{1}) ⪯_{id} by the induction hypothesis
TE ⊢ θ′e′_{1}  ⪯_{θ′} since dom θ′∩ FV(TE) = { }
TE ⊢ e′_{1}

In summary we have shown that:

TE ⊢ M(e) ⪯_{id} TE ⊢ e′

which completes this case, and hereby the proof. □

The theorem was stated and proven for any derivable type τ for \overline{e}. In particular if we want to find the minimal annotation for \overline{e}, supporting the principal typing of \overline{e}, we can compose M with W.

7 Presence of cut-type variables

Algorithm M was only shown to give the minimal annotation for expressions without cut type variables. This crucial condition (and thereby theorem 6) was only used to perform induction on applications and a single place for \underline{let} constructions. From the limited use of theorem 6, it might seem that the extra condition could be avoided, but as we will see, examples show that there are expressions with several incomparable minimal annotations.

The reason for this is that the cut-type variables can be instantiated to any (ground) type without affecting the external type of the expression. With respect to the ordering ⪯ there are therefore infinitely many minimal incomparable annotations for expressions with cut-type variables.

In the first place one could try to relax the ordering ⪯ to a weaker ordering ⪯′ given below:

• x ι  ⪯′_{θ} x ι′  always
• e_{1} e_{2}  ⪯′_{θ} e′_{1} e′_{2}  iff e_{1} ⪯′_{θ} e′_{1} ∧ e_{2} ⪯′_{θ} e′_{2}
• λx : τ.e  ⪯′_{θ} λx : τ′.e′  iff e ⪯′_{θ} e′
• \underline{let} x : σ = Λα⃗ e_{1} \underline{in} e_{2} ⪯′_{θ} \underline{let} x : σ′ = Λα′ e′_{1} \underline{in} e′_{2}
iff x ∈ FV(e_{2}) ∧ e_{2} ⪯′_{θ} e′_{2} ∧ ∃θ′ · e_{1} ⪯′_{θ′} θe′_{1} ∧ σ <_{θ′} θσ′ ∨
x ∉ FV(e_{2}) ∧ e_{2} ⪯′_{θ} e′_{2}

We see that the ordering ⪯′ only compares the type-schemes associated with let bound variables.

By using this ordering one could hope for a better result, but as examples show, there can still be a set of minimal incomparable typings and there can even be no minimal annotation at all.

7.1 Examples

To simplify the layout of the examples we now allow pairs of expressions, and projections, as an extra construct of the language. Correspondingly products of types are introduced. This is however a nonsignificant addition to the language, as a trivially modified M and the previous proofs carry through without problems, with this addition. One can also choose to define (x, y) =^{def} λz.z x y and π_{1}x =^{def} x λx.λy.x, π_{2}x =^{def} x λx.λy.y, whereby the language is not augmented.

An example (example 1) where there is a minimal annotation, but where M might fail to find it, is given below:

\underline{let}

id = λx.x

\underline{in}

π_{2}(λz.id z, id 3)

which can be minimally annotated:

\underline{let}

id : int → int = λx : int.x

\underline{in}

π_{2}(λz : int.id z, id 3) : int

but when W is applied to the expression, the type bound to z is a fresh type variable. M then returns:

\underline{let}

id : ∀α_{1}.α_{1} → α_{1} = λx : α_{1}.x

\underline{in}

π_{2}(λz : α_{2}.id[α_{2}] z, id[int] 3) : int

The example suggests that it is possible to reduce polymorphism when W returns type variables invisible in the external type, simply by instantiating those type variables appropriately.

The next example (no. 2) removes all hope that a trivial modification of M can find the minimal annotation. It shows that in general there are no unique minimal annotations, but a set of minimal incomparable typings.

\underline{let}

f = λx.x,
g = λx.(x, x)

\underline{in}

π_{2}(λx_{1}.((f x_{1}, f 3), (g x_{1}, g true)), 4)

which can have the two (incomparable) minimal annotations:

\underline{let}

f : ∀α.α → α = λx : α.x,
g : bool → bool × bool = λx : bool.(x, x)

\underline{in}

π_{2}(λx_{1} : bool.((f [bool] x_{1}, f [int] 3), (g x_{1}, g true)), 4) : int

and

\underline{let}

f : int → int = λx : int.x,
g : ∀β.β → β × β = λx : β.(x, x)

\underline{in}

π_{2}(λx_{1} : int.((f x_{1}, f 3), (g [int] x_{1}, g [bool] true)), 4) : int

Sometimes there may be no minimal annotation at all. An illustration of this is in the final example (example 3):

\underline{let}

id = λx.x,

\underline{in}

π_{2}(λx_{1}.(id x_{1}, id λx_{2}.π_{1}(x_{1}, x_{2} + 1)), 0)

in which id can be typed:

∀α.α → α

> ∀α.(int → α) → (int → α)

> ∀α.(int → (int → α)) → (int → (int → α))

> ∀α.(int → (int → (int → α))) → (int → (int → (int → α)))

> …

The examples, however unrealistic they may be as real programs, illustrate how nasty the problem of finding a minimal annotation gets when one allows arbitrary instantiations of cut-types.

In the section introducing cut-type variables we demonstrated that cut-type variables do not occur in programs in normal form. However we can say much more than that. Where the computations do not invole sideeffects cut-type variables reflect dead code i.e. redundant computation. It is questionable whether the chance of finding such programs in real life is realistic. The problem of finding a least annotation subsuming all minimal incomparable (example 2) and stopping at the top step of the descending chains (ex. 3), is therefore less attractive to solve. A guideline how to solve it is given in the appendix, for those very curious to see it. However the treatment given there is so complex, because of its many special cases that it only gives very little insight in this form. Instead we prefer to give a short informal argument why example 2 and 3 are generic in the sense that they represent all the ways an expression may fail to have minimal annotations.

7.2 Two ways to fail minimality

For this dicussion it suffices to focus at one particular type-scheme σ associated with a let bound variable x. Let τ_{1}, …, τ_{n} be the types σ gets instantiated to.

Now anti-unification of τ_{1}, …, τ_{n} finds a type τ subsuming all of τ_{1} to τ_{n}, however it fails to instantiate cut-type variables in τ_{1} to τ_{n} to other types, which could lead to a more refined generalization τ′. This was illustrated in the first example. We repeat by another example: Consider the types π_{1} → π_{2}, π_{3} → π_{4} and γ, where γ is a cut-type variable and π_{1} − π_{4} are type constants. If we instantiate γ to a function type γ_{1} → γ_{2}, we would have the antiunifier α_{1} → α_{2}, instead of α_{1}.

We therefore look for a substitution S of the cut-type variables in τ_{1}, …, τ_{n} such that Sτ_{1}, …, Sτ_{n} is least possible w.r.t. the substitution subsumption ordering on terms. S is in fact a kind of unifier, however we do not require that Sτ_{1} = … = Sτ_{n}, but only that AntiUnify⟨Sτ_{1}, …, Sτ_{n}⟩ is least possible.

Now examples 2 and 3 show that it is not always possible to find such an S. The reasons are the same that make unification fail: “name-clash” and “occurs-check”.

Example 2 illustrates “name-clash”, which also can be illustrated by the instatiated types τ_{1} : γ → γ, τ_{2} : π_{1} → π_{2} where γ is a cut-type variable. One substitution S_{1} = [γ ↦ π_{1}] yields a semi-unifier π_{1} → α of S_{1}τ_{1} and S_{1}τ_{2}; another S_{2} = [γ ↦ π_{2}] yields α → π_{2}, but clearly we cannot use the unifying π_{1} → π_{2}. The name-clash in example 2 is a bit more sophisticated, as it here is possible to find an appropriate substitution S_{1} for the instantiations τ_{1}, …, τ_{n} of σ and an S_{2} for ν_{1}, …, ν_{n} of σ′, but S_{1} and S_{2} diverge in the substitution of a cut-type variable.

Example 3 illustrates failiure upon “occurs check”: one type is γ (a cut-type variable) and the other τ_{2} is a composite type containing γ. Obviously by iterating the substitution [γ ↦ τ_{2}] on γ and τ_{2} one gets more and more refined anti-unifiers.

For standard unification “name-clash” and “occurs-check” are clearly the only ways for failiure. For our modified version of unification the claim is that these are also the only ways one can fail to find our S. Though the above is not a full argument, the tight connection with unification is a clear indication that this is the case.

Example 2 and 3 are therefore generic in the sense that they capture the two ways expressions may fail to have most specific annotations with respect to the ordering ⪯′.

8 Conclusion

Via an ordering relation for annotated expressions we have shown that there are unique minimal elements for expressions without cut-type variables. For expressions that have typing derivations including cut-type variables this will in general not be the case.

One can therefore claim that it is not so interesting to implement M, which only is guaranteed to find a minimal annotation for cutfree expressions. In opposition to this claim one can insist that cut-type variables only occur in connection with β redexes that keep redundant information, that is dead code. For the purely applicative language we have studied presence of cut-type variables therefore indicates that the program is poorly written. With side effects the matter is slightly different, but it i questionable whether the situation is so bad after all, since M will anyway be able to eliminate most redundant polymorphism.

The author therefore concludes that M for all practical purposes is the algorithm one should use to find a least typing derivation.

Besides the potential use of M, this paper should also hopefully have given some insight on typing derivations.

A Searching for an Approximate Optimization

In this part we sketch an algorithm that for cases like example 1 page 22 finds a lesser annotation that M w.r.t. the ordering ⪯′. For the cases where there is a nonempty set of minimal annotations it finds the least upper bound for these annotations. That is to instantiate the cut-type variables as much as possible but still have an annotation subsuming all the minimal. For the cases without minimal annotations it stops at the topmost step of the descending chain. It can therefore be regarded as a more detailed treatment than given in section 7.2.

In all its embarrassing simplicity this is just a matter of finding a substitution for the cut-type variables that allows M to find an annotation for \overline{e} where all the type-schemes are general enough to cover all minimal incomparable. The way to find this substitution is by several variants of the standard unification algorithm where only the cut-type variables are true variables. Where the unifications algorithms fail on occurscheck it indicates presence of the descending chains, while nameclash indicates two minimal incomparable annotations.

The task of describing the actual algorithm in all its details and verifying the above statements about it is however another not so simple task.

We do therefore not claim to have developed a totally verified approach towards the solution of the problem.

The solution found further suggests that the task of finding a least annotation subsuming all minimal is asymptotically so complex that it is uninteresting as a real algorithm.

A.1 The algorithm

Suppose we want to find the least derivation for TE ⊢ \overline{e} : τ i.e. the least annotation e, such that TE ⊢ e : τ. First let (S, e, τ_{p}) =W(TE,\overline{e}) and θ be the substitution from τ_{p} to τ (the external type wanted). For every let bound variable x which is not used in Se, erase the quantification on the associated type-schemes, call the new expression e′. The (maximal) set of cut(type) variables CV is now TV(θe′)\ (FV(τ)∪FV(S TE)).

Like done in M we let a map collect instantiations in θe′, but this time the map is used for global postprocessing. For convenience we also modify the type of the map to Var →^{fin} (TyVar →^{fin} Type^{∗}), and name elements of this type with the letter B (instead of A).

We proceed as one specific let bound variable is considered at a time. Given a let bound variable, x, we notice that there are two ways to reduce the associated type-scheme (∀α⃗.ν): quantified variables can be further instantiated (find an instantiation of α_{i} to a more specific type) or different quantified variables can be identified (identify α_{i_{1}}, …, α_{i_{j}} to the variable α_{i_{1}}). These two reductions can comfortably be treated separately.

Instantiation of quantified variables

Further instantiation of a quantified variable α is investigated by examining the list ⟨τ_{1}, …, τ_{n}⟩ = B(x)(α). The task is to find a substitution of the cut variables such that the list has a anti-unifier smaller than AntiUnify⟨τ_{1}, …, τ_{n}⟩.

The contents of the list may be divided into three parts: the cut variables, type variables bound under quantification in other let bound variables, and thirdly everything else (meaning typevariables occurring in τ, type constants and function types). As it will be evident it is convenient to disassemble the list with respect to these three parts, as sketched below: disassemble⟨τ_{1}, …, τ_{n}⟩ =^{def}

let (⟨ν_{1}, …, ν_{m}⟩, Cs, BV) = divide ⟨τ_{1}, …, τ_{n}⟩ for each α_{i} ∈ BV do

let

x be the let bound variable whose type-scheme binds α_{i} in

(Cs_{i}, l_{i}) = disassemble(B(x)(α_{i}))

in (Cs ∪ Cs_{1} ∪ … ∪ Cs_{n}, ⟨ν_{1}, …, ν_{m}⟩ l_{1} … l_{n})

Cutvariables are collected in the set Cs (⊆ CV), while type variables originating from other let bound variables are instantiated resulting in new lists which are recursively disassembled. This recursive disassembling results in the sets Cs_{1} to Cs_{n} of cutvariables and lists of of types (none of which are cutvariables or quantified type variables). To keep notation short we have not bothered to pass B, CV or the expression as arguments although they are used to divide the input list.

Ideally the set of cutvariables extracted from the original list can be instantiated to anything, so depending on the structure of the remaining list of non-cutvariables, it can be decided what to instantiate those cutvariables to (if at all) in order to find a further instantiation of α. There are in essence four different possibilities for the structure of the remaining list: it is empty, all its components are functiontypes, all elements are equal or there are inherently incomparable types. These four cases are treated separately in the next algorithm sketched:

InstUnify : Type^{∗}× TyVar-set × TyVar-set × Substitution → TyVar-set × TyVar-set × Substitution

InstUnify(⟨τ_{1}, …, τ_{n}⟩, CV, UV, m) =^{def}

let

(Cs, ⟨τ_{i_{1}}, …, τ_{i_{j}}⟩) = disassemble⟨τ_{1}, …, τ_{n}⟩ in case ⟨τ_{i_{1}}, …, τ_{i_{j}}⟩ of ⟨⟩ ⇒ let

γ be a fresh variable UV′ = UV ∪ {γ} m′ = MapUnify_{UV′}(m, [v ↦ γ|v ∈ Cs])

in

(CV, UV′, m′) handle FAIL(Cs′) ⇒ (CV \ Cs, UV, m \ Cs)

⟨τ_{i_{1}}^{1} → τ_{i_{1}}^{2}, …, τ_{i_{j}}^{1} → τ_{i_{j}}^{2}⟩

⇒ let (γ_{1}^{1}, γ_{2}^{1}), …, (γ_{1}^{k}, γ_{2}^{k}) be fresh cut variables, assuming |Cs| = k. UV′ = UV ∪ {γ_{1}^{1}, …, γ_{2}^{k}} m′ = MapUnify_{UV′}(m, [v_{i} ↦ γ_{1}^{i} → γ_{2}^{i}|v_{i} ∈ Cs]) ⟨ν_{1}^{1} → ν_{2}^{1}, …, ν_{1}^{k} → ν_{2}^{k}⟩ = ⟨m′(v_{i})|v_{i} ∈ Cs⟩ (CV_{1}, UV_{1}, m_{1}) = InstUnify(⟨τ_{i_{1}}^{1}, …, τ_{i_{j}}^{1}⟩ ⟨ν_{1}^{1}, …, ν_{1}^{k}⟩, CV, UV′, m′) (CV_{2}, UV_{2}, m_{2}) = InstUnify(⟨τ_{i_{1}}^{2}, …, τ_{i_{j}}^{2}⟩ ⟨ν_{2}^{1}, …, ν_{2}^{k}⟩, CV_{1}, UV_{1}, m_{1})

in

(CV_{2}, UV_{2}, m_{2}) handle FAIL(Cs′) ⇒ (CV \ Cs′, UV, m \ Cs′)

⇒ if τ_{i_{1}} = … = τ_{i_{j}} then

let

{γ_{1}, …, γ_{m}} = FV(τ_{i_{1}}) ∩ CV
γ′_{1}, …, γ′_{m} be new type variables
τ = [γ_{j} ↦ γ′_{j}]τ_{i_{1}}
UV′ = UV ∪ {γ′_{1}, …, γ′_{m}}

m′ = MapUnify_{UV′}(m, [v ↦ τ|v ∈ Cs] ∪ [γ_{j} ↦ γ′_{j}|j ∈ {1, …, m}]) in

(CV, UV′, m′) handle FAIL(Cs′) ⇒ (CV \ Cs′, UV, m \ Cs′) else (CV, UV, m)

A unification algorithm MapUnify is called in three cases: Like the normal unification algorithm, MapUnify takes a set, UV′, of the only entities which can be treated as variables, and returns a map of the unified range elements. MapUnify is thus a kind of unification on records.

Whenever MapUnify fails with the exception FAIL(Cs′) it means that there are two different substitutions of cutvariables in Cs′(⊆ Cs) leading to two different minimal incomparable typeschemes for x. They should remain uninstantiated to maintain a type-scheme subsuming all the minimal incomparable. A way to indicate this restriction is to remove these cut variables from the set of freely instantiable cutvariables as well as the domain of possible instantiations. We remain by this very loose description of MapUnify, as it appears that a precise formal is very complicated.

The four cases function as follows:

• If the remaining list of types is empty all the cut-type variables have to unify to a common type. We therefore introduce a new variable which connects the variables in Cs.

• If there is a nonempty list of only function types each variable in Cs has to be unifiable to some function type in order to substitute the quantified variable α with something more refined (a function type).

For further refinement of the functiontype recursive calls are invoked.

Note that if MapUnify fails on occurs check it means that there is an infinite descending chain.

• If there is a nonempty list of equal types which are not function types, each variable in Cs has to be instantiated to this type to eliminate the bound variable.

• If the nonempty list have different types, there is no hope of refining the type-scheme where α occurs, neither CV, UV nor m have therefore to be changed.

InstUnify is called for every let bound variable x and every type variable in B(x) where it successively modifies m, UV and CV, to get a substitution of the cut-type variables which still gives type-schemes for \overline{e} subsuming all minimal incomparable. More formally we may define the first modification as:

modify_{1}(CV, m) =^{def} initially UV = { }; for each x ∈ B do

for each α ∈ B(x) do (CV, UV, m) := InstUnify(B(x)(α), CV, UV, m)

Identifying quantified Variables

The other way to reduce type-schemes associated with the let bound variables is to identify several quantified type variables into one quantified variable.

The existence of such an specialization is determined by a pairwise comparation of the instantiations of the bound type variables; or restated: Let x be a let bound variable with the associated type-scheme ∀α⃗.τ and B(x) the map: [α_{1} ↦ l_{1}, …, α_{n} ↦ l_{n}]. If two different lists l_{i} and l_{j} unify with respect to the cut-type variables, then α_{i} and α_{j} can be replaced by one bound variable (when the cut-type variables are instantiated according to the unifier).

Apparently it should be possible to realize this part by a trivial variant of the unification algorithm, which just unifies a pair lists. But the potential presence of type variables bound by other let expressions again complicates the matter slightly. These type variables might further be eliminated or instantiated resulting in a new situation for the unification process.

A precise formulation of how to treat the various cases is given below:

pair(l_{1}, l_{2}) =^{def} if null l_{1}, l_{2} then ⟨⟩ else ⟨(hd l_{1}, hd l_{2})⟩ pair(tl l_{1}, tl l_{2})

IdUnify: TyVar-set × Type^{∗}× Type^{∗} → Substitution IdUnify_{CV} (l_{1}, l_{2}) =^{def} fold IU_{CV} (pair(l_{1}, l_{2})) [ ] IU: TyVar-set × Type× Type → Substitution → Substitution

IU_{CV} (τ_{1}, τ_{2})S =^{def} case (Sτ_{1}, Sτ_{2}) of

(α, α′) ⇒ let x, x′ be the let bound variables whose typeschemes bind α and α′. γ be a fresh variable

in

if x = x′ then fold IU_{CV} (pair(B(x)(α), B(x)(α′)) S else
fold IU_{CV ∪{γ}} (pair(B(x)(α), ⟨γ, …, γ⟩))
(fold IU_{CV ∪{γ}} (pair(B(x′)(α′), ⟨γ, …, γ⟩)) S)

(α, τ),

(τ, α) ⇒ let x be the let bound variable whose type-scheme binds α. γ be a fresh variable

in if τ ∈ CV ∧ τ is local to the expression typing x then [τ ↦ α] ∘ S else fold IU_{CV ∪{γ}} (pair(⟨τ⟩ B(x)(α), ⟨γ, …, γ⟩)) S

(τ_{1} → τ′_{1}, τ_{2} → τ′_{2})

⇒ fold IU_{CV} ⟨(τ_{1}, τ_{2}), (τ′_{1}, τ′_{2})⟩ S (τ_{1}, τ_{2}) ⇒ unify_{CV} (τ_{1}, τ_{2}) ∘ S

First a function pair, which takes two equally lengthed lists and returns a list of pairs from the two lists, is defined.

IdUnify finds the unifier for two lists l_{1}, l_{2} of types associated with α_{i} respectively α_{j}. It is conveniently defined via IU which unifies a pair of types.

In IU casesplit is made according to whether the types represent type variables bound in other typeschemes. These bound variables are identified by α’s.

• In the first case both types are type variables bound by quantification in other let bound variables x and x′. If x = x′ we only require that B(x)(α) and B(x)(α′) unify as lists, i.e. via recursive calls of IU. If the type variables however origin from different let bound variables they have to be instantiable to the same type. This means that the types in the two lists B(x)(α) and B(x′)(α′) have to unify. For this purpose we introduce an extra variable γ connecting the two lists.

• If only one of the types is a variable bound in a type-scheme another comparison is made. If the other type is a cut variable it may be replaced by the bound variable, provided (off course) that the cut-type variable is local to the expression where the type of x is bound (otherwise there would occur problems of generalization upon free variables in the surrounding type environment). When the other type is not a cutvariable the bound type variable must have a unifying instantiation.

• When both types are function types recursive calls of UI provides the necessary unification.

• For every other case normal unification does the job. We notice that if unification fails it is not possible to identify the bound type variables in mind.

This comparation is made for each pair of bound variables in a typescheme.

The problem that can arise during this process is that two different pairs of instantiations have unifiers on which MapUnify fails. It means that α_{i} and α_{j} respectively α_{k} and α_{l} can be identified by suitable instantiations of the cut-type variables, but not at the same time. Like done for the instantiation of quantified variables those entities for which MapUnify fails can be discarded as freely instantiable cut-type variables, since different instantiations lead to different incomparable annotations.

The second modification of m and the set of cut-type variables can therefore be formalized as:

modify_{2}(m, CV) =^{def} for each x ∈ dom B do

for each pair α_{i}, α_{j} ∈ dom B(x) do

m′ := IdUnify_{CV} (B(x)(α_{i}), B(x)(α_{j})) handle Unify ⇒ [ ]
(m, CV) := (MapUnify_{CV} (m, m′), CV) handle FAIL(Cs′) ⇒ (m \ Cs′, CV \ Cs′)

Assembling it all

Through the identification and instantiation of the bound variables the two described algorithms InstUnify and IdUnify develop and modify a substitution of the cut type-variables simply by sequencing the two modifications:

m := [ ]; modify_{1}(CV, m); modify_{2}(CV, m)

The resulting substitution m can now be applied to θe′, where finally algorithm M is used: M(mθe′).

B Notes on M

In the design of M we have chosen to preform anti-unification on the instantiated type-schemes. For the purpose of clarifying the exposition this approach fit comfortably, but it is obvious that it’s only necessary to anti-unify the instantiations.

We have therefore devised an algorithm especially for this purpose. It is more complicated, but works for the same reasons as the anti-unification algorithm, moreover it finds the substitution θ and the new set of bound variables β⃗ directly.

The algorithm falls in two parts, the first is the AntiUnify (generalized to lists), the second is the algorithm Find Substitution which calls AntiUnify with instantiations of the bound variables and which finds the substitution θ and the set β⃗:

Find Substitution: (TyVar →^{fin} Type^{∗}) × TyVar−set → Substitution × TyVar-set Def Find Substitution (m, BV) =^{def}

initially m1 := [ ]; m2 := [ ]; m3 := [ ]; m4 := [ ]; β⃗ := {};

for each ⟨τ_{1}, …, τ_{n}⟩ ∈ rng m do

let (τ, m′) = AntiUnify⟨τ_{1}, …, τ_{n}⟩ in

m1 := m1 ∪ [α ↦ τ|m(α) = ⟨τ_{1}, …, τ_{n}⟩];
m2 := m2 ∪ m′;
for each ⟨τ_{1}, …, τ_{n}⟩ ∈ rng m2 do

let α be a fresh type variable in m3 := m3 ∪ [β ↦ α | m2(β) = ⟨τ_{1}, …, τ_{n}⟩];

β⃗ := β⃗ ∪ {α};

for each γ ∈ BV ∩ FV(rng m1) do let γ′ be a fresh type variable in m4 := m4 ∪ [γ ↦ γ′];

β⃗ := β⃗ ∪ {γ′};

return (m4 ∘ m3 ∘ m1, β⃗)

Besides changing M to collect a map of the form B, introduced in appendix A, the treatment of let constructions is altered to call Find Substitution. The revised part of M therefore reads:

\underline{let} x : ∀α⃗.τ = e_{1} \underline{in} e_{2} ⇒

let (e′_{2}, B_{2}, BV_{2}) = M(e_{2}) (θ, β⃗) = if x ∈ dom B_{2} then Find Substitution(B_{2}(x), BV_{2}) else ([ ], α⃗) (e′_{1}, B_{1}, BV_{1}) = M(θ e_{1})

in (\underline{let} x : ∀β⃗.θτ = e′_{1} \underline{in} subst(x, θ, β⃗, e′_{2}), B_{1} + (B_{2} \ \{x\}), BV_{1} ∪ BV_{2} ∪ β⃗)

C Notes on implementation

The algorithm M has been implemented in standard ML and tested on a selection of examples.

In difference from the algorithm presented in this paper the input is not an annotated expression but a well formed typing derivation, i.e. a prooftree. This is only a minor change to the M presented, because as we noticed every typing derivation represents a unique annotated expression. Otherwise M is implemented in its original form, the alternative from appendix B thus ignored here.

References

[Dam84] Luis Manuel Martins Damas. Type Assignment in Programming Languages Ph.D. Thesis University of Edinburgh. 1984.

[Xavier] Xavier Leroy. Unboxed objects for polymorphic typing Conference paper, 1992 published by ACM.

[MilDam82] Luis Manuel Martins Damas and Robin Milner. Principal type-schemes for functional programs. Proc. 9’th Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, 1982.

[Girard] Jean-Yves Girard, Yves Lafont, Paul Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 1989.

[MitHarp88] John C. Mitchell and Robert Harper. The Essence of ML 1988 ACM POPL.

[Plotkin70] G. Plotkin. A note on inductive generalization Math. Intell. 5 1970.

[Reynolds70] J. C. Reynolds. Transformation systems and the algebraic structure of atomic formulas Math. Intell. 5 1970.