Notes on Sconing and Relators

John C. Mitchell^{∗}  Andre Scedrov^{†}

Abstract

This paper describes a semantics of typed lambda calculi based on relations. The main mathematical tool is a category-theoretic method of sconing, also called glueing or Freyd covers. Its correspondence to logical relations is also examined.

1 Introduction

Many modern programming languages feature rather sophisticated typing mechanisms. For instance, languages such as ML include polymorphic data types, which allow considerable flexibility and abstraction to the user. Several notions of polymorphism were introduced into computer science by Strachey [Str67], among them the important notion of parametric polymorphism. Strachey’s intuitive definition is that a polymorphic function is parametric if it has a uniformly given algorithm in all types, that is, if the function’s behavior is independent of the type at which the function is instantiated. Reynolds [Rey83] proposed a mathematical definition of parametric polymorphic functions by means of invariance with respect to certain relations induced by types. Unfortunately, the mathematical tools used in [Rey83] were limited to a standard set-theoretic framework, which Reynolds later showed to be vacuous in the case of so-called second order polymorphic lambda calculus (see Pitts [Pit87]).

We describe a general mathematical framework for semantics of type disciplines based on relations. This framework, which is also proposed independently by Ma and Reynolds [MaR92], may be used to give a mathematically correct notion of relational invariance proposed in [Rey83] and a rigorous framework for the considerations in Wadler [Wad89]. A syntactic counterpart of this semantic framework is proposed by Abadi et al. [ACC93]. The relational semantic framework we describe is also useful in investigating other aspects of programming languages. Abramsky and Jensen [AbJ91] use it for strictness analysis and O’Hearn and Tennent [OHT93] use it in studying semantics of local variables.

The main mathematical tool used in this work is the category-theoretic method of sconing described in Freyd and Scedrov [FrS90] and also called glueing or Freyd covers, see Lambek and Scott [LS86]. To our knowledge, the first application of this method to type disciplines is given in Appendix C of Lafont [Laf88]. In the case of simple types, this method corresponds closely to so-called logical relations, described for instance in Plotkin [Plo80], Statman [Sta85], and Mitchell [Mit90]. We examine this correspondence in detail. In order to make the methods and arguments accessible to readers with minimal background in category theory, we choose a much more relaxed style of presentation than would be usual in a research paper. In this vein, here we discuss only the basic framework for simple types and for implicit polymorphism. The extension to explicit polymorphism should be routine to readers thoroughly familiar with [Pit87, See87, Gir86, Wad89]. (Note to specialists: the extension to second order polymorphism differs significantly from second order logical relations proposed by Mitchell and Meyer [MM85]; we shall take this up elsewhere.)

∗jcm@cs.stanford.edu Department of Computer Science, Stanford University, Stanford, CA 94305. Supported in part by an NSF PYI Award, matching funds from Digital Equipment Corporation, the Powell Foundation, and Xerox Corporation; and the Wallace F. and Lucille M. Davis Faculty Scholarship.

†andre@cis.upenn.edu Department of Mathematics, University of Pennsylvania, Philadelphia, PA 19104-6395.

Partially supported by NSF Grant CCR-91-02753 and by ONR Grants N00014-88-K-0635 and N00014-92-J-1916.

It is a pleasure to acknowledge the collaboration with Samson Abramsky and Philip Wadler in the initial stages of this work. We would like to thank John Reynolds for many inspiring discussions of polymorphism.

2 Simple typed lambda calculus

2.1 Types and terms

We will consider typed lambda calculus with terminator (terminal object) 1, product and function types, and any set S of basic types b_{1}, b_{2}, . . .. We will use the symbol “⇒” in function types, and reserve the single arrow “→” for morphisms in a category (including functions between sets). The well-formed terms over any set of types are defined using the subsidiary notion of type assignment. A type assignment Γ is a finite set of formulas x: σ associating types to variables, with no variable x occurring twice. We write Γ, x: σ for the type assignment

Γ, x: σ = Γ ∪ {x: σ},

where, in writing this, we assume that x does not appear in Γ. Terms will be written in the form Γ ▷ M: σ, which may be read, “M has type σ relative to Γ.” The well-formed terms are given by the following rules, where we assume ∗ is a constant symbol of type 1. For simplicity, we will assume that this is the only constant symbol.

(var) x: σ ▷ x: σ

(cst) ∅ ▷ c: σ, c a constant of type σ

(⇒ E)  \frac{Γ ▷ M: σ ⇒ τ, Γ ▷ N: σ}{Γ ▷ MN: τ}

(⇒ I)  \frac{Γ, x: σ ▷ M: τ}{Γ ▷ λx: σ.M: σ ⇒ τ}

(× E)  \frac{Γ ▷ M: σ × τ}{Γ ▷ Proj_{1}^{σ,τ} M: σ, Γ ▷ Proj_{2}^{σ,τ} M: τ}

(× I)  \frac{Γ ▷ M: σ, Γ ▷ N: τ}{Γ ▷ ⟨M, N⟩: σ × τ}

(add hyp)  \frac{Γ ▷ M: τ}{Γ, x: σ ▷ M: τ}

2.2 Equations

Given our formulation of terms, it is natural to write equations in the form

Γ ▷ M = N : τ

where we assume that Γ ▷ M: τ and Γ ▷ N: τ. The equational axioms and inference rules are as follows.

(one) Γ ▷ x = ∗ : 1 (Proj_{1}) Γ ▷ Proj_{1}⟨M, N⟩ = M : σ (Proj_{2}) Γ ▷ Proj_{2}⟨M, N⟩ = N : τ (Pair) Γ ▷ ⟨Proj_{1} M, Proj_{2} M⟩ = M : σ × τ (α) Γ ▷ λx: σ.M = λy: σ.[y/x]M : σ ⇒ τ, provided y ∉ F V (M) (β) Γ ▷ (λx: σ.M) ·_{σ} N = [N/x]M : τ (η) Γ ▷ λx: σ.(M ·_{σ} x) = M : σ ⇒ τ, provided x ∉ F V (M) (ref ) Γ ▷ M = M : σ

(sym)  \frac{Γ ▷ M = N : σ}{Γ ▷ N = M : σ}
(trans)  \frac{Γ ▷ M = N : σ, Γ ▷ N = P : σ}{Γ ▷ M = P : σ}
(ξ)  \frac{Γ, x: σ ▷ M = N : τ}{Γ ▷ λx: σ.M = λx: σ.N : σ ⇒ τ} .
(μ)  \frac{Γ ▷ M_{1} = M_{2} : σ ⇒ τ, Γ ▷ N_{1} = N_{2} : σ}{Γ ▷ M_{1}N_{1} = M_{2}N_{2} : τ}
(add hyp)  \frac{Γ ▷ M = N : σ}{Γ, x: τ ▷ M = N : σ}

3 Cartesian closed categories

A cartesian closed category (or ccc) is a category with specified terminal object, products and exponentials. This means that a category C is cartesian closed only if the following additional data are provided:

• An object 1 with unique arrow O^{A}: A → 1 for each object A,

• A binary object map × with, for any objects A, B and C, specified arrows Proj_{1}^{A,B}, Proj_{2}^{A,B}, and map ⟨ · , · ⟩_{C,A,B} on arrows such that for every f: C → A and g: C → B, the arrow ⟨f, g⟩_{C,A,B}: C → A × B is the unique h satisfying

[figure: Proj_{1}; Proj_{2}; A; B; f; g; h; A × B; C]

• A binary object map ⇒ with, for any objects A, B and C, a specified arrow App^{A,B} and map Curry^{A,B,C} on arrows such that for every f: A × C → B, the arrow Curry^{A,B,C}(f) is the unique h satisfying

[figure: h × 1_{A}; App; f; B; (A ⇒ B) × A; C × A]

A category C is well-pointed if, for any f, g: A → B, we have f = g iff for every x: 1 → A, we have f ∘ x = g ∘ x. Another phrase for “well-pointed” is generated by 1.

Functors that preserve cartesian closed structure will play an important role in our discussion. A representation of cartesian closed categories (or simply ccc-representation) is a functor F: C ⟶ D from one cartesian closed category to another that preserves terminator, products and exponentials (function spaces). In the literature, ccc-representations are sometimes called cartesian closed functors, or cc-functors.

4 Sconing

Let C be a category with a terminator (terminal object) 1. We will define a functor | · | from C to Set, the category of sets and functions, which associates to each object its set of global elements. For any object A in C, let |A| be the set of all morphisms 1 → A in C. For any morphism x: A → A′ in C let |x|: |A| → |A′| be the function defined by composition, according to the following diagram.

[figure: 1; A′; x; A]

It is not hard to see that the functor | · | from C to Set preserves products. The functor also preserves equalizers, but we shall not use this fact.

The category Ĉ, called the scone of C, is defined as follows. The objects of Ĉ are triples ⟨S, f, A⟩, where S is a set, A is an object of C , and f: S → |A| is a function (in Set). The morphisms ⟨S, f, A⟩ →⟨S′, f′, A′⟩ in Ĉ are pairs ⟨t, x⟩, where t: S → S′ is a function and x: A → A′ is a morphism in C such that:

S  t  S′ |A|  |x|  |A′|f′ f

The reader may easily verify that ⟨|1|, id, 1⟩ is a terminator in Ĉ. There is a canonical “forgetful” functor π: Ĉ ⟶ C which takes ⟨S, f, A⟩ to A and ⟨t, x⟩ to x. Category theorists will recognize the scone as a special case of a comma category, namely Ĉ = (id ↓ | · |), where id is the identity functor on Set; see, e.g. , [McL71]. It is common to overload notation and use the symbol Set for the identity functor from sets to sets (and similarly for other categories). With this convention, we may write Ĉ = (Set ↓ | · |).

