BRICS LS-95-3 M. I. Schwartzbach: Polymorphic Type Inference

BRICS

Basic Research in Computer Science

Polymorphic Type Inference

Michael I. Schwartzbach

BRICS Lecture Series LS-95-3 ISSN 1395-2048 June 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Lecture Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Polymorphic Type Inference

Michael I. Schwartzbach

Michael I. Schwartzbach

BRICS^{1}

Department of Computer Science

University of Aarhus

Ny Munkegade DK-8000 Aarhus C, Denmark

1Basic Research In Computer Science, Centre of the Danish National Research Foundation.

Preface

We will present a tiny functional language and gradually enrich its type system. We shall cover the basic Curry-Hindley system and Wand’s constraint-based algorithm for monomorphic type inference; briefly observe the Curry-Howard isomorphism and notice that logical formalism may serve as the inspiration for new type rules; present the polymorphic Milner system and the Damas-Milner algorithm for polymorphic type inference; see the Milner-Mycroft system for polymorphic recursion; and sketch the development of higher type systems. We will touch upon the relationship between types and logic and show how rules from logic may give inspiration for new type rules. En route we shall encounter the curious discovery that two algorithmic problems for type systems, which have been implemented in popular programming languages, have turned out to be respectively complete for exponential time and undecidable.

References

[1] Luis Damas and Robin Milner. Principal type schemes for functional programming. In 9th Symposium on Principles of Programming Languages, 1982.

[2] F. Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15, 1993.

[3] P. Kanellakis and J. Mitchell. Polymorphic unification and ML typing. In 16th Symposium on Principles of Programming Languages. ACM Press, January 1989.

[4] A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15, 1993.

[5] Harry G. Mairson. Decidability of ML typing is complete for deterministic exponential time. In 17th Symposium on Principles of Programming Languages. ACM Press, January 1990.

[6] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17, 1978.

[7] A. Mycroft. Polymorphic type schemes and recursive definitions. In 6th International Conference on Programming. Springer-Verlag, 1984.

[8] M. S. Paterson and M. N. Wegman. Linear unification. Journal of Computer and System Sciences, 16, 1978.

[9] J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12, 1965.

[10] M. Wand. A simple algorithm and proof for type inference. Fundamentae Informaticae, X, 1987.

Contents

1 Type Checking and Type Inference 1 2 A Tiny Functional Language 2 3 A Simple Type System 2 4 Simple Type Inference 4 5 Types and Logic 8 6 Polymorphic Types 11 7 Polymorphic Type Inference 13 8 Polymorphism and Recursion 17 9 Higher Type Systems 18 10 Problems 20 viii

Polymorphic Type Inference

1 Type Checking and Type Inference

Two main reasons for introducing types into a programming language are safety and readability.

Let us first consider the safety aspect. Not all expressions in an untyped language are thought to be sensible. For example, computing the quotient of a text and a function or the square root of a banana is plain nonsense. Let us agree upon the existence of a subset of bad expressions, the run-time behaviors of which are undesirable or undefined. Any non-trivial choice of badness leads to an uncomputable subset. Thus, the compiler cannot distinguish the good from the bad.

To ensure safety of programs we introduce a type system and reluctantly sacrifice some good expressions. This happens because we require our type system to ensure that only good expressions are typable. However, since type checking must be decidable, it is clear that some good expressions are not typable. The following diagram illustrates this situation.

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; slack; typable expressions; bad expressions]

The slack in a type system is the set of good expressions that it unfairly rejects. The desire to minimize this slack is a driving force in the development of type systems, which leads towards ever more complex type rules. This trend is curbed by the fact that the type discipline should not encumber the actual programming too much. This last concern is the reason why arithmetical errors such as index out of range and division by zero are not prevented by most type systems.

The issue of readability wishes for the types to be succinct hints to the semantics of expressions. For example, when trying to understand the workings of a function, it is quite nice to know in advance that it computes booleans from lists of integers. This leads towards more expressive and intuitive types—limited by the need for decidability of type checking.

The ideal situation seems to arise when our type system admits automatic inference of types. Then we obtain all the advantages described above, without the need to bother with the type rules ourselves.

In the following sections we study the basic development of type systems for functional languages.

2 A Tiny Functional Language

We define a tiny vanilla-flavored functional language to serve as the basis for this presentation. It is designed to resemble the core of languages such as Scheme, Miranda, or ML.

Exp ::= 0 | true | false | x | pred(Exp) | succ(Exp) | iszero(Exp) | cons(Exp,Exp) | car(Exp) | cdr(Exp) | nil | null(Exp) | if Exp then Exp else Exp fi | fun(x) Exp end | Exp(Exp) | let f = Exp in Exp end

Thus, we have integers, booleans, lists and functions. The let-construct defines a local scope and at the same time permits us to give simple recursive definitions.

The semantics of this language is entirely standard and will not be formalized. Note, though, that there are various expressions that we intuitively recognize as meaningless, such as: succ(true), false(0), and car(fun(x) x end). These are the bad expressions that our type system must exclude.

Exercise 2.1 Program a length function on lists. □

3 A Simple Type System

We choose a language of types that describes the different values of our expressions: integers, booleans, lists and functions.

Type ::= Int | Bool | list(Type) | Type → Type

We must now decide on the rules for assigning types to expressions. Some are very easy; for example, true is of type Bool and fun(x) succ(x) end is of type Int → Int. Bad expressions are excluded by imposing type restrictions; for example, cdr only works on lists, the two branches of an if-expression must have the same type, and in function calls the formal and actual arguments types must be equal.

