Theorems for free!

Philip Wadler University of Glasgow^{∗}

June 1989

Abstract

From the type of a polymorphic function we can derive a theorem that it satisfies. Every function of the same type satisfies the same theorem. This provides a free source of useful theorems, courtesy of Reynolds’ abstraction theorem for the polymorphic lambda calculus.

1 Introduction

Write down the definition of a polymorphic function on a piece of paper. Tell me its type, but be careful not to let me see the function’s definition. I will tell you a theorem that the function satisfies.

The purpose of this paper is to explain the trick. But first, let’s look at an example.

Say that r is a function of type

r : ∀X. X^{∗} → X^{∗}.

Here X is a type variable, and X^{∗} is the type “list of X ”. From this, as we shall see, it is possible to conclude that r satisfies the following theorem: for all types A and A′ and every total function a : A → A′ we have

a^{∗} ∘ r_{A} = r_{A′} ∘ a^{∗}.

Here ∘ is function composition, and a^{∗} : A^{∗} → A′^{∗} is the function “map a” that applies a elementwise to a list of A yielding a list of A′, and r_{A} : A^{∗} → A^{∗} is the instance of r at type A.

The intuitive explanation of this result is that r must work on lists of X for any type X . Since r is provided with no operations on values of type X , all it can do is rearrange such lists, independent of the values contained in them. Thus applying a to each element of a list and then rearranging yields the same result as rearranging and then applying a to each element.

For instance, r may be the function reverse : ∀X. X^{∗} → X^{∗} that reverses a list, and a may be the function code : Char → Int that converts a character to its ASCII code. Then we have

code^{∗} (reverse_{Char} [‘a’, ‘b’, ‘c’])
= [99 , 98 , 97 ]
= reverse_{Int} (code^{∗} [‘a’, ‘b’, ‘c’])

which satisfies the theorem. Or r may be the function tail : ∀X. X^{∗} → X^{∗} that returns all but the first element of a list, and a may be the function inc : Int → Int that adds one to an integer. Then we have

inc^{∗} (tail_{Int} [1 , 2 , 3 ])
= [3 , 4 ]
= tail_{Int} (inc^{∗} [1 , 2 , 3 ])

which also satisfies the theorem.

On the other hand, say r is the function odds : Int^{∗} → Int^{∗} that removes all odd elements from a list of integers, and say a is inc as before. Now we have

inc^{∗} (odds_{Int} [1 , 2 , 3 ])
= [2 , 4 ]
≠ [4 ]
= odds_{Int}(inc^{∗} [1 , 2 , 3 ])

and the theorem is not satisfied. But this is not a counterexample, because odds has the wrong type: it is too specific, Int^{∗} → Int^{∗} rather than ∀X. X^{∗} → X^{∗}.

This theorem about functions of type ∀X. X^{∗} → X^{∗} is pleasant but not earth-shaking. What is more exciting is that a similar theorem can be derived for every type.

∗Author’s address: Department of Computing Science, University of Glasgow, G12 8QQ, Scotland. Electronic mail:

wadler@cs.glasgow.ac.uk.

This is a slightly revised version of a paper appearing in: 4’th Internationl Symposium on Functional Programming Languages and Computer Architecture, London, September 1989.

Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the ACM copyright notice and the title of the publication and its date appear, and notice is given that copying is by permission of the Association for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific permission.

The result that allows theorems to be derived from types will be referred to as the parametricity result, because it depends in an essential way on parametric polymorphism (types of the form ∀X. T ). Parametricity is just a reformulation of Reynolds’ abstraction theorem: terms evaluated in related environments yield related values [Rey83]. The key idea is that types may be read as relations. This result will be explained in Section 2 and stated more formally in Section 6.

Some further applications of parametricity are shown in Figure 1, which shows several types and the corresponding theorems. Each name was chosen, of course, to suggest a particular function of the named type, but the associated theorems hold for any function that has the same type (so long as it can be defined as a term in the pure polymorphic lambda calculus). For example, the theorem given for head also holds for last, and the theorem given for sort also holds for nub (see Section 3).

The theorems are expressed using operations on functions that correspond to operations on types. Corresponding to the list type A^{∗} is the map operation a^{∗} that takes the function a : A → A′ into the function a^{∗} : A^{∗} → A′^{∗}. Similarly, corresponding to the product type A × B is the operation a × b that takes the functions a : A → A′ and b : B → B′ into the function a × b : A × B → A′ × B′; it is defined by (a × b) (x, y) = (a x, b y). As we shall see, it will be necessary to generalise to the case where a, b, a^{∗}, and a × b are relations.

How useful are the theorems so generated? Only time and experience will tell, but some initial results are encouraging:

• In general, the laws derived from types are of a form useful for algebraic manipulation. For example, many of the laws in Figure 1 allow one to “push map through a function”.

• Three years ago, Barrett and I wrote a paper on the derivation of an algorithm for compiling pattern-matching in functional languages [BW86]. The derivation used nine general theorems about higher-order functions such as map and sort. Looking at the paper again now, it turns out that of the nine theorems, five follow immediately from the types.

• Sheeran has developed a formal approach to the design of VLSI circuits that makes heavy use of mathematical laws. She has found that many of the laws she needs can be generated from types using the methods described here, and has already written a paper describing how to do so [She89].

Not surprisingly, using a more specific type system allows even more theorems to be derived from the type of a function; this has already been explored to a certain extent by Sheeran [She89]. So there is reason to believe that further research will further extend the applicability of this method.

Many functional languages, including Standard ML [Mil84, Mil87], Miranda^{1} [Tur85], and Haskell [HW88], are based on the Hindley/Milner type system [Hin69, Mil78, DM82]. This system is popular because types need not be given explicitly; instead, the principal (most general) type of a function can be inferred from its definition. However, for the purposes of this paper it is more convenient to use the Girard/Reynolds type system [Gir72, Gir86, Rey74, Rey83] (also known as the polymorphic lambda calculus, the second order lambda calculus, and System F). In the Girard/Reynolds system it is necessary to give the types of bound variables explicitly. Further, if a function has a polymorphic type then type applications must be explicitly indicated. This is done via subscripting; for example, the instance of the function r : ∀X. X^{∗} → X^{∗} at the type A is written r_{A} : A^{∗} → A^{∗}.

Every program in the Hindley/Milner system can automatically be translated into one in the Girard/Reynolds system. All that is required is a straightforward modification of the type inference algorithm to decorate programs with the appropriate type information. On the other hand, the inverse translation is not always possible, because the Girard/Reynolds system is more powerful than Hindley/Milner.