An illustrative first example is the scone of a partially ordered set C with a top element top. In this case, Ĉ is again partially ordered, with a “new” element (indicated by ∗ below) just below top.

[figure: top; C; ∗; top; Ĉ]

A remarkable feature of sconing in general is that it preserves almost any additional categorical structure that C might have. For further discussion, see [FrS90], for example. The sconing construction is also discussed in [LS86] and [ScS82], where Ĉ is called the Freyd cover of C. We will be concerned with sconing and cartesian closed structure.

Proposition 4.1 If C is a cartesian closed category, then Ĉ is cartesian closed and the canonical functor Ĉ ⟶ C is a representation of cartesian closed categories.

Proof. Let X = ⟨S, f, A⟩ and Y = ⟨S′, f′, A′⟩ be objects of Ĉ. Then the object

X × Y = ⟨S × S′, f × f′, A × A′⟩,

is a product of X and Y, where (f × f′)⟨s, s′⟩ = ⟨f(s), f′(s′)⟩. An exponential of X and Y (an object of functions from X to Y) is given by

X ⇒ Y = ⟨M, h, A ⇒ A′⟩,

where M is the set of morphisms X → Y in Ĉ and h(⟨t, x⟩): 1 → A ⇒ A′ is the morphism in C obtained from x: A → A′ by currying.

In order to make a connection with logical predicates and logical relations described e.g. in [Mit90], we will be interested in a subcategory C̃ of the scone which we call the subscone of C. The objects of the subscone C̃ are the triples ⟨S, f, A⟩ with f: S ↪ |A| an inclusion of sets. The morphisms ⟨S, f, A⟩ →⟨S′, f′, A′⟩ of C̃ are the same as for Ĉ, so C̃ is a full subcategory of Ĉ. Notice, however, that if ⟨t, x⟩ is a morphism in C̃, then the set function t: S → S′ is uniquely determined by x and S. Specifically, t is the restriction of |x| to S. The subcategory C̃ inherits (an isomorphic copy of) the cartesian closed structure of Ĉ. More precisely, C̃ is isomorphic to a full sub-cartesian-closed category of Ĉ. The reader may enjoy constructing exponentials in the subscone. In Section 4.1, we will work out the special case where C is a product of two ccc’s.

It is category-theoretic folklore that Proposition 4.1 (and its proof) extend to a more general setting with Set replaced by any cartesian closed category C′ with equalizers and the functor | · |: C ⟶ Set replaced by any functor F: C ⟶ C′ that preserves products. This generalization takes us from the specific comma category Ĉ = (Set ↓ | · |) to a more general case of the form (C′ ↓ F), see [Laf88, MaR92].

Proposition 4.2 Let C and C′ be cartesian closed categories and assume C′ has equalizers. Let F: C ⟶ C′ be a functor that preserves products. Then the comma category (C′ ↓ F) is a cartesian closed category and the canonical functor (C′ ↓ F) ⟶ C is a representation of cartesian closed categories.

4.1 A special case: sconing with relations

An illuminating case is the scone of a product category. Let us consider a product category C = A × B, where both categories A and B have a terminator. We remind the reader that the objects of A × B are ordered pairs of objects from A and B and the morphisms ⟨A, B⟩ →⟨A′, B′⟩ are pairs ⟨x, y⟩, where x: A → A′ is a morphism in A and y: B → B′ is a morphism in B . When A and B are cartesian closed, so is A × B, with coordinatewise cartesian closed structure. A terminator of A × B is ⟨1, 1⟩. It is easy to see that |⟨A, B⟩|C = |A|A × |B|B, where the cartesian product of |A|A and |B|B is taken in sets. We will often omit the subscripts from various | · |’s, since these are generally clear from context. We will focus on the scone of product categories for the rest of this section.

The objects of the scone Â×B may be described as tuples ⟨S, f, g, A, B⟩ , with S a set, A an object in A, B an object in B, and f and g functions that form a so-called span:

[figure: S; g; f; |A|; |B|]

The morphisms ⟨S, f, g, A, B⟩ →⟨S′, f′, g′, A′, B′⟩ in Â×B may be described as tuples ⟨t, x, y⟩ , with x: A → A′ a morphism in A, y: B → B′ a morphism in B, and t: S → S′ a function such that:

[figure: |A|; |x|; |A′|; f; g; f′; g′; |B|; |y|; |B′|; S; t; S′]

Morphisms in the scone of a product category resemble transformations of structors, described in [Fre92].

Let us now concentrate on the subcategory Ã×B of Â×B. Working through the definition of Ã×B, we may regard the the objects of this subcategory as tuples ⟨S, f, g, A, B⟩, where f and g are the coordinate functions of an inclusion S ↪ |A| × |B|. In other words, since S, f and g determine a subset of |A| × |B|, an object ⟨S, f, g, A, B⟩ is essentially an ordinary binary relation on |A| × |B|. We will therefore simplify notation and suppress the coordinate functions f and g. We will write S: |A| − ×|B| to indicate that S is a binary relation on |A| × |B|. This notation makes it possible to express properties of relations using diagrams instead of formulas. As noted above, for morphisms ⟨t, x, y⟩ between objects of Ã×B, the set map t is uniquely determined by A and B maps x and y, and the relation S. Specifically, t is the restriction of |x| × |y| to S. Omitting the redundant set map, the definition of morphism has an appealing diagramatic presentation as a pair ⟨x, y⟩ satisfying:

|A|  |x|  |A′| |B|  |y|  |B′| S′ S  ⊆

The “⊆” in this diagram means that the relation |y| ∘ S is included in the relation S′ ∘ |x|. It is readily seen that this condition, expressible as a universal Horn clause, states exactly that for all morphisms a: 1 → A in A and b: 1 → B in B :

a S b implies (x ∘ a) S′ (y ∘ b),

where we use relational notation a S b to indicate that S relates a to b , and similarly for S′.

It is instructive to write out the exponentials (function spaces) in the cartesian closed category Ã×B. Supressing the coordinates of inclusions, ⟨S, A, B⟩ ⇒⟨S′, A′, B′⟩ is given by ⟨R, A ⇒ A′, B ⇒ B′⟩ , where R: |A ⇒ A′| −×|B ⇒ B′| is the binary relation such that for all morphisms e: 1 → A ⇒ A′ in A and d: 1 → B ⇒ B′ in B :

e R d iff a S b implies App ∘ ⟨e, a⟩ S′ App ∘ ⟨d, b⟩
for all a: 1 → A in A, b: 1 → B in B.

We may also write out products in a similar fashion. Because C̃ is isomorphic to a sub-cartesian-closed category of Ĉ, the restriction of the forgetful representation Ĉ → C to C̃ is also a representation. The main properties of Ã×B are summarized in the following proposition, which is easily verified using the ideas presented in the above discussion.

Proposition 4.3 Let C = A × B be the cartesian product of two ccc’s. Then C̃ is a cartesian closed category, with canonical functor C̃ ⟶ C a representation of cartesian closed categories. Furthermore, products and exponentials are given by

⟨S, A, B⟩ × ⟨S′, A′, B′⟩ = ⟨S × S′, A × A′, B × B′⟩,
⟨S, A, B⟩ ⇒⟨S′, A′, B′⟩ = ⟨S ⇒ S′, A ⇒ A′, B ⇒ B′⟩,

where relations S × S′ and S ⇒ S′ have the following characterizations:

a (S × S′) b iff (Proj_{1} ∘ a) S (Proj_{1} ∘ b) and (Proj_{2} ∘ a) S′ (Proj_{2} ∘ b)
e (S ⇒ S′) d iff ∀a: 1 → A. ∀b: 1 → B. a S b implies App ∘ ⟨e, a⟩ S′ App ∘ ⟨d, b⟩.

The descriptions of products and exponentials in this proposition correspond to the definition of logical relations given e.g. in [Mit90].

Note that although much of the development uses Set, we do not assume that functors | · |A: A ⟶ Set and | · |B: B ⟶ Set are one-to-one on morphisms. In other words, we do not assume that categories A and B are well-pointed (generated by 1). In the argument above, we are simply using the one-to-one correspondence between the morphisms C → C′ and the morphisms 1 → C ⇒ C′, which holds in any cartesian closed category. In the special case of well-pointed cartesian closed categories, we may compare sconing to logical relations for Henkin models of simply typed lambda calculus (see [Sta85, Mit90]). We shall presently do so in the next section.

We conclude this section with a “binary version” of a general sconing framework given by means of comma categories in Proposition 4.2. This binary version (as well as the k-ary version) can be obtained from Proposition 4.2 itself.

Proposition 4.4 Let A, B, and C′ be cartesian closed categories and assume C′ has equalizers. Let F: A ⟶ C′ and G: B ⟶ C′ be functors that preserve finite products. Let H: A×B ⟶ C′ be the functor given by H(A, B) = F(A)×G(B) , and likewise on morphisms. Then the comma category (C′ ↓ H) is a cartesian closed category and the canonical functor (C′ ↓ H) ⟶ A × B is a representation of cartesian closed categories.

5 Sconing and Logical Relations

In this section, we will describe the connection between the subscone and the so-called logical relations over Henkin models. We rely on the basic correspondence between well-pointed ccc’s and Henkin models described, e.g. in [LS86, MS89]. Logical relations are discussed e.g. in [Sta85, Mit90]. Specifically, if C is the cartesian closed category determined by a Henkin model A, then the logical predicates over A have a direct correspondence with the ccc-representations from a free cartesian closed category into the subscone of C. Since binary relations are often more intuitive than predicates, we will continue to illustrate the main ideas using binary relations. We will begin by reviewing the free cartesian closed category over some set of types.