It would not be hard to write down a few manual pages describing this type system. However, we choose an extremely compact notation that is inspired by a connection between types and logic that we shall explore further in a later section. A type judgment is of the form:

A ⊢ e : τ

Here A is a symbol table, i.e., a mapping from identifiers to types; e is an expression; and τ is a type. Its meaning is simply: relatively to the symbol

3. A Simple Type System

table A, the expression e has type τ. Type judgments are combined into type rules of the form:

\frac{J_{1}; J_{2}; …; J_{n}}{J}

Its meaning is: if the judgments J_{i} all hold, then so does the judgment J. Using these notational conventions, we can express all aspects of our type system in the following manner.

\overline{A ⊢ 0 : Int}

A ⊢ true : Bool

A ⊢ false : Bool

\frac{A ⊢ e : Int}{A ⊢ pred(e) : Int}

\frac{A ⊢ e : Int}{A ⊢ succ(e) : Int}  \frac{A ⊢ e : Int}{A ⊢ iszero(e) : Bool}

\frac{A ⊢ e_{1} : τ; A ⊢ e_{2} : list(τ)}{A ⊢ cons(e_{1},e_{2}) : list(τ)}  \frac{A ⊢ e : list(τ)}{A ⊢ car(e) : τ}

\frac{A ⊢ e : list(τ)}{A ⊢ cdr(e) : list(τ)}  \overline{A ⊢ nil : list(τ)}

\frac{A ⊢ e : list(τ)}{A ⊢ null(e) : Bool}  \frac{A ⊢ e_{1} : Bool; A ⊢ e_{2} : τ; A ⊢ e_{3} : τ}{A ⊢ if e_{1} then e_{2} else e_{3} fi : τ}

\frac{A,x : σ ⊢ e : τ}{A ⊢ fun(x) e end : σ → τ}  \frac{A ⊢ e_{1} : σ → τ; A ⊢ e_{2} : σ}{A ⊢ e_{1}(e_{2}) : τ}

\overline{…, x : σ, … ⊢ x : σ}  \frac{A,f : σ ⊢ e_{1} : σ; A,f : σ ⊢ e_{2} : τ}{A ⊢ let f = e_{1} in e_{2} end : τ}

This is the Curry-Hindley type system dating back to the 1960s.

Exercise 3.1 What is the rôle of the rule in the lower left-hand corner? □

Exercise 3.2 How can we tell that the let-construct allows recursive definitions? □

The claim that a given expression has a particular type can be verified by a systematic (and seemingly pedantic) application of the above rules. Consider for example the function:

fun(g)

fun(x) succ(g(x))

end end

We wish to show that it has type (Bool → Int) → (Bool → Int). A formal derivation looks as follows.

\frac{_{\overline{g : Bool → Int, x : Bool ⊢ g : Bool → Int} \overline{g : Bool → Int, x : Bool ⊢ x : Bool}}}{\frac{g : Bool → Int, x : Bool ⊢ g(x) : Int}{\frac{g : Bool → Int, x : Bool ⊢ succ(g(x)) : Int}{\frac{g : Bool → Int ⊢ fun(x) succ(g(x)) end : Bool → Int}{⊢ fun(g) fun(x) succ(g(x)) end end : (Bool → Int) → (Bool → Int)}}}}

Exercise 3.3 Go through the above derivation bottom-up and explain which type rules are used. □

It is quite easy to implement a top-down type checker based on such derivations, since the outermost type constructor and expression operator always determine the type rule that must be applied.

At this point we should pause to consider whether our type system is sound, in the sense that only good expressions are typable. To say anything about this, we would need a formal semantics of our language and a specification of goodness. The usual strategy is then to show a property called subject reduction: an expression of type τ can only evaluate to a value of type τ. Soundness then follows, since bad expressions do not evaluate to values of any type.

4 Simple Type Inference

As explained, we do not want to provide the types explicitly. Rather, we wish for the compiler to find appropriate typings of our expressions or to inform us if none exists. This spares us the trouble of writing down complicated type expression that often only clutter up our nice programs.

Another often cited advantage is the hope that a clever type inference algorithm may come up with more general types than we ourselves could, thus keeping the slack to an absolute minimum.

An obvious idea is to use a bottom-up procedure that traverses the parse tree and computes the type of every subexpression. But this only works for constant expressions without variables. As a trivial counter-example consider the term: succ(x). In a strict bottom-up procedure we must first choose a type for x. But unless we happen to select Int, we will mistakenly conclude that the expression is not typable.

4. Simple Type Inference

We can still use a bottom-up procedure, but we should collect all types, rather than just a single specimen. However, we must somehow deal with the possibility that expressions may have infinitely many types. For example, the function:

fun(g)

fun(x)

succ(g(x)) end

end

for which we earlier derived the type (Bool → Int) → (Bool → Int), has in fact every possible type of the form (α → Int) → (α → Int). But by this example we have already given the solution to our problem: an infinite set of types sometimes has a finite symbolic representation.

We define a type scheme to be a type that may contain occurrences of type variables. Formally, the syntax is as follows.

Types ::= Int | Bool | list(Types) | Types→Types | Var Var ::= α | β | …

A type scheme defines a set of types: those that can be obtained by substituting types for variables in a consistent manner. For example, the type scheme (α → β)→ list(α) defines the following infinite set:

(Int→Int) → list(Int)
(Bool→Int) → list(Bool)
(Bool→Bool) → list(Bool)
(Int→Bool) → list(Int)
⋮
((Int→Bool)→list(Bool)) → list(Int→Bool)
⋮