Both the Hindley/Milner and the Girard/Reynolds system satisfy the strong normalisation property: every term has a normal form, and every reduction sequence leads to this normal form. As a corollary, it follows that the fixpoint operator,

fix : ∀X. (X → X ) → X

cannot be defined as a term in these systems. For many purposes, we can get along fine without the fixpoint operator, because many useful functions (including all those shown in Figure 1) may be defined in the Girard/Reynolds system without its use. Indeed, every recursive function that can be proved total in secondorder Peano arithmetic can be written as a term in the Girard/Reynolds calculus [FLO83, Gir72, GLT89]. This includes, for instance, Ackerman’s function (see [Rey85]), but it excludes interpreters for most languages (including the Girard/Reynolds calculus itself).

If the power of unbounded recursion is truly required, then fix can be added as a primitive. However, adding fixpoints weakens the power of the parametricity theorem. In particular, if fixpoints are allowed then the Assume a : A → A′ and b : B → B′.

1 Miranda is a trademark of Research Software Limited.

head : ∀X. X^{∗} → X
a ∘ head_{A} = head_{A′} ∘ a^{∗}
tail : ∀X. X^{∗} → X^{∗}
a^{∗} ∘ tail_{A} = tail_{A′} ∘ a^{∗}
(++) : ∀X. X^{∗} → X^{∗} → X^{∗}

a^{∗} (xs ++_{A} ys) = (a^{∗} xs) ++_{A′} (a^{∗} ys)

concat : ∀X. X^{∗∗} → X^{∗} a^{∗} ∘ concat_{A} = concat_{A′} ∘ a^{∗∗}

fst : ∀X. ∀Y. X × Y → X a ∘ fst_{AB} = fst_{A′B′} ∘ (a × b)

snd : ∀X. ∀Y. X × Y → Y b ∘ snd_{AB} = snd_{A′B′} ∘ (a × b)

zip : ∀X. ∀Y. (X^{∗} × Y^{∗}) → (X × Y )^{∗} (a × b)^{∗} ∘ zip_{AB} = zip_{A′B′} ∘ (a^{∗} × b^{∗})

filter : ∀X. (X → Bool) → X^{∗} → X^{∗} a^{∗} ∘ filter_{A} (p′ ∘ a) = filter_{A′} p′ ∘ a^{∗}

sort : ∀X. (X → X → Bool) → X^{∗} → X^{∗} if for all x, y ∈ A, (x < y) = (a x <′ a y) then

a^{∗} ∘ sort_{A} (<) = sort_{A′} (<′) ∘ a^{∗}

fold : ∀X. ∀Y. (X → Y → Y ) → Y → X^{∗} → Y

if for all x ∈ A, y ∈ B, b (x ⊕ y) = (a x) ⊗ (b y) and b u = u′ then b ∘ fold_{AB} (⊕) u = fold_{A′B′} (⊗) u′ ∘ a^{∗}

I : ∀X. X → X
a ∘ I_{A} = I_{A′} ∘ a
K : ∀X. ∀Y. X → Y → X

a (K_{AB} x y) = K_{A′B′} (a x) (b y)

Figure 1: Examples of theorems from types theorems in Figure 1 hold in general only when the functions a and b are strict (that is, when a ⊥ = ⊥ and b ⊥ = ⊥)^{2} . For this reason, the bulk of this paper assumes that fixpoints are not provided; but the necessary adjustment to allow fixpoints is described in Section 7.

The fundamental idea of parametricity is not new. A restricted version of it appears in Reynolds’ original paper on the polymorphic lambda calculus [Rey74], where it is called the representation theorem, and a version similar to that used here appears in [Rey83], where it is called the abstraction theorem. Other versions include the logical relations of Mitchell and Meyer [MM85, Mit86]; and the dinatural transformations of Bainbridge, Freyd, Girard, Scedrov, and Scott [BFSS87, FGSS88], from whom I have taken the name “parametricity”.

So far as I am aware, all uses of parametricity to date have been “general”: they say something about possible implementations of the polymorphic lambda calculus (e.g. that the implementation is correct independent of the representation used) or about its models (e.g. that models should only be allowed that satisfy parametricity). The main contribution of this paper is to suggest that parametricity also has “specific” applications: it says interesting things about particular functions with particular types^{3} .

An updated statement and proof of the abstraction theorem is presented. The main reason for including these is to make the paper self-contained. In the process, it is easy to repair a minor lacunae in Reynold’s original presentation [Rey83]. That version is expressed in terms of a “naive” set-theoretic model of the polymorphic lambda calculus; Reynolds later proved that such models do not exist [Rey84]. There is nothing wrong with the theorem or the proof itself, just the context in which it is set, and it is straightforward to transpose it to another context. This paper uses the frame models of Bruce, Meyer, and Mitchell [BM84, MM85]. For other models of the polymorphic lambda calculus, see [BTC88, Mes89, Pit87].

The characterisation of parametricity given in this paper can be formulated more concisely in terms of category theory, where it can be re-expressed in terms of lax natural transformations. This will be the subject of a further paper.

The remainder of this paper is organised as follows. Sections 2 and 3 present the main new results: Section 2 presents the parametricity theorem, and Section 3 gives further applications. Sections 4–6 fill in the formalities: Section 4 describes the syntax of the polymorphic lambda calculus, Section 5 shows how its syntax can be given using frame models, and Section 6 gives the full statement of the parametricity theorem. Section 7 shows how the parametricity theorem should be adjusted to account for languages that use the fixpoint operator.

Acknowledgements. I am grateful to Harold Simmons for helping to formulate and prove the result about map in Section 3.5, and to Samson Abramsky, Val Breazu-Tannen, Peter Freyd, John Hughes, John Launchbury, John Reynolds, Andre Scedrov, and Mary Sheeran for their comments on this work.

2 Parametricity explained

The key to extracting theorems from types is to read types as relations. This section outlines the essential ideas, using a naive model of the polymorphic lambda calculus: types are sets, functions are set-theoretic functions, etc. The approach follows that in [Rey83].

Cognoscenti will recognise a small problem here— there are no naive set-theoretic models of polymorphic lambda calculus! (See [Rey84].) That’s ok; the essential ideas adopt easily to frame models [BM84, MM85]. This section sticks to the simple but naive view; the i’s will be dotted and the t’s crossed in Sections 4–6, which explain the same notions in the context of frame models.

