This is a preprint of a paper that will appear in the Proceedings of the 1991 Mathematical Foundations of Programming Semantics Conference, ed. S. Brookes, M. Main, A. Melton, M. Mislove, and D. A. Schmidt, to be published in the Springer-Verlag Lecture Notes in Computer Science.

Types, Abstraction, and Parametric Polymorphism, Part 2^{∗}

QingMing Ma and John C. Reynolds School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890, USA

qingming.ma@cs.cmu.edu john.reynolds@cs.cmu.edu

Abstract

The concept of relations over sets is generalized to relations over an arbitrary category, and used to investigate the abstraction (or logical-relations) theorem, the identity extension lemma, and parametric polymorphism, for Cartesian-closed-category models of the simply typed lambda calculus and PL-category models of the polymorphic typed lambda calculus. Treatments of Kripke relations and of complete relations on domains are included.

In [1], the idea that type structure enforces abstraction was formalized by an “abstraction theorem” that was proved for both the simply typed (or first-order) lambda calculus and the polymorphic (or second-order) lambda calculus [2, 3, 4]. In the polymorphic case this theorem led naturally to a definition of “parametric” polymorphism that captured the intuitive concept first described by Strachey [5]. Unfortunately, however, most of the results of [1] were limited to a classical set-theoretic model. Thus the abstraction theorem for the simply typed case was merely a repetition of the logical-relations theorem for the typed lambda-calculus [6], while the developments for the polymorphic case were vacuous, since it was later shown that there is no classical set-theoretic model of the polymorphic lambda calculus [7, 8].

∗This research was sponsored in part by National Science Foundation Grant CCR-8922109 and in part by the Avionics Lab, Wright Research and Development Center, Aeronautical Systems Division (AFSC), U.S. Air Force, Wright-Patterson AFB, OH 45433-6543 under Contract F33615-90-C-1465, Arpa Order No. 7597. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government.

In the present paper, we will recast these ideas in a general category-theoretic setting, using the framework of Cartesian closed categories for the simply typed case and the framework of PL-categories [9, 10, 11] for the polymorphic case.

Abstraction or logical-relations theorems, parametric polymorphism, and related topics have been explored by a variety of researchers. A comparison with their work is given in the final section of this paper.

We use the category-theoretic notations of [8], except that we write Ob K to denote the class of objects of a category K, and Ob F to denote the object part of a functor F. Also, for Cartesian closed categories, we will extend the exponentiation operator ⇒ to accept morphisms as well as objects as its righthand argument: If K is a Cartesian closed category and f ^{∈} k′ ⟶_{K} k′′, we write k ⟹_{K} f for the unique morphism from k ⟶_{K} k′ to k ⟶_{K} k′′ such that

[figure: (k ⇒ k′) × k; k′; (k ⇒ k′′) × k; k′′; ap; ap; (k ⇒ f) × I; f]

commutes in K. (It is well known that k ⇒ (−) is a functor that is the right adjoint of (−) × k.)

1 Syntax

In defining the syntax of the polymorphic lambda calculus, we take a slightly unusual view based on [11]. We use natural numbers as type variables, and also regard a natural number as the set of its predecessors, so that each n is both a finite set of type variables and the first type variable not in that set. Let Ω_{n} be the least family of sets satisfying:

Type Variables If i ^{∈} n then i ^{∈} Ω_{n} .
Functional Types If ω, ω′ ^{∈} Ω_{n} then ω → ω′ ^{∈} Ω_{n} .
Polymorphic Types If ω ^{∈} Ω_{n+1} then Δn. ω ^{∈} Ω_{n} .

Then Ω_{n} is the set of type expressions, over the type variables in n, of the second-order or polymorphic typed lambda calculus (or, if the final property is omitted, of the first-order or simply typed lambda calculus).

The novelty here is that the outermost bound type variable of a type expression in Ω_{n} must be n. This has the advantage that expressions are canonical with respect to alpha variation, but the disadvantage that Ω_{n} is not a subset of Ω_{n+1}. Instead, for each ω ^{∈} Ω_{n}, there is a corresponding ω̂ ^{∈} Ω_{n+1} obtained by incrementing each bound variable.

More generally, if ω ^{∈} Ω_{m} and σ ^{∈} (Ω_{n})^{m} then the type substitution ω/σ ^{∈} Ω_{n} is defined by

i/σ = σi
(ω → ω′)/σ = (ω/σ) → (ω′/σ)
(Δm. ω)/σ = Δn. (ω/[ σ | m: n]) ,

where [ σ | m: n] denotes the function with domain dom σ ∪ {m} such that [ σ | m: n]k = if k = m then n else σk. As special cases, if ω ^{∈} Ω_{n} then

ω̂ =^{def} ω/J_{n⊆Ω_{n+1}} ^{∈} Ω_{n+1} ,

where J_{n⊆Ω_{n+1}} is the identity injection from n to Ω_{n+1}, and if ω ^{∈} Ω_{n+1} and ω′ ^{∈} Ω_{n} then

ω/n → ω′ =^{def} ω/[ I_{n} | n: ω′] .

For type assignments and ordinary expressions, we treat type variables (but not ordinary variables) in the same way. A type assignment π over n is a function from some finite set dom π of ordinary variables to Ω_{n}; we write Ω_{n}^{∗} for the set of type assignments over n. Type substitution is defined pointwise on type assignments, i.e. (π/σ)v =^{def} (πv)/σ. As with type expressions, we write π̂ for π/J_{n⊆Ω_{n+1}} and π/n → ω′ for π/[ I_{n} | n: ω′].

The typing judgement π ⊢_{n} e : ω, that the ordinary expression e has type ω ^{∈} Ω_{n} under the type assignment π ^{∈} Ω_{n}^{∗}, holds iff it can be derived from the following inference rules:

Ordinary Variables

\overline{π ⊢_{n} v : πv} when v ^{∈} dom π

Applications

\frac{π ⊢_{n} e_{1} : ω → ω′ π ⊢_{n} e_{2} : ω}{π ⊢_{n} e_{1} e_{2} : ω′}

Abstractions

\frac{[ π | v: ω] ⊢_{n} e : ω′}{π ⊢_{n} λv_{ω}. e : ω → ω′}

Type Applications

\frac{π ⊢_{n} e : Δn. ω}{π ⊢_{n} e[ω′] : ω/n → ω′} when ω′ ^{∈} Ω_{n}

Type Abstractions

\frac{π̂ ⊢_{n+1} e : ω}{π ⊢_{n} Λn. e : Δn. ω}

(For the first-order typed lambda calculus, the last two rules are omitted.) We write E_{nπω} for the set of ordinary expressions e such that π ⊢_{n} e : ω.

The operation of type substitution can also be defined for ordinary expressions. If π ⊢_{m} e : ω and σ ^{∈} (Ω_{n})^{m} then one can define e/σ such that (π/σ) ⊢_{n} (e/σ) : (ω/σ). (We omit the definition, which is equivalent to that given in [11].) As with type expressions, we write ê for e/J_{n⊆Ω_{n+1}} and e/n → ω′ for e/[ I_{n} | n: ω′].

2 The First-Order Case

For the simply typed lambda calculus, semantics is provided by Cartesian closed categories. For such a category K, the meaning of type expressions and assignments is given by a family of semantic functions

[[−]]_{n}^{K} ^{∈} (Ω_{n} ∪ Ω_{n}^{∗}) → (Ob K)^{(Ob K)^{n}}

satisfying:

Type Variables If i ^{∈} n then

[[i]]_{n}θ = θi .

Functional Types If ω, ω′ ^{∈} Ω_{n} then

[[ω → ω′]]_{n}θ = [[ω]]_{n}θ ⟹_{K} [[ω′]]_{n}θ .

Type Assignments If π ^{∈} Ω_{n}^{∗} then

[[π]]_{n}θ = \begin{matrix}∏ & K \\ v^{∈}dom π \end{matrix}[[πv]]_{n}θ .

(where k ⟹_{K} k′ denotes the exponentiation of k′ by k), and the meaning of ordinary expressions is given by a family

[[−]]_{nπω}^{K} ^{∈} E_{nπω} → ∏_{θ^{∈}(Ob K)^{n}}([[π]]_{n}^{K}θ ⟶_{K} [[ω]]_{n}^{K}θ)

satisfying:

Ordinary Variables If π ⊢_{n} v : πv then [[v]]_{nπ πv} is the projection morphism from [[π]]_{n}θ = \begin{matrix}∏ & K \\ v^{∈}dom π \end{matrix}[[πv]]_{n}θ to [[πv]]_{n}θ.

Applications If π ⊢_{n} e_{1} : ω → ω′ and π ⊢_{n} e_{2} : ω then

[[e_{1}e_{2}]]_{nπω′}θ = ⟨[[e_{1}]]_{nπ ω→ω′}θ, [[e_{2}]]_{nπω}θ⟩; ap ,

where ⟨[[e_{1}]]_{nπ ω→ω′}θ, [[e_{2}]]_{nπω}θ⟩ is the mediating morphism from [[π]]_{n}θ to the product ([[ω]]_{n}θ ⟹_{K} [[ω′]]_{n}θ) × [[ω]]_{n}θ, and ap is the application morphism from this product to [[ω′]]_{n}θ.

Abstractions If [ π | v: ω] ⊢_{n} e : ω′ then

[[λv_{ω}. e]]_{nπ ω→ω′}θ = ab(¶; [[e]]_{n [π|v:ω] ω′}θ) ,

where ¶ is the mediating morphism from [[π]]_{n}θ×[[ω]]_{n}θ to [[[ π | v: ω]]]_{n}θ (which is an isomorphism when v ∉ dom π).

The classical set-theoretic model is obtained by taking K to be SET, the category of sets and functions. In [1], an abstraction theorem for this model was developed by introducing an additional semantic function that interprets types as binary relations (or more generally as relations of some fixed arity). Let Ob REL denote the class of binary relations (anticipating that we will extend this class to a category momentarily), and let

[[−]]_{n}^{REL} ^{∈} (Ω_{n} ∪ Ω_{n}^{∗}) → (Ob REL)^{(Ob REL)^{n}}

be the semantic function satisfying:

Type Variables If i ^{∈} n then

⟨x_{1}, x_{2}⟩ ^{∈} [[i]]_{n}^{REL}ψ iff ⟨x_{1}, x_{2}⟩ ^{∈} ψi .

Functional Types If ω, ω′ ^{∈} Ω_{n} then

⟨f_{1}, f_{2}⟩ ^{∈} [[ω → ω′]]_{n}^{REL}ψ iff (∀⟨x_{1}, x_{2}⟩ ^{∈} [[ω]]_{n}^{REL}ψ) ⟨f_{1}x_{1}, f_{2}x_{2}⟩ ^{∈} [[ω′]]_{n}^{REL}ψ .

Type Assignments If π ^{∈} Ω_{n}^{∗} then

⟨η_{1}, η_{2}⟩ ^{∈} [[π]]_{n}^{REL}ψ iff (∀v ^{∈} dom π) ⟨η_{1}v, η_{2}v⟩ ^{∈} [[πv]]_{n}^{REL}ψ .

Then the first-order abstraction theorem of [1] (or the logical-relations theorem of [6]) was

Suppose ψ maps each i ^{∈} n into a binary relation ψi between the sets θ_{1}i and θ_{2}i. If π ⊢_{n} e : ω and ⟨η_{1}, η_{2}⟩ ^{∈} [[π]]_{n}^{REL}ψ then

⟨[[e]]_{nπω}θ_{1}η_{1}, [[e]]_{nπω}θ_{2}η_{2}⟩ ^{∈} [[ω]]_{n}^{REL}ψ .

In retrospect, it is easy to see how to restate this theorem categorically. One defines a category REL whose objects are relations:

⟨r_{1}, r_{2}, r_{⊤}⟩ ^{∈} Ob REL iff

r_{1}, r_{2}, r_{⊤} ^{∈} Ob SET and r_{⊤} ⊆ r_{1} × r_{2} ,

⟨f_{1}, f_{2}⟩ ^{∈} ⟨r_{1}, r_{2}, r_{⊤}⟩ ⟶_{REL} ⟨r′_{1}, r′_{2}, r′_{⊤}⟩ iff

f_{1} ^{∈} r_{1} → r′_{1} and f_{2} ^{∈} r_{2} → r′_{2} and (∀⟨x_{1}, x_{2}⟩ ^{∈} r_{⊤}) ⟨f_{1}x_{1}, f_{2}x_{2}⟩ ^{∈} r′_{⊤} ,

with componentwise composition and identities, and a forgetful functor U from REL to SET × SET:

U⟨r_{1}, r_{2}, r_{⊤}⟩ = ⟨r_{1}, r_{2}⟩  and  U⟨f_{1}, f_{2}⟩ = ⟨f_{1}, f_{2}⟩ .

Then the key to the abstraction theorem is:

The category REL is Cartesian closed, with componentwise products and

⟨r_{1}, r_{2}, r_{⊤}⟩ ⟹_{REL} ⟨r′_{1}, r′_{2}, r′_{⊤}⟩ = ⟨r_{1} → r′_{1}, r_{2} → r′_{2}, ⟨r_{1}, r_{2}, r_{⊤}⟩ ⟶_{REL} ⟨r′_{1}, r′_{2}, r′_{⊤}⟩⟩ ,

and the functor U is a morphism of Cartesian closed categories (i.e. preserving products and exponentiations, including terminal objects and projection and application morphisms).

From a categorical viewpoint, this is all there is to the matter, since the abstraction theorem becomes a consequence of the fact that a morphism of Cartesian closed categories preserves the meaning of the simply typed lambda calculus:

Proposition 1 If U is a morphism of Cartesian closed categories from R to K and

[figure: n; Ob R; Ob K; ψ; θ; Ob U]

commutes, then both

[figure: Ω_{n} ∪ Ω_{n}^{∗}; Ob R; Ob K; [[−]]_{n}^{K}θ; Ob U; [[−]]_{n}^{R}ψ; and; E_{nπω}; [[π]]_{n}^{R}ψ ⟶_{R} [[ω]]_{n}^{R}ψ; [[π]]_{n}^{K}θ ⟶_{K} [[ω]]_{n}^{K}θ; [[−]]_{nπω}^{K}θ; Mor U; [[−]]_{nπω}^{R}ψ]

commute.