The only requirement is that both occurrences of α must be substituted with the same type. If we also allow variables to be substituted with other type schemes, then we obtain a preorder σ ≥ τ on type schemes, which holds exactly when τ is obtained from σ through a substitution.

Exercise 4.1 What is a preorder? □

Exercise 4.2 Which pairs among the following type schemes are ordered?

α
β
α → β
α → α
(α → β)→ list(α)

□

Exercise 4.3 Argue that when σ ≥ τ, then the set of types determined by σ is a superset of that determined by τ. □

The key to an efficient type inference algorithm is the following fundamental observation: for every typable expression e there is a type scheme σ that exactly defines all possible types of e. We call σ the principal type scheme for e. The task of type inference is then to construct the principal type scheme (for every subexpression) or to fail if the expression is untypable.

We present the algorithm in the style of Wand [10] from 1987. For every parse tree node n we introduce a type variable [[n]] which denotes the (as yet) unknown type scheme for the subexpression rooted in n. To capture scope rules correctly, we require that all parse tree nodes corresponding to occurrences of the same identifier in a scope must share the same type variable. In examples below, we use the slightly ambiguous notation [[e]] for the type variable corresponding to the subexpression e.

Exercise 4.4 Why is this notation ambiguous? □

Every kind of expression imposes its own kind of constraints on type variables. Consider the case of a function application e_{1}(e_{2}). We know from the type rule for application that the following equation must hold.

[[e_{1}]] = [[e_{2}]] → [[e_{1}(e_{2})]]

That is, e_{1} must be a function that accepts arguments of the same type as e_{2}. The full collection of constraints is as follows.

0 : [[0]] = Int
true : [[true]] = Bool
false : [[false]] = Bool
pred(e) : [[pred(e)]] = [[e]] = Int
succ(e) : [[succ(e)]] = [[e]] = Int
iszero(e) : [[iszero(e)]] = Bool, [[e]] = Int
cons(e_{1},e_{2}) : [[cons(e_{1},e_{2})]] = [[e_{2}]] = list([[e_{1}]])
car(e) : [[e]] = list([[car(e)]])
cdr(e) : [[cdr(e)]] = [[e]] = list(α)
nil : [[nil]] = list(α)
null(e) : [[null(e)]] = Bool, [[e]] = list(α)
if e_{1} then e_{2} else e_{3} fi : [[if e_{1} then e_{2} else e_{3} fi]] = [[e_{2}]] = [[e_{3}]], [[e_{1}]] = Bool
fun(x) e end : [[fun(x) e end]] = [[x]] → [[e]]
e_{1}(e_{2}) : [[e_{1}]] = [[e_{2}]] → [[e_{1}(e_{2})]]
let f = e_{1} in e_{2} end : [[let f = e_{1} in e_{2} end]] = [[e_{2}]], [[f]] = [[e_{1}]]

In the above, we assume that each α is a fresh variable distinct from all others.

We now know how to generate the constraints for any expression. For example, the expression:

fun(g)

fun(x)

succ(g(x)) end

end

yields the following constraints.

[[fun(g) fun(x) succ(g(x)) end end]] = [[g]] → [[fun(x) succ(g(x)) end]]
[[fun(x) succ(g(x)) end]] = [[x]] → [[succ(g(x))]]
[[succ(g(x))]] = [[g(x)]] = Int
[[g]] = [[x]] → [[g(x)]]

Exercise 4.5 Explain the origin of each of the above constraints. □

We are then left with the problem of solving these constraints. We must assign to each type variable a type scheme such that all constraints are satisfied. Fortunately, this is exactly the well-known unification problem. It has an efficient linear-time algorithm that even computes a solution consisting of unique principal type schemes. The above example has the following solution.

[[fun(g) fun(x) succ(g(x)) end end]] = ([[x]] → Int) → ([[x]] → Int)
[[fun(x) succ(g(x)) end]] = [[x]] → Int
[[succ(g(x))]] = Int
[[g(x)]] = Int
[[g]] = [[x]] → Int
[[x]] = [[x]]

Exercise 4.6 Verify that the above is indeed a solution. □

We now present a simple algorithm for solving constraints. The constraint system is given as x_{i} = σ_{i}. The solution S is a function from type variables to type schemes. We use the notation S(σ) to indicate the type scheme obtained from σ by substituting every type variable with its value in S. If σ and τ are type schemes, then Δ(σ,τ) is the set of two subtrees on which they first differ in a preorder traversal.

let S(x_{i}) = x_{i};

while S is not a solution do let {s,t} = Δ(S(x_{i}),S(σ_{i})), where S(x_{i})≠S(σ_{i}); if s and t are both type constructors then fail fi; Assume s=x_{j}; if x_{j} occurs in t then fail fi; let S(x_{i}) = {x_{j} ↦ t}(S(x_{i}))

end

This algorithm, which was presented by Robinson [9] in 1965, runs in exponential time. The linear time algorithm is from 1978 by Paterson and Wegman [8].

Exercise 4.7 Generate and solve the type constraints for the following expression.

fun(x)

fun(y)

x((car(y))(x)) end

end

□

When an expression is untypable, then we obtain an unsolvable collection of constraints. Consider the suspect expression: cons(succ(x),car(x)). It generates these constraints.

[[cons(succ(x),car(x))]] = list([[succ(x)]])
[[car(x)]] = list([[succ(x)]])
[[x]] = list([[car(x)]])
[[succ(x)]] = Int
[[x]] = Int