The usual way to read a type is as a set. The type Bool corresponds to the set of booleans, and the type Int corresponds to the set of integers. If A and B are types, then the type A × B corresponds to a set of pairs drawn from A and B (the cartesian product), the type A^{∗} corresponds to the set of lists with elements in A, and the type A → B corresponds to a set of functions from A to B. Further, if X is a type variable and A(X ) is a type depending on X , then the type ∀X. A(X ) corresponds to a set of functions that take a set B and return an element in A(B).

An alternative is to read a type as a relation. If A and A′ are sets, we write A : A ⇔ A′ to indicate that A is a relation between A and A′, that is, that A ⊆ A × A′. If x ∈ A and x′ ∈ A′, we write (x, x′) ∈ A to indicate that x and x′ are related by A. A special case of a relation is the identity relation I_{A} : A ⇔ A, defined by I_{A} = {(x, x) | x ∈ A}. In other words, if x, x′ ∈ A, then (x, x′) ∈ I_{A} iff x = x′. More generally, any function a : A → A′ may also be read as a relation {(x, a x) | x ∈ A}. In other words, if x ∈ A and x′ ∈ A′, then (x, x′) ∈ a iff a x = x′.

2 This is similar to the restriction to strict coercion functions in [BCGS89], and is adopted for a similar reason.

3 Since this paper was written, I have learned that Peter de-Bruin has recently discovered similar applications [deB89], and that John Reynolds already knew of the application in Section 3.8.

To read types as relations, we give a relational equivalent for constant types and for each of the type constructors A×B, A^{∗}, A → B, and ∀X. A(X ). Constant types, such as Bool and Int, may simply be read as identity relations, I_{Bool} : Bool ⇔ Bool and I_{Int} : Int ⇔ Int.

For any relations A : A ⇔ A′ and B : B ⇔ B′, the relation A × B : (A × B) ⇔ (A′ × B′) is defined by

((x, y), (x′, y′)) ∈ A × B

iff (x, x′) ∈ A and (y, y′) ∈ B.

That is, pairs are related if their corresponding components are related. In the special case where a and b are function, then a × b is the function defined by (a × b) (x, y) = (a x, b y).

For any relation A : A ⇔ A′, the relation A^{∗} : A^{∗} ⇔ A^{′∗} is defined by

([x_{1} , …, x_{n}], [x′_{1} , …, x′_{n}]) ∈ A^{∗}

iff (x_{1} , x′_{1} ) ∈ a and … and (x_{n}, x′_{n}) ∈ A.

That is, lists are related if they have the same length and corresponding elements are related. In the special case where a is a function, a^{∗} is the familiar “map” function defined by a^{∗} [x_{1} , …, x_{n}] = [a x_{1} , …, a x_{n}].

For any relations A : A ⇔ A′ and B : B ⇔ B′, the relation A → B : (A → B) ⇔ (A′ → B′) is defined by

(f , f′) ∈ A → B

iff for all (x, x′) ∈ A, (f x, f′ x′) ∈ B.

That is, functions are related if they take related arguments into related results. In the special case where a and b are functions, the relation a → b will not necessarily be a function, but in this case (f , f′) ∈ a → b is equivalent to f′ ∘ a = b ∘ f .

Finally, we have to interpret ∀ as an operation on relations. Let F(X) be a relation depending on X. Then F corresponds to a function from relations to relations, such that for every relation A : A ⇔ A′ there is a corresponding relation F(A) : F (A) ⇔ F′(A′). Then the relation ∀X. F(X) : ∀X. F (X ) ⇔ ∀X′. F′(X′) is defined by

(g, g′) ∈ ∀X. F(X)

iff for all A : A ⇔ A′, (g_{A}, g′_{A′}) ∈ F(A).

That is, polymorphic functions are related if they take related types into related results. (Note the similarities in the definitions of A → B and ∀X. F(X).)

Using the definitions above, any closed type T (one containing no free variables) can be read as a relation T : T ⇔ T . The main result of this paper can now be described as follows:

Proposition. (Parametricity.) If t is a closed term of type T , then (t, t) ∈ T , where T is the relation corresponding to the type T .

A more formal statement of this result appears in Section 6, where it is extended to types and terms containing free variables.

3 Parametricity applied

This section first explains in detail how parametricity implies some of the theorems listed in the introduction and then presents some more general results.

3.1 Rearrangements

The result in the introduction is a simple consequence of parametricity. Let r be a closed term of type

r : ∀X. X^{∗} → X^{∗}.

Parametricity ensures that

(r, r) ∈ ∀X. X^{∗} → X^{∗}.

By the definition of ∀ on relations, this is equivalent to

for all A : A ⇔ A′, (r_{A}, r_{A′}) ∈ A^{∗} → A^{∗}

By the definition of → on relations, this in turn is equivalent to

for all A : A ⇔ A′,

for all (xs, xs′) ∈ A^{∗},

(r_{A} xs, r_{A′} xs′) ∈ A^{∗}

This can be further expanded in terms of the definition of A^{∗}. A more convenient version can be derived by specialising to the case where the relation A is a function a : A → A′. The above then becomes

for all a : A → A′, for all xs,

a^{∗} xs = xs′ implies a^{∗} (r_{A} xs) = r_{A′} xs′

or, equivalently,

for all a : A → A′, a^{∗} ∘ r_{A} = r′_{A} ∘ a^{∗}.

This is the version given in the introduction.

3.2 Fold

The function fold has the type

fold : ∀X. ∀Y. (X → Y → Y ) → Y → X^{∗} → Y .

Parametricity implies that

(fold, fold) ∈ ∀X. ∀Y. (X → Y → Y) → Y → X^{∗} → Y .

Let a : A → A′ and b : B → B′ be two functions. Applying the definition of ∀ on relations, twice, specialised to functions, gives

(fold_{AB}, fold_{A′B′}) ∈ (a → b → b) → b → a^{∗} → b

Applying the definition of → on relations, twice, gives

for all (⊕, ⊕′) ∈ (a → b → b),

for all (u, u′) ∈ b, (fold_{AB} (⊕) u, fold_{A′B′} (⊕′) u′) ∈ a^{∗} → b.

Here (⊕) is just the name of a function of two arguments; by the usual convention, (⊕) x y may be written in the infix form x ⊕ y. Further expansion shows that the condition (⊕, ⊕′) ∈ (a → b → b) is equivalent to

for all x ∈ A, x′ ∈ A′, y ∈ B, y′ ∈ B′, a x = x′ and b y = y′ implies b (x ⊕ y) = x′ ⊕′ y′.

The result as a whole may then be rephrased,