Proof : This is often proved by constructing a free Cartesian closed category from equivalence classes of typed lambda expressions (as in [12]). A more elementary approach is to use structural induction on type expressions for the left diagram and on ordinary expressions for the right diagram. (End of Proof )

Now we can ask how to generalize REL beyond relations on sets. The first step is to realize that an equivalent reformulation of REL and U is given by replacing each subset r_{⊤} ⊆ r_{⊥} by a monic (i.e. injective) function whose image is that subset:

⟨r_{1}, r_{2}, r_{⊤}, r_{↓}⟩ ^{∈} Ob REL iff

r_{1}, r_{2}, r_{⊤} ^{∈} Ob SET, and r_{↓} ^{∈} r_{⊤} → r_{1} × r_{2} is monic ,

⟨f_{1}, f_{2}, f_{⊤}⟩ ^{∈} ⟨r_{1}, r_{2}, r_{⊤}, r_{↓}⟩ ⟶_{REL} ⟨r′_{1}, r′_{2}, r′_{⊤}, r′_{↓}⟩ iff

f_{1} ^{∈} r_{1} → r′_{1} and f_{2} ^{∈} r_{2} → r′_{2} and f_{⊤} ^{∈} r_{⊤} → r′_{⊤}

and

[figure: r_{⊤}; r_{1} × r_{2}; r_{↓}; r′_{⊤}; r′_{1} × r′_{2}; r′_{↓}; f_{⊤}; f_{1} × f_{2}]

commutes in SET,

with componentwise composition and identities, and

U⟨r_{1}, r_{2}, r_{⊤}, r_{↓}⟩ = ⟨r_{1}, r_{2}⟩  and  U⟨f_{1}, f_{2}, f_{⊤}⟩ = ⟨f_{1}, f_{2}⟩ .

The essential idea is that ⟨x_{1}, x_{2}⟩ belongs to the relation ⟨r_{1}, r_{2}, r_{⊤}, r_{↓}⟩ iff there is a “witness” z ^{∈} r_{⊤} such that ⟨x_{1}, x_{2}⟩ = r_{↓}z. Then in the morphism ⟨f_{1}, f_{2}, f_{⊤}⟩, the existence of the function f_{⊤} insures that related arguments ⟨x_{1}, x_{2}⟩ are mapped into related results ⟨f_{1}x_{1}, f_{2}x_{2}⟩ since f_{⊤} maps a witness to ⟨x_{1}, x_{2}⟩ into a witness to ⟨f_{1}x_{1}, f_{2}x_{2}⟩.

In this formulation, except for the monicity requirement, REL is simply a comma category. (Requiring the r_{↓} to be monic has little importance in the first-order case, but will be vital for dealing with polymorphism.) This suggests the following generalization:

Definition Let K and B be categories and F be a functor from K to B. Then REL(K, B, F), called a category of relations over K, is the category such that:

⟨r_{⊥}, r_{⊤}, r_{↓}⟩ ^{∈} Ob REL(K, B, F) iff

r_{⊥} ^{∈} Ob K, r_{⊤} ^{∈} Ob B, and r_{↓} ^{∈} r_{⊤} ⟶_{B} F r_{⊥} is monic ,

⟨f_{⊥}, f_{⊤}⟩ ^{∈} ⟨r_{⊥}, r_{⊤}, r_{↓}⟩ ⟶_{REL(K,B,F)} ⟨r′_{⊥}, r′_{⊤}, r′_{↓}⟩ iff

f_{⊥} ^{∈} r_{⊥} ⟶_{K} r′_{⊥} and f_{⊤} ^{∈} r_{⊤} ⟶_{B} r′_{⊤}

and

[figure: r_{⊤}; F r_{⊥}; r_{↓}; r′_{⊤}; F r′_{⊥}; r′_{↓}; f_{⊤}; F f_{⊥}]

commutes in B,

with componentwise composition and identities, and U is the functor from REL to K such that

U⟨r_{⊥}, r_{⊤}, r_{↓}⟩ = r_{⊥}  and  U⟨f_{⊥}, f_{⊤}⟩ = f_{⊥} .

(Notice that the monicity condition on r′_{↓} insures that U is a faithful functor.) This generalization includes our previous REL as the category REL(SET×SET, SET, −×_{SET}−) of binary relations over SET. But the crucial test of the generalization is that, under reasonable conditions, one has a Cartesian closed structure:

Proposition 2 If K and B are Cartesian closed, B has pullbacks, and F preserves finite products, then REL(K, B, F) is Cartesian closed and U is a morphism of Cartesian closed categories.

(Note that F need not be a morphism of Cartesian closed categories.)

Proof : The reader may verify that products can be defined componentwise. To define exponentiation, suppose r and r′ are relations, i.e. objects of R = REL(K, B, F). Since B is Cartesian closed, we can define t to be the unique morphism such that

[figure: F (r_{⊥} ⟹_{K} r′_{⊥}) × r_{⊤}; F (r_{⊥} ⟹_{K} r′_{⊥}) × F r_{⊥}; (r_{⊤} ⟹_{B} F r′_{⊥}) × r_{⊤}; F r′_{⊥}; I × r_{↓}; ap; t × I; F ap]  (1)

commutes in B. (To keep the proof straightforward, we are assuming here that F preserves distinguished products.) We also introduce r_{⊤} ⟹_{B} r′_{↓}, which is the unique morphism such that

[figure: (r_{⊤} ⟹_{B} r′_{⊤}) × r_{⊤}; r′_{⊤}; (r_{⊤} ⟹_{B} F r′_{⊥}) × r_{⊤}; F r′_{⊥}; ap; ap; (r_{⊤} ⟹_{B} r′_{↓}) × I; r′_{↓}]  (2)

commutes. Since r′_{↓} is monic, r_{⊤} ⟹_{B} r′_{↓} is monic, for if f_{1} ; (r_{⊤} ⟹_{B} r′_{↓}) = f_{2} ; (r_{⊤} ⟹_{B} r′_{↓}) then

(f_{1} × I) ; ((r_{⊤} ⟹_{B} r′_{↓}) × I); ap = (f_{2} × I) ; ((r_{⊤} ⟹_{B} r′_{↓}) × I); ap

(f_{1} × I) ; ap ; r′_{↓} = (f_{2} × I) ; ap ; r′_{↓} by 2

(f_{1} × I) ; ap = (f_{2} × I) ; ap since r′_{↓} is monic

and f_{1} = f_{2} by the uniqueness property for exponentiation.

Next we define the exponentiation r ⟹_{R} r′, along with a morphism u, to be the pullback

[figure: (r ⟹_{R} r′)_{⊤}; F ((r ⟹_{R} r′)_{⊥} =^{def} r_{⊥} ⟹_{K} r′_{⊥}); r_{⊤} ⟹_{B} r′_{⊤}; r_{⊤} ⟹_{B} F r′_{⊥}; (r ⟹_{R} r′)_{↓}; r_{⊤} ⟹_{B} r′_{↓}; u; t]  (3)

Because this is a pullback and r_{⊤} ⟹_{B} r′_{↓} is monic, (r ⟹_{R} r′)_{↓} is monic (see [13, Section 1.6, Lemma 2]). Moreover, since

((r ⟹_{R} r′)_{↓} × r_{↓}); F ap

= ((r ⟹_{R} r′)_{↓} × I); (I × r_{↓}) ; F ap

= ((r ⟹_{R} r′)_{↓} × I); (t × I) ; ap by 1

= (u × I) ; ((r_{⊤} ⟹_{B} r′_{↓}) × I); ap by 3

= (u × I) ; ap ; r′_{↓} , by 2

the following diagram commutes and can be used to define the application morphism ap_{rr′}^{R}:

[figure: (r ⟹_{R} r′)_{⊤} × r_{⊤}; F (r_{⊥} ⟹_{K} r′_{⊥}) × F r_{⊥}; r′_{⊤}; F r′_{⊥}; (r_{⊤} ⟹_{B} r′_{⊤}) × r_{⊤}; u × I; ap; (r ⟹_{R} r′)_{↓} × r_{↓}; r′_{↓}; (ap_{rr′}^{R})_{⊤} =^{def} (u × I) ; ap; F ((ap_{rr′}^{R})_{⊥} =^{def} ap^{K})]  (4)

Now suppose r̂ is any object of R and f = ⟨f_{⊥}, f_{⊤}⟩ ^{∈} r̂ × r ⟶_{R} r′, so that

[figure: r̂_{⊤} × r_{⊤}; F (r̂_{⊥} × r_{⊥}); r′_{⊤}; F r′_{⊥}; r̂_{↓} × r_{↓}; r′_{↓}; f_{⊤}; F f_{⊥}]  (5)

Then ((r̂_{↓} ; F (ab^{K} f_{⊥}) ; t) × I); ap = (r̂_{↓} × I) ; (F (ab^{K} f_{⊥}) × I); (t × I) ; ap = (r̂_{↓} × I) ; (F (ab^{K} f_{⊥}) × I); (I × r_{↓}) ; F ap by 1 = (r̂_{↓} × r_{↓}) ; (F (ab^{K} f_{⊥}) × I); F ap = (r̂_{↓} × r_{↓}) ; F ((ab^{K} f_{⊥} × I) ; ap) = (r̂_{↓} × r_{↓}) ; F f_{⊥} by definition of ab

= f_{⊤} ; r′_{↓} by 5

= (ab^{B} f_{⊤} × I) ; ap ; r′_{↓} by definition of ab

= (ab^{B} f_{⊤} × I) ; ((r_{⊤} ⟹_{B} r′_{↓}) × I); ap by 2

= ((ab^{B} f_{⊤} ; (r_{⊤} ⟹_{B} r′_{↓})) × I); ap ,

so by the uniqueness property of exponentiation, the perimeter of

[figure: (r ⟹_{R} r′)_{⊤}; F (r_{⊥} ⟹_{K} r′_{⊥}); r_{⊤} ⟹_{B} r′_{⊤}; r_{⊤} ⟹_{B} F r′_{⊥}; r̂_{⊤}; F r̂_{⊥}; (r ⟹_{R} r′)_{↓}; r_{⊤} ⟹_{B} r′_{↓}; u; t; r̂_{↓}; F (ab^{K} f_{⊥}); ab^{B} f_{⊤}; g_{⊤}]  (6)

commutes and is a cone for the pullback in Diagram 3.

Finally, we note that g is a morphism in r̂ ⟶_{R} (r ⟹_{R} r′) that makes

[figure: r̂ × r; (r ⟹_{R} r′) × r; r′; ap^{R}; f; g × I]  (7)

commute in R iff g = ⟨g_{⊥}, g_{⊤}⟩, where

[figure: r̂_{⊤}; F r̂_{⊥}; (r ⟹_{R} r′)_{⊤}; F (r ⟹_{R} r′)_{⊥}; r̂_{↓}; (r ⟹_{R} r′)_{↓}; g_{⊤}; F g_{⊥}; r̂_{⊥} × r_{⊥}; (r_{⊥} ⟹_{K} r′_{⊥}) × r_{⊥}; r′_{⊥}; ap^{K}; f_{⊥}; g_{⊥} × I; r̂_{⊤} × r_{⊤}; (r ⟹_{R} r′)_{⊤} × r_{⊤}; r′_{⊤}; (ap_{rr′}^{R})_{⊤}; f_{⊤}; g_{⊤} × I]

all commute. But the middle diagram is equivalent to g_{⊥} = ab^{K} f_{⊥}, which makes the left diagram equivalent to the parallelogram on the left of 6, and, by 4, the right diagram is equivalent to f_{⊤} = ((g_{⊤}; u) × I) ; ap^{B}, which is equivalent to ab^{B} f_{⊤} = g_{⊤}; u, which is the triangle in 6. Thus all three diagrams commute iff g_{⊥} = ab^{K} f_{⊥} and g_{⊤} is the mediating morphism in 6. Thus the uniqueness of the mediating morphism for pullbacks makes the solution of 7 unique, and it follows that R = REL(K, B, F) is Cartesian closed with ab^{R} f = g.

From (r ⟹_{R} r′)_{⊥} = (r_{⊥} ⟹_{K} r′_{⊥}) and (ap_{rr′}^{R})_{⊥} = ap_{r_{⊥}r′_{⊥}}^{K}, and similar properties of the componentwise product, it is evident that U is a morphism of Cartesian closed categories.

(End of Proof )

From Propositions 1 and 2, we have the following “abstract” version of the abstraction theorem:

Proposition 3 Suppose R = REL(K, B, F), where K and B are Cartesian closed, B has pullbacks, and F preserves finite products. Let U be the forgetful functor from R to K. If e ^{∈} E_{nπω}, ψ ^{∈} (Ob R)^{n}, and θ = ψ ; Ob U ^{∈} (Ob K)^{n}, then there is a unique

g ^{∈} [[π]]_{n}^{R}ψ ⟶_{R} [[ω]]_{n}^{R}ψ

such that

[[e]]_{nπω}^{K}θ = Ug .

Proof : Let g = [[e]]_{nπω}^{R}ψ. Since U is faithful, g is unique. (End of Proof )

At first sight, it might appear that this proposition is limited to unary relations. But multinary relations are encompassed by taking K to be a product of Cartesian closed categories (which will also be Cartesian closed). Specifically, relations of arity a over K_{1},…, K_{a} are the objects of

REL(K_{1} × ⋯ × K_{a}, B, F_{1}(−_{1}) ×_{B} ⋯ ×_{B} F_{a}(−_{a})) ,

where each F_{i} is a finite-product-preserving functor from K_{i} to B. When dealing with such categories of multinary relations, we will write U_{i} for the composition of the functor U with the projection functor from K_{1} × ⋯ × K_{a} to K_{i}.

As a special case, relations of arity a over a single category K are the objects of

REL(K^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})) ,

where F is a finite-product-preserving functor from K to B. Since it will eventually be pertinent to our discussion of parametricity, we give here the specialization of Proposition 3 to this case:

Proposition 4 Suppose R = REL(K^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})), where K and B are Cartesian closed, B has pullbacks, and F preserves finite products. If e ^{∈} E_{nπω}, ψ ^{∈} (Ob R)^{n}, and, for all i ^{∈} a, θ_{i} = ψ ; Ob U_{i} ^{∈} (Ob K)^{n}, then there is a unique

g ^{∈} [[π]]_{n}^{R}ψ ⟶_{R} [[ω]]_{n}^{R}ψ

such that

⟨[[e]]_{nπω}^{K}θ_{1},…, [[e]]_{nπω}^{K}θ_{a}⟩ = Ug .