For any set S of basic types, there is a free cartesian closed category F[S] generated by S. The objects of the category F[S] are types built from the basic types in S and the morphisms A → B are β, η-equivalence classes of lambda terms of type B with exactly one free variable of type A. The freeness of F[S] means that for any assignment S → D mapping the basic types in S to objects of D there is a unique representation of cartesian closed categories such that

[figure: D; F[S]; S]

where the map S → F[S] is the inclusion of S into the set of objects of F[S]. The representation of F[S] into D is the categorical equivalent of a meaning function A[[ ·]] associated with a Henkin model A. Since a representation is a functor that preserves cartesian closed structure, this representation gives both a map from simple types over S to objects of C̃ and a map from of simply typed lambda terms to morphisms of C̃. Moreover, these functions together preserve all typing and equational rules of simply typed lambda calculus. One difference between the Henkin model and categorical settings is that we usually consider the mapping from type expressions to sets σ ↦ A^{σ} part of the Henkin model A, whereas the associations of basic types to objects is not part of a cartesian closed category (hence the dependence on a function S → D). Additional discussion and details may be found in [LS86, MS89] and elsewhere.

Since the subscone C̃ is a cartesian closed category, any assignment of basic types S to objects of C̃ determines a representation from F[S] to C̃. For product categories, if A and B are given by Henkin models A and B of simply typed lambda calculus, then C = A × B and C̃ are again well-pointed cartesian closed categories. A mapping from simple types to objects of C̃, as mentioned above, is a type-indexed family of relations R^{σ} ⊆ A^{σ} × B^{σ} between the Henkin models. It is easy to see from Proposition 4.3 that the family of relations determined by the object map of a representation F[S] → C̃ is in fact a logical relation.

Proposition 5.1 Let A and B be well-pointed cartesian closed categories and let A and B be the corresponding Henkin models of simply typed lambda calculus. Then logical relations on A × B are exactly the object parts of representations of the free cartesian closed category (on a given set of generators) in the cartesian closed category Ã×B.

This correspondence and the Basic Lemma for logical relations, c.f. e.g. [Mit90] , are consequences of a straightforward diagram, given in the following proposition.

Proposition 5.2 Let S be a set of basic types (symbols), let C be a cartesian closed category, and consider any mapping S → C̃ from basic types to objects of the subscone of C. Composing with the canonical functor C̃ → C, we obtain a corresponding map S → C. Given these two maps from S, and the injection of S into the types of the free ccc F[S] over S, there exist unique ccc representations commuting with the canonical functor C̃ → C as follows:

[figure: C; C̃; S; F[S]]

Proof. Let functions from S to objects of the ccc’s C, C̃ and F[S] be given as in the statement of the theorem. It is a trivial consequence of the definitions that the triangle involving S, C̃ and C commutes. By the freeness of F[S], the representations F[S] → C and F[S] → C̃ are uniquely determined. This implies that the two triangles with vertices S, F[S] and either C̃ or C commute. Finally, since the canonical functor C̃ → C is a ccc-representation (see Proposition 4.3), the two uniquely determined representations of F[S] must commute with this functor.

The Basic Lemma follows from this diagram. Indeed, let us consider the special case that A and B are given by Henkin models A and B of simply typed lambda calculus. Then both C = A × B and C̃ are well-pointed cartesian closed categories. The representation F[S] → C maps a typed lambda term x: σ ▷ M: τ to the pair of morphisms giving the meaning of M in A as a function of x and, respectively, the meaning of M in B. The representation F[S] → C maps a typed lambda term x: σ ▷ M: τ to a morphism from some subset S ⊆ σA × σB to a subset S′ ⊆ τA × τB, where σA is the object of A given by type expression σ over basic types S, according to the chosen map S → C (= A × B), and similarly for the other subscripted type expressions. As noted in Section 4.1, such a morphism in the subscone is a product map f × g with f: σA → τA and g: σB → τB which maps a pair ⟨u, v⟩ with u S v to a pair ⟨f(u), f(v)⟩ with f(u) S′ g(v). Since the two representations of F[S] commute with the forgetful functor C̃ → C, f must be the meaning f = A[[x: σ ▷ M: τ]] of the term M in A, regarded as a function of the free variable x, and similarly g = B[[x: σ ▷ M: τ]]. Since the term x: σ ▷ M: τ was arbitrary, and σ may be a cartesian product of any types, we have shown that given logically related interpretations of the free variables, the meaning of any term in A is logically related to the meaning of this term in B. This is precisely the Basic Lemma for logical relations over Henkin models.

6 Generalizations of sconing

In Section 4, we noted that to the scone Ĉ = (Set ↓ | · |) defined using Set may be generalized to certain comma categories, see Proposition 4.2. Thus we also obtain the following generalization of Proposition 5.2:

Proposition 6.1 Let C and C′ be cartesian closed categories and assume C′ has equalizers. Let F: C ⟶ C′ be a functor that preserves products and let D be a sub-cartesian-closed category of the comma category (C′ ↓ F). Let S be a set of basic types (symbols), and consider any mapping S → D from basic types to objects of D. Composing with the canonical forgetful functor D → C, we obtain a corresponding map S → C. Given these two maps from S, and the injection of S into the types of the free ccc F[S] over S, there exist unique ccc representations commuting with the canonical functor D → C as follows:

[figure: C; D; S; F[S]]

We remind the reader of the binary version given in Proposition 4.4. In the present setting that would yield the above diagram with A × B instead of C.

In this section we compare this straightforward categorical generalization with three forms of logical relations that have already appeared in the literature, Kripke logical relations [Plo80, MM91], cpo logical relations [MS76, Rey74], and the relational setting over PER models used in section 4 of [BFS90]. These cases are still “concrete” enough so that it makes sense to consider an analogue of a subscone, a certain sub-ccc of a comma category consisting of those objects for which relevant mappings are given by inclusions. Hence in these cases we will be able to assume that the objects of the category D from Proposition 6.1 also have this form.

6.1 Sconing with Kripke models

Let P be a partially ordered set. P may be considered as a category whose objects are the elements of P, and where for each p, p′ in P there is at most one morphism p → p′, which exists iff p ≤ p′ in P. It is shown in Section 4 of [MM91] that each Kripke lambda model with P as the set of “possible worlds” determines a cartesian closed category C and a finite product preserving functor F from C to the functor category Set^{P}. (The functor F need not be a cccrepresentation. Furthermore, any ccc is equivalent as a category to a ccc arising this way, see [MM91]. This framework covers the case when C arises from an ordinary Henkin model, see our Section 5. Indeed, we let F(C) for each object C of C be the constant functor P → Set whose value is the domain set in the given Henkin model that corresponds to C.)

Let D be the full subcategory of the comma category (Set^{P} ↓ F) that consists of objects ⟨S, f, A⟩ with f_{p}: S(p) ↪ F(A)(p) an inclusion for each p in P. We may conveniently omit f when referring to objects of D. D is a sub-ccc of (Set^{P} ↓ F). In describing exponentials (i.e., function spaces) in D we may use natural transformations F(app_{A,A′}): F(A ⇒ A′) × F(A) ⟶ F(A′) because the functor F preserves binary products. For each object C in C and each p ≤ p′ in P, we also use the transition function F(C)(p ≤ p′): F(C)(p) → F(C)(p′) given by the action of the functor F(C): P → Set on the order of P. Specifically, ⟨S, A⟩ ⇒⟨S′, A′⟩ may be given as ⟨P, A ⇒ A′⟩, where A ⇒ A′ is taken in C and P: P → Set is the functor such that the set P (p) consists of all t in F(A ⇒ A′)(p) for which for all p′ ≥ p and all a in F(A)(p′), if a belongs to S(p′), then the element F(app_{A,A′})_{p′}(F(A ⇒ A′)(p ≤ p′)(t), a) in F(A′)(p′) belongs to S′(p′). In other words, the object parts of the free ccc-representations in D considered in Proposition 6.1 in this case amount to, in the terminology of [MM91], the Kripke logical predicates on the Kripke lambda model that corresponds to F.

In the binary case, let A and B be cartesian closed categories and F: A → Set^{P} and G: A → Set^{P} finite product preserving functors given, e.g. by Kripke lambda models A and B, each with P as the poset of possible worlds). Let H: A × B → Set^{P} be the functor given by H(A, B) = F(A) × G(B). One now continues as above, with C = A × B and with H instead of F. In this case the object parts of the free ccc-representations in D considered in Proposition 6.1 are exactly the Kripke logical relations on Kripke lambda models A and B.

6.2 Sconing with cpo domains

Let Cpo be the category whose objects are posets with suprema of countably infinite chains, i.e., cpos, and whose morphisms are monotone maps that preserve suprema of countably infinite chains, i.e., continuous maps. Cpo is a cartesian closed category with equalizers. Finite products and equalizers are given as in Set, and P ⇒ Q consists of all continuous maps P → Q, with pointwise order. Let P cpo be the full subcategory of Cpo whose objects are pointed cpos, i.e., cpos with the least element, usually denoted ⊥. Because P ⇒ Q as given in Cpo is pointed if Q is pointed, with ⊥ in P ⇒ Q being the constant function with value ⊥ in Q, P cpo is a sub-ccc of Cpo. We shall denote the inclusion functor by I.