for all a : A → A′, b : B → B′, if for all x ∈ A, y ∈ B, b (x ⊕ y) = (a x) ⊕′ (b y), and b u = u′ then b ∘ fold_{AB} (⊕) u = fold_{A′B′} (⊕′) u′ ∘ a^{∗}.

The theorems derived from types can often be given a reading with an algebraic flavour, and the result about fold provides an illustration of this. Let (A, B, ⊕, u) and (A′, B′, ⊕′, u′) be two algebraic structures. The functions a and b form a homomorphism between these if b (x ⊕ y) = (a x) ⊕′ (b y) for all x and y, and if b u = u′. Similarly, let (A^{∗}, B, fold_{AB} (⊕) u) and (A^{′∗}, B′ , fold_{A′B′} (⊕′) u′) also be two algebraic structures. The functions a^{∗} and b form a homomorphism between these if b (fold_{AB} (⊕) u xs) = fold_{A′B′} (⊕′) u′ (a^{∗} xs). The result about fold states that if a and b form a homomorphism between (A, B, c, n) and (A′, B′, c′, n′), then a^{∗} and b form a homomorphism between (A^{∗}, B, fold_{AB} (⊕) u) and (A^{′∗}, B′, fold_{A′B′} (⊕′) u′).

3.3 Sorting

Let s be a closed term of the type

s : ∀X .(X → X → Bool) → (X^{∗} → X^{∗})

Functions of this type include sort and nub:

sort_{Int}(<_{Int})[3 , 1 , 4 , 2 , 5 ] = [1 , 2 , 3 , 4 , 5 ]
nub_{Int}(=_{Int})[1 , 1 , 2 , 2 , 2 , 1 ] = [1 , 2 , 1 ]

The function sort takes an ordering function and a list and returns the list sorted in ascending order, and the function nub takes an equality predicate and a list and returns the list with adjacent duplicates removed.

Applying parametricity to the type of s yields, for all a : A → A′,

if for all x, y ∈ A, (x ≺ y) = (a x ≺′ a y) then a^{∗} ∘ s_{A}(≺) = s_{A′}(≺′) ∘ a^{∗}

(Recall that Bool as a relation is just the identity relation of booleans.) As a corollary, we have

if for all x, y ∈ A, (x < y) = (a x <′ a y) then sort_{A′} (<) ∘ a^{∗} = a^{∗} ∘ sort_{A} (<′)

so maps commute with sort, when the function mapped preserves ordering. (If < and <′ are linear orderings, then the hypothesis is equivalent to requiring that a is monotonic.) As a second corollary, we have

if for all x, y ∈ A, (x ≡ y) = (a x ≡′ a y) then nub_{A′} (≡) ∘ a^{∗} = a^{∗} ∘ nub_{A} (≡′)

so maps commute with nub, when the function mapped preserves equivalence. (If ≡ and ≡′ are equality on A and A′, then the hypothesis is equivalent to requiring that a is one-to-one.)

3.4 Polymorphic equality

The programming language Miranda [Tur85] provides a polymorphic equality function, with type

(=) : ∀X. X → X → Bool.

Applying parametricity to the type of (=) yields, for all a : A → A′,

for all x, y ∈ A, (x =_{A} y) = (a x =_{A′} a y).

This is obviously false; it does not hold for all a, but only for functions a that are one-to-one.

This is not a contradiction to the parametricity theorem; rather, it provides a proof that polymorphic equality cannot be defined in the pure polymorphic lambda calculus. Polymorphic equality can be added as a constant, but then parametricity will not hold (for terms containing the constant).

This suggests that we need some way to tame the power of the polymorphic equality operator. Exactly such taming is provided by the eqtype variables of Standard ML [Mil87], or more generally by the type classes of Haskell [HW88, WB89]. In these languages, we can think of polymorphic equality as having the type

(=) : ∀^{(=)}X . X → X → Bool.

Here ∀^{(=)}X . F (X ) is a new type former, where X ranges only over types for which equality is defined. Corresponding to the type constructor ∀^{(=)} is a new relation constructor:

(g, g′) ∈ ∀^{(=)}X . F(X)

iff

for all A : A ⇔ A′ respecting (=), (g_{A}, g′_{A′}) ∈ F(A).

A relation A : A ⇔ A′ respects (=) if A relates equals to equals; that is, if whenever x =_{A} y and (x, x′) ∈ A and (y, y′) ∈ A then x′ =_{A′} y′, where (=_{A}) is equality on A and (=_{A′}) is equality on A′. In the case where A is a function a, this is equivalent to requiring that a be one-to-one.

With this definition, we can prove that the polymorphic equality operator, typed as above, satisfies the parametricity theorem. In our extended language we can define, for example, the function

nub : ∀^{(=)}X . X^{∗} → X^{∗}

and the corresponding parametricity condition is the same as that for the previous version of nub.

Thus, the more refined type structures of Standard ML and Haskell add exactly the information necessary to maintain parametricity. In Standard ML this trick works only for equality (which is built into the language), whereas in Haskell it works for any operators defined using the type class mechanism.

3.5 A result about map

Suppose that I tell you that I am thinking of a function m with the type

m : ∀X .∀Y .(X → Y ) → (X^{∗} → Y^{∗})

You will immediately guess that I am thinking of the map function, m(f ) = f^{∗}. Of course, I could be thinking of a different function, for instance, one that reverses a list and then applies f^{∗} to it. But intuitively, you know that map is the only interesting function of this type: that all others must be rearranging functions composed with map.

We can formalise this intuition as follows. Let m be a function with the type above. Then

m_{AB}(f ) = f^{∗} ∘ m_{AA}(I_{A}) = m_{BB}(I_{B}) ∘ f^{∗}

where I_{A} is the identity function on A. The function m_{AA}(I_{A}) is a rearranging function, as discussed in the preceding section. Thus, every function m of the above type can be expressed as a rearranging function composed with map, or equivalently, as map composed with a rearranging function.

The proof is simple. As we have already seen, the parametricity condition for m is that

if f′ ∘ a = b ∘ f then m_{A′B′}(f′) ∘ a^{∗} = b^{∗} ∘ m_{AB}(f )

Taking A′ = B′ = B, b = f′ = I_{B}, a = f satisfies the hypotheses, giving as the conclusion

m_{BB}(I_{B}) ∘ f^{∗} = (I_{B})^{∗} ∘ m_{AB}(f )

which gives us the second equality above, since (I_{B})^{∗} = I_{B^{∗}}. The first equality may be derived by commuting the permuting function with map; or may be derived directly by a different substitution.