In the case of multinary relations over a single category, we can introduce the concept of identity relations. Specifically, we can define a functor J mapping each object k of K into the identity relation on k:

Definition Given a category R = REL(K^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})) of relations of arity a over K, we write J for the functor from K to R such that

Jk = ⟨⟨k,…, k⟩, F k, ⟨I_{F k},…, I_{F k}⟩⟩ ,

where ⟨I_{F k},…, I_{F k}⟩ is the mediating morphism from F k to F k×_{B}⋯×_{B}F k = (F k)^{a}, and

Jf = ⟨⟨f,…, f⟩, F f⟩ ,

or diagrammatically,

[figure: F k; (F k)^{a}; F k′; (F k′)^{a}; ⟨I_{F k},…, I_{F k}⟩; ⟨I_{F k′},…, I_{F k′}⟩; F f; (F f)^{a}]

In [1], the set-theoretic relational semantics of the simply typed lambda calculus was shown to satisfy a further proposition, called the “Identity Extension Lemma”, that any type expression denotes an identity relation if its free type variables all denote identity relations. In the present setting, this result follows from proposition that, under reasonable conditions that are somewhat more stringent than for the abstraction theorem, J is a morphism of Cartesian closed categories. Specifically:

Proposition 5 If K and B are Cartesian closed, B has pullbacks, F preserves finite products, and either a = 1 or ab^{B}(F ap_{kk′}^{K}) is monic for all k, k′ ^{∈} Ob K, then J is a morphism of Cartesian closed categories, and the compositions

[figure: K; REL(K^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})); K; J; U_{i}]

are identity functors.

Proof : The only nonobvious argument is to show that J preserves exponentiations and application morphisms. Let R = REL(K^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})), r = Jk, and r′ = Jk′. We want to show that (r ⟹_{R} r′) = J(k ⟹_{K} k′) and ap_{rr′}^{R} = J ap_{kk′}^{K}.

In the construction of the proof of Proposition 2, Diagram 1 becomes

[figure: (F (k ⟹_{K} k′))^{a} × F k; (F (k ⟹_{K} k′))^{a} × (F k)^{a}; (F k ⟹_{B} (F k′)^{a}) × F k; (F k′)^{a}; (F (k ⟹_{K} k′) × F k)^{a}; I × ⟨I,…, I⟩; ap; t × I; ≃; (F ap)^{a}] (8)

(where the isomorphism ≃ arises because, although the functor F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a}) preserves products, it does not preserve distinguished products), and the pullback of Diagram 3 becomes

[figure: (r ⟹_{R} r′)_{⊤}; (F (k ⟹_{K} k′))^{a}; F k ⟹_{B} F k′; F k ⟹_{B} (F k′)^{a}; (r ⟹_{R} r′)_{↓}; F k ⟹_{B} ⟨I,…, I⟩; u; t]  (9)

We will show that this pullback condition is satisfied by

[figure: F (k ⟹_{K} k′); (F (k ⟹_{K} k′))^{a}; F k ⟹_{B} F k′; F k ⟹_{B} (F k′)^{a}; ⟨I,…, I⟩; F k ⟹_{B} ⟨I,…, I⟩; ab(F ap); t]  (10)

This implies that, to within an isomorphism, r ⟹_{R} r′ is the left side of Diagram 10, which is J(k ⟹_{K} k′), and u = ab^{B}(F ap_{kk′}^{K}). Then Diagram 4 gives (ap_{rr′}^{R})_{⊤} = (u×I);ap_{F k,F k′}^{B} = F ap_{kk′}^{K} and (ap_{rr′}^{R})_{⊥} = ⟨ap_{kk′}^{K},…, ap_{kk′}^{K}⟩, which implies ap_{rr′}^{R} = J ap_{kk′}^{K}.

To show that Diagram 10 commutes, let p_{i} denote the ith projection morphism for various a-ary products in B. Then (using various properties of products) we have

((t; (F k ⟹_{B} p_{i})) × I); ap

= (t × I) ; ((F k ⟹_{B} p_{i}) × I); ap

= (t × I) ; ap ; p_{i} by definition of F k ⟹_{B} (−) = (I × ⟨I,…, I⟩); ≃; (F ap)^{a} ; p_{i} by 8 = (I × ⟨I,…, I⟩); ≃; p_{i} ; F ap = (I × ⟨I,…, I⟩); (p_{i} × p_{i}) ; F ap = (p_{i} × I) ; F ap = (p_{i} × I) ; (ab(F ap) × I); ap by definition of ab = ((p_{i} ; ab(F ap)) × I); ap ,

so that the uniqueness property of exponentiation gives

t; (F k ⟹_{B} p_{i}) = p_{i} ; ab(F ap) .

More simply, the functorial nature of F k ⟹_{B} (−) gives

(F k ⟹_{B} ⟨I,…, I⟩); (F k ⟹_{B} p_{i}) = F k ⟹_{B} (⟨I,…, I⟩; p_{i}) = I .

Since the functor F k ⟹_{B} (−) is a right adjoint, it preserves products, so that the F k ⟹_{B} p_{i} are projections. Thus Diagram 10 commutes iff its composition with each of the F k ⟹_{B} p_{i} commutes, which follows from the above equations for t and F k ⟹_{B} ⟨I,…, I⟩.

Finally, to complete the argument that Diagram 10 is a pullback, consider

[figure: F (k ⟹_{K} k′); (F (k ⟹_{K} k′))^{a}; F k ⟹_{B} F k′; F k ⟹_{B} (F k′)^{a}; b; ⟨I,…, I⟩; F k ⟹_{B} ⟨I,…, I⟩; ab(F ap); t; g; f; h]  (11)

and assume the perimeter commutes. Composing the perimeter with F k ⟹_{B} p_{i} and using

the equations for t and F k ⟹_{B} ⟨I,…, I⟩ gives

[figure: b; F (k ⟹_{K} k′); F k ⟹_{B} F k′; g ; p_{i}; f; ab(F ap)]  (12)

Since ab(F ap) is monic (or trivially in the case of unary relations) the g ; p_{i} are equal. Then the lefthand triangle in 11 commutes iff h = g ; p_{i}, and this equation and 12 imply that the upper triangle in 11 commutes. Thus g; p_{i} is the unique mediating morphism in Diagram 11. (End of Proof )

The identity extension lemma is an immediate consequence of this result and Proposition 1 (with R and K interchanged):

Proposition 6 Let R = REL(K^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})). If K and B are Cartesian closed, B has pullbacks, F preserves finite products, and either a = 1 or ab^{B}(F ap_{kk′}^{K}) is monic for all k, k′ ^{∈} Ob K, then, whenever ω ^{∈} Ω_{n} ∪ Ω_{n}^{∗} is a type or type assignment of the first-order typed lambda calculus and θ ^{∈} (Ob K)^{n},

[[ω]]_{n}^{R}(θ; J) = ([[ω]]_{n}^{K}θ) ; J .

3 The Second-Order Case

We will develop the semantics of the polymorphic typed lambda calculus in the framework of PL categories [9, 10, 11]. To ease the introduction of this highly abstract framework, we proceed in two stages: Before defining the full-fledged PL categories that are needed for the second-order case, we define “pre-PL” categories, which give a more abstract semantics to the simply typed lambda calculus with type variables than that given in Section 2.

The idea behind pre-PL categories is that type and ordinary expressions in n type variables have abstract meanings in a Cartesian closed category K_{n}, which are obtained directly without any application to assignments of objects to type variables. However, such assignments induce relationships between the different K_{n}: For any assignment α ^{∈} (Ob K_{n})^{m}, there is a morphism of Cartesian closed categories Kα from K_{m} to K_{n} that describes the effect of substituting (a type expression whose meaning is) αi for each type variable i in m.

The rest of the story is that the sets n of type variables and the assignments α can be organized into a base category |K| that is a Lawvere theory [14, 15] of type expressions, and that K itself then becomes a functor from |K|^{op} to the large category CCC of Cartesian closed categories (i.e. a model of the theory |K| in CCC). Thus we have:

Definition A pre-PL category K = ⟨|K|, K⟩ consists of a base category |K| such that

• Ob |K| is the set of natural numbers,

• 0 is terminal and + is a binary product, so that n is the nth power of 1,

• I_{n}^{|K|}i is the ith projection morphism from n to 1 (applied to the unique member of the set 1),

and a functor K from |K|^{op} to CCC such that

[figure: ^{|K|^{op}}; CCC; CLASS; CLASS; Ob; K; Hom_{|K|}(−, m); (−)^{m}]  (13)

(Here CLASS is the large category of classes and functions.) Applying the functors in the above diagram to n ^{∈} Ob |K| gives

n ⟶_{|K|} m = (Ob K_{n})^{m} .

Note that a member of this set can be composed in two ways: either as a morphism in |K| or as an ordinary function (from m to Ob K_{n}). The relationship between these two composition operators is obtained by applying the functors in the above diagram to α ^{∈} n_{1} ⟶_{|K|} n_{2} and then applying the results to α′ ^{∈} n_{2} ⟶_{|K|} m, which gives

α;_{|K|} α′ = α′ ; Ob(Kα) .  (14)

Also note that the application I_{n}^{|K|}i makes sense when i ^{∈} n, since I_{n}^{|K|} ^{∈} n ⟶_{|K|} n = (Ob K_{n})^{n}.

Each pre-PL category K determines an abstract meaning of the simply typed lambda calculus, as opposed to the concrete meanings described in Section 2. Specifically, the abstract meaning of type expressions and assignments is given by a family of semantic functions

⟨⟨−⟩⟩_{n}^{K} ^{∈} (Ω_{n} ∪ Ω_{n}^{∗}) → Ob K_{n}

satisfying:

Type Variables If i ^{∈} n then

⟨⟨i⟩⟩_{n} = I_{n}^{|K|}i .

Functional Types If ω, ω′ ^{∈} Ω_{n} then

⟨⟨ω → ω′⟩⟩_{n} = ⟨⟨ω⟩⟩_{n} ⟹_{K_{n}} ⟨⟨ω′⟩⟩_{n} .

Type Assignments If π ^{∈} Ω_{n}^{∗} then

⟨⟨π⟩⟩_{n} = \begin{matrix}∏ & K_{n} \\ v^{∈}dom π \end{matrix}⟨⟨πv⟩⟩_{n} .

and the abstract meaning of ordinary expressions is given by a family

⟨⟨−⟩⟩_{nπω}^{K} ^{∈} E_{nπω} → (⟨⟨π⟩⟩_{n}^{K} ⟶_{K_{n}} ⟨⟨ω⟩⟩_{n}^{K})

satisfying:

Ordinary Variables If π ⊢_{n} v : πv then ⟨⟨v⟩⟩_{nπ πv} is the projection morphism

from ⟨⟨π⟩⟩_{n} = \begin{matrix}∏ & K_{n} \\ v^{∈}dom π \end{matrix}⟨⟨πv⟩⟩_{n} to ⟨⟨πv⟩⟩_{n}.

Applications If π ⊢_{n} e_{1} : ω → ω′ and π ⊢_{n} e_{2} : ω then

⟨⟨e_{1}e_{2}⟩⟩_{nπω′} = ⟨⟨⟨e_{1}⟩⟩_{nπ ω→ω′}, ⟨⟨e_{2}⟩⟩_{nπω}⟩; ap ,

where ⟨⟨⟨e_{1}⟩⟩_{nπ ω→ω′}, ⟨⟨e_{2}⟩⟩_{nπω}⟩ is the mediating morphism from ⟨⟨π⟩⟩_{n} to the product (⟨⟨ω⟩⟩_{n} ⟹_{K_{n}} ⟨⟨ω′⟩⟩_{n}) × ⟨⟨ω⟩⟩_{n}, and ap is the application morphism from this product to ⟨⟨ω′⟩⟩_{n}.

Abstractions If [ π | v: ω] ⊢_{n} e : ω′ then

⟨⟨λv_{ω}. e⟩⟩_{nπ ω→ω′} = ab(¶; ⟨⟨e⟩⟩_{n [π|v:ω] ω′}) ,

where ¶ is the mediating morphism from ⟨⟨π⟩⟩_{n} × ⟨⟨ω⟩⟩_{n} to ⟨⟨[ π | v: ω]⟩⟩_{n}.

As in [11], one can show that these abstract semantic functions (and their extensions to the second-order case) satisfy a substitution law:

Proposition 7 Suppose ω ^{∈} Ω_{m}, π ^{∈} Ω_{m}^{∗}, e ^{∈} E_{mπω}, and σ ^{∈} (Ω_{n})^{m}. Then
⟨⟨ω/σ⟩⟩_{n} = K(λi ^{∈} m. ⟨⟨σi⟩⟩_{n})⟨⟨ω⟩⟩_{m}
⟨⟨π/σ⟩⟩_{n} = K(λi ^{∈} m. ⟨⟨σi⟩⟩_{n})⟨⟨π⟩⟩_{m}
⟨⟨e/σ⟩⟩_{n (π/σ) (ω/σ)} = K(λi ^{∈} m. ⟨⟨σi⟩⟩_{n})⟨⟨e⟩⟩_{mπω} .

As a special case, ⟨⟨π̂⟩⟩_{n+1} = Φ_{n}⟨⟨π⟩⟩_{n}, where

Φ_{n} =^{def} K(λi ^{∈} n. ⟨⟨i⟩⟩_{n+1}) = K(λi ^{∈} n. I_{n+1}^{|K|}i) = K(J_{n⊆n+1} ; I_{n+1}^{|K|}) ,  (15)

and J_{n⊆n+1} is the identity injection from n to n + 1. (It is easily seen that J_{n⊆n+1} ; I_{n+1}^{|K|} is the mediating morphism from the product n + 1 to n.)

Now consider what must be added to the above semantic equations to give meaning to the polymorphic calculus. For each type ω ^{∈} Ω_{n+1}, there is a polymorphic type Δn. ω ^{∈} Ω_{n}. Thus there should be a function Δ_{n} from Ob K_{n+1} to Ob K_{n} such that

Polymorphic Types If ω ^{∈} Ω_{n+1} then

⟨⟨Δn. ω⟩⟩_{n} = Δ_{n}⟨⟨ω⟩⟩_{n+1} .

For each ordinary expression e satisfying π̂ ⊢_{n+1} e : ω there is a type abstraction Λn. e satisfying π ⊢_{n} Λn. e : Δn. ω. Thus there should be a function tab_{n} from