While in P cpo one loses equalizers, one is compensated by gaining, for each object P, a canonical morphism fix_{P}: (P ⇒ P) → P that yields fixed-points. If f is an element of (P ⇒ P) given by a continuous map P → P, then fix_{P} (f) is the least fixed-point of f, given by fix_{P} (f) = ⋁{f^{n}(⊥)}. Thus the ccc P cpo has the property that for each object P, there exists a canonical morphism fix_{P}: (P ⇒ P) → P such that for every morphism f targeted at P ⇒ P , the morphism p = fix_{P} ∘ f targeted at P satisfies app ∘ ⟨f, fix_{P} ∘ f⟩ = fix_{P} ∘ f.

A ccc with this property may be called a ccc with fixed-point operators. For any such ccc C, the free ccc-representation F[S] ⟶ C (induced, as always, by a mapping S ⟶ C that interprets basic types in C) factors through the free ccc with fixed-points on the given collection S of basic types. This latter category F_{fix}[S] is the term category of simply typed lambda calculus (on the given collection S of basic types) with a constant fix_{σ} of type (σ ⇒ σ) ⇒ σ for each type σ, for which we impose

Γ ▷ M(fix_{σ}M) = fix_{σ}M : σ.

In addition, the ccc-representation F_{fix}[S] ⟶ C involved in the factorization of F[S] ⟶ C also preserves the canonical fixed-point operators.

Let us consider the full sub-ccc of the comma category (Cpo ↓ I) whose objects are of the form ⟨P, f, A⟩, where f is the inclusion P ↪ A. In other words, P is a sub-cpo of pcpo A. Yet another equivalent description is that P is an inductive predicate on A in the sense that P is monotone in A and for any chain Q in A, if Q ⊆ P , then ⋁ Q ∈ P. We omit f when referring to these objects. In this full sub-ccc the exponentials, i.e., function spaces ⟨P, A⟩ ⇒⟨P′, A′⟩ may be described as ⟨R, A ⇒ A′⟩, where A ⇒ A′ is taken in Cpo, i.e., it is the cpo of continuous functions g: A → A′ ordered pointwise, and where R consists of all such g for which g(a) ∈ P′ whenever a ∈ P. The object parts of free ccc-representations in this sub-ccc of (Cpo ↓ I) are exactly inductive logical predicates.

It is also useful to consider a further sub-ccc D whose objects are of the form < P, A >, where P ↪ A is a sub-pcpo, i.e., in addition to being inductive, P is also strict in the sense that ⊥_{A}∈ P. The ccc structure is still the same, but in D we also get canonical fixed-point operators, and the forgetful ccc-representation D → P cpo preserves them. The object parts of free ccc-representations in D are exactly strict, inductive logical predicates. As we observed above, each such ccc-representation can be lifted to a free ccc-representation that preserves fixed-point operators. In the binary case, so we let H(A, B) = A × B and we consider D be the full sub-ccc of (Cpo × Cpo ↓ H) whose objects are of the form ⟨S, A, B⟩, where S is a sub-pcpo of pcpo A × B, i.e., S is a strict, inductive relation from A to B,

It is immediate to generalize this entire discussion from chains to directed families. Furthermore, it would be instructive to work out a treatment of sconing with cpos from the point of view of computational monads [Mgg89].

6.3 Sconing with partial equivalence relations

Let P er be the category whose objects are partial equivalence relations (i.e., symmetric, transitive relations) on natural numbers, and whose morphisms R → S are equivalence classes of partial recursive functions f that are defined on the domain of R and that preserve R in the sense that whenever n R k, then n S k. Two such partial recursive functions f, f′ are considered equivalent iff whenever n R k, then f(n) S f′(k) . It is folklore that P er is a ccc. The “indiscriminate” relation that relates any two numbers serves as a terminal object. Given a computable pairing function, the product R × S may be described as relating < n, k > and < n′, k′ > iff n R n′ and k S k′. Given a gödelnumbering of partial recursive functions, R ⇒ S may be described as relating e and e′ iff e and e′ are gödelnumbers of partial recursive functions that represent per morphisms R → S and are equivalent as such.

Let I be the identity functor on P er. Let D be the full sub-ccc of the comma category (P er ↓ I) of objects ⟨S, f, A⟩ , where f is named by the identity function on the natural numbers, and where S is saturated in A in the sense that S = A ∘ S ∘ A as binary relations on natural numbers (i.e., S is a restriction of A to a subset of the domain of A that is a union of A-equivalence classes), see Section 4 of [BFS90]. We omit f when referring to objects of D. It is readily verified that ⟨S, A⟩ ⇒⟨S′, A′⟩ in D is given by ⟨R, A ⇒ A′⟩, where the right component is as in P er, and where e R e′ iff e A ⇒ A′ e′ and the partial recursive functions with gödelnumbers e and e′ also represent per morphisms S → S′ and are equal as such.

In the binary case the relevant comma category is (P er × P er ↓ H), where H is the binary product functor in P er. The objects of the relevant full sub-ccc may be presented in the form ⟨S, A, B⟩, where S is an ordinary relation from the domain of A to the domain of B subject to the saturation condition S = A ∘ S ∘ B , see Section 4 in [BFS90]. The ccc structure may be described as above.

7 Implicit polymorphism

In this section we turn our attention to a slight extension of simply typed lambda calculus. Syntactically, the language λ^{→,t} we consider is still very close to simply typed lambda calculus. The only difference is that types may contain type variables as well as basic type symbols. However, our interest in λ^{→,t} lies in the fact that the terms of the calculus depend on type variables, and therefore we have a simple form of polymorphism. We will refer to this as “implicit” polymorphism since the quantification over type variables is implicit, rather than explicit.

Given a cartesian closed category C, let Obj C be the set (or class) of objects of C. As with any set (or class), Obj C may be considered as a discrete category, the only morphisms of which are the identities. We may interpret the types of λ^{→,t} as functors from Obj C to C, and terms as natural transformations. Note that to interpret types with n type variables, we need functors (Obj C)^{n} → C, and so the interpretation naturally involves a different category for each set (or number of) type variables. The reader will note that the functors (Obj C)^{n} → C are basically just n-ary functions from the set (or class) Obj C to Obj C. In order to account for type substitution, these functor categories must “fit together” as n varies. A proper general categorical framework for this motivating example is based on indexed or fibred categories, see [See87, Pit87, Mog91]. This framework, discussed below, generalizes readily to explicit polymorphism. In addition, a special case of this categorical view is a construction on Henkin models described, e.g. , in [Mit90].

7.1 Categorical models of implicit polymorphism

If we consider the type expressions apart from lambda terms, we have an “algebraic” language with type constants (basic types), variables, and the binary operation ⇒. We may regard any such language as an “algebraic theory,” in Lawvere’s terminology, or a category with a terminator, binary products, and a distinguished object representing the carrier of the algebra. For definiteness, we will assume a “base” category B with distinguished object V which generates B, in the sense that each object is a finite power V^{n} for some natural number n. This gives us the terminator as V^{0}. Intuitively, the arrows V^{i} → V^{j} in B may be regarded as j-tuples of type expressions, each having all type variables among t_{1}, …, t_{i}. Composition in B corresponds to substitution of types for type variables. This relatively standard interpretation of an algebraic language is explained in [KR77], for example. It is helpful to note that we may regard an arrow V^{i} → V^{j} as either a j-tuple of types, or a context Γ = {x_{1}: τ_{1}, …, x_{j}: τ_{j}} of length j, with all type expressions over the same set of i type variables.

We now consider the interpretation of terms. For each finite set of type variables, λ^{→,t} includes all simply typed terms over these variables, regarded as basic types. Therefore, we expect a categorical interpretation to provide a ccc for each finite number of type variables. More specifically, if we regard a morphism g: V^{i} → V of B as a context {x: τ}, we would expect to have some kind of assignment “from” g for each term {x: τ} ▷ M: σ. We may use the type variable structure of B to index categories of types and terms. We assume that for each object V^{i} in B, there is a category F_{i} whose objects correspond to type expressions with i type variables and morphisms represent terms of these types. This assignment is assumed to be functorial in i, i.e., F is a (contravariant) functor to Cat, the category of categories. The structure of B is linked to F_{i} by assuming that objects of F_{i} are the same as morphims V^{i} → V in B. Similar indexed categories may be found in [See83, See87, Pit87, Mog91].

Definition 7.1 An iml-category is given by:

• a base category B with finite products, generated by some distinguished object V,

• a functor F: B^{op} ⟶ Cat such that:

– for each object I in B, the category F(I) is cartesian closed,

– for each morphism f: I → J in B, the functor F(f): F(J) → F(I) is a ccc representation,

– for each object I in B, the class of objects Obj (F(I)) is the same as the class of morphisms I → V in B,

– for each morphism f: I → J in B, F(f) acts on objects by composition.

This definition may be rephrased by means of the category Class of classes and mappings and the category Ccc of cartesian closed categories and representations thereof. In particular, a base category B with finite products generated by some distinguished object V and a functor F: B^{op} ⟶ Ccc such that the functor Obj ∘ F: B^{op} ⟶ Class is the representable functor B( · , V). Here Obj: Ccc ⟶ Class is the forgetful functor that takes a ccc to its underlying set (or class) of objects and a ccc representation to the associated object map. (Probably the most expedient way of dealing with the question of a set vs. a class of objects is to regard “smallness” as relative to each example.) Let us also observe that following [Pit87, Mog91], we use a tighter definition of indexed categories than usual in category theory; we are asking for data up to equality rather than just up to canonical isomorphisms.