Exercise 4.8 Argue that the above constraints are unsolvable. □

5 Types and Logic

Earlier, the peculiar notation for type rules was blamed on their connection with logic. For very pure type systems, this connection is known as the Curry-Howard isomorphism. It is so famous that we shall frame it.

Types are formulas, and expressions are proofs.

The isomorphism between types and formulas is simply syntactic: Int and Bool correspond to facts, and the type constructor → corresponds to the logical connective ⇒. The relationship between expressions and proofs is a bit more

5. Types and Logic

subtle, but we only need to know its main consequence: a formula is valid if and only if the corresponding type is not empty.

Furthermore, our type rules mirror exactly the inference rules from logic. For example, there are two rules involving the function type:

\frac{A,x : σ ⊢ e : τ}{A ⊢ fun(x) e end : σ → τ} \frac{A ⊢ e_{1} : σ → τ; A ⊢ e_{2} : σ}{A ⊢ e_{1}(e_{2}) : τ}

If we ignore the expressions and apply the isomorphism, then we immediately recognize two familiar rules from logic:

\frac{A,σ ⊢ τ}{A ⊢ σ ⇒ τ} \frac{A ⊢ σ ⇒ τ; A ⊢ σ}{A ⊢ τ}

These are respectively deduction and modus ponens. For example, consider the formula (A ⇒ B) ⇒ ((C ⇒ A) ⇒ (C ⇒ B)). Is this a tautology? Yes, because the expression:

fun(x)

fun(y)

fun(z)

x(y(z)) end

end end

has the principal type scheme (α → β) → ((γ → α) → (γ → β)).

Exercise 5.1 Why must a type scheme inferred for an expression necessarily be a tautology? □

Exercise 5.2 Complete the proof that (A ⇒ B) ⇒ ((C ⇒ A) ⇒ (C ⇒ B)) is a tautology. □

In contrast, common sense tells us that the formula (A ⇒ B) ⇒ (B ⇒ A) is not a tautology, which means that no expression has principal type scheme (α → β) → (β → α).

Exercise 5.3 Argue that no expression has the principal type scheme (α → β) → (β → α). Reconcile this with the fact that e.g. the expression: fun(x)

fun(y) 0 end

end

has type (Int → Bool) → (Bool → Int). □

Notice that, from a logical perspective, type inference is a rather bizarre activity: we have a proof and are looking for the corresponding formula.

Our tiny functional language so far excludes product and sum types. Using the Curry-Howard isomorphism, we can easily figure out how to add them. The usual rules from logic for conjunction give us the rules for products:

\frac{A ⊢ e_{1} : τ_{1}; A ⊢ e_{2} : τ_{2}}{A ⊢ pair(e_{1},e_{2}) : τ_{1} × τ_{2}}  \frac{A ⊢ e : τ_{1} × τ_{2}}{A ⊢ fst(e) : τ_{1}; A ⊢ snd(e) : τ_{2}}

There are certainly no surprises here. Similarly, we have an isomorphism between sums and disjunction:

\frac{A ⊢ e_{1} : τ_{1}}{A ⊢ left(e_{1}) : τ_{1} + τ_{2}}  \frac{A ⊢ e_{2} : τ_{2}}{A ⊢ right(e_{2}) : τ_{1} + τ_{2}}

\frac{A ⊢ e : τ_{1} + τ_{2}; A ⊢ e_{1} : τ_{1} → σ; A ⊢ e_{2} : τ_{2} → σ}{A ⊢ decide(e,e_{1},e_{2}) : σ}

This should be rather familiar from a programming language point of view. However, closer scrutiny reveals that we have obtained some unusual logical rules: a proof of a disjunction must necessarily disclose which disjunct is being proved. This is not true for standard logic, which allows proofs to be considerably more indirect. The somewhat weaker logic that corresponds exactly to type theory is known as intuitionistic logic and has in fact been proposed by logicians for purely philosophical reasons.

Exercise 5.4 What are the type inference constraints for these new expressions? □

Exercise 5.5 Find a type whose translation into logic is a classical tautology but which do not have any expressions and thus does not yield an intuitionistic tautology. □

It is harder to see how the type rules for lists resemble logic in any way. But this is only because we have chosen the wrong operators. In the following version

6. Polymorphic Types

we see clearly the logical origins of lists.

\frac{A ⊢ e_{1} : τ; A ⊢ e_{2} : list(τ)}{A ⊢ cons(e_{1},e_{2}) : list(τ)}

\frac{A ⊢ base : σ; A ⊢ step : σ × τ → σ}{A ⊢ induct(base,step) : list(τ) → σ}

Thus, lists are all about counting and induction. The induct operator is vastly more general than car and cdr. For example, the length operator is easily defined as: induct(0,fun(x) succ(fst(x)) end).

Exercise 5.6 Use induct to define the operators car and cdr. □

Still, the practical advantage of the connection between types and logic is that we have a source of inspiration for missing type rules. Consider a novel type constructor stream(τ) which defines infinite lists of τ-values. Such streams are in a certain formal sense the dual concept of lists. Correspondingly, the dual concept of induction is called coinduction. Looking up its definition, we magically get the following type rules for streams.

\frac{A ⊢ base : σ; A ⊢ step : σ → σ × τ}{A ⊢ coinduct(base,step) : stream(τ)}

\frac{A ⊢ e : stream(τ)}{A ⊢ car(e) : τ; A ⊢ cdr(e) : stream(τ)}

The coinduct operator constructs streams—not inductively, but coinductively. And we might as well use the term cocounting to describe the actions of car and cdr.