⟨⟨π̂⟩⟩_{n+1} ⟶_{K_{n+1}} ⟨⟨ω⟩⟩_{n+1} = Φ_{n}⟨⟨π⟩⟩_{n} ⟶_{K_{n+1}} ⟨⟨ω⟩⟩_{n+1}

to

⟨⟨π⟩⟩_{n} ⟶_{K_{n}} ⟨⟨Δn. ω⟩⟩_{n} = ⟨⟨π⟩⟩_{n} ⟶_{K_{n}} Δ_{n}⟨⟨ω⟩⟩_{n+1}

such that

Type Abstractions If π̂ ⊢_{n+1} e : ω then

⟨⟨Λn. e⟩⟩_{nπ Δn.ω} = tab_{n}⟨⟨e⟩⟩_{n+1 _{π} ω} .

Moreover, one can argue that the soundness of β-type-reduction requires tab_{n} to be injective, and the soundness of η-type-reduction requires tab_{n} to be surjective. Thus it is natural to require Δ_{n} to be a right adjoint of Φ_{n}. This motivates the following definition:

Definition A PL category K = ⟨|K|, K, Δ^{K}⟩ consists of

• A pre-PL category ⟨|K|, K⟩,

• A natural transformation Δ^{K} ^{∈} K(− + 1) ⟶_{|K|^{op}⇒CAT} K such that each

Δ_{n}^{K} is a right adjoint of Φ_{n}^{K} = K(λi ^{∈} n. I_{n+1}^{|K|}i) and, for all α ^{∈} n ⟶_{|K|} m, K(α + 1), Kα is a map of adjunctions [16, Section IV.7] from Φ_{m}, Δ_{m} to Φ_{n}, Δ_{n}.

Here + denotes the product functor for |K|. It can be shown that

α + 1 = [ α; Ob Φ_{n} | m: I_{n+1}^{|K|}n] .  (16)

We write tap_{n} for the counits and tab_{n} for the isomorphisms of the adjunctions. As is well known [16, Section IV.1, Theorem 2(iv)], each adjunction is completely determined by giving, for each k′ ^{∈} Ob K_{n+1}, an object Δ_{n}k′ ^{∈} Ob K_{n} and a morphism tap_{n} k′ ^{∈} Φ_{n}(Δ_{n}k′) ⟶_{K_{n+1}} k′ such that, for all k ^{∈} Ob K_{n} and f′ ^{∈} Φ_{n}k ⟶_{K_{n+1}} k′, there is a unique morphism tab_{n} f′ ^{∈} k ⟶_{K_{n}} Δ_{n}k′ making

[figure: Φ_{n}k; Φ_{n}(Δ_{n}k′); k′; Φ_{n}(tab_{n} f′); f′; tap_{n} k′]  (17)

commute in K_{n+1}. Moreover, for α ^{∈} n ⟶_{|K|} m, since Kα; Φ_{n} = Φ_{m} ; K(α + 1) holds for any pre-PL category, it can be shown that a sufficient condition for K(α + 1), Kα to be a map of adjunctions is that

Kα(Δ_{m}k′) = Δ_{n}(K(α + 1)k′)
K(α + 1)(tap_{m} k′) = tap_{n}(K(α + 1)k′)

should hold for all k′ ^{∈} Ob K_{m+1}.

Given a PL category, the abstract semantics of the second-order typed lambda calculus is determined by the semantic equations we have given above, plus

Type Applications If π ⊢_{n} e : Δn. ω and ω′ ^{∈} Ω_{n} then

⟨⟨e[ω′]⟩⟩_{nπ (ω/n→ω′)} = ⟨⟨e⟩⟩_{nπ Δn.ω} ;_{K_{n}} K⟨I_{n}^{|K|}, ⟨⟨ω′⟩⟩_{n}⟩(tap_{n}⟨⟨ω⟩⟩_{n+1}) ,

where ⟨I_{n}^{|K|}, ⟨⟨ω′⟩⟩_{n}⟩ is the mediating morphism in n ⟶_{|K|} n+1 (regarding n+1 as the product of n and 1).

(This semantic equation can be derived from the substitution law and the soundness of β-type-reduction.)

Next, we introduce morphisms of pre-PL and PL categories:

Definition A pre-PL morphism U = ⟨|U|, U⟩ from R to K consists of a product-preserving functor |U| from |R| to |K| that is an identity on objects, and a natural transformation

U ^{∈} R ⟶_{|R|^{op}⇒CCC} |U|; K

that satisfies

|U|β = β ; Ob U_{n}

for all β ^{∈} n ⟶_{|R|} m = (Ob R_{n})^{m}.

A PL morphism U = ⟨|U|, U⟩ from R to K is a pre-PL morphism such that, for each n, the pair U_{n+1}, U_{n} is a map of adjunctions from Φ_{n}^{R}, Δ_{n}^{R} to Φ_{n}^{K}, Δ_{n}^{K}.

Since the naturality of U implies U_{n} ; Φ_{n}^{K} = Φ_{n}^{R} ; U_{n+1}, it can be shown that a sufficient condition for U_{n+1}, U_{n} to be a map of adjunctions is that

U_{n}(Δ_{n}^{R}r′) = Δ_{n}^{K}(U_{n+1}r′)
U_{n+1}(tap_{n}^{R} r′) = tap_{n}^{K}(U_{n+1}r′)

should hold for all r′ ^{∈} R_{n+1}.

Either pre-PL or PL categories, along with the corresponding morphisms, form a category. In both cases, the composition of U with U′ is ⟨|U′′|, U′′⟩, where |U′′| is the functorial composition |U| ; |U′| and each U′′_{n} is the functorial composition U_{n} ; U′_{|U|n} (or more simply, U_{n}; U′_{n}, since |U| is an identity on objects), and the identity on K is ⟨I_{|K|}, I⟩, where I_{|K|} is the identity functor on |K| and each I_{n} is the identity functor on K_{n}.

As one might expect, PL morphisms preserve abstract semantics:

Proposition 8 If U is a PL morphism (or in the first-order case, a pre-PL morphism), then both

[figure: Ω_{n} ∪ Ω_{n}^{∗}; ^{Ob R^{n}}; _{Ob K_{n}}; ⟨⟨−⟩⟩_{n}^{K}; Ob U_{n}; ⟨⟨−⟩⟩_{n}^{R}; and; E_{nπω}; ⟨⟨π⟩⟩_{n}^{R} ⟶_{R_{n}} ⟨⟨ω⟩⟩_{n}^{R}; ⟨⟨π⟩⟩_{n}^{K} ⟶_{K_{n}} ⟨⟨ω⟩⟩_{n}^{K}; ⟨⟨−⟩⟩_{nπω}^{K}; Mor U_{n}; ⟨⟨−⟩⟩_{nπω}^{R}]

commute.

Proof : This was originally proved by Seely [9]. A more elementary approach is to use structural induction on type expressions for the left diagram and on ordinary expressions for the right diagram. (End of Proof )

From the abstract semantic functions ⟨⟨−⟩⟩_{−}, we can define concrete semantic functions, akin to those of Section 2, that give to all expressions meanings in the category K_{0} (which plays the same role as K did previously). We define

[[−]]_{n}^{K} ^{∈} (Ω_{n} ∪ Ω_{n}^{∗}) → (Ob K_{0})^{(Ob K_{0})^{n}}

[[−]]_{nπω}^{K} ^{∈} E_{nπω} → ∏_{θ^{∈}(Ob K_{0})^{n}}([[π]]_{n}^{K}θ ⟶_{K_{0}} [[ω]]_{n}^{K}θ)

by

\begin{matrix}[[ω]]_{n}^{K}θ = Kθ⟨⟨ω⟩⟩_{n}^{K} \\ [[e]]_{nπω}^{K}θ = Kθ⟨⟨e⟩⟩_{nπω}^{K} . \end{matrix}  (18)

Using this definition and taking K = K_{0}, one can derive the concrete semantic equations given in Section 2. Thus, in the first-order, pre-PL case the [[−]]_{−}^{K} defined here coincide with the the [[−]]_{−}^{K} defined earlier. In the second-order case, however, the concrete semantics must be defined in terms of the abstract semantics, since one cannot give semantic equations directly for the concrete semantics of the additional constructions.

Nevertheless, one can prove the obvious generalization of Proposition 1:

Proposition 9 If U is a PL morphism (or, in the first-order case, a pre-PL morphism) from R to K and

[figure: n; ^{Ob R^{0}}; _{Ob K_{0}}; ψ; θ; _{Ob U_{0}}]

commutes, then both

[figure: Ω_{n} ∪ Ω_{n}^{∗}; ^{Ob R^{0}}; _{Ob K_{0}}; [[−]]_{n}^{K}θ; _{Ob U_{0}}; [[−]]_{n}^{R}ψ; and; E_{nπω}; [[π]]_{n}^{R}ψ ⟶_{R_{0}} [[ω]]_{n}^{R}ψ; [[π]]_{n}^{K}θ ⟶_{K_{0}} [[ω]]_{n}^{K}θ; [[−]]_{nπω}^{K}θ; _{Mor U_{0}}; [[−]]_{nπω}^{R}ψ]

commute.

Proof : From Proposition 8, using the naturality of U. (End of Proof )

Just as the key to the first-order abstraction theorem was to show that categories of relations are Cartesian closed, so the key in the second-order case is to show that such categories can be extended to PL categories. As a first step, we consider the extension to pre-PL categories:

Proposition 10 Suppose K is a pre-PL category, R is a Cartesian closed category, and U is a morphism of Cartesian closed categories from R to K = K_{0}. Then there is a pre-PL category R and a pre-PL morphism U from R to K such that R = R_{0} and U = U_{0}.

Proof : Intuitively, the essence of constructing R and U is that the naturality of U requires

[figure: R_{n}; K_{n}; U_{n}; R_{0} = R; K_{0} = K; U_{0} = U; Rψ; K(|U|ψ) = K(ψ ; Ob U)]

to commute for all ψ ^{∈} 0 ⟶_{|R|} n = (Ob R)^{n}. Since this requires each R_{n} to be a certain kind of cone, we define it to be the limiting cone.

This leads to the following construction, in which the objects and morphisms of the R_{n} are pairs:

• The category R_{n} is such that ⟨k, r⟩ ^{∈} Ob R_{n} iff

k ^{∈} Ob K_{n} and r ^{∈} (Ob R)^{(Ob R)^{n}} and (∀ψ ^{∈} (Ob R)^{n}) K(ψ ; Ob U)k = U(rψ)

and ⟨f, g⟩ ^{∈} ⟨k, r⟩ ⟶_{R_{n}} ⟨k′, r′⟩ iff

f ^{∈} k ⟶_{K_{n}} k′ and g ^{∈} r ⟶_{R^{(Ob R)^{n}}} r′ and (∀ψ ^{∈} (Ob R)^{n}) K(ψ ; Ob U)f = U(gψ) ,

with composition and identities defined by pointwise extension from K_{n} and R.

• For β ^{∈} n ⟶_{|R|} m = (Ob R_{n})^{m}, the functor Rβ from R_{m} to R_{n} is such that

Rβ⟨k, r⟩ = ⟨K(λi ^{∈} m. (βi)_{1})k, λψ ^{∈} (Ob R)^{n}. r(λi ^{∈} m. (βi)_{2}ψ)⟩  (19)

when ⟨k, r⟩ is either an object or morphism of R_{m}.

• For all i ^{∈} n,

I_{n}^{|R|}i = ⟨I_{n}^{|K|}i, λψ ^{∈} (Ob R)^{n}. ψi⟩ .  (20)

• U_{n} is the functor such that

U_{n}⟨k, r⟩ = k ,  (21)

when ⟨k, r⟩ is either an object or morphism of R_{n}.

• For all β ^{∈} n ⟶_{|R|} m,

|U|β = λi ^{∈} m. (βi)_{1} .  (22)

We leave it to the reader to check that these entities have the required properties. (End of Proof )

The further extension to PL categories requires an additional assumption about the relation categories:

Definition We say that R = REL(K, B, F) is suitable for polymorphism when, for each r_{⊥} ^{∈} Ob K, r ^{∈} (Ob R)^{Ob R}, and f ^{∈} ∏_{ρ^{∈}Ob R} r_{⊥} ⟶_{K} (rρ)_{⊥}, there is a limit r_{⊤}, r_{↓}, g that makes

[figure: r_{⊤}; (rρ)_{⊤}; F r_{⊥}; F (rρ)_{⊥}; gρ; F (fρ); r_{↓}; (rρ)_{↓}]  (23)

commute in B for all ρ ^{∈} Ob R.

(It is easily shown that the monicity of the (rρ)_{↓} implies the monicity of r_{↓}, so that the left side of this diagram is an object of R.)

One might expect suitability for polymorphism to be rare since ρ ranges over the entire class Ob R. But this difficulty is neutralized by the monicity of the (rρ)_{↓}. For example, REL(K, B, F) is suitable for polymorphism whenever B is SET, for then one can take r_{⊤} to be the set of x ^{∈} F r_{⊥} such that, for all ρ ^{∈} Ob R, F (fρ)x belongs to the image of (rρ)_{↓}. Then r_{↓}x = x, and gρx is the unique x′ ^{∈} (rρ)_{⊤} such that (rρ)_{↓}x′ = F (fρ)x.

Using the assumption of suitability for polymorphism, we obtain:

Proposition 11 Suppose K is a PL category, R = REL(K_{0}, B, F) is a Cartesian closed category that is suitable for polymorphism, and the forgetful functor U from R to K = K_{0} is a morphism of Cartesian closed categories. Then there is a PL category R and a PL morphism U from R to K such that R = R_{0} and U = U_{0}.

Proof : Much of the argument that follows will be quantified over the variables ψ ^{∈} (Ob R)^{n} and ρ ^{∈} Ob R. In such contexts, we will use the following abbreviations:

ψ̂ =^{def} ψ ; Ob U ψ′ =^{def} [ ψ | n: ρ] ψ̂′ =^{def} ψ′ ; Ob U = [ ψ̂ | n: Uρ] .