3.6 A result about fold

Analogous to the previous result about map is a similar result about fold. Let f be a function with the type

f : ∀X .∀Y .(X → Y → Y ) → Y → X^{∗} → Y

Then

f_{AB} c n = fold_{AB} c n ∘ f_{AA^{∗}} cons_{A} nil_{A}

Note that f_{AA^{∗}} cons_{A} nil_{A} : A^{∗} → A^{∗} is a function that rearranges a list, so this says that every function with the type of fold can be expressed as fold composed with a rearranging function.

The proof is similar to the previous one. The parametricity condition for f is that

if c′ ∘ (a × b) = b ∘ c and n′ = b(n) then f_{A′B′} c′ n′ ∘ a^{∗} = b ∘ f_{AB} c n

Taking A = A′, B = A^{∗}, a = I_{A}, b = fold_{A′B′} c′ n′, c = cons_{A}, n = nil_{A} satisfies the hypothesis, giving as the conclusion

f_{AB′} c′ n′ ∘ I_{A}^{∗} = fold_{AB′} c′ n′ ∘ f_{AA^{∗}} cons_{A} nil_{A}

The I_{A}^{∗} term is just an identity, and so drops out, leaving us with the desired equality if we rename c′, n′, B′ to c, n, B.

3.7 A result about filter

Let f be a function with the type

f : ∀X .(X → Bool) → X^{∗} → X^{∗}

Three functions with this type are filter, takewhile, and dropwhile. For example,

filter odd [3 , 1 , 4 , 5 , 2 ] = [3 , 1 , 5 ]
takewhile odd [3 , 1 , 4 , 5 , 2 ] = [3 , 1 ]
dropwhile odd [3 , 1 , 4 , 5 , 2 ] = [4 , 5 , 2 ]

See [BW88] for the definitions of these functions.

For every such f we can define a corresponding function of type

g : ∀X .(X × Bool)^{∗} → X^{∗}

such that f and g are related by the equation

f_{A}(p) = g_{A} ∘ ⟨I_{A}, p⟩ (∗)

where ⟨I_{A}, p⟩ x = (x, p x). That is, f_{A} is passed a predicate p of type A → Bool and a list of A, whereas g_{A} is passed a list of A × Bool pairs, the second component of the pair being the result of applying p to the first component. Intuitively, this transformation is possible because the only values that p can be applied to are of type A, so it suffices to pair each value of type A with the result of applying p to it.

A little thought shows that a suitable definition of g is

g_{A} = fst^{∗} ∘ f_{A×Bool}(snd)

We can use parametricity to show that f and g satisfy (∗), for all functions f of the given type. The parametricity conditions for f tells us that for any a : A → A′ and any p : A → Bool and p′ : A′ → Bool we have

if p′ ∘ a = I_{Bool} ∘ p then f_{A′}(p′) ∘ a^{∗} = a^{∗} ∘ f_{A}(p)

Take A′ = A × Bool and a = ⟨I_{A}, p⟩ and p′ = snd. Then the hypothesis becomes snd ∘ ⟨I_{A}, p⟩ = p, which is satisfied, yielding the conclusion

f_{A×Bool}(snd) ∘ ⟨I_{A}, p⟩^{∗} = ⟨I_{A}, p⟩^{∗} ∘ f_{A}(p).

Compose both sides with fst^{∗}, giving

fst^{∗} ∘ f_{A×Bool}(snd) ∘ ⟨I_{A}, p⟩^{∗} = fst^{∗} ∘ ⟨I_{A}, p⟩^{∗} ∘ f_{A}(p).

Then apply the definition of g, and observe that fst ∘ ⟨I_{A}, p⟩ = I_{A}, resulting in the equation

g_{A} ∘ ⟨I_{A}, p⟩^{∗} = f_{A}(p)

as desired.

3.8 An isomorphism

The preceding applications can all be expressed in the Hindley/Milner fragment of the polymorphic lambda calculus: all universal quantifiers appear at the outside of a type. This section presents an application that utilises the full power of the Girard/Reynolds system.

Let A be an arbitrary type. Intuitively, this type is isomorphic to the type ∀X. (A → X ) → X , which we will abbreviate as Ã. The apparent isomorphism between A and Ã is expressed by the functions:

i : A → Ã
i = λx : A. ΛX. λg : A → X. g x
j : Ã → A
j = λh : Ã. h_{A} (λx : A. x)

That is, i takes an element x of A to the element of Ã that maps a function g (of type A → X ) to the value g x (of type X ). The inverse function j recovers the original element by applying a value in Ã to the identity function.

To prove that this truly is an isomorphism, we must verify that j ∘ i and i ∘ j are both identities. It is easy enough to verify the former:

j (i x)

= j (ΛX. λg : A → X. g x)
= (λg : A → A. g x) (λx : A. x)
= (λx : A. x) x
= x

However, the inverse identity is problematic. We can get as far as

i (j h)

= i (h_{A} (λx : A. x))
= ΛX. λg : A → X. g (h_{A} (λx : A. x))

and now we are stuck. Here is where parametricity helps. The parametricity condition for h : ∀X. (A → X ) → X is that, for all b : B → B′ and all f : A → B,

b (h_{B} f ) = h_{B′} (b ∘ f )

Taking B = A, B′ = X , b = g, and f = (λx : A. x) gives

ΛX. λg : A → X. g (h_{A} (λx : A. x))
= ΛX. λg : A → X. h_{X} (g ∘ (λx : A. x))
= ΛX. λg : A → X. h_{X} g
= h

which completes the second identity.

The second identity depends critically on parametricity, so the isomorphism holds only for models in which all elements satisfy the parametricity constraint. Alas, the parametricity theorem guarantees only that elements of the model that correspond to lambda terms will be parametric; many models contain additional elements that are non-parametric. One model that contains only parametric elements is that in [BTC88].

X̄ ; x̄, x : T ⊢ x : T

→I \frac{X̄ ; x̄, x : U ⊢ v : V}{X̄ ; x̄ ⊢ λx : U. v : U → V}

→E \frac{X̄ ; x̄ ⊢ t : U → V X̄ ; x̄ ⊢ u : U}{X̄ ; x̄ ⊢ t u : V}

∀I \frac{X̄ ; x̄ ⊢ t : T}{X̄ , X ; x̄ ⊢ ΛX. t : ∀X. T}

∀E \frac{X̄ ; x̄ ⊢ t : ∀X. T}{X̄ ; x̄ ⊢ t_{U} : T [U /X ]}