Since the objects of B have the form U^{n} for some natural number n, we may identify the objects of B with the natural numbers. This simplifies notation. The category F(n) , which we also write as F_{n} , is often called the fiber over n. Again, the intuition behind this definition is that n stands for a set of n distinct type variables, the objects of F_{n} for type expressions on these type variables, the morphisms of F_{n} for typed terms over these type variables, and F(f) for type substitution. This intuition may be made precise by defining a term iml-category for each λ^{→,t} language and theory, analogously to [See87, Pit87].

Example 7.2 Given any ccc C, we may construct an iml-category C_{iml} as follows. We let the base category B have natural numbers as objects, and let the morphisms i → j be functors (Obj C)^{i} → (Obj C)^{j}. Fiber F_{n} over n is the functor category (Obj C)^{n} → C. We emphasize that these functors are basically just functions from n-tuples of objects to objects, and therefore the ccc structure of F_{n} is in this example given pointwise by the ccc structure of C. For instance, (F ⇒ G)(A) = F (A) ⇒ G(A). Finally, if H: m → n is a morphism of the base category, and therefore a functor (Obj C)^{m} → (Obj C)^{n}, we define the functor F(H): F_{n} → F_{m} by composition with H. More precisely, F(H): F_{n} → F_{m} takes a morphism t: F → G of the fiber F_{n} to the morphism (t ∘ H): F ∘ H → G ∘ H of the fiber F_{m}, where for any m-tuple A of objects of C (t ∘ H)_{A} = t_{H(A)}. It is easy to check that F(H): F_{n} → F_{m} is a ccc representation. We thus see that C_{iml} is an iml-category for any cartesian closed category C.

Example 7.3 A more subtle example of an iml-category may be found in the setting used in [Gir86]. Consider the category Qd_{emb} of qualitative domains and embedding-projection pairs. This is not a cartesian closed category. Let the morphisms k → n of the base category B be n-tuples of functors (Qd_{emb})^{k} ⟶ Qd_{emb} that preserve pullbacks and directed colimits. The fiber F_{n} is the ccc whose objects are functors (Qd_{emb})^{n} ⟶ Qd_{emb} that preserve pullbacks and directed colimits, i.e., variable types, in the terminology of [Gir86]. The morphisms t: F → G of the fiber F_{n} are certain “stable” families of stable maps t_{P}: F (P) → G(P), where P ranges over n-tuples of qualitative domains, i.e., in the terminology of [Gir86], objects of variable type F ⇒ G. Here (F ⇒ G)(P) = F (P) ⇒ G(P), the latter in the sense of the ccc Qd of qualitative domains and stable maps. The action of F ⇒ G on embeddings is explained in [Gir86]. If H: k → n is a morphism in the base category B, then the ccc-representation F(H): F_{n} → F_{k} takes a morphism t: F → G of the fiber F_{n} to the morphism (t ∘ H): F ∘ H → G ∘ H of the fiber F_{k}, where for any k-tuple Q of qualitative domains (t ∘ H)_{Q} = t_{H(Q)}.

Example 7.4 Let us now describe the iml-category P ER. We recall the category P er of pers and per morphisms discussed in Section 6.3. Let the morphisms k → n of the base category be n-tuples of maps in k arguments from pers to pers. The fiber F_{n} is a ccc whose objects are maps in n arguments from pers to pers, and whose morphisms t: F → G are “realizable” families of per morphisms t_{P}: F (P) → G(P), where P ranges over n-tuples of pers, given by a single partial recursive function that names each per morphism t_{P}. Two partial recursive functions name the same realizable family of per morphisms t_{P}: F (P) → G(P) iff they name the same per morphism t_{P} for each n-tuple P of pers. If H: k → n is a morphism in the base category, then the cccrepresentation F(H): F_{n} → F_{k} takes a morphism t: F → G of the fiber F_{n} to the morphism (t ∘ H): F ∘ H → G ∘ H of the fiber F_{k}, where for any k-tuple Q of pers (t ∘ H)_{Q} = t_{H(Q)}.

So far we have defined iml-categories and discussed several examples. Let us now define iml-representations:

Definition 7.5 Let (B, F), (B′, F′) be iml-categories. An iml-representation (B, F) ⟶ (B′, F′) is given by:

• a functor T: B → B′ that preserves finite products so that T (n) = n, together with

• a natural transformation t: F ⟶ (F′ ∘ T) such that for each n, the functor t_{n}: F_{n} → F′_{n} is a ccc-representation,

such that for any morphism H: n → 1 in B, the morphism T (H): n → 1 in B′ is the object t_{n}(H) in the fiber F′_{n} when H is considered as an object in the fiber F_{n} .