Let |R|, R, |U|, and U be as in the proof of Proposition 10. If ⟨k, r⟩ is an object or morphism of R_{n} then, for all ψ ^{∈} (Ob R)^{n}, (rψ)_{⊥} = U(rψ) = Kψ̂k. Thus an object ⟨k, r⟩ ^{∈} Ob R_{n} is exactly specified by giving k ^{∈} Ob K_{n} and, for each ψ ^{∈} (Ob R)^{n}, (rψ)_{⊤} ^{∈} Ob B and (rψ)_{↓} ^{∈} (rψ)_{⊤} ⟶_{B} F (Kψ̂k). Similarly, a morphism ⟨f, g⟩ ^{∈} ⟨k_{1}, r_{1}⟩ ⟶_{R_{n}} ⟨k_{2}, r_{2}⟩ is exactly specified by giving f ^{∈} k_{1} ⟶_{K_{n}} k_{2} and, for each ψ ^{∈} (Ob R)^{n}, a morphism (gψ)_{⊤} making

[figure: (r_{1}ψ)_{⊤}; (r_{2}ψ)_{⊤}; F (Kψ̂k_{1}); F (Kψ̂k_{2}); (r_{1}ψ)_{↓}; (r_{2}ψ)_{↓}; (gψ)_{⊤}; F (Kψ̂f)]  (24)

commute in B.

Now suppose ψ ^{∈} (Ob R)^{n} and ρ ^{∈} Ob R. Then, whenever ⟨k, r⟩ is an object or morphism of R_{n}, by Equations 15, 19, and 20,

(Φ_{n}^{R}⟨k, r⟩)_{2}ψ′ = (R(λi ^{∈} n. I_{n+1}^{|R|}i)⟨k, r⟩)_{2}ψ′ =
r(λi ^{∈} n. (I_{n+1}^{|R|}i)_{2}ψ′) = r(λi ^{∈} n. ψ′i) = rψ ,

(25)

and thus

Kψ̂′(Φ_{n}^{R}⟨k, r⟩)_{1} = U((Φ_{n}^{R}⟨k, r⟩)_{2}ψ′) = U(rψ) = Kψ̂k .  (26)

Our first task is to specify, for each ⟨k′, r′⟩ ^{∈} Ob R_{n+1}, the object Δ_{n}^{R}⟨k′, r′⟩ ^{∈} Ob R_{n} and the morphism tap_{n}^{R} ⟨k′, r′⟩ ^{∈} Φ_{n}^{R}(Δ_{n}^{R}⟨k′, r′⟩) ⟶_{R_{n+1}} ⟨k′, r′⟩. The first components of these entities are determined by Equation 21 and the requirement that U must preserve adjunctions:

(Δ_{n}^{R}⟨k′, r′⟩)_{1} = U_{n}(Δ_{n}^{R}⟨k′, r′⟩) = Δ_{n}^{K}(U_{n+1}⟨k′, r′⟩) = Δ_{n}^{K}k′
(tap_{n}^{R} ⟨k′, r′⟩)_{1} = U_{n+1}(tap_{n}^{R} ⟨k′, r′⟩) = tap_{n}^{K}(U_{n+1}⟨k′, r′⟩) = tap_{n}^{K} k′ .

To complete the specification, we note that ((tap_{n}^{R} ⟨k′, r′⟩)_{2}ψ′)_{⊤} must satisfy a diagram similar to 24. Using Equations 25 and 26 to eliminate the occurrences of Φ_{n}^{R}, we find that

[figure: ((Δ_{n}^{R}⟨k′, r′⟩)_{2}ψ)_{⊤}; (r′ψ′)_{⊤}; F (Kψ̂(Δ_{n}^{K}k′)); F (Kψ̂′k′); ((Δ_{n}^{R}⟨k′, r′⟩)_{2}ψ)_{↓}; (r′ψ′)_{↓}; ((tap_{n}^{R} ⟨k′, r′⟩)_{2}ψ′)_{⊤}; F (Kψ̂′(tap_{n}^{K} k′))]  (27)

must commute in B for all ψ ^{∈} (Ob R)^{n} and ρ ^{∈} Ob R. To insure this, for each ψ ^{∈} (Ob R)^{n}, we specify ((Δ_{n}^{R}⟨k′, r′⟩)_{2}ψ)_{⊤}, ((Δ_{n}^{R}⟨k′, r′⟩)_{2}ψ)_{↓}, and λρ. ((tap_{n}^{R} ⟨k′, r′⟩)_{2}ψ′)_{⊤} to be the limit that makes Diagram 27 commute for all ρ ^{∈} Ob R. (The existence of these limits is assured by the assumption that R is suitable for polymorphism.)

Our next task is to show that we have an adjunction. Suppose ⟨k, r⟩ ^{∈} Ob R_{n} and ⟨f′, g′⟩ ^{∈} Φ_{n}^{R}⟨k, r⟩ ⟶_{R_{n+1}} ⟨k′, r′⟩. We must show that there is exactly one tab_{n}^{R} ⟨f′, g′⟩ ^{∈}

⟨k, r⟩ ⟶_{R_{n}} Δ_{n}^{R}⟨k′, r′⟩ such that

[figure: Φ_{n}^{R}⟨k, r⟩; Φ_{n}^{R}(Δ_{n}^{R}⟨k′, r′⟩); ⟨k′, r′⟩; Φ_{n}^{R}(tab_{n}^{R} ⟨f′, g′⟩); ⟨f′, g′⟩; _{tapR n ⟨k′, r′⟩}]  (28)

commutes in R_{n+1}. This will be true iff there is exactly one (tab_{n}^{R} ⟨f′, g′⟩)_{1} ^{∈} k ⟶_{K_{n}} Δ_{n}^{K}k′ and, for each ψ ^{∈} (Ob R)^{n}, exactly one ((tab_{n}^{R} ⟨f′, g′⟩)_{2}ψ)_{⊤} ^{∈} (rψ)_{⊤} ⟶_{B} (Δ_{n}^{R}⟨k′, r′⟩)_{2}ψ)_{⊤} such that the following conditions all hold:

• The diagram obtained from 28 by taking first components commutes in K_{n+1}. Since K is a PL category, the uniqueness of tab_{n}^{K} f′ in Diagram 17 insures that this will occur iff

(tab_{n}^{R} ⟨f′, g′⟩)_{1} = tab_{n}^{K} f′ .  (29)

• For all ψ ^{∈} (Ob R)^{n} and ρ ^{∈} Ob R, the diagram obtained from 28 by taking second components, applying them to ψ′, and taking ⊤-components commutes in B. With the use of Equation 25 to eliminate the occurrences of Φ_{n}^{R}, this diagram becomes the upper triangle in

[figure: F (Kψ̂k); ((Δ_{n}^{R}⟨k′, r′⟩)_{2}ψ)_{⊤}; F (Kψ̂(Δ_{n}^{K}k′)); F (Kψ̂′k′); (rψ)_{⊤}; (r′ψ′)_{⊤}; F (Kψ̂(tab_{n}^{K} f′)); (rψ)_{↓}; (r′ψ′)_{↓}; (g′ψ′)_{⊤}; F (Kψ̂′f′); ((Δ_{n}^{R}⟨k′, r′⟩)_{2}ψ)_{↓}; ((tab_{n}^{R} ⟨f′, g′⟩)_{2}ψ)_{⊤}; ((tap_{n}^{R} ⟨k′, r′⟩)_{2}ψ′)_{⊤}; F (Kψ̂′(tap_{n}^{K} k′))] (30)

• For all ψ ^{∈} (Ob R)^{n}, ((tab_{n}^{R} ⟨f′, g′⟩)_{2}ψ)_{⊤} must satisfy a diagram similar to 24. With the use of Equations 25 and 26 to eliminate the occurrences of Φ_{n}^{R}, and the substitution of Equation 29, this diagram becomes the lefthand parallelogram in 30.

The lower triangle in Diagram 30 can be obtained from Diagram 17 by applying Kψ̂′ and using Equation 26. The large parallelogram commutes since it is the version of Diagram 24 for the morphism ⟨f′, g′⟩ in R_{n+1}. Thus the perimeter of 30 commutes, and since the rectangle is a limit, the last two conditions above hold iff ((tab_{n}^{R} ⟨f′, g′⟩)_{2}ψ)_{⊤} is the unique mediating morphism. In conjunction with Equation 29, this determines tab_{n}^{R} ⟨f′, g′⟩ uniquely, so that Δ_{n}^{R} is a right adjoint of Φ_{n}^{R}.

Our final task is to show that, for all β ^{∈} n ⟶_{|R|} m, R(β + 1), Rβ is a map of adjunctions, i.e. that, for all ⟨k′, r′⟩ ^{∈} Ob R_{m+1},

Rβ(Δ_{m}^{R}⟨k′, r′⟩) = Δ_{n}^{R}(R(β + 1)⟨k′, r′⟩)
R(β + 1)(tap_{m}^{R} ⟨k′, r′⟩) = tap_{n}^{R}(R(β + 1)⟨k′, r′⟩) .

To show the equalities between the first components of each side of these equations, we use Equations 19 and 22, and the fact that |U| preserves products and thus distributes with +, to rewrite these equalities as

K(|U|β)(Δ_{m}^{K}k′) = Δ_{n}^{K}(K(|U|β + 1)k′) K(|U|β + 1)(tap_{m}^{K} k′) = tap_{n}^{K}(K(|U|β + 1)k′) ,

which hold because K(|U|β + 1), K(|U|β) is a map of adjunctions.

To complete the proof we must show that, for all ψ ^{∈} (Ob R)^{n}, ((Rβ(Δ_{m}^{R}⟨k′, r′⟩))_{2}ψ)_{⊤} = ((Δ_{n}^{R}(R(β + 1)⟨k′, r′⟩))_{2}ψ)_{⊤} ((Rβ(Δ_{m}^{R}⟨k′, r′⟩))_{2}ψ)_{↓} = ((Δ_{n}^{R}(R(β + 1)⟨k′, r′⟩))_{2}ψ)_{↓} ,

and for all ψ ^{∈} (Ob R)^{n} and ρ ^{∈} Ob R,

((R(β + 1)(tap_{m}^{R} ⟨k′, r′⟩))_{2}ψ′)_{⊤} = ((tap_{n}^{R}(R(β + 1)⟨k′, r′⟩))_{2}ψ′)_{⊤} .

Using Equation 19, these equations may be rewritten as ((Δ_{m}^{R}⟨k′, r′⟩)_{2}ϕ)_{⊤} = ((Δ_{n}^{R}⟨k′′, r′′⟩)_{2}ψ)_{⊤}

((Δ_{m}^{R}⟨k′, r′⟩)_{2}ϕ)_{↓} = ((Δ_{n}^{R}⟨k′′, r′′⟩)_{2}ψ)_{↓}  (31)
((tap_{m}^{R} ⟨k′, r′⟩)_{2}ϕ′)_{⊤} = ((tap_{n}^{R} ⟨k′′, r′′⟩)_{2}ψ′)_{⊤} ,

where

ϕ = λi ^{∈} m. (βi)_{2}ψ
ϕ′ = λi ^{∈} m + 1. ((β + 1)i)_{2}ψ′
k′′ = K(λi ^{∈} m + 1. ((β + 1)i)_{1})k′ = K(|U|β + 1)k′
r′′ = λψ′ ^{∈} (Ob R)^{n+1}. r′ϕ′ .

Moreover, from Equations 16, 15, 19, and 20, when i < m,

((β + 1)i)_{2}ψ′ = (Φ_{n}^{R}(βi))_{2}ψ′ = (R(λi ^{∈} n. I_{n+1}^{R}i)(βi))_{2}ψ′ = (βi)_{2}(λi ^{∈} n. (I_{n+1}^{R}i)_{2}ψ′) = (βi)_{2}(λi ^{∈} n. ψ′i) = (βi)_{2}ψ ,

and when i = m,

((β + 1)i)_{2}ψ′ = (I_{n+1}^{R}n)_{2}ψ′ = ψ′n = ρ ,

so that

ϕ′ = [ λi ^{∈} m. (βi)_{2}ψ | m: ρ] = [ ϕ | m: ρ] .

Thus Equations 31 assert the equality of the limits that make

[figure: ((Δ_{m}^{R}⟨k′, r′⟩)_{2}ϕ)_{⊤}; (r′ϕ′)_{⊤}; F (Kϕ̂(Δ_{m}^{K}k′)); F (Kϕ̂′k′); ((Δ_{m}^{R}⟨k′, r′⟩)_{2}ϕ)_{↓}; (r′ϕ′)_{↓}; ((tap_{m}^{R} ⟨k′, r′⟩)_{2}ϕ′)_{⊤}; F (Kϕ̂′(tap_{m}^{K} k′))]

(where ϕ̂ = ϕ; Ob U and ϕ̂′ = ϕ′ ; Ob U = [ ϕ̂ | m: Uρ]), and

[figure: ((Δ_{n}^{R}⟨k′′, r′′⟩)_{2}ψ)_{⊤}; (r′′ψ′)_{⊤}; F (Kψ̂(Δ_{n}^{K}k′′)); F (Kψ̂′k′′); ((Δ_{n}^{R}⟨k′′, r′′⟩)_{2}ψ)_{↓}; (r′′ψ′)_{↓}; ((tap_{n}^{R} ⟨k′′, r′′⟩)_{2}ψ′)_{⊤}; F (Kψ̂′(tap_{n}^{K} k′′))]

commute in B for all ρ ^{∈} Ob R. To show that these limits are equal, we show the equality of the righthand sides and of the bottoms. We have already seen that r′′ψ′ = r′ϕ′. For the bottoms, we first note that, since (β + 1)i ^{∈} Ob R_{n+1}, Equation 22, the fact that |U| preserves products, and Equation 14 give

ϕ̂′ = λi ^{∈} m + 1. U(((β + 1)i)_{2}ψ′) = λi ^{∈} m + 1. Kψ̂′((β + 1)i)_{1} =
|U|(β + 1) ; Ob(Kψ̂′) = (|U|β + 1) ; Ob(Kψ̂′) = ψ̂′ ;_{|K|} (|U|β + 1) .

Then

Kϕ̂′(tap_{m}^{K} k′) = Kψ̂′(K(|U|β + 1)(tap_{m}^{K} k′)) =
Kψ̂′(tap_{n}^{K}(K(|U|β + 1)k′)) = Kψ̂′(tap_{n}^{K} k′′)

since K(|U|β + 1), K(|U|β) is a map of adjunctions. (End of Proof )

Finally, from Propositions 2, 9 and 11, we obtain the second-order abstraction theorem:

Proposition 12 Suppose K is a PL category, R = REL(K_{0}, B, F) is suitable for polymorphism, B is Cartesian closed and has pullbacks, and F preserves finite products. Let U be the forgetful functor from R to K_{0} and R and U be the PL category and morphism constructed in Proposition 11 such that R = R_{0} and U = U_{0}. If e ^{∈} E_{nπω}, ψ ^{∈} (Ob R)^{n}, and θ = ψ ; Ob U ^{∈} (Ob K_{0})^{n}, then there is a unique

g ^{∈} [[π]]_{n}^{R}ψ ⟶_{R} [[ω]]_{n}^{R}ψ

such that

[[e]]_{nπω}^{K}θ = Ug .

Proof : Let g = [[e]]_{nπω}^{R}ψ. As before, since U is faithful, g is unique. (End of Proof )

4 Parametricity

When Strachey originally introduced the notion of polymorphism [5], he distinguished parametric polymorphic functions, whose behavior does not depend upon the types to which they are applied, from ad hoc polymorphic functions, which can exhibit arbitrarily different behavior for different types. In [1], this distinction was connected with the identity extension lemma: the lemma does not hold for arbitrary models of the polymorphic lambda calculus, but when it does hold, it implies that the model is parametric, in a reasonable formalization of Strachey’s intuitive concept.

To recast this development in the more general setting of PL categories, we begin with what we believe is the appropriate generalization of the identity extension lemma, in its role as a hypothesis that insures parametricity:

Definition Two (pre-)PL categories K and R, such that R_{0} is the category REL(K_{0}^{a}, B, F (−_{1})×_{B} ⋯×_{B} F (−_{a})) of relations of arity a over K_{0}, are said to satisfy the parametricity hypothesis iff there are (pre-)PL morphisms J from K to R, and U^{1},…, U^{a} from R to K such that J_{0} is the identity-relation functor J, each U_{0}^{i} is the forgetful projection functor U_{i}, and the compositions

[figure: K; R; K; J; U^{i}]

are (pre-)PL identity morphisms.

An immediate consequence of this definition, via Proposition 9, is that the parametricity hypothesis indeed implies the identity extension lemma, i.e. the second-order analogue of Proposition 6:

Proposition 13 If PL categories K and R satisfy the parametricity hypothesis, with R_{0} = REL(K_{0}^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})), then, whenever ω ^{∈} Ω_{n} ∪ Ω_{n}^{∗} is a type or type assignment of the second-order typed lambda calculus and θ ^{∈} (Ob K_{0})^{n},

[[ω]]_{n}^{R}(θ; J) = ([[ω]]_{n}^{K}θ) ; J .

The reader will note that the parametricity hypothesis is defined for pre-PL categories as well as PL categories. Of course, pre-PL categories only suffice to model the firstorder typed lambda calculus, and in this case Proposition 6 asserts the same thing as Proposition 13 without requiring the parametricity hypothesis. Nevertheless, even in the first-order case, the hypothesis is connected with parametricity.

Even in the simply-typed lambda calculus, the inclusion of type variables introduces a kind of polymorphism, since we can regard ordinary expressions in n type variables, say in E_{nπω}, as denoting polymorphic functions in n type arguments. However, we cannot use such polymorphic functions as arguments to ordinary functions, so that polymorphic functions are not “first-class values”. We have a limited form of polymorphism similar to the kind that Milner introduced in ML [17, 18, 19].

From this viewpoint, the first-order abstraction theorem, especially in the multinary form of Proposition 4, asserts that the meaning of an ordinary expression containing type variables is a parametric polymorphic function. In particular, it asserts that the values of such a function at different types must satisfy a rich family of relations.

However, the kind of model described in Section 2 is not itself parametric. Although the expressions in E_{nπω} all have parametric meanings, the only “set” prescribed for these meanings is the enormous product ∏_{θ^{∈}(Ob K)^{n}}([[π]]_{n}^{K}θ ⟶_{K} [[ω]]_{n}^{K}θ), which imposes no constraining relation between the values obtained by applying a member to different θ, and thus contains all the type-correct functions that Strachey called “ad hoc”.

On the other hand, when the simply typed lambda calculus is modeled by a pre-PL category, the above product is replaced by the potentially more restricted morphism class ⟨⟨π⟩⟩_{n}^{K} ⟶_{K_{n}} ⟨⟨ω⟩⟩_{n}^{K}. In this situation (and also when the second-order calculus is modeled by a PL category) the parametricity hypothesis implies that all members of the morphism class satisfy the relations that are imposed by Proposition 4 on just those members that are meanings of expressions:

Proposition 14 Suppose pre-PL categories (PL categories) K and R satisfy the parametricity hypothesis, with R = R_{0} = REL(K_{0}^{a}, B, F (−_{1}) ×_{B} ⋯ ×_{B} F (−_{a})), and ω ^{∈} Ω_{n} and π ^{∈} Ω_{n}^{∗} are a type and type assignment of the firstorder (second-order) calculus. If f ^{∈} ⟨⟨π⟩⟩_{n}^{K} ⟶_{K_{n}} ⟨⟨ω⟩⟩_{n}^{K}, ψ ^{∈} (Ob R)^{n}, and, for all i ^{∈} a, θ_{i} = ψ ; Ob U_{i} ^{∈} (Ob K)^{n}, then there is a unique

g ^{∈} [[π]]_{n}^{R}ψ ⟶_{R} [[ω]]_{n}^{R}ψ

such that

⟨Kθ_{1}f,…, Kθ_{a}f⟩ = Ug .

Proof : By the parametricity hypothesis and Proposition 8,

J_{n}f ^{∈} J_{n}⟨⟨π⟩⟩_{n}^{K} ⟶_{R_{n}} J_{n}⟨⟨ω⟩⟩_{n}^{K} = ⟨⟨π⟩⟩_{n}^{R} ⟶_{R_{n}} ⟨⟨ω⟩⟩_{n}^{R} .

Since ψ ^{∈} 0 ⟶_{|R|} n, the definition of concrete semantics by Equation 18 gives

Rψ(J_{n}f) ^{∈} Rψ⟨⟨π⟩⟩_{n}^{R} ⟶_{R} Rψ⟨⟨ω⟩⟩_{n}^{R} = [[π]]_{n}^{R}ψ ⟶_{R} [[ω]]_{n}^{R}ψ ,

so that we make take g to be Rψ(J_{n}f). Then the naturality of the U^{i} makes the diagram of functors

[figure: R_{n}; K_{n}; R_{0}; K_{0}; U_{n}^{i}; U_{0}^{i} = U_{i}; Rψ; K(|U^{i}|ψ) = K(ψ ; Ob U_{0}^{i}) = K(ψ ; Ob U_{i}) = Kθ_{i}]

commute, so that the parametricity hypothesis gives

Kθ_{i}f = Kθ_{i}(U_{n}^{i}(J_{n}f)) = U_{i}(Rψ(J_{n}f)) = U_{i}g = P_{i}(Ug) ,

and since the P_{i} are projection functors, ⟨Kθ_{1}f,…, Kθ_{a}f⟩ = Ug. Since U is faithful, g is unique. (End of Proof )

Finally, when the parametricity hypothesis holds for a PL category modeling the second-order typed lambda calculus, it implies parametricity in the sense of [1], i.e. for the morphism sets ⟨⟨π⟩⟩_{n}^{K} ⟶_{K_{n}} ⟨⟨Δn. ω⟩⟩_{n}^{K} corresponding to polymorphic types. (Actually, the result is stated more simply in terms of the isomorphic sets ⟨⟨π̂⟩⟩_{n+1}^{K} ⟶_{K_{n+1}} ⟨⟨ω⟩⟩_{n+1}^{K}.)

Proposition 15 Suppose PL categories K and R satisfy the parametricity hypothesis, with R = R_{0} = REL(K_{0}^{a}, B, F (−_{1})×_{B}⋯×_{B}F (−_{a})), and ω ^{∈} Ω_{n+1} and π ^{∈} Ω_{n}^{∗} are a type and type assignment of the second-order typed lambda

calculus. If f ^{∈} ⟨⟨π̂⟩⟩_{n+1}^{K} ⟶_{K_{n+1}} ⟨⟨ω⟩⟩_{n+1}^{K}, θ ^{∈} (Ob K_{0})^{n}, r ^{∈} Ob R, and, for all

i ^{∈} a, k_{i} = U_{i}r, then there is a unique

g ^{∈} [[π]]_{n}^{R}(θ; Ob J) ⟶_{R} [[ω]]_{n+1}^{R}[ θ; Ob J | n: r]

such that

⟨K[ θ | n: k_{1} ]f,…, K[ θ | n: k_{a}]f⟩ = Ug .

Proof : In Proposition 14, take n to be n + 1, π to be π̂, ψ to be ψ′ =^{def} [ θ ; Ob J | n: r], and θ_{i} to be [ θ | n: k_{i}]. It follows that there is a unique

g ^{∈} [[π̂]]_{n+1}^{R}ψ′ ⟶_{R} [[ω]]_{n+1}^{R}ψ′

such that ⟨K[ θ | n: k_{1} ]f,…, K[ θ | n: k_{a}]f⟩ = Ug. However, by Equation 14,

ψ′ ;_{|R|} (J_{n⊆n+1} ; I_{n+1}^{|R|}) = J_{n⊆n+1} ; I_{n+1}^{|R|} ; Ob(Rψ′) =
J_{n⊆n+1} ; (ψ′ ;_{|R|} I_{n+1}^{|R|}) = J_{n⊆n+1} ; ψ′ = θ; Ob J ,

so that

[[π̂]]_{n+1}^{R}ψ′ = Rψ′⟨⟨π⟩⟩_{n+1}^{R} = Rψ′(Φ_{n}^{R}⟨⟨π⟩⟩_{n}^{R}) =
Rψ′(R(J_{n⊆n+1} ; I_{n+1}^{|R|})⟨⟨π⟩⟩_{n}^{R}) = R(θ; Ob J)⟨⟨π⟩⟩_{n}^{R} = [[π]]_{n}^{R}(θ; Ob J) .

(End of Proof )

5 Kripke Relations

In [20], G. D. Plotkin generalized the abstraction (or logical-relations) theorem for the simply typed lambda calculus by introducing Kripke relations, and showed that the result characterizes “lambda-definabilty”: every meaning satisfying the generalized logicalrelations property (what we might call every meaning that is parametric in the Kripke sense) is the meaning of some expression. This generalization fits nicely into our present framework.

Conventionally, an a-ary Kripke relation on sets r_{1},…, r_{a} is a family of relations { r_{⊤}w ⊆ r_{1} × ⋯ × r_{a} | w ^{∈} W } indexed by a preordered set W and satisfying r_{⊤}w ⊆ r_{⊤}w′ whenever w ≤ w′. From our viewpoint, each r_{⊤}w becomes the domain of a monic function r_{↓}w into r_{1}×⋯×r_{a}. Moreover, r_{⊤} is extended to a functor from W to SET and a naturality condition is imposed on r_{↓}: whenever w ≤ w′, the diagram

[figure: r_{⊤}w; r_{⊤}w′; r_{1} × ⋯ × r_{a}; r_{⊤}(w ≤ w′); r_{↓}w; r_{↓}w′]

commutes in SET, so that the image of r_{↓}w is a subset of the image of r_{↓}w′.

Thus the category of a-ary Kripke relations is REL(K, B, F), where K is SET^{a}, B is SET^{W}, and F is the functor from SET^{a} to SET^{W} such that

F ⟨s_{1},…, s_{a}⟩w = s_{1} × ⋯ × s_{a} F ⟨s_{1},…, s_{a}⟩(w ≤ w′) = I_{s_{1}×···×s_{a}}

whenever ⟨s_{1},…, s_{a}⟩ is an object or morphism of SET^{a}.

An obvious generalization is to let K be any Cartesian closed category and F be such that

F kw = Gk F k(w ≤ w′) = I_{Gk} ,

where G is any product-preserving functor from K to SET. It is well-known that SET^{W} is Cartesian closed, and easy to see that SET^{W} has pointwise pullbacks and that F preserves products. Thus Proposition 2 applies and the first-order abstraction theorem holds.

However, in REL(K, SET^{W} , F) it is the natural transformations r_{↓} that must be monic, while in a Kripke relation we have said that the component functions r_{↓}w must be monic (i.e. injective). Fortunately these two conditions are equivalent:

Proposition 16 Suppose r_{↓} ^{∈} r_{⊤} ⟶_{SET^{W}} F r_{⊥} where F is such that F kw = Gk
and F k(w ≤ w′) = I_{Gk}. Then r_{↓} is monic iff r_{↓}w is injective for all w ^{∈} W.

Proof : It is easy to see that r_{↓} is monic when every r_{↓}w is monic. To complete the proof, we will show that r_{↓} is not monic whenever some r_{↓}w is not injective. So suppose that there are w_{0} ^{∈} W and distinct x_{1}, x_{2} ^{∈} r_{⊤}w_{0} such that r_{↓}w_{0}x_{1} = r_{↓}w_{0}x_{2}.

Let b be the functor from W to SET such that bw is the singleton set {y} when w_{0} ≤ w and the empty set otherwise, and b(w ≤ w′) is the unique function from bw to bw′. (One cannot have bw = {y} and bw′ empty when w ≤ w′.) For i ^{∈} {1, 2}, let δ_{i} ^{∈} b ⟶_{SET^{W}} r_{⊤} be such that δ_{i}wy = r_{⊤}(w_{0} ≤ w)x_{i} when w_{0} ≤ w, and δ_{i}w is the empty function otherwise. The naturality of the δ_{i} is easily seen. Moreover, δ_{i}w; r_{↓}w is independent of i, since when w_{0} ≤ w, r_{↓}w(δ_{i}wy) = r_{↓}w(r_{⊤}(w_{0} ≤ w)x_{i}) = r_{↓}w_{0}x_{i} by the naturality of r_{↓}, and when w_{0} ≤ w is false, δ_{i}w; r_{↓}w is the empty function.

Thus δ_{i};_{SET}^{W} r_{↓} is independent of i, while the δ_{i} themselves are distinct (when applied to w_{0}). Therefore r_{↓} is not monic. (End of Proof )

As a consequence of this proposition, the limits in Diagram 23 can be taken pointwise. Thus Kripke relations are suitable for polymorphism, Proposition 11 applies, and the second-order abstraction theorem holds.

6 Complete Relations on Domains