Figure 2: Typing rules

4 Polymorphic lambda calculus

We now turn to a more formal development of the parametricity theorem. We begin with a quick review of the polymorphic lambda calculus.

We will use X , Y , Z to range over type variables, and T , U , V to range over types. Types are formed from type variables, function types, and type abstraction:

T ::= X | T → U | ∀X. T

We will use x, y, z to range over individual variables, and t, u, v to range over terms. Terms are formed from individual variables, abstraction and application of individuals, and abstraction and application of types:

t ::= x | λx : U. t | t u | ΛX. t | t_{U}

We write T [U /X ] to denote substitution of U for the free occurrences of X in T , and t[u/x] and t[U /X ] similarly.

A term is legal only if it is well typed. Typings are expressed as assertions of the form

X̄ ; x̄ ⊢ t : T

where X̄ is a list of distinct type variables X_{1} , …, X_{m}, and x̄ is a list of distinct individual variables, with types, x_{1} : T_{1} , …, x_{n} : T_{n}. This assertion may be read as stating that t has type T in a context where each x_{i} has type T_{i}. Each individual variable that appears free in t should appear in x̄, and each type variable that appears free in T of x̄ should appear in X̄ . The type inference rules are shown in Figure 2.

Two terms are equivalent if one can be derived from the other by renaming bound individual or type variables (α conversion). In addition, we have the familiar reduction rules:

(β)  (λx : U. t) u ⇒ t[u/x]
(ΛX. t)_{U} ⇒ t[U /X ]
(η)  λx : U. t x ⇒ t
ΛX. t_{X} ⇒ t

where in the η rules x and X do not occur free in t. As is well known, familiar types such as booleans, pairs, lists, and natural numbers can be defined as types constructed from just → and ∀; see for example [Rey85] or [GLT89]. Alternatively, we could add suitable types and individual constants to the pure language described above.

5 Semantics of polymorphic lambda calculus

We will give a semantics using a version of the frame semantics outlined in [BM84] and [MM85]. We first discuss the semantics of types, and then discuss the semantics of terms.

5.1 Types

A type model consists of a universe U of type values, and two operations, → and ∀ that construct types from other types. There is a distinguished set [U → U] of functions from U to U. If A and B are in U, then A → B must be in U, and if F is in [U → U], then ∀F must be in U.

Let T be a type with its free variables in X̄ . We say that Ā is a type environment for X̄ if it maps each type variable in X̄ into a type value in U. The corresponding value of T in the environment Ā is written [[T ]]Ā and is defined as follows:

[[X ]]Ā  = Ā[[X ]]
[[T → U ]]Ā = [[T ]]Ā → [[U ]]Ā
[[∀X. T ]]Ā = ∀(λA. [[T ]]Ā[A/X ])

Here Ā[[X ]] is the value that Ā maps X into, and Ā[A/X ] is the environment that maps X into A and otherwise behaves as Ā. (The reader may find that the above looks more familiar if Ā is replaced everywhere by a Greek letter such as η.)

5.2 Terms

Associated with each type A in U is a set D_{A} of the values of that type.

For each A and B in U, the elements in D_{A→B} represent functions from D_{A} to D_{B}. We do not require that the elements are functions, merely that they represent functions. In particular, associated with each A and B in U there must be a set [D_{A} → D_{B}] of functions from D_{A} to D_{B}, and functions

ϕ_{A,B} : D_{A→B} → [D_{A} → D_{B}]
ψ_{A,B} : [D_{A} → D_{B}] → D_{A→B}

such that ϕ_{A,B} ∘ ψ_{A,B} is the identity on [D_{A} → D_{B}]. We will usually omit the subscripts and just write ϕ and ψ.

If F is a function in [U → U], the elements in D_{∀F} represent functions that take a type A into an element of D_{F(A)}. In particular, associated with each F there must be a set [∀A : U. D_{F(A)}] of functions that map each A in U into an element of D_{F(A)}, and functions

Φ_{F} : D_{∀F} → [∀A : U. D_{F(A)}]
Ψ_{F} : [∀A : U. D_{F(A)}] → D_{∀F}

such that Φ_{F} ∘ Ψ_{F} is the identity on [∀A : U. D_{F(A)}]. Again, we will usually omit the subscripts and just write Φ and Ψ.

Let t be a term such that X̄ ; x̄ ⊢ t : T . We say that Ā, ā are environments respecting X̄ , x̄ if Ā is a type environment for X̄ and ā is an environment mapping variables to values such that for each x̄_{i} : T_{i} in x̄, we have that ā[[x_{i}]] ∈ D_{[[T_{i} ]]Ā}. The value of t in the environments Ā and ā is written [[t]]Ā ā and is defined as follows:

[[x]]Ā ā  = ā[[x]]
[[λx : U. v]]Ā ā = ψ (λa. [[v]]Ā ā[a/x])
[[t u]]Ā ā  = ϕ ([[t]]Ā ā) ([[u]]Ā ā)
[[ΛX. v]]Ā ā  = Ψ (λA. [[v]]Ā[A/X ] ā)
[[t_{U} ]]Ā ā  = Φ ([[t]]Ā ā) ([[U ]]Ā)

Here ā[[x]] is the value that ā maps x into, and ā[a/x] is the environment that maps x into a and otherwise behaves as ā.