A special case of this definition is when an iml-category (B, F) is a sub-iml-category of an iml-category (B′, F′) in the sense that base category B is a subcategory of base category (B′, (the objects of either are natural numbers), for each n the fiber F_{n} is a sub-ccc of the fiber F′_{n}, and for each morphism H: k → n the ccc-representation F(H): F_{n} → F_{k} is a restriction of the ccc-representation F′(H): F′_{n} → F′_{k} . For instance, the iml-category P ER described in Example 7.4 is a sub-iml-category of P er_{iml}.

Let (B, F) be any iml-category. The intuitive motivation, mentioned above, that relates morphisms of B to types of λ^{→,t} of and morphisms of fibers to terms of λ^{→,t} can now be restated in a precise way. For any iml-category (B, F) there is a unique iml-representation from the term iml-category (see above) to (B, F) that extends a given assignment of objects of the fiber F0 to basic type symbols. In other words, the term iml-category on the given set S of basic type symbols is the free iml-category on S. Indeed, for each n, types and terms with n type variables are mapped to the objects and morphisms of the fiber F_{n}, respectively, by the unique ccc-representation of the free ccc in the ccc F_{n}. These ccc-representations commute with type substitution.

On the other hand, while it may seem at first that for any ccc C the canonical cccrepresentation C̃ → C naturally induces an iml-representation (C̃)_{iml} → C_{iml}, a second thought reveals a problem already for fibers over 1: what would be t1 in the setting of Definition 7.5 ? In order to address this problem, we turn our attention to relators.

7.2 Relators

Two of the main concepts discussed in this paper are relators and relator transformations. These concepts and their basic properties will be derived in Section 7.3 by a combination of sconing and the construction described in Example 7.2. Nevertheless, let us first spell out a concrete presentation of relators and relator transformations, not necessarily in most general terms. As with logical relations and sconing for simply typed lambda calculus, binary relators seem to give the most intuitive and visual picture of the general case.

Definition 7.6 Let C, D be categories with terminators. A (binary) relator from C to D consists of:

• an object map F: Obj C ⟶ Obj D, together with

• a mapping that to any binary relation S: |A| − ×|B| associates a binary relation S′: |F (A)| − ×|F (B)| .

The more general case of a binary relator of n arguments is defined similarly, using C^{n} in place of C as the domain. In other words, a binary relator of n arguments from C to D consists of an object map F: (Obj C)^{n} ⟶ Obj D, together with a mapping that to any n-tuple of binary relations S_{i}: |A_{i}| − ×|B_{i}| , where i = 1, …, n, associates a binary relation S′: |F (A_{1}, …, A_{n})| − ×|F (B_{1}, …, B_{n})| . Even more generally, k-ary relators take k-ary relations to k-ary relations. Further generalizations will be considered in Section 7.3. When C = D we shall speak of relators on C.

Note. In [AbJ91] a relator is also required to map identity relations to identity relations. This stricter notion also fits in our framework, see Example 7.10.

Definition 7.7 Let F, G be relators from C to D. A relator transformation from F to G is a family of morphisms t_{A}: F (A) → G(A) in D , with A ranging over the objects of C , such that for each binary relation S: |A| − ×|B|

|F (A)|  |t_{A}|  |G(A)| |F (B)|  |t_{B}|  |G(B)| S′′ S′  ⊆

where S′ and S′′ are the relations assigned to S by F and G, respectively.

We remind the reader that, as in Section 4.1, the “⊆” in this diagram means that the relation |t_{B}| ∘ S′ is included in the relation S′′ ∘ |t_{A}|. It is readily seen that this condition, expressible as a universal Horn clause, states exactly that for all morphisms a: 1 → F (A) and b: 1 → F (B) in D :

a S′ b implies (t_{A} ∘ a) S′′ (t_{B} ∘ b),

where we use relational notation a S′ b to indicate that S′ relates a to b , and similarly for S′′.

These concepts were motivated by work of Wadler [Wad89]. In a modified form (see Example 7.10), they have been applied to the so-called strictness analysis [AbJ91]. We also note that although relators are slightly more general than tabular structors proposed in [Fre92], the Horn clause condition involved in the definition of relator transformations is basically the same as the condition defining transformations of tabular structors given in [Fre92]. Tabular structors map morphisms to relations rather than relations to relations, so the change from tabular structors to relators is required to account for type substitution.

There are three natural notions of composition involving relators and relator transformations. The first one is composition of relators, which corresponds to substitution of types for type variables in types. It is transparent that composing two relators yields a relator. (Tabular structors, on the other hand, do not compose.) Secondly, one has composition of relator transformations, which corresponds to substitution of terms for variables in terms. If t: F → G and u: G → H are relator transformations between relators from C to D, let (u ∘ t) be the family (u ∘ t)_{A} = u_{A} ∘ t_{A} of morphisms in D, with A ranging over the objects of C. It is straightforward to check that this family is a relator transformation from F to H. The third notion of composition corresponds to substitution of types for type variables in terms. If t: F → G is a relator transformation between relators from C to D and if H is a relator from B to C, then consider the family (t ∘ H)_{A} = t_{H(A)} of morphisms in D, where A ranges over the objects of B. It is again readily checked that this is a relator transformation, this time from F ∘ H to G ∘ H.

7.3 Sconing and iml-categories

Let us now return to the problem mentioned at the end of Section 7.1. An interesting application of the iml-category construction described in Example 7.2 arises when C is the scone Ĉ, or the subscone C̃, see Section 4. By Example 7.2, both (Ĉ)_{iml}, and (C̃)_{iml} are iml-categories. We may regard (Ĉ)_{iml} as a kind of “scone” of C_{iml}, and (C̃)_{iml} as a kind of “subscone” of C_{iml} . However, both of these categories are in a sense too generous in the collection of morphisms of the base category. For instance, without restricting our attention to a smaller sub-iml-category than (C̃)_{iml}, we would not have a straightforward forgetful iml-representation of this new imlcategory in C_{iml} itself. The reader will recall that the existence of a ccc-representation of C̃ in C was essential for the sconing method, and particularly in Propositions 5.1 and 5.2.

The problem may be stated more precisely: since even (C̃)_{iml} is constructed using all functions from Obj C̃ to Obj C̃, there may be morphisms in the new base category which do not correspond to functions from Obj C to Obj C. Therefore, given an arbitrary function Φ: Obj C̃ ⟶ Obj C̃, we would like to ensure the existence of a function F: Obj C ⟶ Obj C with

Φ(S, A) = (S′, F (A))

for every object < S, A > of C̃. Notice that if there is such a function on Obj C, it is unique. The equation above can be restated as

Obj C̃  Φ  ^{Obj C̃} Obj C  F  Obj C

where vertical maps are given by the canonical functor that forgets S in < S, A >. When there is a function F with this property, we say that Φ is an extension of F.

A function Φ: Obj C̃ ⟶ Obj C̃ that extends some function F: Obj C ⟶ Obj C is just a (unary) relator on C. In other words, the unary relators on C are object maps on C̃ that extend object maps on the “underlying” category C. Equivalently, a (unary) relator on C consists of an object map F: Obj C ⟶ Obj C, together with a mapping that associates a subset S′ ↪ |F (A)| to any subset S ↪ |A|. The more general notion of a (unary) relator of n arguments may be derived similarly, using C^{n} in place of C in the domain of F and (C̃)^{n} in place of C̃ in the domain of Φ. We thus obtain the unary case of Definition 7.6.

Rather than consider arbitrary natural transformations between (unary) relators on C, we will be interested in natural transformations that “extend” natural transformations of C_{iml}. More precisely, let Φ, Ψ: Obj C̃ ⟶ C̃ be functors from the discrete category Obj C̃ to C̃. While these functors are essentially object maps Obj C̃ ⟶ Obj C̃, the natural transformations between them are families of arbitrary morphisms τ_{(S,A)}: Φ(S, A) → Ψ(S, A) in C̃ , with (S,A) ranging over arbitrary objects of C̃. (These are not the same as natural transformations between functors Obj C̃ ⟶ Obj C̃ into the discrete category.) If Φ, Ψ are relators that extend object maps F, G: Obj C ⟶ Obj C, a natural transformation τ: Φ ⟶ Ψ that extends a (necessarily unique) natural transformation t between the associated functors F, G: Obj C ⟶ C is precisely a relator transformation from Φ to Ψ. It is worth observing that if τ is a relator transformation extending t, then in fact t also determines τ uniquely. (We observed a similar fact in regard to the morphisms in subscones in Section 4.) Therefore, we often say that t is a relator transformation. In other words, if Φ, Ψ are relators on C with object maps F, G: Obj C ⟶ Obj C, a relator transformation t from Φ to Ψ is a family of morphisms t_{A}: F (A) → G(A) in C, with A ranging over arbitrary objects of C, such that for any subset S ↪ |A|, t_{A} induces a (necessarily unique) morphism Φ(S, A) → Ψ(S, A) in C̃.

It can now be easily verified that:

Proposition 7.8 Let D = C̃. The category of (unary) relators of n arguments and relator transformations on a ccc C is a sub-ccc of the fiber F_{n} = D^{(Obj D)^{n}} of the iml-category D_{iml}. Furthermore, let the morphisms k → n of the new base category be n-tuples of relators of k arguments over C. Then the indexed category of relators and relator transformations on a ccc C is a sub-iml-category of D_{iml} and the canonical forgetful functor to C_{iml} is an iml-representation.

We saw in Section 4.1 that the binary case of sconing is an instance of sconing. The notion of binary relator on a ccc C given in Definition 7.6 may be similarly derived from the notion of unary relator just discussed. Notice that it is not sufficient to simply let D be the subscone of C × C and then proceed as in Proposition 7.8 because we would get too many object maps. Indeed, we would get all maps (Obj C)^{2} ⟶ (Obj C)^{2} , whereas for binary relators we need only those maps induced by pairs of maps F′, F′′: Obj C ⟶ Obj C , i.e., those mapping a pair of objects (A, B) to (F′(A), F′′(A)). (In addition, we should restrict further F′ = F′′, but this further restriction can be dealt with naturally, see below.) Here the relevant iml-category is the product iml-category C_{iml} × C_{iml}. In general, the product of two iml-categories is the iml-category whose base category morphisms k → n are pairs of such morphisms from the two given base categories, and whose fiber over n is the ordinary product of the two given fibers over n.

With this in mind, we can revisit the commutative square above but with C̃ replaced by D, where D is the subscone of C × C, and with C replaced by C × C. Moreover, F ranges over objects of the fiber over 1 in the product iml-category C_{iml} × C_{iml}. Such maps Φ: D ⟶ D are given by two object maps F′, F′′: Obj C ⟶ Obj C by the requirement Φ(S, A, B) = (S′, F′(A), F′′(B)). The restriction on transformations follows the unary case: we consider only the families of morphisms Φ(S, A, B) → Ψ(S, A, B) in D, with (S, A, B) ranging over the objects of D, that extend the families of morphisms in C × C given by pairs of morphisms F′(A) → G′(A) , F′′(B) → G′′(B) in C. In this way we obtain a sub-ccc of the fiber over 1 of D_{iml}. Binary relators on C and relator transformations are clearly a further subcategory of this ccc, and as such they inherit the ccc structure.

For n arguments, we consider the analogous commutative square condition, with D^{n} in place of D in the domain of Φ, and with (C × C)^{n} in place of C × C in the domain of F, obtaining a sub-ccc of the fiber over n of D_{iml}. We have constructed an iml-category (with base morphisms given in the obvious way so as to have an iml-category) for which the canonical forgetful functor to C_{iml} × C_{iml} is an iml-representation. Furthermore, binary relators and their transformations form a sub-iml-category of the iml-category we have just constructed. Thus the image of the free iml-representation of the term iml-category in the iml-category we have constructed contains only binary relators, i.e., the free iml-representation factors through the iml-category of binary relators and relator transformations.

Having observed a specialization of Proposition 7.8 to the binary case (k-ary case is analogous), let us also observe that a similar reasoning allows us to generalize Proposition 7.8 along the lines of Proposition 6.1. For this purpose we let D be a sub-cartesian-closed category of the comma category (C′ ↓ F), where C and C′ are cartesian closed categories and C′ has equalizers, and where F: C ⟶ C′ is a functor that preserves finite products. For now let us also assume that the canonical ccc-representation D → C is surjective on objects. (This additional surjectivity condition does hold in interesting cases for Kripke models, cpos, and pers.) Let us reconsider the commutative square given above with this new choice of D in place of C̃. We say that Φ is a (unary) D-relator on C that extends a (necessarily unique) object map F. If Φ, Ψ are D-relators that extend object maps F, G: Obj C ⟶ Obj C, a natural transformation τ: Φ ⟶ Ψ that extends a (necessarily unique) natural transformation t between the associated functors F, G: Obj C ⟶ C is said to be a D-relator transformation from Φ to Ψ. (While in general t does not determines τ , we have already remarked after Proposition 6.1 that Kripke models, cpos, and pers are “concrete” enough so that we may assume that in the objects of D the mapping components are given by inclusions, and hence that t determines τ uniquely.) We obtain:

Proposition 7.9 Let C and C′ be cartesian closed categories, C′ with equalizers. Let F: C ⟶ C′ be a functor that preserves products. Let D be a sub-cartesian-closed category of the comma category (C′ ↓ F), such that the canonical ccc-representation D → C is surjective on objects. Then the category of (unary) D-relators of n arguments and D-relator transformations on a ccc C is a sub-ccc of the fiber F_{n} = D^{(Obj D)^{n}} of the iml-category D_{iml}. Furthermore, let the morphisms k → n of the new base category be n-tuples of D-relators of k arguments over C. Then the indexed category of D-relators and relator transformations on a ccc C is a sub-iml-category of D_{iml} and the canonical forgetful functor to C_{iml} is an iml-representation.

Example 7.10 Let us illustrate the notions involved in Proposition 7.9 in the setting used in [AbJ91] for the purposes of the so-called strictness analysis. In this example C′ is the category Cpo of cpos and continuous maps, C is the full subcategory P cpo of pointed cpos, and F is the inclusion functor I. We concentrate on the binary case, so we let H(A, B) = A × B and we let D be the full subcategory of (Cpo × Cpo ↓ H) whose objects are of the form < S, A, B >, where S is a sub-pcpo of pcpo A × B, i.e., S is a strict, inductive relation from A to B, see Section 6.2. D is a sub-ccc of the comma category and furthermore D is a ccc with fixed-point operators. A binary pcpo-relator on P cpo consists of a mapping F from pcpos to pcpos, together with a mapping that to any strict, inductive relation S: A −×B associates a strict, inductive relation S′: F (A) −×F (B) . If F, G are pcpo-relators on pcpos, a relator transformation from F to G is a family of continuous maps t_{A}: F (A) → G(A), with A ranging over pcpos, such that for each strict, inductive relation S: A −×B and strict, inductive relations S′: F (A) − ×F (B) and S′′: G(A) −×G(B) assigned to S by F and by G, respectively, it is the case that the composite relation t_{B} ∘ S′ is included in the relation S′′ ∘ t_{A}. This condition states exactly that for all elements a in pcpo F (A) and b in pcpo F (B) , a S′ b implies (t_{A}(a)) S′′ (t_{B}(b)). We have described the fiber over 1 in the iml-category of pcpo-relators over P cpo and their transformations, a special case of Proposition 7.9. This iml-category has fixed-point operators in the sense that each fiber is a ccc with fixed-point operators and they are preserved by the cccrepresentations F_{n} → F_{k} induced by morphisms k → n in the base category. Pcpo-relators over P cpo that take identity relations to identity relations form a sub-iml-category with fixed-point operators. Thus the free iml-representation of the λ^{→,t} term iml-category in the iml-category of pcpo-relators over P cpo (determined by an interpretation of basic types in D) factors through the sub-iml-category of pcpo-relators that take identities to identities. Furthermore, since this sub-iml-category also has fixed-point operators, the latter iml-representation factors through the term iml-category of λ^{→,t} with fixed-point operators, as in Section 6.2. Thus the main soundness theorem in [AbJ91] follows.

7.4 Relators over iml-categories

Proposition 7.8 may also be generalized in another way. The reader will notice that in our definition of (unary) relators on a ccc C, the required object maps F: Obj C ⟶ Obj C are exactly the objects of the fiber over 1 in the iml-category C_{iml}, where the fiber over 0 is the ccc C. In other words, we have constructed an iml-category of relators and relator transformations, starting from a particular kind of iml-category, C_{iml} .

However, the construction easily generalizes to arbitrary iml-categories. Let us recall that in any iml-category (B, F), the objects of the fiber F_{n} over n are exactly the morphisms n → 1 in the given base category B. In particular, an object of the fiber F1 is a morphism 1 → 1 in B , and hence it composes in B with any morphism 0 → 1 to produce again a morphism 0 → 1. In this way an object of the fiber F1 induces an object map F: Obj F0 ⟶ Obj F0 . Hence in the more general definition of a relator over an iml-category F it makes sense to consider only those object maps F: Obj F0 ⟶ Obj F0 induced by the objects of the fiber F1 by composition. An object of the fiber F_{n} similarly induces an object map of n arguments on F0 by composition with n-tuples of morphisms 0 → 1 (i.e., with morphisms 0 → n) in B .

Definition 7.11 A (unary) relator of n arguments over an iml-category (B, F) is given by an object A of the fiber F_{n} , together with a (unary) relator of n arguments on F0, whose object map is induced by A by composition.

Relator transformations over an iml-category (B, F) may be defined in a similar manner. Let Φ, Ψ be relators over (B, F) , whose object maps F, G are induced by objects A, B of the fiber F1. Any morphism x: A → B in the fiber F1 induces a family of morphisms t_{C}: F (C) → G(C) in the fiber F0 , with C ranging over the objects of the fiber F0 , as follows. Because F(C): F1 ⟶ F0 is a functor , it is the case that F(C)(x): F(C)(A) → F(C)(B) . Furthermore, the functor F(C) acts on objects by composition, so F(C)(A) = A ∘ C and F(C)(B) = B ∘ C , and thus in fact F(C)(x): A ∘ C → B ∘ C . But F (C) = A ∘ C and G(C) = B ∘ C . We shall be interested only in those relator transformations Φ ⟶ Ψ for which the associated families t are induced by morphisms of the fiber F1 by composition, as just described. Similarly, for relators of n arguments over (B, F) , we shall be interested only in those relator transformations for which the associated transformations between object maps are induced by morphisms of the fiber F_{n} .

Definition 7.12 Let (A, Φ), (B, Ψ) be relators of n arguments over an iml-category (B, F). Let F, G: (Obj F0)^{n} ⟶ F0 be functors induced by A and by B, respectively. A relator transformation (A, Φ) ⟶ (B, Ψ) over (B, F) is given by a morphism x: A → B of the fiber F_{n} together with a relator transformation Φ ⟶ Ψ whose associated transformation F ⟶ G is induced by the morphism x by composition.

Proposition 7.8 thus extends to:

Theorem 7.13 Let (B, F) be an iml-category. Let the morphisms k → n of the new base category B′ be n-tuples of relators of k arguments over (B, F). Then the indexed category (B′, F̃) whose fiber over n is the category of relators of n arguments and relator transformations over (B, F) is an iml-category. Furthermore, the canonical forgetful functor (B′, F̃) ⟶ (B, F) is an iml-representation.

Proof. Let us outline the main points. We shall actually show that when dealing with relators and relator transformations over (B, F), both of which are defined as certain pairs, in the left coordinate one may work in (B, F) and in the right coordinate one may work in the iml-category of relators and relator transformations on ccc F0 given in Proposition 7.8.

First, observe that Definition 7.11 is stable under composition: if (A, Φ) is a relator of n arguments over (B, F) and (B_{1}, Ψ_{1}), …, (B_{n}, Ψ_{n}) relators of k arguments over (B, F), then (A ∘ ⟨B_{1}, …, B_{n}⟩, Φ ∘ ⟨Ψ_{1}, …, Ψ_{n}⟩) is a relator of k arguments over (B, F). Here the n-tuple ⟨B_{1}, …, B_{n}⟩ is the morphism k → n in the given base category B with products. In this way each morphism k → n of the new base category B′ induces a mapping from relators of n arguments to relators of k arguments, i.e., from the objects of the new fiber (F̃)_{n} over n to the objects of the new fiber (F̃)_{k} over k. This mapping will be the object part of the required functor (F̃)_{n} → (F̃)_{k}.

Similarly, let (x, τ): (A, Φ) ⟶ (A′, Φ′) be a relator transformation between relators of n arguments over (B, F) and let k → n be a morphism in the new base category B′ given by an n-tuple ⟨(B_{1}, Ψ_{1}), …, (B_{n}, Ψ_{n})⟩ of relators of k arguments over (B, F). We shall define the associated relator transformation between relators of k arguments over (B, F). Let a: k → n be the morphism in the starting base category B given by ⟨B_{1}, …, B_{n}⟩. Let D = F(a)(A) = A∘a , D′ = F(a)(A′) = A′∘a, and y = F(a)(x). Let Θ = Φ∘⟨Ψ_{1}, …, Ψ_{n}⟩, Θ′ = Φ′∘⟨Ψ_{1}, …, Ψ_{n}⟩, and σ = τ ∘ ⟨Ψ_{1}, …, Ψ_{n}⟩ , as defined in the iml-category of relators on F0. Then (y, σ): (D, Θ) ⟶ (D′, Θ′) is the required relator transformation between relators of k arguments over (B, F). The reader will readily check that this assignment is functorial, i.e., it preserves composition of relator transformations.

We also verify that each new fiber (F̃)_{n} is a ccc in such way that the ccc structure is preserved under composition. Finite products in (F̃)_{n} are clearly given coordinatewise and hence preserved under composition. Let us calculate (A, Φ) ⇒(B, Ψ) in (F̃)_{n}. Here A, B are objects in F_{n} and Φ, Ψ are relators of n arguments on the ccc F0, whose object maps are induced by composition by A, B, respectively. Note that for any morphism C: 0 → n in the given base category B, (A ⇒ B) ∘ C = (A ∘ C) ⇒(B ∘ C) because F(C): F_{n} ⟶ F0 is a ccc representation such that F(C)(D) = D ∘ C for any object D in the ccc F_{n}. But this means exactly that A ⇒ B induces the object map of Φ ⇒ Ψ as determined in the ccc of relators of n arguments on ccc F0, see Proposition 7.8.

Finally, erasing the right coordinate yields both a functor L: B′ ⟶ B that preserves finite products so that L(n) = n, as well as a natural transformation l: F̃ ⟶ (F ∘ L) such that for each n, l_{n}: (F̃)_{n} → F_{n} is a ccc representation.

Example 7.14 The discussion of the so-called total objects in the Appendix D of [Gir86] provides an interesting special case of Theorem 7.13. The starting iml-category (B, F) is given in Example 7.3. Object maps of the relevant relators on the ccc Qd of qualitative domains and stable maps are precisely the object maps of functors from the category Qd_{emb} of qualitative domains and embeddings to Qd_{emb} that preserve pullbacks and directed colimits. For any type σ in n type variables, the free iml-representation in (B, F) assigns to σ a functor A: (Qd_{emb})^{n} ⟶ Qd_{emb} that preserves pullbacks and directed colimits. By Theorem 7.13, the canonical forgetful functor from the iml-category of relators over (B, F) to (B, F) is an iml-representation. Furthermore, because free iml-representation (of the term iml-category) in any given iml-category is unique, the unique free iml-representation in (B, F) must factor through the free iml-representation to the iml-category of relators over (B, F). Therefore this latter representation assigns to type σ a relator of n arguments over (B, F) that must be of the form (A, Φ). In this particular case, this means simply that the object map of A is the object map of the relator Φ of n arguments on Qd. The total elements of A, defined in the Appendix D of [Gir86], are in our terminology those morphisms 1 → A in F_{n} that induce relator transformations 1 → Φ. Thus the first order part of Theorem D.1 in [Gir86] follows from our Theorem 7.13.

Theorem 7.13 also specializes to the m-ary case, by working over the m-fold power of a given iml-category. For instance, a binary relator over an iml-category (B, F) is given by an object A of the fiber F1 , together with a unary relator on F0 × F0, whose object map is induced by the object < A, A > of the fiber (F × F)1 by composition.

Let us also mention that Theorem 7.13 may be generalized along the lines of Proposition 7.9. The reader will note that the additional condition in Proposition 7.9 that the canonical cccrepresentation D → C is surjective on objects may now be omitted because the object map of a D-relator over a given iml-category (B, F) is given explicitly by an object of the fiber F1.

Theorem 7.15 Let (B, F) be an iml-category. Let C′ be a cartesian closed categories with equalizers. Let G: F0 ⟶ C′ be a functor that preserves products. Let D be a sub-cartesian-closed category of the comma category (C′ ↓ G). Let the morphisms k → n of the new base category B′ be n-tuples of D-relators of k arguments over (B, F). Then the indexed category (B′, F̃) whose fiber over n is the category of relators of n arguments and relator transformations over (B, F) is an iml-category. Furthermore, the canonical forgetful functor (B′, F̃) ⟶ (B, F) is an iml-representation.

Example 7.16 Let us give an example of the binary case of Theorem 7.15. Recalling Section 6.3, let D be the full sub-ccc of the comma category (P er × P er ↓ H) whose objects are saturated binary relations on pers, i.e., objects of the form ⟨S, P, Q⟩, where S is a saturated binary relation from the domain of per P to the domain of per Q. Let the starting iml-category (B, F) be the iml-category P ER discussed in Example 7.4, a sub-iml-category of P er_{iml}. In particular, the fiber over 0 in P ER is the ccc P er of pers and per morphisms. A (binary) D-relator over P ER is simply a (binary) D-relator on P er, i.e., it consists of a mapping F from pers to pers and a mapping Φ: Obj D ⟶ Obj D such that Φ(S, P, Q) = (S′, F (P), F (Q)). However, a D-relator transformation over P ER is not simply a D-relator transformation on P er, because it must be given by a realizable family of per morphisms. Indeed, let < F, Φ > and < G, Ψ > be D-relators over P ER. A D-relator transformation t: < F, Φ >⟶< G, Ψ > over P ER is given by a partial recursive function f that names each per morphism t_{P}: F (P) → G(P), with P ranging over pers, and such that for every saturated relation S from the domain of P to the domain of Q and the associated saturated relations S′ and S′′ given by Φ and Ψ, respectively, it is the case that the composite relation t_{Q} ∘ S′ is included in the relation S′′ ∘ t_{P}. (Each per morphism induces a saturated relation.) In other words, for all pers P and Q and all numbers n in the domain of F (P) and k in the domain of F (Q) , n S′ k implies f(n) S′′ f(k). Thus the first order part of the Soundness Theorem in Section 4.7 of [BFS90] is a special case of our Theorem 7.15.

Example 7.17 Another example of this more general situation is the iml-category of pcporelators whose associated object maps are not just arbitrary maps from pcpos to pcpos, but functors from the category P cpo_{emb} of pcpos and embedding-projection pairs to P cpo_{emb}. Here the fiber F_{n} of the starting iml-category is the ccc whose objects are functors (P cpo_{emb})^{n} ⟶ P cpo_{emb} and the morphisms t: F → G of the fiber F_{n} are certain families of continuous maps t_{P}: F (P) → G(P), where P ranges over n-tuples of pcpos, see [CGW89].

References

[ACC93] M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. In Proc. 20-th ACM Symposium on Principles of Programming Languages, 1993.

[AbJ91] S. Abramsky and T.P. Jensen. A relational approach to strictness analysis for higherorder polymorphic functions. In Proc. 18-th ACM Symposium on Principles of Programming Languages, 1991.

[BFS90] E.S. Bainbridge, P.J. Freyd, A. Scedrov, and P.J. Scott. Functorial Polymorphism. Theoretical Computer Science, 70:35–64 ,1990. Corrigendum ibid., 71:431, 1990.

[BMM90] K. B. Bruce, A. R. Meyer, and J. C. Mitchell. The semantics of second-order lambda calculus. Information and Computation, 85(1):76–134, 1990. Reprinted in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 213– 273.

[CMS91] L. Cardelli, J.C. Mitchell, S. Martini, and A. Scedrov. An extension of system F with Subtyping. To appear in Information and Computation. Extended abstract in T.Ito and A.R. Meyer (eds.), Theoretical Aspects of Computer Software, pages 750–770. Springer-Verlag LNCS 526, 1991.

[CGW89] T. Coquand, C.A. Gunter, and G. Winskel. Domain theoretic models of polymorphism. Information and Computation, 81:123–167, 1989.

[Fre92] P.J. Freyd. Structural polymorphism. Theoretical Computer Science, to appear.

[FRR92] P.J. Freyd, E.P. Robinson, and G. Rosolini. Functorial parametricity. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, pages 444–452, 1992.

[FrS90] P.J. Freyd and A. Scedrov. Categories, Allegories. Mathematical Library, North-Holland, 1990.

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

[GLT89] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989.

[GSS91] J.-Y. Girard, A. Scedrov, and P.J. Scott. Normal forms and cut-free proofs as natural transformations. In: Y.N. Moschovakis, editor, Logic from Computer Science, Proc. M.S.R.I. Workshop, Berkeley, 1989. M.S.R.I. Series, Springer-Verlag, 1991.

[KR77] A. Kock, G.E. Reyes. Doctrines in categorical logic. In J. Barwise, editor, Handbook of Mathematical Logic, pages 283–313. North-Holland, 1977.

[Laf88] Y. Lafont. Logiques, Categories & Machines. Thèse de Doctorat, Université Paris VII, 1988.

[LS86] J. Lambek and P.J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge studies in advanced mathematics 7, Cambridge University Press, 1986.

[MaR92] Q. Ma and J.C. Reynolds. Types, abstraction, and parametric polymorphism, Part 2. In S. Brookes et al., editors, Mathematical Foundations of Programming Semantics, Proceedings 1991, pages 1–40. Springer-Verlag LNCS 598, 1992.

[McL71] S. Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics, Springer-Verlag, 1971.

[Mai91] H. Mairson. Outline of a proof theory of parametricity. In Proc. 5-th Intern. Symp. on Functional Programming and Computer Architecture, 1991.

[MS76] R.E. Milne and C. Strachey. A theory of programming language semantics. Chapman and Hall, London, and Wiley, New York, 1976.

[Mit86] J.C. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions. In ACM Conference on LISP and Functional Programming, pages 308–319, August 1986. Revised version in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 195–212.

[Mit88] J.C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76(2/3):211–249, 1988. Reprinted in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 153–194.

[Mit90] J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 365–458. North-Holland, 1990.

[MM85] J.C. Mitchell and A.R. Meyer. Second-order logical relations. In Logics of Programs, pages 225–236. Springer-Verlag LNCS 193, June 1985.

[MM91] J.C. Mitchell and E. Moggi. Kripke-style models for typed lambda calculus. Annals Pure Appl. Logic, 51:99–124, 1991.

[MS89] J.C. Mitchell and P.J. Scott. Typed lambda calculus and cartesian closed categories. In J. W. Gray and A. Scedrov, editors, Proc. Conf. Categories in Computer Science and Logic, June 14-20, 1987, Univ. Colorado Boulder, Contemporary Mathematics, vol. 92, pages 301–316. Amer. Math. Society, 1989.

[Mgg89] E. Moggi. Computational lambda calculus and monads. In Proc. 4^{th} IEEE Symposium on Logic in Computer Science, pages 14–23, IEEE Computer Society Press, 1989.

[Mog91] E. Moggi. A category-theoretic account of program modules. Math. Structures in Computer Science, 1(1):103–139, 1991.

[OHT93] P.W. O’Hearn and R.D. Tennent. Relational parametricity and local variables. In Proc. 20-th ACM Symposium on Principles of Programming Languages, 1993.

[Pit87] A.M. Pitts. Polymorphism is set-theoretic, constructively. In Category Theory and Computer Science, Proceedings Edinburgh, 1987, pages 12–39. Springer-Verlag LNCS volume 283, 1987.

[Plo80] G.D. Plotkin. Lambda definability in the full type hierarchy. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363–373. Academic Press, 1980.

[Rey74] J.C. Reynolds. On the relation between direct and continuation semantics. In Second Colloq. Automata, Languages and Programming, pages 141–156. Springer-Verlag LNCS, 1974.

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

[ScS82] A. Scedrov and P.J. Scott. A note on the Friedman slash and Freyd covers. In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Symposium, pages 443–452. North-Holland, 1982.

[See83] R.A.G. Seely. Hyperdoctrines, natural deduction, and the Beck condition. em Zeitschr. f. math. Logik und Grundlagen d. Math., 29:505–542, 1983.

[See87] R.A.G. Seely. Categorical semantics for higher order polymorphic lambda calculus. Journal of Symbolic Logic, 52:969–989, 1987.

[Sta85] R. Statman. Logical relations and the typed lambda calculus. Information and Control, 65:85–97, 1985.

[Str67] C. Strachey. Fundamental concepts in programming languages. Unpublished lecture notes, International Summer School in Computer Programming, Copenhagen, August, 1967.

[Wad89] P. Wadler. Theorems for free! In 4th Internat. Symp. on Functional Programming Languages and Computer Architecture, London, pages 347–359, Assoc. for Comp. Machinery, 1989.