In [1], in a brief lapse from the set-theoretic view, the abstraction theorem was proved for complete relations over a model of the simply typed lambda calculus using the category CPO of complete partial orders (posets with least elements and least upper bounds of directed sets) and continuous functions. Conventionally, a complete (unary) relation on a c.p.o. r_{⊥} is a complete subset r_{⊤} ⊆ r_{⊥}, i.e. a subset containing the least element of r_{⊥} and closed under least upper bounds (in r_{⊥}) of directed subsets. From our present viewpoint, such a relation is a triple ⟨r_{⊥}, r_{⊤}, r_{↓}⟩ where r_{↓} ^{∈} r_{⊤} ⟶_{CPO} r_{⊥} is strict and bimonotone, i.e.

r_{↓}(⊥) = ⊥  and  r_{↓}x ⊑ r_{↓}y iff x ⊑ y ,

since the images of such functions are exactly the complete subsets of r_{⊥}. (Note that bimonotonicity implies monicity.)

Unfortunately, the category of complete relations does not quite fit the Procrustean bed developed in the previous sections; it is not a category of the form REL(K, B, F), although it is a full subcategory of REL(CPO, CPO, I). Nevertheless it is Cartesian closed, so that the first-order abstraction theorem still holds.

Before proving this, we generalize to allow K to be any Cartesian closed category with a product-preserving functor F from K to CP O that satisfies a certain strictness condition. This is necessary to deal with multinary relations, and also to encompass a variety of models of the polymorphic lambda calculus in which K_{0} is a subcategory of CPO or a category whose objects represent c.p.o.’s. (Examples include categories of closures [21], finitary retracts [22], finitary projections [23], qualitative domains [24], and DI-domains [25]. Such models are formulated as PL categories in [11]. A more concrete viewpoint is found in [26].)

Definition Let K be a category and F be a functor from K to CPO. Then COMREL(K, F) is the full subcategory of REL(K, CPO, F) whose objects ⟨r_{⊥}, r_{⊤}, r_{↓}⟩ are such that r_{↓} is strict and bimonotone.

Proposition 17 If K is Cartesian closed, F is product-preserving, and the function ab^{CPO}(F ap_{kk′}^{K}) is strict for all k, k′ ^{∈} Ob K, then COMREL(K, F) is Cartesian closed, and the forgetful functor U from COMREL(K, F) to K is a morphism of Cartesian closed categories.

Proof : Essentially, we recapitulate the proof of Proposition 2 while showing that exponentiation preserves the special nature of objects. (A superficial complication is that CPO does not have all pullbacks; however it has pullbacks of diagrams whose morphisms are strict, which is all that is necessary.) Thus we will assume that r′_{↓} is strict and bimonotone (a similar condition on r_{↓} is unnecessary), and show that this implies that the pullback defining r ⟹_{R} r′ is well-defined and that (r ⟹_{R} r′)_{↓} is strict and bimonotone.

By applying the composition of functions in Diagram 1 to ⟨⊥, x⟩ ^{∈} F (r_{⊥} ⟹_{K} r′_{⊥}) × r_{⊤}, and using the specific nature of CPO (including the fact that the least element of a function space is the constant function giving the least result) and the strictness condition on F, we have

t⊥x = ap⟨t⊥, x⟩ = ((t × I) ; ap)⟨⊥, x⟩ =
((I × r_{↓}) ; F ap)⟨⊥, x⟩ = F ap ⟨⊥, r_{↓}x⟩ = ab(F ap)⊥(r_{↓}x) = ⊥(r_{↓}x) = ⊥ ,

and since this holds for all x ^{∈} r_{⊤}, t is strict.

A similar argument applied to Diagram 2 shows that r_{⊤} ⟹_{CPO} r′_{↓} is strict since r′_{↓} is strict. Moreover, when applied to ⟨f_{i}, x⟩, Diagram 2 gives

(r_{⊤} ⟹_{CPO} r′_{↓})f_{i}x = ap⟨(r_{⊤} ⟹_{CPO} r′_{↓})f_{i}, x⟩ = (((r_{⊤} ⟹_{CPO} r′_{↓}) × I) ; ap)⟨f_{i}, x⟩ =

(ap ; r′_{↓})⟨f_{i}, x⟩ = r′_{↓}(f_{i}x) ,

so that (r_{⊤} ⟹_{CPO} r′_{↓})f_{1}x ⊑ (r_{⊤} ⟹_{CPO} r′_{↓})f_{2}x implies r′_{↓}(f_{1}x) ⊑ r′_{↓}(f_{2}x), and since r′_{↓} is bimonotone, f_{1}x ⊑ f_{2}x. Since this holds for all x ^{∈} r_{⊤},

(r_{⊤} ⟹_{CPO} r′_{↓})f_{1} ⊑ (r_{⊤} ⟹_{CPO} r′_{↓})f_{2} implies f_{1} ⊑ f_{2} ,

and since the opposite implication holds for all continuous functions, r_{⊤} ⟹_{CPO} r′_{↓} is bimonotone.

Since pullbacks in CPO are essentially the same as in SET, the pullback in Diagram 3 is

(r ⟹_{R} r′)_{⊤} = { ⟨f, g⟩ | f ^{∈} F (r_{⊥} ⟹_{K} r′_{⊥}) and g ^{∈} r_{⊤} ⟹_{CPO} r′_{⊤} and tf = (r_{⊤} ⟹_{CPO} r′_{↓})g }

with pointwise ordering; the functions (r ⟹_{R} r′)_{↓} and u are the obvious projections. Since t and r_{⊤} ⟹_{CPO} r′_{↓} are strict, the pullback is a c.p.o. and, as is easily seen, the projections are strict.

Moreover, suppose (r ⟹_{R} r′)_{↓}⟨f_{1}, g_{1}⟩ ⊑ (r ⟹_{R} r′)_{↓}⟨f_{2}, g_{2}⟩. Since (r ⟹_{R} r′)_{↓} is the first projection, f_{1} ⊑ f_{2}. Then tf_{1} ⊑ tf_{2}, and by the equation constraining the ⟨f, g⟩ ^{∈} (r ⟹_{R} r′)_{⊤}, (r_{⊤} ⟹_{CPO} r′_{↓})g_{1} ⊑ (r_{⊤} ⟹_{CPO} r′_{↓})g_{2}, and since r_{⊤} ⟹_{CPO} r′_{↓} is bimonotone, g_{1} ⊑ g_{2}. Thus ⟨f_{1}, g_{1}⟩ ⊑ ⟨f_{2}, g_{2}⟩, so that (r ⟹_{R} r′)_{↓} is bimonotone. (End of Proof )

This establishes the abstraction theorem for the first-order typed lambda calculus, but the second-order case is more complex, since COMREL(K, F) is not “suitable for polymorphism”. The construction of the necessary limits is the same for CPO as for SET, but — much as with the pullbacks in the previous proof — it may give an r_{⊤} that has no least element. However, the limit exists in CPO whenever the functions F (fρ) at the bottom of Diagram 23 are strict for all ρ ^{∈} Ob R. (The functions at the right of this diagram must be strict since rρ is a complete relation.) Thus, for the proof of Proposition 11 to go through, it is sufficient for the functions at the bottom of Diagram 27 to be strict. Happily, this is a reasonable property to expect of domain-theoretic PL-category models of any extension of the second-order polymorphic lambda calculus that includes a polymorphic fixed-point operator.

If the language contains a polymorphic fixed-point operator then, for any type expression ω ^{∈} Ω_{n}, one can write a closed ordinary expression e ^{∈} E_{n⟨⟩ω} (where ⟨⟩ is the empty type assignment) denoting the least element of type ω. In terms of concrete semantics, this means that, for all θ ^{∈} (Ob K_{0})^{n}, F ([[e]]_{n⟨⟩ω}θ) is a constant function yielding the least element of F ([[ω]]_{n}θ) (at least if F preserves least morphisms). Then the connection with abstract semantics given by Equation 18 shows that there is a morphism ⟨⟨e⟩⟩_{n⟨⟩ω} ^{∈} ⊤ ⟶_{K_{n}} ⟨⟨ω⟩⟩_{n} (where ⊤ is the distinguished terminal object of K_{n}) such that F (Kθ⟨⟨e⟩⟩_{n⟨⟩ω}) is a constant function yielding a least element.

It is reasonable to assume that this property holds, not just for the objects ⟨⟨ω⟩⟩_{n} of K_{n} that are the meanings of type expressions, but for all objects of K_{n}. Thus:

Definition A PL category K and a functor F from K_{0} to CPO are said to express least elements polymorphically iff, for all k ^{∈} K_{n}, there is a morphism f ^{∈} ⊤ ⟶_{K_{n}} k such that, for all θ ^{∈} (Ob K_{0})^{n}, F (Kθf) is a constant function yielding the least element of F (Kθk).

Then the following proposition establishes the abstraction theorem for the second-order case:

Proposition 18 Suppose K is a PL category and R = COMREL(K_{0}, F). If F is product-preserving, ab^{CPO}(F ap_{kk′}^{K_{0}}) is strict for all k, k′ ^{∈} Ob K_{0}, and K and F express least elements polymorphically, then there is a PL category R and a PL morphism U from R to K such that R = R_{0} and U = U_{0}.

Proof : In Diagram 17, take k to be the terminal object of K_{n}; then since Φ_{n} is a morphism of Cartesian closed categories, Φ_{n}k is the terminal object of K_{n+1}. For ψ̂′ ^{∈} (Ob K_{0})^{n+1}, applying the functors Kψ̂′ and F to this diagram gives

[figure: F (Kψ̂′(⊤)); F (Kψ̂′(Φ_{n}(Δ_{n}k′))); F (Kψ̂′(k′)); F (Kψ̂′(Φ_{n}(tab_{n} f′))); F (Kψ̂′(f′)); F (Kψ̂′(tap_{n} k′))]

Since K and F express least elements polymorphically, there is an f′ such that F (Kψ̂′(f′)) is a constant function yielding the least element of F (Kψ̂′(k′)). But then the diagram can commute only if F (Kψ̂′(tap_{n} k′)) is a strict function.

The rest of the proof is the same as that of Proposition 11, except that the limit in Diagram 27 exists because the functions at the bottom of the diagram are strict.

(End of Proof )

7 Summary and Connections with Other Work

We have generalized the concept of relations over sets to that of a category REL(K, B, F) of relations over a category K, which we have used to investigate the abstraction theorem, the identity extension lemma, and parametric polymorphism, in three cases:

• CCC: where a Cartesian closed category models the first-order lambda calculus,

• pre-PL: where a pre-PL category models the first-order lambda calculus,

• PL: where a PL category models the second-order lambda calculus.

In each of the last two cases, we defined a “parametricity hypothesis”.

Under reasonable conditions, the abstraction theorem holds in the CCC case (Proposition 3), and also in the pre-PL case since the concrete semantics for a pre-PL category K is the same as that for the Cartesian closed category K_{0}. Under more stringent conditions, the abstraction theorem also holds in the PL case (Proposition 12).

The identity extension lemma holds under reasonable conditions in the CCC case (Proposition 6), and also in the pre-PL case since the concrete semantics is the same. It does not hold for all reasonable models in the PL case, but it is implied by the parametricity hypothesis (Proposition 13).

Even in the simply typed lambda calculus, polymorphic functions appear as the meanings of ordinary expressions containing type variables. One can regard the abstraction theorem as asserting that the meanings of such expressions are parametric polymorphic functions. But in general, the sets (or classes) of meanings that are prescribed for various types by a model will also contain ad hoc parametric functions. Such ad hoc functions occur in all nontrivial instances of the CCC case.

In the pre-PL and PL cases, however, the parametricity hypothesis implies the parametricity of all members of the sets (or classes) ⟨⟨π⟩⟩_{n}^{K} ⟶_{K_{n}} ⟨⟨ω⟩⟩_{n}^{K} of meanings appropriate to expressions containing type variables (Proposition 14). In the PL case, the parametricity hypothesis also implies the parametricity of the sets ⟨⟨π⟩⟩_{n}^{K} ⟶_{K_{n}} ⟨⟨Δn. ω⟩⟩_{n}^{K} of meanings appropriate to expressions with polymorphic types (Proposition 15). (Of course, the parametricity hypothesis may be unnecessarily strong: there may be parametric models for which the hypothesis is false, e.g. in which ab^{B}(F ap^{K}) is not monic.)

Kripke relations fit nicely into our framework (Proposition 16). On the other hand, complete relations on domains are more problematical; they are a full subcategory of a category REL(K, CPO, F) of relations. Nevertheless, the first-order abstraction theorem still holds under reasonable conditions (Proposition 17), and the second-order abstraction theorem holds under more stringent conditions that are reasonable for models that can accommodate a polymorphic fixed-point operator (Proposition 18).

We have used the term “PL category” even though R. Seely’s original definition [9] differs from ours in requiring the base category |K| to be Cartesian closed, in order to model the Ω-order typed lambda calculus. (However, Seely does discuss modeling of the second-order language briefly.) Our definition is closer to the 2TλC-hyperdoctrine of A. Pitts [10], except that Pitts only requires Diagram 13 to hold within an isomorphism.

Closest to our definition is the “framework” of B. Narayanan [11]. His K_{n} is the same as ours, his A_{n} is our I_{n}^{|K|}, and for α ^{∈} (Ob K_{n})^{m}, his H_{mn}α is our Kα. Thus his Σ is the dual of our base category |K|, and his adjoint functors Φ_{n} and Δ_{n} are the same as ours.

Although we have retained the term “abstraction theorem” to emphasize continuity with [1], the term “logical relations” was used in what seems to be the earliest instance of the theorem (for the set-theoretic model of the simply typed lambda calculus), which appeared in [6], where G. D. Plotkin attributed it to M. Gordon. A special case of the concept, where the relation assigned to the single primitive type is the ordering of the natural numbers, was also devised by W. A. Howard (in order to define hereditarily majorizable functionals) in [27].

In [6], Plotkin also proved a logical-relations theorem for Scott models of the untyped lambda calculus. We will not attempt to survey the other papers that have explored or used logical relations for either the simply typed or the untyped lambda calculus, in either syntactic or semantic (though usually not category-theoretic) versions; important examples include [20] (where Kripke relations were introduced) and [28].