Similar (co)induction principles are defined for arbitrary (monotone) recursive types.

Exercise 5.7 Use coinduct to construct the stream (0,1,2,3,4,…). □

Exercise 5.8 Define the type rules for finite and infinite binary trees. □

6 Polymorphic Types

The expression below seems at a first glance quite reasonable, but it is not typable. It is in fact an example of slack in our type system. let f = fun(x)

cons(x,nil) end in pair(f(0),f(true))

The problem is of course that we must assign a single type to the function f. We need instead the usual notion of polymorphism. For this purpose we extend our type schemes as follows.

Types ::= Int | Bool | list(Types) | Types → Types | Var Var ::= α | β | … Poly ::= ∀ Var.Poly | Types

The polymorphic type ∀α.α → list(α) describes a function that will accept an argument of any type and yield as result a list of values of that given type. This is exactly the type we want for the function f above. We will only allow polymorphism in connection with let-definitions.

The use of a universal quantifier hints at another connection with logic. Indeed, the types rules for polymorphic functions are those from logic, except that the layer of syntax is rather thicker this time.

\frac{A,f : σ ⊢ e_{1} : σ; A,f : ∀ᾱ.σ ⊢ e_{2} : τ}{A ⊢ let f = e_{1} in e_{2} end : τ} ᾱ ∉ A

\frac{A ⊢ f : ∀ᾱ.σ}{A ⊢ f : τ} σ ≥ τ

Here ᾱ indicates several type variables. The requirement ᾱ ∉ A means that A must not contain any assumptions about ᾱ. The requirement σ ≥ τ means that τ is a specialization of σ, as described in Section 4 (except that only variables from ᾱ may be substituted). This type system was introduced by Milner [6] in 1978.

Exercise 6.1 What is the connection with logic? □

Here is a formal derivation showing that the earlier example expression is typable. Unfortunately it is so large that we must cut it into several pieces.

7. Polymorphic Type Inference

\frac{\frac{A}{f:α→list(α) ⊢ fun(x)… end : α→list(α)} \frac{B}{f:∀α.α→list(α) ⊢ pair(…) : list(Int)×list(Bool)}}{⊢ let f = fun(x) cons(x,nil) end in pair(f(0),f(true)) : list(Int) × list(Bool)}

The A -piece is concerned with typing the function f.

\frac{_{\overline{f : α→list(α), x : α ⊢ x : α} \overline{f : α→list(α), x : α ⊢ nil : list(α)}}}{f : α→list(α), x : α ⊢ cons(x,nil) : list(α)}

The B -piece is concerned with typing the pair-expression.

\frac{\frac{\overline{f : ∀α.α→list(α) ⊢ f : ∀α.α→list(α)}}{f : ∀α.α→list(α) ⊢ f : Int→list(Int)} \overline{f : ∀α.α→list(α) ⊢ 0:Int}}{f : ∀α.α→list(α) ⊢ f(0) : list(Int)} C

Exercise 6.2 Complete the C -piece and verify each step in the above derivation. □

Why is the requirement ᾱ ∉ A necessary? If we remove it, the function:

fun(x)

let f = x in f end

can be shown to have type scheme α → Int. This is manifestly false, since the function acts as the identity. The purported derivation is as follows.

\frac{\frac{\overline{x : α, f : α ⊢ x : α} \frac{\overline{x : α, f : ∀α.α ⊢ f : ∀α.α}}{x : α, f : ∀α.α ⊢ f : Int}}{x : α ⊢ let f = x in f : Int}}{⊢ fun(x) let f = x in f end : α → Int}

Exercise 6.3 Catch the error in the above derivation. □

Exercise 6.4 What is the corresponding logical fallacy? □

7 Polymorphic Type Inference

The task of type inference seems to become vastly more complex with the introduction of the polymorphic let-construct. However, there is certainly a very naïve idea that we can fall back on. Using a simple syntactic transformation that unfolds let-definitions, we can expand a polymorphic program into an equivalent monomorphic version. For the expression:

let f = fun(x)

cons(x,nil) end in pair(f(0),f(true))

we obtain the equivalent version:

pair ( let f = fun(x) cons(x,nil) end in f(0) , let f = fun(x) cons(x,nil) end in f(true) )

which certainly is typable in the monomorphic type system. The only disadvantage is that the expanded version of an expression may be exponentially larger than the original.

Exercise 7.1 Find an example where a program of size O(n) expands to one of size Ω(2^{n}). □

Exercise 7.2 Argue that the expanded version is typable in the monomorphic system if and only if the original version is typable in the polymorphic system. □

Can we do better than this exponential algorithm? An obvious idea is to use a form of dynamic programming where the principal type schemes of let-definitions are saved, so that they need only be computed once. This is essentially the Damas-Milner [1] algorithm from 1982 which is implemented in the ML system. For almost ten years it was folklore that this algorithm had low polynomial time complexity. This also corresponded well with the practical experiences of ML programmers.

This belief was thorougly shattered when Mairson [5] in 1989 proved that the polymorphic type inference problem is complete for exponential time. This means that any correct implementation must use an exponential amount of time on infinitely many inputs. His proof is an awesome construction of an ML program that directly simulates a given deterministic Turing machine running in exponential time, and where typability of the program coincides with acceptance by the machine. PSPACE-hardness alone was proved by Kanellakis and Mitchell [3] earlier in 1989.