A frame is a structure specifying U, →, ∀ and D, ϕ, ψ, Φ, Ψ satisfying the constraints above. A frame is an environment model if for every X̄ ; x̄ ⊢ t : T and every Ā, ā respecting X̄ , x̄, the meaning of [[t]]Ā ā as given above exists. (That is, a frame is a model if the sets [U → U], [[D_{A} → D_{B}], and [∀A : U. D_{F(A)}] are “big enough”.)

We write X̄ ; x̄ ⊧ t : T if for all environments Ā, ā respecting X̄ , x̄, we have [[t]]Ā ā ∈ D_{[[T]]Ā}.

Proposition. (Soundness of types.) For all X̄ , x̄, t and T , if X̄ ; x̄ ⊢ t : T then X̄ ; x̄ ⊧ t : T .

The type soundness result simply states that the meaning of a typed term corresponds to the meaning of the corresponding type. The proof is a straightforward induction over the structure of type inferences. Parametricity is an analogue of this result, as we shall see in the next section.

6 The parametricity theorem

In the previous section, we defined a semantics where a type environment Ā consists of a mapping of type variables onto types, and the semantics of a type T in the environment Ā is a set denoted D_{[[T]]Ā}. In this section, we define an alternative semantics where a type environment Ā consists of a mapping of type variables onto relations, and the semantics of a type T in the environment Ā is a relation denoted [[T ]]Ā.

We can then formally state the parametricity theorem: terms in related environments have related values. We can think of environments Ā and Ā′ as specifying two different representations of types, related by Ā, which is why Reynolds’ called his version of this result “the abstraction theorem”. A key point of this paper is that this theorem has applications other than change of representation, hence the change in name from “abstraction” to “parametricity”

A function type may be regarded as a relation as follows. If A : A ⇔ A′ and B : B ⇔ B′ are two relations, then we define

A → B : (A → B) ⇔ (A′ → B′)

to be the relation

A → B = \{ (f , f′) | \begin{matrix}(a, a′) ∈ A implies \\ (ϕ f a, ϕ f′ a′) ∈ B \} \end{matrix}

In other words, functions are related if they map related arguments into related results.

A type abstraction may be regarded as a relation as follows. Let F be a function from U to U, and F′ be a function from U′ to U′, and for each A in U and A′ in U′, let F be a function that takes a relation A : A ⇔ A′ and returns a relation F(A) : F (A) ⇔ F′(A′). Then we define

∀F : ∀F ⇔ ∀F′

to be the relation

∀F = \{ (g, g′) | \begin{matrix}for all A, A′, and A : A ⇔ A′, \\ (Φ(g)(A), Φ(g′)(A′)) ∈ F(A) \} \end{matrix}

In other words, type abstractions are related if they map related types into related results.

A relation environment maps each type variable into a relation. Let Ā be a relation environment for X̄ , and let Ā, Ā′ be two type environments for X̄ . We write Ā : Ā ⇔ Ā′ if for each X in X̄ we have Ā[[X ]] : Ā[[X ]] ⇔ Ā′[[X ]].

Given a relation environment Ā we can interpret a type T as a relation [[T ]]Ā as follows:

[[X ]]Ā  = Ā[[X ]]
[[U → V ]]Ā = [[U ]]Ā → [[V ]]Ā
[[∀X. V ]]Ā = ∀(λA. [[V ]]Ā[A/X ])

Let Ā, ā respect X̄ , x̄ and Ā′, ā′ respect X̄ , x̄. We say that Ā, Ā, Ā′, ā, ā′ respect X̄ , x̄ if Ā : Ā ⇔ Ā′ and (ā[[x_{i}]], ā′[[x_{i}]]) ∈ [[T_{i}]]Ā for each x_{i} : T_{i} in x̄. It is easy to see that if Ā, Ā, Ā′, ā, ā′ respect X̄ , x̄ then Ā, ā respect X̄ , x̄ and Ā′, ā′ respect X̄ , x̄.

We say that X̄ ; x̄ |⊧ t : T iff for every Ā, Ā, Ā′, ā, ā′ that respect X̄ , x̄ we have ([[t]]Āā, [[t]]Ā′ā′) ∈ [[T ]]Ā.

Proposition. (Parametricity.) For all X̄ , x̄, t, and T , if X̄ ; x̄ ⊢ t : T then X̄ ; x̄ |⊧ t : T .

Proof. The proof is a straightforward induction over the structure of type inferences. For each of the inference rules in Figure 2, we replace ⊢ by |⊧ and show that the resulting inference is valid. (End of proof.)

As mentioned previously, data types such as booleans, pairs, lists, and natural numbers can be defined in terms of → and ∀.

As an example, consider the construction for pairs. The type X × Y is defined as an abbreviation:

X × Y =^{def} ∀Z. (X → Y → Z ) → Z

Every term of type X × Y is equivalent to a term of the form pair_{XY} x y, where x : X and y : Y , and pair is defined by

pair =^{def} ΛX. ΛY. λx : X. λy : Y. ΛZ. λp : X → Y → Z. p x y

The type of pair is, of course,

pair : ∀X. ∀Y. X → Y → X × Y

where X × Y stands for the abbreviation above. It follows from the parametricity theorem that if A : A → A′ and B : B → B′, and (a, a′) ∈ A and (b, b′) ∈ B, then

( \begin{matrix}[[pair_{XY} x y]][A/X , B/Y ] [a/x, b/y], \\ [[pair_{XY} x y]][A′/X , B′/Y ] [a′/x, b′/y] ) \end{matrix}

∈ [[X × Y ]][A/X , B/Y ].

That is, pairs are related if their corresponding components are related, as we would expect.

It can be shown similarly, using the standard construction for lists, that lists are related if they have the same length and corresponding elements are related.

Alternatively, suitable type constructors and individual constants may be added to the pure polymorphic lambda calculus. In this case, for each new type constructor an appropriate corresponding relation must be defined; suitable definitions of relations for pair and list types were given in Section 2. Further, for each new constant the parametricity condition must be verified: if c is a constant of type T , we must check that |⊧ c : T holds. It then follows that parametricity holds for any terms built from the new type constructors and constants.

7 Fixpoints

Every term in typed lambda calculus is strongly normalising, so if a fixpoint operator is desired it must be added as a primitive. This section mentions the additional requirements necessary to ensure that the fixpoint primitive satisfies the abstraction theorem.

Frame models associate with each type A a set D_{A}. In order to discuss fixpoints, we require that each set have sufficient additional structure to be a domain: it must be provided with an ordering ⊑ such that each domain has a least element, ⊥, and such that limits of directed sets exist. Obviously, we also require that all functions are continuous.

What are the requirements on relations? The obvious requirement is that they, too, be continuous. That is, if A : A ⇔ A′, and x_{i} is a chain in A, and x′_{i} is a chain in A′, and (x_{i}, x′_{i}) ∈ A for every i, then we require that (⨆ x_{i}, ⨆ x′_{i}) ∈ A also. But in addition to this, we need a second requirement, namely that each relation A is strict, that is, that (⊥_{A}, ⊥_{A′}) ∈ A. If we restrict relations in this way, then it is no longer true that every function a : A → A′ may be treated as a relation; only strict functions may be treated as such.

With this restricted view of relations, it is easy to show that the fixpoint operator satisfies the parametricity theorem. As usual, for each type A define fix_{A} as the function

fix : ∀X. (X → X ) → X

such that fix_{A} f = ⨆ f^{i} ⊥_{A}. Parametricity holds if (fix, fix) ∈ ∀A. (A → A) → A. This will be true if for each A : A ⇔ A′ and each (f , f′) ∈ A → A we have (fix_{A} f , fix_{A′} f′) ∈ A. Recall that the condition on f and f′ means that if (x, x′) ∈ A then (f x, f′ x′) ∈ A. Now, since all relations are strict, it follows that (⊥_{A}, ⊥_{A′}) ∈ A; hence (f ⊥_{A}, f′ ⊥_{A′}) ∈ A; and, in general, (f^{i} ⊥_{A}, f′^{i} ⊥_{A′}) ∈ A. It follows, since all relations are continuous, that (⨆ f^{i} ⊥_{A}, ⨆ f′^{i} ⊥_{A′}) ∈ A, as required.

Note that the restriction to strict relations here is similar to the restriction to strict coercion functions in [BCGS89], and is adopted for similar reasons.

The requirement that relations are strict is essential. For a counterexample, take A to be the domain {⊥, true, false}, and take A : A → A to be the constant relation such that (x, true) ∈ A for all x. The relation A is continuous but not strict. Let f be the constant function f x = false and let f′ be the identity function f′ x = x. Then A → A relates f to f′, but A does not relate fix_{A} f = false to fix_{A} f′ = ⊥.

The restriction to strict arrows is not to be taken lightly. For instance, given a function r of type

r : ∀A.A^{∗} → A^{∗}

parametricity implies that

r_{A′} ∘ a^{∗} = a^{∗} ∘ r_{A}

for all functions a : A → A′. If the fixpoint combinator appears in the definition of r, then we can only conclude that the above holds for strict a, which is a significant restriction.

The desire to derive theorems from types therefore suggests that it would be valuable to explore programming languages that prohibit recursion, or allow only its restricted use. In theory, this is well understood; we have already noted that any computable function that is provably total in second-order Peano arithmetic can be defined in the pure polymorphic lambda calculus, without using the fixpoint as a primitive. However, practical languages based on this notion remain terra incognita.

References

[BCGS89] V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov, Inheritance and explicit coercion. In 4’th Annual Symposium on Logic in Computer Science, Asilomar, California, June 1989.

[BFSS87] E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P. J. Scott, Functorial polymorphism. In G. Huet, editor, Logical Foundations of Functional Programming, Austin, Texas, 1987. Addison-Wesley, to appear.

[BM84] K. B. Bruce and A. R. Meyer, The semantics of second-order polymorphic lambda calculus. In Kahn, MacQueen, and Plotkin, editors, Semantics of Data Types, Sophia-Antipolis, France, 1984, pp. 131–144. LNCS 173, Springer-Verlag.

[BTC88] V. Breazu-Tannen and T. Coquand, Extensional models for polymorphism. Theoretical Computer Science, 59:85–114, 1988.

[BW86] G. Barrett and P. Wadler, Derivation of a pattern-matching compiler. Manuscript, Programming Research Group, Oxford, 1986.

[BW88] R. Bird and P. Wadler, Introduction to Functional Programming. Prentice Hall, 1988.

[DM82] L. Damas and R. Milner, Principal type schemes for functional programs. In Proceedings of the 9’th Annual Symposium on Principles of Programming Languages, Albuquerque, N.M., January 1982.

[deB89] P. J. deBruin, Naturalness of polymorphism. Submitted to Category Theory and Computer Science, Manchester, 1989.

[FGSS88] P. J. Freyd, J. Y. Girard, A. Scedrov, and P. J. Scott, Semantic parametricity in polymorphic lambda calculus. In 3’rd Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, June 1988.

[FLO83] S. Fortune, D. Leivant, and M. O’Donnell, The expressiveness of simple and secondorder type structures. Journal of the ACM, 30(1):151–185, January 1983.

[Gir72] J.-Y. Girard, Interprétation functionelle et élimination des coupures dans l’arithmétique d’ordre supérieure. Ph.D. thesis, Université Paris VII, 1972.

[Gir86] J.-Y. Girard, The system F of variable types, fifteen years later. Theoretical Computer Science, 45, pp. 159–192.

[GLT89] J.-Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types. Cambridge University Press, 1989.

[Hin69] R. Hindley, The principal type scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, pp. 29–60, December 1969.

[HW88] P. Hudak and P. Wadler, editors, Report on the Functional Programming Language Haskell. Technical Report YALEU/DCS/ RR656, Yale University, Department of Computer Science, December 1988; also Technical Report, Glasgow University, Department of Computer Science, December 1988.

[Mes89] J. Meseguer, Relating models of polymorphism. In 16’th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989.

[Mil78] R. Milner, A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, pp. 348–375, 1978.

[Mil84] R. Milner, A proposal for Standard ML. In ACM Symposium on Lisp and Functional Programming, Austin, Texas, August 1984.

[Mil87] R. Milner, Changes to the Standard ML core language. Report ECS-LFCS-87-33, Edinburgh University, Computer Science Dept., 1987.

[Mit86] J. C. Mitchell, Representation independence and data abstraction. In 13’th ACM Symposium on Principles of Programming Languages, pp. 263–276.

[MM85] J. C. Mitchell and A. R. Meyer, Second-order logical relations. In R. Parikh, editor, Logics of Programs, Brooklyn, New York, 1985. LNCS 193, Springer-Verlag.

[Pit87] A. M. Pitts, Polymorphism is set theoretic, constructively. In D. H. Pitt, et al., editors, Category Theory and Computer Science, Edinburgh, 1987. LNCS 283, Springer-Verlag.

[Rey74] J. C. Reynolds, Towards a theory of type structure. In B. Robinet, editor, Proc. Colloque sur la Programmation, LNCS 19, Springer-Verlag.

[Rey83] J. C. Reynolds, Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pp. 513–523. North-Holland, Amsterdam.

[Rey84] J. C. Reynolds, Polymorphism is not set theoretic. In Kahn, MacQueen, and Plotkin, editors, Semantics of Data Types, Sophia-Antipolis, France, 1984, pp. 145–156. LNCS 173, Springer-Verlag.

[Rey85] J. C. Reynolds, Three approaches to type structure. In Mathematical Foundations of Software Development, LNCS 185, Springer-Verlag, 1985.

[She89] M. Sheeran, Categories for the working hardware designer. In Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects, Cornell, July 1989.

[Tur85] D. A. Turner, Miranda: A non-strict functional language with polymorphic types. In Proceedings of the 2’nd International Conference on Functional Programming Languages and Computer Architecture, Nancy, France, September 1985. LNCS 201, Springer-Verlag, 1985.

[WB89] P. Wadler and S. Blott, How to make adhoc polymorphism less ad hoc. In 16’th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989.