Closer to our concerns is [29], where Mitchell and Meyer give a logical-relations theorem for the polymorphic lambda calculus, using the Bruce-Meyer-Mitchell concept of a model [30]. It is tricky to compare the Bruce-Mitchell-Meyer framework with that of PL categories [31, 32]. Nevertheless, we suspect that the “fundamental theorem of SΛ logical relations” in [29] is weaker than our corresponding Proposition 11, since their Condition LR.3 (in Section 4.2) imposes a single relation between the applications of polymorphic functions c and d to particular arguments a and b, while our limit condition 27 is quantified over all ρ ^{∈} Ob R, where (in the binary case) Ob R contains many (indeed all) relations with domain a and codomain b.

The approach of [29] is also used by P. Wadler in [33], where the “parametricity theorem” is what we would call an abstraction theorem. The proof is murky, but the paper contains fascinating examples of the use of parametricity. A treatment of parametricity by an extension of the Bruce-Mitchell-Meyer framework is given by R. Hasegawa [34].

There are also a variety of category-theoretic ideas that are relevant to our work. The “scone” [35, Section 1(10)] or “Freyd cover” [12, Part II, Section 22] of a category K with a terminal object ⊤ would be the same as REL(K, SET, Hom_{K}(⊤, −)) if we had not imposed monicity on the r_{↓}’s. As it is, REL(K, SET, Hom_{K}(⊤, −)) is a full sub-Cartesian closed category of the scone of K (and is equivalent to a “subscone” as defined in [36]).

In [37], Bainbridge, Freyd, Scedrov, and Scott explicate parametricity by means of dinatural transformations [16, Section IX.4]. Although their general development is limited to the first-order case, a relational approach to second-order parametricity is worked out for the specific case of PER models. Dinaturality also plays a major role in [38]. We do not fully understand the connection between dinaturality and the work presented here.

More recently, Freyd introduced the idea of “structors” [39] and connected it with parametricity. Let C and K be categories and R be REL(K × K, K, −_{1} ×_{K} −_{2}) without the monicity requirement. Then (from our point of view) a structor from C to K is a pair of maps k ^{∈} (Ob K)^{Ob C} and r ^{∈} (Ob R)^{Mor C} such that, for all c ^{∈} Ob C and all μ ^{∈} Mor C,

k(dom μ) = U_{1}(rμ)  k(cod μ) = U_{2}(rμ)  r(id c) = J(kc) ,

where dom and cod map morphisms of C into their domains and codomains, while id maps objects into their identity morphisms. Similarly, a morphism of structors from ⟨k, r⟩ to ⟨k′, r′⟩ is a pair of maps f ^{∈} ∏_{c^{∈}Ob C} kc ⟶_{K} k′c and g ^{∈} ∏_{μ^{∈}Mor C} rμ ⟶_{R} r′μ such that, for all c ^{∈} Ob C and all μ ^{∈} Mor C,

f(dom μ) = U_{1}(gμ)  f(cod μ) = U_{2}(gμ)  g(id c) = J(fc) .

From a more abstract perspective, the category of structors from C to K is the limit in the category of categories of the diagram

[figure: K^{Ob C}; K^{Mor C}; K^{Mor C}; R^{Ob C}; R^{Mor C}; K^{dom}; K^{cod}; J^{Ob C}; U_{1}^{Mor C}; U_{2}^{Mor C}; R^{id}]

Still closer to our ideas is current work by Mitchell and Scedrov [36] (with contributions by S. Abramsky and P. Wadler in the initial phase). These authors state Proposition 2, which they describe as “category-theoretic folklore”, and they treat generalized relations in the framework of “iml-categories”, which are equivalent to pre-PL categories. Proposition 2 has also been discovered independently by G. M. Kelly [40].

Central to [36] is the concept of “relators”, which, like structors, can be described as limits. Let R = REL(K × K, SET, Hom_{K}(⊤, −_{1}) × Hom_{K}(⊤, −_{2})) and R = REL(K′ × K′, SET, Hom_{K′}(⊤, −_{1}) × Hom_{K′}(⊤, −_{2})). Then the category of (binary) relators from K to K′ is the limit of

[figure: K^{′Ob K}; K^{′Ob R}; K^{′Ob R}; R^{′Ob R}; K^{′Ob U_{1}}; K^{′Ob U_{2}}; U_{1}^{′Ob R}; U_{2}^{′Ob R}]

A slightly different definition, where relators are required to preserve identity relations, is used by Abramsky and Jensen in [41]. Their category of relators is the limit of

[figure: K^{′Ob K}; K^{′Ob R}; K^{′Ob R}; R^{′Ob K}; R^{′Ob R}; K^{′Ob U_{1}}; K^{′Ob U_{2}}; J^{′Ob K}; U_{1}^{′Ob R}; U_{2}^{′Ob R}; R^{′Ob J}]

In [1], it was stated without proof that, in the (nonexistent) parametric set-theoretic model of the polymorphic calculus, types in which the Δ operations occur on the outside and →’s do not nest more than two deep on the left have meanings that are sorts of initial anarchic many-sorted algebras. (The analogous syntactic result, that the corresponding sets of closed normal forms are such algebras, was shown by Böhm and Berarducci [42], and by Leivant [43]. The basic idea is anticipated in the work of Martin-Löf [44] and was probably known to early proof theorists such as Takeuti.) The simplest nontrivial case is that the meanings of type Δ0. (0 → 0) → (0 → 0) are in a one-to-one correspondence (given by the Church numerals) with the natural numbers.

The generalization of this result (to models that exist) has been a concern in, for example, [37], [45], [8], [39], and [34]. The question of whether such a result can be obtained from our parametricity hypothesis is undoubtedly the outstanding open problem raised by the ideas in this paper. Beyond this we hope to investigate particular models to determine whether they are, or can be modified to be, parametric.

References

[1] Reynolds, J. C. Types, Abstraction and Parametric Polymorphism. in: Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, September 19–23, 1983, edited by R. E. A. Mason. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1983, pp. 513–523.

[2] Girard, J.-Y. Une Extension de l’Interprétation de Gödel à l’Analyse, et son Application à l’Élimination des Coupures dans l’Analyse et la Théorie des Types. in: Proceedings of the Second Scandinavian Logic Symposium, University of Oslo, June 18–20, 1970, edited by J. E. Fenstad. Studies in Logic and the Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971, pp. 63–92.

[3] Girard, J.-Y. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur, Thèse de doctorat d’état. Université Paris VII, June 1972.

[4] Reynolds, J. C. Towards a Theory of Type Structure. in: Programming Symposium, Proceedings, Colloque sur la Programmation, Paris, April 9–11, edited by B. Robinet. Lecture Notes in Computer Science, vol. 19, Springer-Verlag, Berlin, 1974, pp. 408–425.

[5] Strachey, C. Fundamental Concepts in Programming Languages. Unpublished lecture notes, International Summer School in Computer Programming, Copenhagen, August 1967.

[6] Plotkin, G. D. Lambda-Definability and Logical Relations. Memorandum, no. SAI– RM–4, University of Edinburgh, School of Artificial Intelligence, October 1973.

[7] Reynolds, J. C. Polymorphism is not Set-Theoretic. in: Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27–29, edited by G. Kahn, D. B. MacQueen, and G. D. Plotkin. Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, 1984, pp. 145–156.

[8] Reynolds, J. C. and Plotkin, G. D. On Functors Expressible in the Polymorphic Typed Lambda Calculus. Report, no. CMU–CS–90–147, Carnegie Mellon University, School of Computer Science, July 6, 1990.

[9] Seely, R. A. G. Categorical Semantics for Higher Order Polymorphic Lambda Calculus. Journal of Symbolic Logic, vol. 52 (1987), pp. 969–989.

[10] Pitts, A. M. Polymorphism is Set Theoretic, Constructively. in: Category Theory and Computer Science, Edinburgh, Scotland, September 7–9, edited by D. H. Pitt, A. Poigné, and D. E. Rydeheard. Lecture Notes in Computer Science, vol. 283, Springer-Verlag, Berlin, 1987.

[11] Narayanan, B. R. A General Framework for Models of Type Polymorphism, Ph. D. Dissertation. Syracuse University, December 1988, vi+155 pp. Report No. CIS-89-1.

[12] Lambek, J. and Scott, P. J. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge, England, 1986, ix+293 pp.

[13] Barr, M. and Wells, C. Toposes, Triples, and Theories. Grundlehren der mathematischen Wissenschaften, vol. 278, Springer-Verlag, New York, 1985, xiii+345 pp.

[14] Lawvere, F. W. Functorial Semantics of Algebraic Theories. Proceedings of the National Academy of Sciences of the United States of America, vol. 50 (1963), pp. 869–872.

[15] Lawvere, F. W. Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories. in: Reports of the Midwest Category Seminar II, edited by S. Mac Lane. Lecture Notes in Mathematics, vol. 61, Springer-Verlag, Berlin, 1968, pp. 41–61.

[16] Mac Lane, S. Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5, Springer-Verlag, New York, 1971, ix+262 pp.

[17] Milner, R. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, vol. 17 (1978), pp. 348–375.

[18] Damas, L. and Milner, R. Principal Type-Schemes for Functional Programs. in: Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, January 25–27. 1982, pp. 207–212.

[19] Harper, R. and Mitchell, J. C. On the Type Structure of Standard ML. ACM Transactions on Programming Languages and Systems, vol. 15 (1993), pp. 211–252.

[20] Plotkin, G. D. Lambda-Definability in the Full Type Hierarchy. in: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, edited by J. P. Seldin and J. R. Hindley. Academic Press, London, 1980, pp. 363–373.

[21] McCracken, N. J. An Investigation of a Programming Language with a Polymorphic Type Structure, Ph. D. Dissertation. Syracuse University, June 1979, iv+126 pp.

[22] McCracken, N. J. A Finitary Retract Model for the Polymorphic Lambda-Calculus. Unpublished, Syracuse University, 1982.

[23] Amadio, R., Bruce, K. B., and Longo, G. The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations. in: Proceedings Symposium on Logic in Computer Science, Cambridge, Massachusetts, June 16–18. 1986, pp. 122–130.

[24] Girard, J.-Y. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science, vol. 45 (1986), pp. 159–192.

[25] Coquand, T., Gunter, C. A., and Winskel, G. DI-Domains as a Model of Polymorphism. in: Mathematical Foundations of Programming Language Semantics, 3rd Workshop, Tulane University, New Orleans, April 8–10, 1987, edited by M. Main, A. Melton, M. Mislove, and D. A. Schmidt. Lecture Notes in Computer Science, vol. 298, Springer-Verlag, Berlin, 1988, pp. 344–363.

[26] Coquand, T., Gunter, C. A., and Winskel, G. Domain Theoretic Models of Polymorphism. Information and Computation, vol. 81 (1989), pp. 123–167.

[27] Howard, W. A. Hereditarily Majorizable Functionals of Finite Type. in: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, edited by A. S. Troelstra. Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973, pp. 454–461. Appendix.

[28] Statman, R. Logical Relations and the Typed λ-Calculus. Information and Control, vol. 65 (1985), pp. 85–97.

[29] Mitchell, J. C. and Meyer, A. R. Second-order Logical Relations (Extended Abstract). in: Logic of Programs, Brooklyn, New York, June 17–19, edited by R. Parikh. Lecture Notes in Computer Science, vol. 193, Springer-Verlag, Berlin, 1985, pp. 225–236.

[30] Bruce, K. B., Meyer, A. R., and Mitchell, J. C. The Semantics of Second-Order Lambda Calculus. Information and Computation, vol. 85 (1990), pp. 76–134.

[31] Jacobs, B. P. F. On the Semantics of Second Order Lambda Calculus: From Bruce-Meyer-Mitchell Models to Hyperdoctrine Models and Vice-Versa. in: Category Theory and Computer Science, Manchester, UK, September 5–8, edited by D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poigné. Lecture Notes in Computer Science, vol. 389, Springer-Verlag, Berlin, 1989, pp. 198–212.

[32] Jacobs, B. P. F. Semantics of the second order Lambda Calculus. Mathematical Structures in Computer Science, vol. 1 (1991), pp. 327–360.

[33] Wadler, P. Theorems for Free. in: Functional Programming Languages and Computer Architecture, FPCA ’89 Conference Proceedings Fourth International Conference, Imperial College, London, September 11–13. ACM, 1989, pp. 347–359.

[34] Hasegawa, R. Categorical Data Types in Parametric Polymorphism. Unpublished, November 16, 1990.

[35] Freyd, P. J. and Scedrov, A. Categories, Allegories. North-Holland Mathematical Library, vol. 39, North-Holland, Amsterdam, 1990, xviii+296 pp.

[36] Mitchell, J. C. and Scedrov, A. Sconing, Relators, and Parametricity. Unpublished draft, October 21, 1991.

[37] Bainbridge, E. S., Freyd, P. J., Scedrov, A., and Scott, P. J. Functorial Polymorphism. Theoretical Computer Science, vol. 70 (1990), pp. 35–64. Corrigendum in (3) 71, 10 April 1990, p. 431.

[38] Girard, J.-Y., Scedrov, A., and Scott, P. J. Normal Forms and Cut-Free Proofs as Natural Transformations. in: Logic from Computer Science, Berkeley, California, November 13–17, 1989, edited by Y. N. Moschovakis. Mathematical Sciences Research Institute Publication, vol. 21, Springer-Verlag, 1992, pp. 217–241.

[39] Freyd, P. J. Structural Polymorphism. Unpublished, January 23, 1989.

[40] Kelly, G. M. Private communication. July 1991.

[41] Abramsky, S. and Jensen, T. P. A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions. in: Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, January 21–23. 1991, pp. 49–54.

[42] Böhm, C. and Berarducci, A. Automatic Synthesis of Typed Λ-Programs on Term Algebras. Theoretical Computer Science, vol. 39 (1985), pp. 135–154.

[43] Leivant, D. Reasoning About Functional Programs and Complexity Classes Associated with Type Disciplines. in: 24th Annual Symposium on Foundations of Computer Science, IEEE, Tucson, Arizona, November 7–9. 1983, pp. 460–469.

[44] Martin-Löf, P. A Construction of the Provable Wellorderings of the Theory of Species. Unpublished.

[45] Freyd, P. J. POLYNAT in PER. in: Categories in Computer Science and Logic, Boulder, Colorado, June 14–20, 1987, edited by J. W. Gray and A. Scedrov. Contemporary Mathematics, vol. 92, American Mathematical Society, Providence, Rhode Island, 1989, pp. 67–68.