In spite of this nasty result, implementations of the ML language seem to be running very well in everyday life. But danger lurks beneath the surface. As a concrete example, regard the following ML program.

       fun pair x y = fn z => z x y;
       let val x1=fn y => pair y y in
         let val x2=fn y => x1(x1(y)) in
           let val x3=fn y => x2(x2(y)) in
             let val x4=fn y => x3(x3(y)) in
               x4(fn z=>z)
             end
           end
         end
       end;

Its principal type scheme is:

(((((((((((((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) ->
('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a -> 'a)
-> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c)
-> 'd) -> 'd) ->  ((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  ->  'a) ->
('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->
'c) -> 'c) -> 'd) -> 'd) -> 'e) -> 'e) ->  ((((((((('a  -> 'a) -> ('a ->
'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) ->
'c) -> ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) -> ('a
-> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) ->  ((((((('a -> 'a) ->
('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->
'c) -> 'c) -> ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a)
-> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> 'e) -> 'e) ->
'f) -> 'f) ->  ((((((((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  ->  'a) ->
('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->
'c) -> 'c) -> 'd) -> 'd) -> ((((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b)
-> ((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> ((((('a  ->
'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b) ->
'b) -> 'c) -> 'c) -> 'd) -> 'd) -> 'e) -> 'e) ->  ((((((((('a  -> 'a) ->
('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->
'c) -> 'c) -> ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a)
-> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> ((((((('a  ->
'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b) ->
'b) -> 'c) -> 'c) -> ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> 'e) ->
'e) -> 'f) -> 'f) -> 'g) -> 'g) ->  ((((((((((((('a -> 'a) -> ('a -> 'a)
-> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c)
->  ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) -> ('a ->
'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> ((((((('a -> 'a) -> ('a
-> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c)
-> 'c) -> ((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) ->
('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) ->  'e)  ->  'e) ->

((((((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) -> ('a ->
'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd)
-> 'd) ->  ((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a)
-> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  ->  'a) -> ('a ->
'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) ->
'c) -> 'd) -> 'd) -> 'e) -> 'e) -> 'f) -> 'f) -> ((((((((((('a -> 'a) ->
('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->
'c) -> 'c) -> ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a)
-> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> ((((((('a  ->
'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b) ->
'b) -> 'c) -> 'c) -> ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> 'e) ->
'e) -> ((((((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) ->
('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a -> 'a)
-> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c)
-> 'd) -> 'd) ->  ((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  ->  'a) ->
('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->
'c) -> 'c) -> 'd) -> 'd) -> 'e) -> 'e) -> 'f) -> 'f) ->  'g)  ->  'g) ->
'h) -> 'h) ->  ((((((((((((((('a  -> 'a) -> ('a -> 'a) ->  'b) -> 'b) ->
((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> ((((('a -> 'a)
-> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b)
-> 'c) -> 'c) -> 'd) -> 'd) ->  ((((((('a -> 'a) -> ('a -> 'a) -> 'b) ->
'b) -> ((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> ((((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> 'e) -> 'e) ->  ((((((((('a  -> 'a)
-> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b)
-> 'c) -> 'c) -> ((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a ->
'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> ((((((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a -> 'a) ->  'b) -> 'b) ->
((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) ->
'e) -> 'e) -> 'f) -> 'f) -> ((((((((((('a -> 'a) -> ('a -> 'a) -> 'b) ->
'b) -> ((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> ((((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) -> 'c) -> 'c) -> 'd) -> 'd) ->  ((((((('a -> 'a) -> ('a -> 'a) ->
'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->
((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) -> ('a -> 'a)
-> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> 'e) ->  'e) ->  ((((((((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a -> 'a) ->  'b) -> 'b) ->
((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) ->
((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a ->
'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd)

8. Polymorphism and Recursion

-> 'd) -> 'e) -> 'e) -> 'f) -> 'f) -> 'g) -> 'g) ->  ((((((((((((('a  ->
'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b) ->
'b) -> 'c) -> 'c) -> ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a
-> 'a) -> ('a -> 'a) -> 'b) -> 'b) ->  'c)  ->  'c)  ->  'd)  ->  'd) ->
((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a ->
'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd)
-> 'd) -> 'e) -> 'e) ->  ((((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b)
-> ((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> ((((('a  ->
'a) -> ('a -> 'a) -> 'b) -> 'b) ->  ((('a -> 'a) -> ('a -> 'a) -> 'b) ->
'b) -> 'c) -> 'c) -> 'd) -> 'd) -> ((((((('a -> 'a) -> ('a -> 'a) -> 'b)
-> 'b) ->  ((('a  -> 'a) -> ('a -> 'a) -> 'b) ->  'b)  ->  'c) -> 'c) ->
((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) -> ('a -> 'a)
-> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> 'e) -> 'e) -> 'f) -> 'f) ->
((((((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) -> ('a
-> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) ->  ('a -> 'a) ->
'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->
'd) -> 'd) ->  ((((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a ->
'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) ->  ((((('a  -> 'a) -> ('a
-> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c)
-> 'c) -> 'd) -> 'd) -> 'e) -> 'e) ->  ((((((((('a  -> 'a) -> ('a -> 'a)
-> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c)
->  ((((('a -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) -> ('a ->
'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) -> ((((((('a -> 'a) -> ('a
-> 'a) -> 'b) -> 'b) -> ((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> 'c)
-> 'c) -> ((((('a  -> 'a) -> ('a -> 'a) -> 'b) -> 'b) -> ((('a -> 'a) ->
('a -> 'a) -> 'b) -> 'b) -> 'c) -> 'c) -> 'd) -> 'd) ->  'e)  ->  'e) ->
'f) -> 'f) -> 'g) -> 'g) -> 'h) -> 'h) -> 'i) -> 'i

Note that by the analogy described in Section 5, the above is a gigantic tautology in propositional logic.

8 Polymorphism and Recursion

We have only allowed polymorphism in let-definitions, and even there we have some limitations. For example, the following reasonable expression is not typable— we have some slack in the polymorphic type system.

let f = fun(i)

fun(x)

if iszero(i) then x

else f(pred(i))(pair(x,x))

fi end

end

in f(87)(true)

Exercise 8.1 Argue that the above expression is not typable in the polymorphic system. □

Exercise 8.2 What is the result of the above expression? □

There are also less contrived examples showing that this restriction is a practical nuisance. The general problem is that a function is only polymorphic from the outside, so to speak. However, this can be remedied by a minor change in our type rule.

\frac{A,f : ∀ᾱ.σ ⊢ e_{1} : σ; A,f : ∀ᾱ.σ ⊢ e_{2} : τ}{A ⊢ let f = e_{1} in e_{2} end : τ} ᾱ ∉ A

Exercise 8.3 What has been changed in the type rule? □

This is the Milner-Mycroft [7] type system from 1984. A corresponding type inference algorithm must necessarily be more obscure than the earlier one, since the naïve expansion of let-definitions may now yield infinite monomorphic versions. Yet, implementations did exist for versions of the ML language. Thus it caused some concern when Henglein [2] and Kfoury, Tiuryn, and Urzyczyn [4] in 1990 simultaneously proved that the type inference problem is in fact undecidable.

The problem seems to obey the laws of cartoon physics, since people were perfectly happy with the proposed implementations before the undecidability was known. The reason is that the semi-algorithm terminates for all typable expressions and only fails to terminate for a very small fraction of untypable expressions.

9 Higher Type Systems

By no means does the development of type systems stop here. There are at least three good reasons to push on.

Firstly, there is always more slack to pick up. Many interesting type rules have been motivated by annoying examples of unfairly rejected expressions. One example is the conjunctive type written ⊢ e : σ ∧ τ, which means that e simultaneously has types σ and τ.

Exercise 9.1 Suggest rules for conjunctive types. How do they differ from products? □

Polymorphism may also be included as an orthogonal feature in the type system. Thus types may look like: ∀α.α → (∀β.β → β → β) → α This is the system F2 studied by Girard and Reynolds. Such extensions are naturally beyond the

9. Higher Type Systems

reach of type inference.

Exercise 9.2 Suggest an expression that could have the polymorphic type ∀α.α → (∀β.β → β → β) → α. □

Secondly, we might stray from a purely functional language. Many efforts have been directed towards incorporating non-functional features into ML-style type systems. For example, the mixture of polymorphism and pointers is very complicated and often requires subtle type rules.

Exercise 9.3 What is wrong with these simple rules for pointers (assume the obvious semantics for the expressions)?

\frac{A ⊢ e : τ}{A ⊢ ref(e) : pointer(τ)} \frac{A ⊢ e: pointer(τ)}{A ⊢ deref(e) : τ}

\frac{A ⊢ x : pointer(τ); A ⊢ e : pointer(τ)}{A ⊢ x:=e : pointer(τ)}

□

Thirdly, it is possible to have types that capture more of the semantics of expressions. This is done by emphasizing the logical connection and building type systems so rich that one can define e.g. a type whose values are just the sorting functions on integer lists. At this point type checking is equivalent to program verification and, hence, undecidable. This means that each program must include a hand-written but compiler-checked proof of its type-correctness.

10 Problems

Problem 10.1 Give a formal derivation showing that the expression:

let Double = fun(x)

if iszero(x) then 0

else succ(succ(Double(pred(x))))

fi end

in Double(succ(0))

has type Int.

Problem 10.2 Infer the principal type scheme for this expression:

fun(x)

fun(y)

cons(car(x),y(true)) end

end

Problem 10.3 List all constant expressions having these polymorphic types.

∀α.α
∀α.list(α)
∀α.α → α → α
∀α.∀β.(α → β) → (α → α) → α → β

Problem 10.4 Oyster of the week. Here are the rules for the existential quantifier in logic.

\frac{A ⊢ σ[α ← τ]}{A ⊢ ∃α.σ} \frac{A ⊢ ∃α.σ; A,σ ⊢ τ}{A ⊢ τ} α ∉ A, α ∉ τ

The notation σ[α ← τ] means σ with all occurrences of α substituted with τ. Explain the logical content of these rules. Introduce an existential quantifier into our type system, along with a reasonable set of expressions, and recognize an important concept from programming languages.

A Selection of Solutions

Exercise 3.1 It allows the type checker to perform lookups in the symbol table. □

10. Problems

Exercise 3.2 In the judgment for the expression being let-defined, we include f in the symbol table: A,f : σ ⊢ e_{1} : σ. □

Exercise 4.1 It is a relation that is reflexive and transitive, but fails to be anti-symmetric, e.g. α ≤ β and β ≤ α but α ≠ β. □

Exercise 4.2

α ≥ {α, β, α → β, α → α, (α → β)→ list(α)}
β ≥ {α, β, α → β, α → α, (α → β)→ list(α)}
α → β ≥ {α → β, α → α, (α → β)→ list(α)}

□

Exercise 4.3 Simply compose the substitutions. □

Exercise 4.4 Two subexpressions with identical syntax may yield different type variables, such as e.g. [[nil]]. However, from the context of each type constraint it is clear to which subexpression a type variable corresponds. □

Exercise 4.8 The two constraints [[x]] = Int and [[x]] = list([[car(x)]]) are contradictory. □

Exercise 5.1 The rules for inferring types correspond to valid inference rules of logic. □

Exercise 5.3 A function with type scheme (α → β) → (β → α) must look like:

fun(x)

fun(y) e end

end

where e has type α. An exhaustive search through the type rules convinces us that we cannot find such an expression. The fact that an expression has type (Int → Bool) → (Bool → Int) is not a problem, since this is merely one instance of the type scheme. □

Exercise 5.4

pair(e_{1},e_{2}) : [[pair(e_{1},e_{2})]] = [[e_{1}]] × [[e_{2}]]
fst(e) : [[e]] = [[fst(e)]] × α
snd(e) : [[e]] = α × [[snd(e)]]
left(e_{1}) : [[left(e_{1})]] = [[e_{1}]] + α
right(e_{2}) : [[right(e_{2})]] = α + [[e_{2}]]
decide(e,e_{1},e_{2}) : [[e_{i}]] = [[e]] → [[decide(e,e_{1},e_{2})]]

□

Exercise 5.5 The formula ((A ⇒ B) ⇒ A) ⇒ A is a classical tautology but translates into an empty type. □

Exercise 5.6 We can only solve this problem, if we allow an expression error that generates a run-time error. Then we have

car = induct(error,fun(x) snd(x) end) cdr = induct(error,fun(x) fst(x) end)

□

Exercise 5.7 (0,1,2,3,4,…) = coinduct(0,fun(x) pair(succ(x),x) end. □

Exercise 5.8 Let finbin(τ) be the type of finite binary trees with τ-values at all nodes. We then have:

\frac{A ⊢ e : τ; A ⊢ e_{1} : finbin(τ); A ⊢ e_{2} : finbin(τ)}{A ⊢ bin(e,e_{1},e_{2}) : finbin(τ)}

\frac{A ⊢ base : σ; step : σ × τ × σ → σ}{A ⊢ induct(base,step) : finbin(τ) → σ}

Let infbin(τ) be the type of infinite binary trees with τ-values at all nodes. We then have:

\frac{A ⊢ base : σ; step : σ → σ × τ × σ}{A ⊢ induct(base,step) : infbin(τ)}

\frac{A ⊢ e : infbin(τ)}{A ⊢ root(e) : τ; A ⊢ leftson(e) : infbin(τ); A ⊢ rightson(e) : infbin(τ)}

□ Exercise 6.1 The logical rules for universal quantification are:

\frac{A ⊢ σ}{A ⊢ ∀α.σ} α ∉ A \frac{A ⊢ ∀α.σ}{A ⊢ σ[α ← τ]}

□

Exercise 6.3 It is not legal to make f polymorphic in α since we have the assumption x : α. □

Exercise 7.1 The ML program on page 17 is like this (with n = 4). □

Exercise 7.2 In both approaches we are allowed to choose fresh type variables for the types of the let-defined expressions. □

Exercise 8.1 The type variable [[x]] must satisfy [[x]] = [[x]] × [[x]], which is not possible. □

Exercise 8.2 It computes a complete binary tree of height i with the value true at each leaf. □

Exercise 8.3 We have universally quantified the type of f in the judgment of e_{1}. □

Exercise 9.3 The type rules allow the typing of bad expressions, such as:

let r = ref(fun(x) x end)

in

let x = r:=ref(fun(x) succ(x) end) in deref(r)(true)

This is type correct, since r is given type ∀α.pointer(α → α) and thus can be instantiated to both pointer(Int→Int) and pointer(Bool→Bool). However, its computation leads to succ(true). □

Problem 10.3 There are no constant expressions of type ∀α.α; for ∀α.list(α) there is only nil; for ∀α.α → α → α we have two functions: fun(x) fun(y) x end end and fun(x) fun(y) y end end; finally, for ∀α.∀β.(α → β) → (α → α) → α → β there are infinitely many functions of the form: fun(f) fun(g) fun(x) f(g^{i}(x)) end end end for i ≥ 0. □

Problem 10.4 If we can prove σ with any specific value τ in place of the variable α, then τ is a witness to the truth of ∃α.σ. Conversely, if this existential quantification holds and we can prove τ using σ but without any assumptions on α, then we can conclude τ.

This corresponds to abstract data types, where the implementation type is hidden. We only need to know that is exists! The type rules are as follows:

\frac{A ⊢ e : σ[α ← τ]}{A ⊢ abs(e) : ∃α.σ} \frac{A ⊢ e_{1} : ∃α.σ; A,x : σ ⊢ e_{2} : τ}{A ⊢ use x = e_{1} in e_{2} : τ} α ∉ A, α ∉ τ

The side conditions exactly state that the implementation type is hidden during use. The type of an abstract implementation of a stack of booleans could be:

∃α.(Int → α) × (α → Bool) × (α × Bool → α) × (α → α × Bool)

corresponding to the stack operations Init, Empty, Push, and Pop. In a concrete implementation the hidden type α could be list(Bool).

A polymorphic, abstract stack would then have the type:

∀β.∃α.(Int → α) × (α → β) × (α × β → α) × (α → α × β)

□

Recent Publications in the BRICS Lecture Series

LS-95-3 Michael I. Schwartzbach. Polymorphic Type Inference. June 1995. viii+24 pp.

LS-95-2 Sven Skyum. Introduction to Parallel Algorithms. June 1995. viii+16 pp.

LS-95-1 Jaap van Oosten. Basic Category Theory. January 1995. vi+75 pp.