Theory and Applications of Categories, Vol. 20, No. 7, 2008, pp. 116–151.

CATEGORY-THEORETIC MODELS OF LINEAR ABADI & PLOTKIN LOGIC

LARS BIRKEDAL AND RASMUS E. MØGELBERG AND RASMUS L. PETERSEN

Abstract. This paper presents a sound and complete category-theoretic notion of models for Linear Abadi & Plotkin Logic [Birkedal et al., 2006], a logic suitable for reasoning about parametricity in combination with recursion. A subclass of these called parametric LAPL structures can be seen as an axiomatization of domain theoretic models of parametric polymorphism, and we show how to solve general (nested) recursive domain equations in these. Parametric LAPL structures constitute a general notion of model of parametricity in a setting with recursion. In future papers we will demonstrate this by showing how many different models of parametricity and recursion give rise to parametric LAPL structures, including Simpson and Rosolini’s set theoretic models [Rosolini and Simpson, 2004], a syntactic model based on Lily [Pitts, 2000, Bierman et al., 2000] and a model based on admissible pers over a reflexive domain [Birkedal et al., 2007].

1. Introduction

When Reynolds introduced relational parametricity in 1983 [Reynolds, 1983] he argued that it could be used to prove representation independence results for abstract data types. Since then a large number of applications of the abstraction property of parametricity have been suggested, for example in security [Tse and Zdancewic, 2004] and to model local variables [O’Hearn and Tennent, 1995]. From a type theoretic perspective, relational parametricity is interesting because it allows rich type systems to be constructed from a few basic type constructors. For example in the second order lambda calculus, general inductive and coinductive types can be constructed using simply polymorphism and function space type constructors. For real programming, one is of course not just interested in a strongly terminating calculus such as the second-order lambda calculus, but also in a language with full recursion. Thus in [Reynolds, 1983] Reynolds also asked for a parametric domain-theoretic model of polymorphism.

However, relational parametricity is too strong a principle to be simply combined with recursion in the second order lambda calculus. One way to see this is that parametricity gives encodings of coproducts, and it is well known that the combination of coproducts, products, exponentials and fixed points exist only in the trivial case of all types being

This work was partly supported by the Danish Agency for Science Technology and Innovation Received by the editors 2006-04-20 and, in revised form, 2008-04-09. Transmitted by Valeria de Paiva. Published on 2008-04-11. 2000 Mathematics Subject Classification: 03B70, 18C50, 68Q55. Key words and phrases: Parametric polymorphism, categorical semantics, axiomatic domain theory,

recursive types, fibrations.

\begin{matrix}c \\ ◯ \end{matrix} Lars Birkedal and Rasmus E. Møgelberg and Rasmus L. Petersen, 2008. Permission to copy for private use granted.

isomorphic [Huwig and Poigné, 1990]. Inspired by domain theory Plotkin suggested an elegant solution to this problem [Plotkin, 1993a, Plotkin, 1993b], which was to study a dual intuitionistic / linear lambda calculus with polymorphism and fixed points. Parametricity should then be available only in the linear part of the calculus and give encodings of datatypes in this, including initial algebras and final coalgebras. Moreover, by Freyd’s theory of algebraically compact categories [Freyd, 1990a, Freyd, 1990b, Freyd, 1991] the inductive and coinductive types in combination with fixed points would give solutions to recursive type equations in the linear calculus.

Recently, Pitts and coworkers [Pitts, 2000, Bierman et al., 2000] have presented the language Lily, essentially Plotkin’s polymorphic intuitionistic / linear lambda calculus equipped with an operational semantics, and shown how Plotkin’s encodings can be used in the syntactic setting.

In parallel with the work presented here, Rosolini and Simpson [Rosolini and Simpson, 2004] have shown how to construct parametric domain-theoretic models in intuitionistic set-theory using synthetic domain-theory. Moreover, they have shown how to give a computationally adequate denotational semantics of Lily.

This paper presents a unifying category-theoretic framework for parametric models of Polymorphic Intuitionistic / Linear Lambda calculus with a fixed point combinator Y (a calculus henceforth referred to as PILL_{Y}). The basis is Linear Abadi & Plotkin Logic (LAPL), an adaptation of Abadi & Plotkin’s logic for parametricity on the second order lambda calculus [Plotkin and Abadi, 1993] to PILL_{Y}, presented by the authors in [Birkedal et al., 2006]. In LAPL the parametricity principle for PILL_{Y} can be formulated and the above mentioned consequences of parametricity including the solutions to recursive type equations can be proved valid. In this paper we present the notion of LAPL structure which is a sound and complete category-theoretic notion of model of LAPL, and we define a subclass of these called parametric LAPL structures to be LAPL structures in which the parametricity principle holds and which satisfy a technical condition called very strong equality. Using reasoning in LAPL we show how to solve recursive domain equations in parametric LAPL structures, and moreover do so in full generality considering parametrized recursive domain equations (needed to model nested recursive types). The recursive types satisfy a parametrised version of the initial dialgebra property, a universal property generalising initial algebras and final coalgebras to general recursive types. We formulate and prove this property using fibred category theory. These results show that the notion of parametric LAPL structure is indeed a useful notion of parametric model of PILL_{Y}, since these satisfy semantic versions of the consequences of parametricity known from logic.

118 LARS BIRKEDAL AND RASMUS E. MØGELBERG AND RASMUS L. PETERSEN

Forthcoming papers will show how the Lily language and the set theoretic constructions mentioned above can be seen as constructing LAPL structures. In [Birkedal et al., 2007] we present a parametric LAPL structure based on admissible pers over a reflexive domain. This model was first suggested by Plotkin [Plotkin, 1993a], but the details have to our knowledge never been worked out before. In [Møgelberg, 2005b] the second author shows how the parametric completion process as in [Robinson and Rosolini, 1994] can be adapted to construct a parametric LAPL structures from a model of PILL_{Y}. The examples show that the notion of parametric LAPL structure is general enough to cover many different models, and the general results about parametric LAPL structures apply to all these models, giving rigourous proofs of consequences of parametricity.

The work presented here builds upon previous work by the first two authors on categorical models of Abadi-Plotkin’s logic for parametricity [Birkedal and Møgelberg, 2005], which includes detailed proofs of consequences of parametricity for polymorphic lambda calculus and also includes a description of a parametric completion process that given an internal model of polymorphic lambda calculus produces a parametric model. It is not necessary to be familiar with the details of [Birkedal and Møgelberg, 2005] to read the present paper, although Appendix A of [Birkedal and Møgelberg, 2005], contains some definitions and theory concerning composable fibrations which are only briefly summarised in this paper.

1.1. Outline. The remainder of this paper is organized as follows. Section 2 briefly recalls PILL_{Y} and Linear Abadi & Plotkin Logic (LAPL), and the main results of [Birkedal et al., 2006], and Section 3 recalls the definition of PILL_{Y} models. Building upon the notion of PILL_{Y} model Section 4 defines the notion of LAPL structure and proves soundness and completeness of the interpretation of LAPL in such structures. In Section 5 we present our definition of a parametric LAPL structure and prove that one may solve recursive domains equations in such.

2. Linear Abadi-Plotkin Logic

This section briefly recalls Linear Abadi-Plotkin Logic (LAPL) as defined in [Birkedal et al., 2006]. LAPL is a logic for reasoning about parametricity for Polymorphic Intuitionistic Linear Lambda calculus with fixed points (PILL_{Y}). The logic is based on Abadi and Plotkin’s logic for parametricity [Plotkin and Abadi, 1993] for the second-order lambda calculus.

2.1. PILL_{Y}. The calculus PILL_{Y} is essentially Barber and Plotkin’s DILL [Barber, 1997] extended with polymorphism and a fixed point combinator. Types are formed using the grammar

σ ::= α | I | σ ⊗ τ | σ ⊸ τ |!σ | ∏α. σ.

where α ranges over type variables. PILL_{Y} can be seen as a type theory for domain theory and polymorphism, and even though polymorphism cannot be modelled in ordinary domain theory it is useful to keep the domain theoretic intuition in mind: types are domains (complete partial orders with a least element), ⊗ denotes the smash product, ⊸ the domain of strict continuous maps and ! denotes lifting. One can make this intuition precise by constructing a DILL model based on the category of domains and strict continuous maps, but we will not do that here. One way to extend the domain theoretic intuition to polymorphism is by considering partial equivalence relations. This is used to construct a PILL_{Y} model and a parametric LAPL structure in [Birkedal et al., 2007].

Terms of PILL_{Y} are written with explicit contexts as

α_{1}, …, α_{k} | x_{1} : σ_{1}, …, x_{n}: σ_{n}; x′_{1} : σ′_{1}, …, x′_{m}: σ′_{m} ⊢ t: τ,

where the list α_{1}, …, α_{k} — called the kind context — contains all the type variables occurring freely in the types σ_{i}, σ′_{i} and τ. The term t has two contexts of free term variables: the list of x’s is called the intuitionistic type context and is often denoted Γ, and the list of x′’s is called the linear type context, often denoted Δ. Variables in the linear context can occur linearly in terms and variables in the intuitionistic context can occur intuitionistically. We use the horizontal line − to denote an empy context, in particular − | −; − ⊢ t: σ denotes a closed term of closed type.

The grammar for terms is:

t ::=x | ⋆ | Y | λ^{∘}x: σ.t | t t | t ⊗ t |!t | Λα: Type. t | t(σ) |
let x: σ ⊗ y: τ be t in t | let !x: σ be t in t | let ⋆ be t in t

The construction λ^{∘}x: σ.t abstracts linear variables in terms and constructs terms of type σ ⊸ τ, which we think of as a linear function space. Intuitionistic function space can be defined using the Girard encoding σ → τ =!σ ⊸ τ, and there is a corresponding lambda abstraction abstracting intuitionistic variables. Because of the encoding of → application of an intuitionistic function f: σ → τ to an input x: σ becomes f(!x). Using the Girard encodings, the type of the fixed point combinator Y can be written as ∏α. (α → α) → α. The subset of PILL_{Y} without the fixed point combinator is referred to as PILL.

Terms of PILL_{Y} are identified up to an equality relation, which we shall call external equality (as opposed to provable equality in the logic LAPL). Rules for external equality includes β and η rules, but we refer to [Birkedal et al., 2006] for a definition.

In the domain theoretic intuition, linearity in PILL_{Y} is modelled by strictness, i.e., we think of a term

− | x_{1} : σ_{1}, …, x_{n}: σ_{n}; x′_{1} : σ′_{1}, …, x′_{m}: σ′_{m} ⊢ t: τ

as a continuous function from ∏_{i≤n}σ_{i} × ∏_{j≤m}σ′_{j} to τ which maps a tuple

(x_{1}, …, x_{n}, x′_{1}; …, x′_{m})

to the least element ⊥ if any one of the x′_{j} is ⊥.

2.2. LAPL. As mentioned, Linear Abadi-Plotkin Logic is a second order logic suitable for reasoning about parametricity over PILL_{Y}. As in Abadi & Plotkin’s logic for parametricity on the second order lambda calculus [Plotkin and Abadi, 1993, Birkedal and Møgelberg, 2005], the logic contains relations and the relational interpretation of types as basic building blocks. We mention two peculiarities about the logic. First, unlike the general PILL_{Y} terms propositions in the logic have no linear context of term variables, only an intuitionistic one. This means that even though PILL_{Y} is dual linear / intuitionistic the reasoning in the logic is purely intuitionistic. We may still reason about linearity of terms of PILL_{Y} since we may consider terms of linear function space type. This restriction of the logic has been chosen for simplicity and because the reasoning that we need in the logic to prove properties of polymorphic encodings in PILL_{Y} is purely intuitionistic.

The second peculiarity is that the logic has two classes of relations, a class of ordinary relations and a class of ”admissible” relations. In the domain theoretic intuition, a relation is just a subset of the product of two domains, whereas an admissible relation must relate ⊥ to ⊥ and be closed under least upper bounds of chains. Indeed the main example of an admissible relation in LAPL is the graph of a linear function f: σ ⊸ τ, and the main example of a relation that is not in general admissible is the graph of an intuitionistic function f: σ → τ. The introduction of admissible relations in the logic is necessary because, as noticed by Plotkin, adding an unrestricted parametricity principle to PILL_{Y} gives an inconsistent logic, a problem which can be remedied by restricting the formulation of the parametricity principle to the class of admissible relations.

The logic has three types of judgements: one for propositions, one for relations and one for admissible relations:

Ξ | Γ | Θ ⊢ ϕ: Prop
Ξ | Γ | Θ ⊢ ρ: Rel(τ, τ′)
Ξ | Γ | Θ ⊢ ρ: AdmRel(τ, τ′).

Here, Ξ and Γ are respectively the kind context and the intuitionistic type context as in PILL_{Y}, and Θ is a context of relational variables of the form

R_{1} : Rel(τ_{1}, τ′_{1}), …, R_{n}: Rel(τ_{n}, τ′_{n}), S_{1} : AdmRel(ω_{1}, ω′_{1}), …, S_{m}: AdmRel(ω_{m}, ω′_{m}).

The grammar for propositions is

ϕ ::= (t =_{σ} u) | ρ(t, u) | ϕ ⊃ ψ | ⊥ | ⊤ | ϕ ∧ ψ | ϕ ∨ ψ | ∀α: Type. ϕ |
∀x: σ. ϕ | ∀R: Rel(σ, τ). ϕ | ∀S: AdmRel(σ, τ). ϕ |
∃α: Type. ϕ | ∃x: σ. ϕ | ∃R: Rel(σ, τ). ϕ | ∃S: AdmRel(σ, τ). ϕ

where ρ is a relation (admissible or not). As an example of a formation rule we mention the one for equality

Ξ | Γ; − ⊢ t: σ Ξ | Γ; − ⊢ u: τ
Ξ | Γ | Θ ⊢ t =_{σ} u: Prop

where the judgements in the hypothesis are typing judgements in PILL_{Y}.

The grammar for relations is

ρ ::= R | (x: σ, y: τ). ϕ | σ[ρ⃗]

Relations can be formed from proposition and vice versa, as determined by the two rules

Ξ | Γ | Θ ⊢ ρ: Rel(σ, τ) Ξ | Γ; − ⊢ t: σ Ξ | Γ; − ⊢ u: τ
Ξ | Γ | Θ ⊢ ρ(t, u): Prop
Ξ | Γ, x: σ, y: τ | Θ ⊢ ϕ: Prop
Ξ | Γ | Θ ⊢ (x: σ, y: τ). ϕ: Rel(σ, τ)

The admissible relations are a subset of the relations closed under a collection of rules for which we refer to [Birkedal et al., 2006] as we do for all other details in this section. Examples of relations include equality relations eq_{τ} defined as (x: τ, y: τ). x =_{τ} y, graphs of linear maps ⟨f⟩: Rel(σ, τ) for f: σ ⊸ τ defined as (x: σ, y: τ). y =_{τ} f(x) and graphs of intuitionistic maps ⟨g⟩: Rel(σ, τ) for g: σ → τ defined as (x: σ, y: τ). y =_{τ} f(!x) of which the first two are admissible, but the last generally is not.

We introduce some notation that is needed later in the text: if ρ: Rel(σ, τ) and f: σ′ ⊸ σ, g: τ′ ⊸ τ, we write (f, g)^{∗}ρ for

(x: σ′, y: τ′). ρ(f(x), g(y))

The relational interpretation of types is the rule

α_{1}, …, α_{n} ⊢ σ(α⃗): Type Ξ | Γ | Θ ⊢ ρ_{1} : AdmRel(τ_{1}, τ′_{1}), …, ρ_{n}: AdmRel(τ_{n}, τ′_{n})

Ξ | Γ | Θ ⊢ σ[ρ⃗]: AdmRel(σ(τ⃗), σ(τ′))

(1)

The PILL_{Y} type constructors ⊸, ⊗,!, ∏α. (−) may all be given relational interpretations, by for example defining ρ ⊸ ρ′ for ρ: Rel(σ, τ), ρ′: Rel(σ′, τ′) to be

(f: σ ⊸ σ′, g: τ ⊸ τ′). ∀x: σ, y: τ. ρ(x, y) ⊃ ρ′(f(x), g(y)).

Using these, the relational interpretation of types in pure PILL_{Y} can be defined by structural induction. However, the relational interpretation of types in LAPL is stronger. This is because LAPL can be used for reasoning about not just pure PILL_{Y} but also other PILL_{Y} -calculi with added type or term constants, the most prominent example being the internal language of a given PILL_{Y} model. Such models may contain open type constants such as α ⊢?(−): Type, and (1) says that each of these need to have a relational interpretation. The inductive definition sketched above is then captured in axioms for LAPL stating for example that (σ ⊸ τ)[R] ≡ σ[R] ⊸ τ[R].

Implication in the logic is formally written as Ξ | Γ | Θ | ϕ_{1}, …, ϕ_{n} ⊢ ψ, meaning that in the context Ξ | Γ | Θ the propositions ϕ_{1}, …, ϕ_{n} collectively imply ψ. For ρ, ρ′: Rel(σ, τ) we use shorthand Ξ | Γ | Θ | ⊤ ⊢ ρ ≡ ρ′ for

Ξ | Γ | Θ | ⊤ ⊢ ∀x: σ, y: τ. ρ(x, y) ⊃⊂ ρ′(x, y).

Using this notation we have already informally stated one axiom of the logic, but we refer to [Birkedal et al., 2006] for details.

In LAPL we can formulate the identity extension schema σ[e⃗q_{τ}] ≡ eq_{σ(τ⃗)}. Identity extension implies the parametricity schema

∀x: ∏α. σ. ∀α, β. ∀R: AdmRel(α, β). σ[R](x α, xβ).

Instantiating the parametricity schema with the type of the fixed point combinator

Y : ∏α. (α → α) → α

\begin{aligned}σ & ≅ & ∏α. (σ ⊸ α) ⊸ α \\ σ ⊗ τ & ≅ & ∏α. (σ ⊸ τ ⊸ α) ⊸ α \\ I & ≅ & ∏α. α ⊸ α \\ 0 & = & ∏α. α \\ 1 & = & ∏α. α \\ σ + τ & = & ∏α. (σ ⊸ α) → (τ ⊸ α) → α \\ σ × τ & = & ∏α. (σ ⊸ α) + (τ ⊸ α) ⊸ α \\ ℕ & = & ∏α. (α ⊸ α) → α ⊸ α \\ ∐α. σ & = & ∏β. (∏α. σ ⊸ β) ⊸ β \\ μα. σ & = & ∏α. (σ ⊸ α) → α \\ να. σ & = & ∐α.!(α ⊸ σ) ⊗ α \end{aligned}

Figure 1: Types definable using parametricity

and applying it to the graph of a linear function h: σ ⊸ τ we find Plotkin’s principle: if f: σ → σ and g: τ → τ are such that h ∘ f = g ∘ h then h(Y (!f)) = Y (!g). The restriction to admissible relations of the universal quantification in the parametricity principle restricts us from instantiating it with the graphs of intuitionistic functions, just like Plotkin’s principle in domain theory only holds for strict maps h.

In [Birkedal et al., 2006] we show how the identity extension schema implies correctness of encodings of certain datatypes in PILL_{Y}, some of which are listed in Figure 1. What is meant by correctness of these is that it is provable in the logic that these satisfy the usual universal properties with respect to linear functions. For example, in the last two of the type encodings in Figure 1, the type variable α is assumed to occur only positively in σ, and such types induce endofunctors on the category of PILL_{Y} types with linear terms as morphisms, for which the types defined are the inductive and coinductive datatypes respectively. One might be tempted to try to define initial algebras and final coalgebras for the functors induced by types on the category of PILL_{Y} types and intuitionistic terms using the encodings from second order lambda calculus. Such an attempt will fail because the parametricity arguments from second order lambda calculus involve instantiations of the parametricity principle with graphs of general intuitionistic functions, and so can not be carried out in LAPL.

The full type theoretical strength of the combination of parametricity and recursion is however, that we can find solutions to general recursive type equations in PILL_{Y}. More precisely, using Freyd’s theory of algebraically compact categories [Freyd, 1990a, Freyd, 1990b, Freyd, 1991] the combination of initial algebras, final coalgebras and fixed points allows us to construct, for any type expression α ⊢ σ in pure PILL_{Y}, a type τ such that σ(τ) ≅ τ. The constructed solutions moreover satisfy the initial dialgebra property, a universal property generalising initial algebras and final coalgebras.

Further details can be found in [Birkedal et al., 2006]. In Section 5.8 we explain in detail the semantic consequences of this construction, defining a semantic notion of recursive domain equations that can be solved in parametric LAPL structures and formulating the universal properties satisfied by the constructed solutions.

As mentioned, the universal conditions satisfied by the polymorphic type encodings, in particular the initial dialgebra property of the recursive types, are formulated with respect to linear maps in PILL_{Y} rather than intuitionistic maps. This corresponds with the domain theoretic intuition for PILL_{Y} given earlier, as the category Cppo_{⊥} of domains and strict continuous maps is algebraically compact and the category Cppo of domains and continuous maps is not.

3. PILL_{Y} models

In this section we recall the category theoretic concept of PILL_{Y} model. The theory draws heavily on prior work on models of intuitionistic / linear lambda calculi in particular [Barber, 1997, Benton, 1995, Maietti et al., 2005, Maneggia, 2004]. For further details we refer to loc. cit., but also to the note [Møgelberg et al., 2005] which summarises the theory needed for PILL_{Y} models from the original references.

Since PILL_{Y} is a language with polymorphism the notion of model is formulated using fibred category theory, and since the category theoretic formulation of models of DILL uses the 2-category of symmetric monoidal categories, we shall use obvious generalisations of the concepts of monoidal category theory to fibred categories.

In this paper we make the general assumption that all fibrations and all fibred structure is split. The assumption of cleavage is similar to the assumption of chosen structure in cartesian closed categories, which is necessary to define an interpretation of simply typed lambda calculus. We assume a split cleavage to avoid having to carry isomorphisms around. All examples of LAPL structures that we are aware of are split.

3.1. Definition. A fibred linear adjunction is a fibred symmetric monoidal adjunction

\xymatrix{ℂ \ar[dr]_{p} \ar[rr]_{G} & ⊥ & 𝔻 \ar[ll]_{F} \ar[dl] \\  & 𝔹,}

where ℂ is fibred symmetric monoidal closed and the fibred monoidal structure on 𝔻 is a fibred cartesian structure.

3.2. Definition. A fibred linear category is a fibred symmetric monoidal closed category ℂ → 𝔹 together with a fibred symmetric monoidal comonad ! on ℂ and fibred symmetric monoidal natural transformations e: !(−) → I, d: !(−) →!(−)⊗!(−) such that

• For each object A in ℂ, (!A, e_{A}, d_{A}) is a commutative comonoid

• For each object A in ℂ, e_{A}, d_{A} define coalgebra maps from the free coalgebra δ_{A}: !A → !!A to the coalgebras m_{I}: I →!I and

\xymatrix{!A⊗!A \ar[r]^{δ_{A}⊗δ_{A}} & !!A⊗!!A \ar[r]^{m} & !(!A⊗!A)}

respectively, where m_{I} and m are the comparison functors corresponding to the fibred symmetric monoidal functor !.

• In each fibre, all comonad maps between free coalgebras preserve the comonoid structure.

In the following we shall often denote a fibred linear category simply by ℂ → 𝔹 letting the rest of the data being given implicitely.

Given a fibred linear adjunction as in Definition 3.1 the induced fibred comonad on ℂ gives a fibred linear category. On the other hand there may be several fibred linear adjunctions inducing the same linear category structure. One extreme is letting 𝔻 be the co-Eilenberg-Moore category for the comonad, as this is fibred cartesian for any fibred linear category.

From here on we name the categories according to their role in the interpretation of PILL_{Y}. We explain the names later.

3.3. Definition. A PILL model is a fibred linear category p: LinType → Kind such that

• The category Kind is cartesian

• LinType → Kind has a generic object O and, writing Ω for pO, has products with respect to the projections of the form K × Ω → K in Kind. These products must satisfy the Beck-Chevalley condition.

A morphism of PILL models from LinType → Kind to LinType′ → Kind′ is a strong fibred morphism of fibred symmetric monoidal closed categories

\xymatrix{LinType \ar[r]^{K} \ar[d] & LinType′ \ar[d] \\ Kind \ar[r]^{L} & _{Kind_{′}}}

preserving generic object, the cartesian structure in the base categories and products in the fibration.

In the following we shall often talk about a fibred adjunction

\xymatrix{LinType \ar[dr]_{p} \ar[rr]_{G} & ⊥ & Type \ar[ll]_{F} \ar[dl] \\  & Kind,}

being a PILL model. By that we shall mean that LinType → Kind together with the induced fibred comonad is a PILL model in the sense of Definition 3.3, and moreover, that Type is the closure of the fibred coKleisli category for the fibred comonad under finite coproducts inside the coEilenberg-Moore category, which as mentioned above is fibred cartesian. The reason for this is that the category Type will turn out to be useful in further developments as we shall see shortly. Notice further that since Type is specified there is no ambiguity in this convention. Using this notion of PILL models as fibred adjunctions, specifying Type we are following [Maietti et al., 2005].

We sketch how PILL is interpreted in PILL models. Kind contexts are interpreted in Kind as [[α_{1}, …, α_{n}]] = Ω^{n}, and a type in kind context α_{1}, …, α_{n} ⊢ σ is interpreted as an object of LinType_{Ω^{n}}. A type variable α_{1}, …, α_{n} ⊢ α_{i} is interpreted as π_{i}^{∗}(O), where π_{i}: Ω^{n} → Ω is the i’th projection. Polymorphic types are interpreted using products with respect to projections in Kind in the usual way. The type constructors ⊗, ⊸, I are interpreted using the fibred symmetric monoidal closed structure and the fibred comonad on LinType to interpret !. A term

α⃗ | x⃗: σ⃗; x′: σ′ ⊢ t: τ

is interpreted as a vertical morphism

![[σ_{1}]] ⊗ … ⊗![[σ_{n}]] ⊗ [[σ′_{1}]] ⊗ … ⊗ [[σ′_{m}]] ⊸ [[τ]]

in LinType. Here we have denoted the morphisms in LinType by ⊸.

Notice how this corresponds to the domain theoretic intuition given earlier for PILL_{Y}: in domain theory strict continuous maps

!A_{1} ⊗ … ⊗!A_{n} ⊗ B_{1} ⊗ … ⊗ B_{m} ⊸ C

correspond to continuous maps

A_{1} × … × A_{n} × B_{1} × … × B_{m} → C

strict in each of the B_{j} variables.

As mentioned earlier, the viewpoint of PILL_{Y} models as adjunctions is often practical even though in the interpretation given above the category Type has not been used. Type is useful because it models the purely intuitionistic terms of PILL_{Y}. To be precise, a PILL_{Y} -term Ξ | x⃗: σ⃗; − ⊢ t: τ is modeled in LinType as a morphism

[[Ξ | x⃗: σ⃗; − ⊢ t: τ]]: ⊗_{i}![[Ξ ⊢ σ_{i}]] ⊸ [[Ξ ⊢ τ]],

and since one can prove ⊗_{i}![[Ξ ⊢ σ_{i}]] ≅ F (∏_{i}G([[Ξ ⊢ σ_{i}]])), we have, using the fibred adjunction F ⊣ G, that such a term corresponds to

[[Ξ | x⃗: σ⃗; − ⊢ t]]_{Type} : ∏_{i}G([[Ξ ⊢ σ_{i}]]) → G([[Ξ ⊢ τ]])

in Type.

The interpretation justifies the suggestive notation used in the definition of PILL models: Kind models kinds, LinType models types and linear maps, and Type models types and intuitionistic maps. We shall continue to use similar suggestive notation throughout the paper, to help the reader keep track of the several categories involved in the definition of the concept of LAPL structure.

3.4. Definition. A PILL_{Y} model is a PILL model, which models the fixed point operator

Y : Πα. (α → α) → α

4. LAPL structures

This section builds on the notion of PILL_{Y} model to define the notion of LAPL structure, which we will prove is a sound and complete category theoretic notion of model for LAPL. The definition proceeds in two steps. First we define the notion of pre-LAPL structure with notion of admissible relations, which models the fraction of LAPL excluding the relational interpretation of types, i.e., the rule (1). In the second step we identify the extra structure required to interpret the relational interpretation of types, and use this to define the notion of LAPL structure. The second step is described in Section 4.5.

The definition of pre-LAPL structure uses two non-standard notions from fibred category theory, that we explain briefly here. The first concerns a notion of contravariant morphisms of fibrations. We would like to define these to be families of contravariant functors between fibre categories respecting reindexing, just like ordinary maps of fibrations can be described as families of functors respecting reindexing. To make sense of this definition we define a construction, which given a fibration p: 𝔼 → 𝔹 produces a fibration p^{fop} : 𝔼^{fop} → 𝔹 where the fibres are the opposite of the fibres of p and reindexing is as in p. Under our standing assumption that all fibrations are split this is easy: by the Grothendieck construction a split fibration p corresponds to a functor p̂: 𝔹^{op} → Cat, and we define p^{fop} to be the fibration corresponding to the functor (−)^{op} ∘ p̂, where (−)^{op} : Cat → Cat is the functor mapping a category to its opposite. In fact p^{fop} can be defined for more general fibrations as described in Appendix A.

The second non-standard notion used in the definition of pre-LAPL structure is the notion of indexed first order logic fibration defined in detail in [Birkedal and Møgelberg, 2005, Appendix A]. This relatively involved categorical notion is needed to model the double indexing occuring here: propositions live in contexts of types and relations which in turn are indexed by contexts of free type variables. We sketch the definitions needed here, but refer to loc. cit. for details. An indexed first order logic fibration is a composition of fibrations

\xymatrix{ℙ \ar[r]^{r} & 𝔼 \ar[r]^{q} & 𝔹}

such that each restriction of r to a fibre of q is a first order logic fibration, i.e., a fibred bicartesian closed preorder, which models universal and existential quantification and equality, subject to the usual Beck-Chevalley conditions, but moreover subject to extra Beck-Chevalley conditions corresponding to reindexing in 𝔹. We also talk about (r, q) having products and coproducts with respect to classes of maps in 𝔹. This means that for every map u in the class in question r has respectively right and left adjoints to reindexing with respect to the cartesian lift of u. These left and right adjoints are subject to two variants of the Beck-Chevalley condition corresponding to maps in 𝔹 and 𝔼 respectively.

A pre-LAPL structure contains a model of PILL_{Y} that the logic will reason about. Moreover, it contains a logic fibration modelling the higher order logic present in LAPL. But LAPL is a higher order logic fibration because of the use of relations, and since relations do not exist naturally in PILL_{Y} models, a pre-LAPL structure contains an extra category called Ctx, which the reader should think of as containing the PILL_{Y} types as well as objects modelling collections of relations. In Definition 4.1 below the collections of objects of relations is given by the functor U, which should be thought of as a contravariant power set functor. The contexts of the mentioned fragment of LAPL are interpreted in Ctx, and the propositions of LAPL are modeled in the fibration Prop → Ctx.

4.1. Definition. A pre-LAPL-structure is

1. a diagram of categories and functors

\xymatrix{ &  & Prop \ar[d]^{r} \\ LinType \ar[drr]_{p} \ar[r] & Type \ar[l] \ar[dr] \ar[r]^{I} & Ctx \ar[d]^{q} \\  &  & Kind}

such that

• the diagram

\xymatrix{LinType \ar[dr]_{p} \ar[rr]_{G} & ⊥ & Type \ar[ll]_{F} \ar[dl] \\  & Kind}

is a model of PILL_{Y}.

• q is a fibration with fibred finite products

• (r, q) is an indexed first-order logic fibration [Birkedal and Møgelberg, 2005] which has products and coproducts with respect to projections K × Ω → K in Kind [Birkedal and Møgelberg, 2005], where Ω again is the p applied to the generic object.

• I is a faithful product-preserving map of fibrations.

2. a morphism of fibrations:

\xymatrix{(LinType ×_{Kind} LinType)^{fop} \ar[rr]^{U} \ar@{-->}[dr] &  & Ctx \ar[dl] \\  & Kind}

3. a family of bijections

Ψ_{X,A,B} : Hom_{Ctx_{K}}(X, U(A, B)) → Obj(Prop_{X×I(G(A)×G(B))})

for A and B in LinType_{K} and X in Ctx_{K} for some K, which

• is natural in X, A, B with respect to vertical maps

• commutes with reindexing functors; that is, if u : K′ → K is a morphism in Kind and f : X → U(A, B) is a morphism in Ctx_{K}, then

Ψ_{u^{∗}(X),u^{∗}(A),u^{∗}(B)}(u^{∗}(f)) = (ū)^{∗}(Ψ_{X,A,B}(f))

where ū is the cartesian lift of u.

Notice that Ψ is only defined on vertical morphisms.

In this definition LinType ×_{Kind} LinType is defined as the pullback

[figure: LinType ×_{Kind} LinType; LinType; p; LinType; p; Kind.]

Since U is uniquely defined by the requirements on the rest of the structure we will often refer to a pre-LAPL structure simply as the diagram in item 1. Very often we shall omit the indexing of Ψ to ease notation.

We shall use K, K′ … to denote objects of Kind, A, B, … to denote objects of LinType and X, Y, … to denote objects of Ctx.

We now explain how to interpret the fragment of LAPL excluding the relational interpretation of types (1) and excluding admissible relations in a pre-LAPL structure. A context

Ξ | x_{1} : σ_{1}, … x_{n}: σ_{n} | R_{1} : Rel(τ_{1}, τ′_{1}), …, R_{m}: Rel(τ_{m}, τ′_{m})

is interpreted in Ctx_{[[Ξ]]} as

∏_{i≤n}IG([[σ_{i}]]) × ∏_{j≤m}U([[τ_{j}]], [[τ′_{j}]]),

where the interpretations of the types is the usual interpretation of types in LinType → Kind.

4.2. Lemma. If Ξ | Γ | Θ is well formed and π: Ω^{n+1} → Ω^{n} is the projection onto the n first coordinates then [[Ξ, α | Γ | Θ]] = π^{∗}[[Ξ | Γ | Θ]].

For notational convenience we shall write [[Ξ | Γ | Θ ⊢ t: τ]] for the interpretation of t in Ctx, that is for

I([[Ξ | Γ; − ⊢ t: τ]]_{Type}) ∘ π

(note the subscript Type), where π is the projection

π: [[Ξ | Γ | Θ]] → [[Ξ | Γ | −]]

in Ctx_{[[Ξ]]}.

The propositions in the logic are interpreted in Prop. Most of the constructions of the logic are interpreted using standard methods from categorical logic, but we present the details here for completeness.

To interpret equality we define

[[Ξ | x: τ, y: τ ⊢ x =_{τ} y]] = ∐_{⟨id_{[[τ]]},id_{[[τ]]}⟩}(⊤),

where ∐_{⟨id_{[[τ]]},id_{[[τ]]}⟩} denotes the left adjoint to reindexing along ⟨id_{[[τ]]}, id_{[[τ]]}⟩: [[τ]] → [[τ]] × [[τ]]. Now we can define

[[Ξ | Γ | Θ ⊢ t =_{σ} u]] = ⟨[[Ξ | Γ | Θ ⊢ t]], [[Ξ | Γ | Θ ⊢ u]]⟩^{∗}[[Ξ | x: τ, y: τ ⊢ x =_{τ} y]].

To interpret ∀x: σ_{i_{0}}.ϕ, recall that a context Ξ | x_{1} : σ_{1}, …, x_{n}: σ_{n} | Θ is interpreted as

∏_{i≤n}IG[[σ_{i}]] × [[Θ]],

where [[σ_{i}]] is the usual interpretation of types in LinType and the product refers to the fibrewise product in Ctx. We may therefore interpret ∀x: σ_{i_{0}}.ϕ using the right adjoint to reindexing along the projection

π: ∏_{i≤n}IG[[σ_{i}]] × [[Θ]] → ∏_{i≠i_{0},i≤n}IG[[σ_{i}]] × [[Θ]].

Likewise, ∀R: Rel(σ, τ). ϕ is interpreted using right adjoints to reindexing functors related to the appropriate projection in Ctx. The existential quantifiers ∃x: σ_{i_{0}}.ϕ and ∃R: Rel(σ, τ.)ϕ are interpreted using left adjoints to the same reindexing functors.

Quantification over types ∀α.ϕ and ∃α.ϕ is interpreted using respectively right and left adjoints to π̄^{∗} where π̄ is the lift of the projection π : [[Ξ, α: Type]] → [[Ξ]] in Kind to Ctx. The existence of these adjoints is the requirement that (r, q) has products and coproducts. To be more precise, by Lemma 4.2 the cartesian lift of π is a map:

π̄: [[Ξ, α | Γ | Θ]] → [[Ξ | Γ | Θ]]

and we define

[[Ξ | Γ | Θ ⊢ ∀α. ϕ]] = ∏π̄[[Ξ, α | Γ | Θ ⊢ ϕ]],

where ∏π̄ is the right adjoint to π̄^{∗}.

Relations with domain σ and codomain τ in contexts Ξ | Γ | Θ are interpreted as maps from [[Ξ | Γ | Θ]] into U([[σ]], [[τ]]). The relation

Ξ | Γ | Θ, R: Rel(σ, τ) ⊢ R: Rel(σ, τ)

is interpreted as the projection, and

[[Ξ | Γ | Θ ⊢ (x: σ, y: τ). ϕ: Rel(σ, τ)]] = Ψ^{−1}([[Ξ | Γ, x: σ, y: τ | Θ ⊢ ϕ]]).

We now define the interpretation of ρ(t, s), for a relation ρ and terms t, s of the appropriate types. First, for Ξ | Γ | Θ ⊢ ρ: Rel(σ, τ), we define

[[Ξ | Γ, x: σ, y: τ | Θ ⊢ ρ(x, y)]] = Ψ([[Ξ | Γ | Θ ⊢ ρ: Rel(σ, τ)]]).

Next, if Ξ | Γ ⊢ t: σ, s: τ, then

[[Ξ | Γ | Θ ⊢ ρ(t, s)]] =
⟨⟨π, ⟨[[Ξ | Γ | Θ ⊢ t]], [[Ξ | Γ | Θ ⊢ s]]⟩⟩, π′⟩^{∗}[[Ξ | Γ, x: σ, y: τ | Θ ⊢ ρ(x, y)]],

where π, π′ are the projections

π: [[Ξ | Γ | Θ]] → [[Ξ | Γ]] π′: [[Ξ | Γ | Θ]] → [[Ξ | − | Θ]].

To interpret admissible relations, we need a little more structure than just a pre-LAPL structure. We need a subfunctor V of U, i.e., a map of fibrations V with domain and codomain as U and a fibred natural transformation V ⇒ U whose components are all monomorphic. Thus, for all K in Kind and all A, B in Ctx_{K}, we can consider V (A, B) as a subobject of U(A, B). We think of V (A, B) as the subobject of all admissible relations from A to B (since the isomorphism Ψ allows us to think of U(A, B) as the object of all relations).

Given such a V we can interpret S: AdmRel(σ, τ) as V ([[σ]], [[τ]]). Admissible relations ρ: AdmRel(σ, τ) are interpreted as maps into V ([[σ]], [[τ]]). For this to make sense we need, of course, to make sure that the admissible relations in the model in fact contain the relations that are admissible in the logic. We need to assume that of the functor V.

4.3. Definition. A pre-LAPL structure together with a subfunctor V of U is said to model admissible relations, if V is closed under the rules for admissible relations in [Birkedal et al., 2006].

We say that an implication

Ξ | Γ | Θ | ϕ_{1}, …, ϕ_{n} ⊢ ψ,

in the fragment of LAPL excluding the relational interpretation of types, holds in a given pre-LAPL structure with notion of admissible relations, if

⋀_{i≤n}[[Ξ | Γ | Θ ⊢ ϕ_{i}]] ≤ [[Ξ | Γ | Θ ⊢ ψ]]

where ≤ refers to the ordering in the preorder Prop_{[[Ξ|Γ|Θ]]}, and the ⋀ refers to the intersection in the same preorder.

4.4. Proposition. For any pre-LAPL structure with given notion of admissible relations the interpretation presented above of the fragment of LAPL excluding the relational interpretation of types is sound in the sense that any implication which is provable in the fragment of the logic also holds in the pre-LAPL structure.

Most of the proof of Proposition 4.4 is straightforward and very similar to the soundness proof of [Birkedal and Møgelberg, 2005], so we omit it here. Details can be found in [Møgelberg, 2005a].

As a consequence of Proposition 4.4 it makes sense to talk about the internal language of a pre-LAPL structure. In this language we may use types and terms from the PILL_{Y} model and propositions and relations from the model to form propositions using the constructions of the mentioned fragment of LAPL. We say that an implication of propositions formed in the internal language holds in the internal logic if it holds in the model.

4.5. Semantics of the relational interpretation of types. In this section we define the extra structure needed to interpret the relational interpretation of types. As in Ma & Reynolds work [Ma and Reynolds, 1992] this data is given by a reflexive graph

( \xymatrix{LinType \ar[d] \\ Kind} )  [figure] ( \xymatrix{LinAdmRelations \ar[d] \\ AdmRelCtx} ) , [figure] [figure]  (2)

this time of PILL models. But unlike in Ma & Reynold’s work, we construct the PILL model on the right hand side from the data of the pre-LAPL structure. For more on relations between our approach to models of parametricity and that of Ma & Reynolds, we refer to [Birkedal and Møgelberg, 2005].

We remark that the reason we need this extra structure is that the relational interpretation of types is not just an inductive construction definable only for types of pure PILL_{Y}. The functor going left to right in (2) will map each type in the PILL_{Y} model to its relational interpretation.

We now aim to define the fibration LinAdmRelations → AdmRelCtx from a given pre-LAPL structure with a notion of admissible relations. The idea is, that it should be a PILL model in which the objects of the total category are admissible relations in the sense of the pre-LAPL structure. The category AdmRelCtx is defined as the pullback

[figure: AdmRelCtx; ⟨∂_{0},∂_{1}⟩; Ctx; Kind × Kind; ×; Kind.]

To define the category LinAdmRelations we consider the construction of vertical comma category: suppose F is a fibred functor as in

\xymatrix{𝔻 \ar[dr]_{p} \ar[rr]^{F} &  & 𝔼 \ar[dl]^{q} \\  & 𝔹.}  (3)

The vertical comma category V (𝔼 ↓ F) has as objects vertical morphisms triples (E, D, ξ) where E, D are objects in 𝔼, 𝔻 respectively and ξ: E → F (D) is a vertical map in 𝔼. A morphism from (E, D, ξ) to (E′, D′, ξ′) is a pair of maps g: E → E′, f: D → D′ in 𝔼, 𝔻 respectively such that ξ′ ∘ g = F (f) ∘ ξ. Note that f, g need not be vertical. The vertical comma category construction has been studied before, and in fact there is a fibration V (𝔼 ↓ F) → 𝔹 making it a comma object in the 2-category of fibrations over 𝔹 [Jacobs, 1993, Sec 9.4], but that is not important for our application. Instead we need the following.

4.6. Lemma. Suppose F is a fibred functor as in (3), and denote by a: V (𝔼 ↓ F) → 𝔻 and b: V (𝔼 ↓ F) → 𝔼 the projections. Then b is a fibration and (a, q) is a morphism of fibrations:

\xymatrix{V (𝔼 ↓ F) \ar[r]^{a} \ar[d]_{b} & 𝔻 \ar[d]^{p} \\ 𝔼 \ar[r]^{q} & 𝔹.}

Now, the functor V in the definition of pre-LAPL structure induces a fibred functor

\xymatrix{(LinType × LinType)^{fop} \ar[rr]^{V′} \ar@{-->}[dr]_{_{(p×p)_{fop}}} &  & AdmRelCtx \ar[dl] \\  & Kind × Kind}

contravariant in each fibre. Using Lemma 4.6, define LinAdmRelations → AdmRelCtx to be V (AdmRelCtx ↓ V′)^{fop} → AdmRelCtx. From Lemma 4.6 we also obtain a fibred functor from LinAdmRelations → AdmRelCtx to LinType × LinType → Kind × Kind. We denote by ∂_{0}, ∂_{1} the two compositions of this fibred functor with the first and second projection respectively:

[figure: (; LinAdmRelations; AdmRelCtx; ); ∂_{0}; ∂_{1}; (; LinType; Kind; )] .

Writing out the construction we see that the objects of AdmRelCtx are triples (K, K′, X) where K, K′ are objects in Kind and X is an object of the fibre category Ctx_{K×K′}. Since such an object can be considered a context in the internal language of the pre-LAPL structure, we write them as K, K′ | X. The fibre of LinAdmRelations over an object K, K′ | X has as Objects: triples (ρ, A, B) where A and B are objects in LinType over K and K′

respectively and ρ is a vertical map

ρ: X → V (π^{∗}A, π^{′∗}B)

in Ctx. Here π, π′ are first and second projection respectively out of K × K′.

Morphisms: A morphism (ρ, A, B) → (ρ′, A′, B′) is a pair of morphism

(t: A ⊸ A′, u: B ⊸ B′)

in LinType_{K} and LinType_{K′} respectively, such that

Ψ(ρ) ≤ Ψ(V (t, u) ∘ ρ′)),

where we have left the inclusion of V into U implicit.

Expressed in the internal language of the pre-LAPL structure objects of the category LinAdmRelations are admissible relations in context, which we shall write as K, K′ | X ⊢ ρ: Rel(A, B) where A is in LinType_{K} and B is in LinType_{K′}, and vertical morphisms are pairs of morphisms t: A ⊸ A′, u: B ⊸ B′ preserving relations in the sense that

∀x: A, y: B . ρ(x, y) ⊃ ρ′(t x, u y)

holds. The fibred functors ∂_{0}, ∂_{1} map K, K′ | X ⊢ ρ: Rel(A, B) to A and B respectively. The following series of lemmas show that the fibration

LinAdmRelations → AdmRelCtx

is a PILL-model and that the maps ∂_{0}, ∂_{1} are morphisms of PILL-models. The proofs of these lemmas express most of the necessary constructions using LAPL as an internal language. In fact the proofs will show that the PILL-model structure of

LinAdmRelations → AdmRelCtx

is given by the relational interpretations of the type constructors of PILL_{Y}, as defined in [Birkedal et al., 2006].

4.7. Lemma. The fibration LinAdmRelations → AdmRelCtx has a fibrewise SMCCstructure and the two maps ∂_{0}, ∂_{1} are fibred strict symmetric monoidal functors.

Proof. The symmetric monoidal closed structure is given by the operations ⊗, ⊸ defined on admissible relations in LAPL for ρ: AdmRel(σ, τ), ρ′: AdmRel(σ′, τ′) as

ρ ⊸ ρ′ = (f: σ ⊸ σ′, g: τ ⊸ τ′). ∀x: σ. ∀y: τ. ρ(x, y) ⊃ ρ′(fx, gy).

and

ρ ⊗ ρ′ = (f_{σ,τ}, f_{σ′,τ′})^{∗}(∀(α, β, R: AdmRel(α, β)). (ρ ⊸ ρ′ ⊸ R) ⊸ R),

where f_{σ,τ} : σ ⊗ τ ⊸ ∏α. (σ ⊸ τ ⊸ α) ⊸ α is the canonical map defined as

f_{σ,τ} x = let x′ ⊗ x′′: σ ⊗ τ be x in Λα. λ^{∘}h: σ ⊸ τ ⊸ α. h x′ x′′.

The unit for the tensor product is the admissible relation I_{Rel}: AdmRel(I, I) defined as

I_{Rel} = (f, f)^{∗}(∀(α, β, R: AdmRel(α, β)). R ⊸ R),

where f: I ⊸ ∏α. α ⊸ α is defined as λ^{∘}x: I. let ⋆ be x in id, for id = Λα. λ^{∘}x: α. x.

As proved in [Birkedal et al., 2006] these map admissible relations to admissible relations and so do indeed define constructions on LinAdmRelations → AdmRelCtx. It is an easy exercise to show that these define functors, and that ⊗ defines a symmetric monoidal structure (this simply involves showing that the maps of the symmetric monoidal structure on LinType preserve relations).

We show that ρ ⊸ − is right adjoint to −⊗ρ. Since we are given a similar adjunction in LinType, all we need to show is that

(t, s): ρ ⊸ (ρ′ ⊸ ρ′′)

iff

(t̂, ŝ): ρ ⊗ ρ′ ⊸ ρ′′,

where t̂, ŝ are the maps corresponding to t, s in the adjunction on LinType. Suppose first that

(t, s): ρ ⊸ (ρ′ ⊸ ρ′′) and x(ρ ⊗ ρ′)y.

The definition of the latter says exactly that, for all (t, s): ρ ⊸ (ρ′ ⊸ ρ′′), we must have ρ′′(t̂x, ŝ y).

Now, suppose (t̂, ŝ): ρ ⊗ ρ′ ⊸ ρ′′ and xρy ∧ x′ρ′y′. Since ρ ⊗ ρ′(x ⊗ x′, y ⊗ y′) also ρ′′(t̂(x ⊗ x′), ŝ(y ⊗ y′)). Hence, since t̂(x ⊗ x′) = t x x′ (likewise for s), we are done.

4.8. Lemma. The fibration LinAdmRelations → AdmRelCtx has a fibred comonad structure. This structure extends to a fibred linear structure, and the maps ∂_{0}, ∂_{1} preserve all this structure on the nose.

Proof. The operation ! on relations is defined in [Birkedal et al., 2006] as

(f_{σ}, f_{τ})^{∗}∀(α, β, R: Rel(α, β)). (ρ → R) ⊸ R.

where f_{σ}: !σ ⊸ ∏α. (σ → α) ⊸ α is defined as

λ^{∘}x: !σ. Λα. λ^{∘}g: σ → α. g(x).

and for any ρ, ρ′ the relation ρ → ρ′ is defined as

ρ → ρ′ = (f: σ → σ′, g: τ → τ′). ∀x: σ, y: τ. ρ(x, y) ⊃ ρ′(f(!x), g(!y)).

We need to check that ! defines a functor, i.e., that if (f, g): ρ ⊸ ρ′, then (!f,!g): !ρ ⊸ !ρ′. From [Birkedal et al., 2006] we know that it suffices to show (!f,!g): ρ →!ρ′, i.e.,

∀x, y.!ρ(!x,!y) ⊃!ρ′((!f)(!x), (!g)(!y)).

But this holds since (!f)(!x) =!(f(x)).

The rest of the proof is a simple check that the counit and comultiplication as well as the underlying structure maps of the fibred linear structure on LinType all preserve relations.

4.9. Lemma. The fibration LinAdmRelations → AdmRelCtx has products in the base, a generic object and, writing Ω′ for the fibration applied to the generic object, simple products with respect to projections in AdmRelCtx of the form (K, K′ | X) × Ω′ → (K, K′ | X). The maps ∂_{0}, ∂_{1} preserve this structure.

Proof. The category AdmRelCtx has products:

(K_{1}, K′_{1} | X_{1}) × (K_{2}, K′_{2} | X_{2}) = K_{1} × K_{2}, K′_{1} × K′_{2} | π^{∗}(X_{1}) × π^{′∗}(X_{2})

by [Jacobs, 1999, Proposition 9.2.1].

The generic object of the fibration is the triple (id_{V (π^{∗}O,(π′)^{∗}O)}, O, O) where π, π′: Ω × Ω → Ω are the projections, since a morphism into that object from K, K′ | X in AdmRelCtx is a pair of maps (f : K → Ω, g : K′ → Ω) in Kind together with a morphism from X to V (π^{∗}(f^{∗}O), (π′)^{∗}(g^{∗}O)) in Ctx_{K×K′}.

We now show that the fibration has the mentioned products. The generic object can be expressed in the internal language as α, β | − | R: AdmRel(α, β), and so we write a product

(K, K′ | X) × (α, β | − | R: AdmRel(α, β))

in AdmRelCtx as (K, α; K′, β | X, R: AdmRel(α, β)). We must show that for any projection in AdmRelCtx of the form π: (K, α; K′, β | X, R: AdmRel(α, β)) → (K; K′ | X) the weakening functor π^{∗} mapping a relation K, K′ | X ⊢ ω: AdmRel(A, A′) to the relation

K, α; K′, β | X, R: AdmRel(α, β) ⊢ ω: AdmRel(A, A′)

has a right adjoint. We define this right adjoint to map a relation

K, α; K′, β | X, R: AdmRel(α, β) ⊢ ρ: AdmRel(B, B′)

to the relation

K, K′ | X ⊢ ∀(α, β, R: AdmRel(α, β)). ρ: AdmRel((∏α: Type. B), (∏β: Type. B′))

defined in [Birkedal et al., 2006] to be

(x, y). ∀α, β: Type. ∀R: AdmRel(α, β). (xα)ρ(yβ).

In the PILL_{Y} model LinType → Kind polymorphic types are modelled using products with respect to projections K × Ω → Ω. This gives for any object A in LinType_{K} a bijective correspondence between morphisms t: A ⊸ B in LinType_{K×Ω} and morphisms t̂: A ⊸ ∏α. B in LinType_{K}. In fact t̂ can be expressed in PILL_{Y} as

K | − ⊢ t̂= λ^{∘}x: A. Λα. (t x): A ⊸ ∏α. B.

Given a relation K, K′ | X ⊢ ω: AdmRel(A, A′) and a pair of morphisms t: A ⊸ B, u: A′ ⊸ B′, one can easily check in LAPL that the pair (t, u) preserves relations iff (t̂, û) does, i.e.,

K, α; K′, β | x : A, y : A′ | X, R: AdmRel(α, β) | xωy ⊢ (t x)ρ(u y)

iff

K, K′ | x : A, y : A′ | X | xωy ⊢ ∀α, β: Type. ∀R: AdmRel(α, β). (t̂x α)ρ(û y β),

and so the correspondence between (t, u) and (t̂, û) gives a bijective correspondence between maps π^{∗}ω ⊸ ρ in the fibre of LinAdmRelations over

K, α; K′, β | X, R: AdmRel(α, β)

and maps ω ⊸ ∀(α, β, R: Rel(α, β)). ρ in the fibre over K; K′ | X proving that we have in fact defined a product.

The Lemmas 4.7, 4.8, 4.9 collectively state the following.

4.10. Proposition. The fibration LinAdmRelations → AdmRelCtx is a PILL model

This model need not be a PILL_{Y} -model, since for general pre-LAPL structures Y does not necessarily preserve relations.

4.11. Definition. An LAPL structure is a pre-LAPL structure modeling admissible relations, together with a map of PILL-models

[figure: (; LinType; Kind; ); J; (; LinAdmRelations; AdmRelCtx; )]

extending ∂_{0}, ∂_{1} to a reflexive graph, i.e., ∂_{0} ∘ J = ∂_{1} ∘ J = id.

Full LAPL can be interpreted in any LAPL structure. To see this we need to show how to interpret the rule

α_{1}, …, α_{n} ⊢ σ(α⃗): Type Ξ | Γ | Θ ⊢ ρ_{1} : AdmRel(τ_{1}, τ′_{1}), …, ρ_{n}: AdmRel(τ_{n}, τ′_{n})

Ξ | Γ | Θ ⊢ σ[ρ⃗]: AdmRel(σ(τ⃗), σ(τ′))

We first define

[[α⃗, β⃗ | − | R⃗: AdmRel(α⃗, β⃗) ⊢ σ[R⃗]]] = J([[α⃗ | σ(α⃗)]])

Note that this makes sense since J is required to preserve products in the base and generic objects, and so J([[α⃗ ⊢ σ(α⃗)]]) is an admissible relation from σ(α⃗) to σ(β⃗) in context [[α⃗; β⃗ | R⃗: AdmRel(α⃗, β⃗)]]. The general σ[ρ] is defined as follows: first reindex J([[α⃗ ⊢ σ(α⃗)]]) to the right Kind context using

⟨[[τ⃗]], [[τ′]]⟩ : [[Ξ]] → Ω^{2n},

thus obtaining

[[Ξ | − | R⃗: AdmRel(τ⃗, τ′) ⊢ σ[R⃗]: Rel(σ(τ⃗), σ(τ′))]] = ⟨[[τ⃗]], [[τ′]]⟩^{∗}J([[α⃗ ⊢ σ(α⃗)]])

and finally we define

[[Ξ | Γ | Θ ⊢ σ[ρ⃗]: AdmRel(σ(τ⃗), σ(τ′))]] =
[[Ξ | − | R⃗: AdmRel(τ⃗, τ′) ⊢ σ[R⃗]]] ∘ [[Ξ | Γ | Θ ⊢ ρ⃗: AdmRel(τ⃗, τ′)]].

where by [[Ξ | Γ | Θ ⊢ ρ⃗: AdmRel(τ⃗, τ′)]] we mean the pairing

⟨[[Ξ | Γ | Θ ⊢ ρ_{1}]], …, [[Ξ | Γ | Θ ⊢ ρ_{n}]]⟩.

4.12. Remark. Linear Abadi & Plotkin Logic can be modified to include arities of parametricity other than binary. To accomodate such modifications in the definition of LAPL structure, the domain of the functors U and V in the definition of pre-LAPL structure with notion of admissible relations must be changed accordingly.

We define the notion of an implication of LAPL holding in an LAPL structure similarly to the notion of implication holding in a pre-LAPL structure as we did before Proposition 4.4.

4.13. Theorem. [Soundness] The interpretation given above of LAPL in LAPL structures is sound in the sense that any implication provable in LAPL also holds in any LAPL structure.

Proof. This theorem extends Proposition 4.4, and like for the proof of Proposition 4.4 we refer to [Møgelberg, 2005a] for details, but do sketch the soundness proof of a few rules.

The rules capturing the inductive definition of relational interpretation of types all hold since J preserves SMCC-structure, generic objects, simple products and !.

Concerning the axiom stating (∏α. (α → α) → α)(Y, Y) , notice that J is required to be a functor. This means that it maps [[Y]]: I ⊸ [[∏α. (α → α) → α]] to a morphism from I_{Rel} to the relational interpretation of ∏α. (α → α) → α. By the requirement, that (J, ∂_{0}, ∂_{1}) is a reflexive graph, this map must be ([[Y]], [[Y]]). Since I_{Rel}(⋆, ⋆) and [[Y]](⋆) = Y we get (∏α. (α → α) → α)(Y, Y).

4.14. Completeness. The completeness theorem states an inverse to the soundness theorem, namely that any LAPL implication holding in any LAPL structure is also provable in LAPL. In fact an even stronger result holds:

4.15. Theorem. [Completeness] There exists an LAPL structure with the property that any formula of LAPL over pure PILL_{Y} holds in this model iff it is provable in LAPL.

Note that Theorem 4.15 only concerns LAPL as a logic on pure PILL_{Y}. One can also formulate LAPL as a logic for the internal language of any PILL_{Y} model, but we do not have a proof of a similar completeness result for this case. The main problem is that we have no way of constructing, for general models of PILL_{Y}, a relational interpretations as in Section 4.5.

Proof. We construct the LAPL structure syntactically, giving the categories in question the same names as in the diagrams of the definitions of pre-LAPL and LAPL structures. The PILL_{Y} model in the LAPL structure is a fibred version of the syntactic DILL constructed in [Barber, 1997].

• The category Kind has as objects PILL_{Y} kind contexts Ξ. A morphism from Ξ to α_{1}, …, α_{n} is an n-vector of PILL_{Y} types (σ_{1}, …, σ_{n}) such that all σ_{i} are well-formed in context Ξ. Composition is by substitution.

• Objects in the fibre of LinType over Ξ are well-formed types in this context. Morphisms in this fibre from σ to τ are equivalence classes of terms t such that Ξ | −; x: σ ⊢ t: τ, under the equivalence relation on PILL_{Y} terms given by external equality. Composition is by substitution, and reindexing with respect to morphisms in Kind is by substitution.

• Objects in the fibre of Type over Ξ are well-formed sequences of types in this context. Morphism in this fibre from σ_{1}, …, σ_{n} to τ_{1}, …, τ_{m} are equivalence classes of sequences of terms (t_{i})_{i≤m}, such that for each i the term

Ξ | x⃗: σ⃗; − ⊢ t_{i}: τ_{i}

is well-formed, under the equivalence relation relating sequences (t_{i}) and (t′_{i}) if, for each i, t_{i} is externally equal to t′_{i}. Reindexing with respect to morphisms in Kind is by substitution.

• The functor LinType → Type maps a morphism −; x: σ ⊢ t: τ to x: σ; − ⊢ t: τ. The functor going the other way maps a sequence of objects (σ_{i}) to ⊗_{i}!σ_{i}. It maps a morphism represented by (t_{i}) from (σ_{i}) to (τ_{i}) to the morphism represented by

Ξ | −; y: ⊗_{i}!σ_{i} ⊢ let ⊗_{i} x′_{i}: ⊗_{i}!σ_{i} be y in let !x⃗ be x′ in ⊗_{i}!t_{i}.

• The category Ctx has as objects in the fibre over Ξ well-formed contexts of LAPL: Ξ | Γ | Θ. A vertical morphism from Ξ | Γ | Θ to

Ξ | Γ′ | R_{1} : Rel(σ_{1}, τ_{1}), …, R_{n}: Rel(σ_{n}, τ_{n}), S_{1} : AdmRel(σ′_{1}, τ′_{1}), …, S_{m}: AdmRel(σ′_{m}, τ′_{m}) is an equivalence class of triples, consisting of a vertical morphism Ξ | Γ → Ξ | Γ′ in Type, a sequence of definable relations (ρ_{1}, …, ρ_{n}), and a sequence of admissible relations (ω_{1}, …, ω_{m}), such that Ξ | Γ | Θ ⊢ ρ_{i}: Rel(σ_{i}, τ_{i}) and Ξ | Γ | Θ ⊢ ω_{i}: AdmRel(σ′_{i}, τ′_{i}). The equivalence relation relates two such morphisms represented by the same type morphism and the definable relations (ρ_{1}, …, ρ_{n}) and (ρ′_{1}, …, ρ′_{n}) and admissible relations (ω_{1}, …, ω_{m}) and (ω′_{1}, …, ω′_{m}), respectively, if, for each i, j, the formulas ρ_{i} ≡ ρ′_{i} and ω_{j} ≡ ω′_{j} are provable in the logic, where, as usual, ρ_{i} ≡ ρ′_{i} is short for

∀x: σ_{i}, y: τ_{i}. ρ_{i}(x_{i}, y_{i}) ⊃⊂ ρ′_{i}(x_{i}, y_{i}),

and likewise for ω_{j} ≡ ω′_{j}. The inclusion functor I is the obvious one. Reindexing is by substitution.

• The fibre of the category Prop over a context Ξ | Γ | Θ has as objects equivalence classes of formulas Ξ | Γ | Θ ⊢ ϕ: Prop, under the equivalence relation given by provable equivalence in LAPL. Each fibre of Prop is a preorder, ordered by implication in the logic: ϕ ≤ ψ iff ϕ ⊃ ψ holds in LAPL. Reindexing is done by substitution: each map in Ctx can be written as a composition of a vertical map followed by a cartesian lift of a map in Kind, and reindexing with respect to cartesian lifts of morphisms from Kind is done by substitution in type-variables, whereas reindexing with respect to vertical maps in Ctx is by substitution in term variables and relation variables.

An easy fibred version of the completeness proof in [Barber, 1997] shows that Kind, Type, LinType together with the functors described above form a PILL_{Y} model. The fibration Ctx → Kind clearly has fibred products formed by appending contexts, and the inclusion functor I is clearly faithful and product-preserving.

We need to prove that Prop → Ctx → Kind is an indexed first-order logic fibration with products and coproducts with respect to simple projections in Kind. The fibrewise bicartesian structure is given by ∨, ∧, ⊃, ⊥, ⊤. Fibred simple products and coproducts are given by quantifying over relations and variables, simple products in the composite fibration is given by quantifying over types. We can in fact prove that the composite fibration has all indexed products and coproducts (in particular, that it has equality).

Suppose (t⃗, ρ⃗) represents a vertical morphism from Ξ | x⃗: σ⃗ | R⃗ to Ξ | y⃗: τ⃗ | S⃗ in Ctx (the vectors R⃗, S⃗ consist of both relations and admissible relations, and the vector ρ⃗ is a concatenation of the corresponding vectors of relations and admissible relations from the definition above). We can then define the product functor in Prop as:

\begin{matrix}∏_{(t⃗,ρ⃗)}(Ξ | x⃗ | R⃗ ⊢ ϕ(x⃗, R⃗)) = \\ Ξ | y⃗ | S⃗ ⊢ ∀x⃗. ∀R⃗(t⃗x⃗ = y⃗ ∧ (ρ⃗(x⃗, R⃗) ≡ S⃗) ⊃ ϕ(x⃗, R⃗)). \end{matrix}

We define coproduct as:

\begin{matrix}∐_{(t⃗,ρ⃗)}(Ξ | x⃗ | R⃗ ⊢ ϕ(x⃗, R⃗)) = \\ Ξ | y⃗ | S⃗ ⊢ ∃x⃗. ∃R⃗. t⃗x⃗ = y⃗ ∧ ρ⃗(x⃗, R⃗) ≡ S⃗ ∧ ϕ(x⃗, R⃗)). \end{matrix}

We remark that the special case of equality in the model is the obvious

(Ξ | Γ, x: σ | Θ ⊢ ϕ) ↦ (Ξ | Γ, x: σ, y: σ | Θ ⊢ ϕ ∧ x =_{σ} y)

The fibred functor U of item 2 in Definition 4.1 is defined as

U(σ, τ) = R: Rel(σ, τ)

and

U(t: σ ⊸ σ′, u: τ ⊸ τ′) = Ξ | R: Rel(σ′, τ′) ⊢ (x: σ, y: τ). R(tx, uy),

where x, y are fresh variables.

The required isomorphism Ψ maps Ξ | Γ | Θ ⊢ ρ: Rel(σ, τ) to Ξ | Γ, x: σ, y: τ | Θ ⊢ ρ(x, y). The functor V is defined as

V (σ, τ) = R: AdmRel(σ, τ)

and

V (t: σ ⊸ σ′, u: τ ⊸ τ′) = Ξ | R: AdmRel(σ′, τ′) ⊢ (x: σ, y: τ). R(tx, uy).

We have defined a pre-LAPL structure modeling admissible relations. If we construct AdmRelCtx as in the definition of LAPL structure, we obtain:

Objects: α⃗, β⃗ | Γ | R⃗: AdmRel(σ⃗(α⃗), τ⃗(β⃗)), R⃗′: Rel(σ′(α⃗), τ′(β⃗)).

Morphisms: A morphism from

α⃗, β⃗ | Γ | R⃗: AdmRel(σ⃗(α⃗), τ⃗(β⃗)), R⃗′: Rel(σ′(α⃗), τ′(β⃗))

to

α′, β⃗′ | Γ′ | S⃗: AdmRel(ω⃗(α′), κ⃗(β⃗′)), S⃗′: Rel(ω′(α′), κ′(β⃗′))

consists of two morphism in Kind:

μ⃗ : α⃗ → α′

and

ν⃗ : β⃗ → β⃗′,

a morphism from α⃗, β⃗ | Γ to α⃗, β⃗ | Γ′[μ⃗, ν⃗/α′, β⃗′] in LinType_{α⃗,β⃗}, and a sequence of admissible relations ρ⃗ and a sequence of relations ρ′ such that, for all i,j,

α⃗, β⃗ | Γ | R⃗: AdmRel(σ⃗(α⃗), τ⃗(β⃗)), R⃗′: Rel(σ′(α⃗), τ′(β⃗)) ⊢ ρ_{i}: AdmRel(ω_{i}(μ⃗), κ_{i}(ν⃗)) α⃗, β⃗ | Γ | R⃗: AdmRel(σ⃗(α⃗), τ⃗(β⃗)), R⃗′: Rel(σ′(α⃗), τ′(β⃗)) ⊢ ρ′_{j}: Rel(ω′_{j}(μ⃗), κ′_{j}(ν⃗)).

As in Ctx these morphisms are identified up to provable equivalence of the relations.

The fibre of LinAdmRelations over an object

α⃗, β⃗ | Γ | R: AdmRel(σ⃗(α⃗), τ⃗(β⃗)), R⃗′: Rel(σ′(α⃗), τ′(β⃗))

in AdmRelCtx becomes:

Objects: Equivalence classes of admissible relations

α⃗, β⃗ | Γ⃗ | R: AdmRel(σ⃗(α⃗), τ⃗(β⃗)), R⃗′: Rel(σ′(α⃗), τ′(β⃗)) ⊢ ρ: AdmRel(σ(α⃗), τ(β⃗)).

Morphisms: A morphism from ρ: AdmRel(σ(α⃗), τ(β⃗)) to ρ′: AdmRel(σ′(α⃗), τ′(β⃗)) is a pair of morphisms t : σ ⊸ σ′, u : τ ⊸ τ′ such that it is provable in the logic that:

∀x: σ. ∀y: τ. ρ(x, y) ⊃ ρ′(tx, uy)

We will construct the map J as a map of fibred linear categories from LinType → Kind to LinAdmRelations → AdmRelCtx as follows. On the base categories J is defined on objects as

J(α_{1}, …, α_{n}) = α_{1}, …, α_{n}; β_{1}, …, β_{n} | R_{1} : AdmRel(α_{1}, β_{1}), …, R_{n}: AdmRel(α_{n}, β_{n}),

where the β⃗ are fresh variables. We define J on the objects of the total categories (and on the morphisms of the base category) as

J(α⃗ ⊢ σ: Type) = α⃗, β⃗ | R⃗: AdmRel(α⃗, β⃗) ⊢ σ[R]: AdmRel(σ(α⃗), σ(β⃗)).

To define J on morphisms of the fibre categories, suppose α⃗ | −; − ⊢ t: σ ⊸ τ. We define J(t) = (t, t). To see that (t, t) in fact is a map from σ[R⃗] to τ[R⃗], notice that the Logical Relations Lemma [Birkedal et al., 2006, Lemma 1.39] tells us that

Λα⃗. t(∏α⃗. σ ⊸ τ)Λα⃗. t,

which means exactly that (t, t): σ[R⃗] ⊸ τ[R⃗].

The rules for the relational interpretation of types tell us that J is a strict fibred symmetric monoidal closed functor preserving products and ! on the nose. Since the counit and comultiplication of the fibred comonad on LinAdmRelations → AdmRelCtx are simply (ϵ, ϵ) and (δ, δ), for ϵ and δ the counit and comultiplication of LinType → Kind respectively, it is clear that J preserve these as well.

Now, by definition, a formula holds in this LAPL structure iff it is provable LAPL.

5. Parametric LAPL structures

This section defines the notion of parametric LAPL structure. These are LAPL structures in which the identity extension schema holds and which satisfy a condition called very strong equality. Identity extension allows us to reason using parametricity in the internal logic of the LAPL structure, and very strong equality allows us to transfer the results from the internal logic to results about the PILL_{Y} model. The need for very strong equality is perhaps best illustrated by an extreme case: suppose we are given an LAPL structure in which Prop = Ctx and the fibration r: Prop → Ctx is the identity functor. In this case the fibres of the fibration are all trivial, and so any proposition in LAPL holds in such a model. In particular, being able to prove that two vertical morphism of LinType with the same domain and codomain are equal in the internal language of the LAPL structure says nothing about them being equal morphisms in LinType.

5.1. Definition. A preorder fibration 𝔼 → 𝔹 modelling equality has very strong equality if for every two morphisms f, g in 𝔹 with same domain and codomain, f = g holds in the logic of the fibration only if f and g are in fact equal. An LAPL structure has very strong equality if each restriction of r: Prop → Ctx to a fibre of q: Ctx → Kind has very strong equality.

As argued in [Birkedal and Møgelberg, 2005] very strong equality implies that the two extensionality schemes

∀α, β: Type. ∀f, g: α ⊸ β. (∀x: α. f(x) =_{τ} g(x)) ⊃ f =_{α⊸β} g
∀x, y: ∏α. σ. (∀α: Type. x α =_{σ} y α) ⊃ x =_{∏ α.σ} y

hold in the internal logic of the LAPL structure.

5.2. Definition. A parametric LAPL structure is an LAPL structure with very strong equality in which identity extension holds in the internal logic.

5.3. Solving recursive domain equations in parametric LAPL structures. This section identifies the semantic notion of recursive domain equation that can be solved using parametricity in LAPL structures. This can be also seen as an example of how we can reason in the internal logic of parametric LAPL structures and use very strong equality to transfer these results to results about the PILL_{Y} model in question.

Below we shall use the notation A^{B} for the closed structure in symmetric monoidal closed categories. This is meant to simplify otherwise lengthy notation.

5.4. Definition. An endofunctor F : 𝔹^{op} × 𝔹 → 𝔹, for 𝔹 a linear category, is called strong if there exists a natural transformation t_{A,B,A′,B′} :!(A^{A′})⊗!((B′)^{B}) ⊸ F (A′, B′)^{F (A,B)} preserving identity and composition:

[figure: I; !îd_{A}⊗!îd_{B}; ∘; \begin{matrix} \\ id & F A \end{matrix}; ∘; !(A^{A})⊗!(B^{B}); t_{A,B,A,B}; ∘; F (A, B)^{F (A,B)}]  !(A^{A′})⊗!((B′)^{B})⊗!((A′)^{A′′})⊗!((B′′)^{B′}) ^{comp}^{∘}_{t⊗t}_{∘}  !(A^{A′′})⊗!((B′′)^{B})_{t}_{∘} F (A′, B′)^{F (A,B)} ⊗ F (A′′, B′′)^{F (A′,B′)} _{comp} _{∘}F (A′′, B′′)^{F (A,B)}.

The natural transformation t is called the strength of the functor F.

One should note that t in the definition above represents the morphism part of the functor F in the sense that it makes the diagram

[figure: I; !f̂⊗!ĝ; ∘; { \atop F (f,g)}; ∘; !(A^{A′})⊗!((B′)^{B}); t_{A,B,A′,B′}; ∘; F (A′, B′)^{F (A,B)}]  (4)

commute, for any pair of morphisms f: A′ ⊸ A, g: B ⊸ B′. This follows from the commutative diagram

[figure: I; îd; ∘; !îd⊗!îd; ∘; !f̂⊗!ĝ; ∘; !A^{A}⊗!B^{B}; t; ∘; !(A^{f})⊗!(g^{B}); ∘; F (A, B)^{F (A,B)}; F (f,g)^{F (A,B)}; ∘; !A^{A′}⊗!(B′)^{B}; t; ∘; F (A′, B′)^{F (A,B)}.]

In fact, (4) shows that we can define the action of F on morphisms from the strength.

5.5. Definition. If 𝔼 → 𝔹 is a fibred SMCC, then a fibred functor

\xymatrix{𝔼^{fop} ×_{𝔹} 𝔼 \ar[dr] \ar[rr]^{F} &  & 𝔼 \ar[dl] \\  & 𝔹}

is called strong fibred if there exists a fibred natural transformation t from

!((=)^{(−)})⊗!((=′)^{(−′)}) to F (−, =′)^{F (=,−′)}

satisfying commutativity of the two diagrams of Definition 5.4 in each fibre. The natural transformation t is called the strength of the functor F.

The fibred strength t is a natural transformation between two fibred functors

\xymatrix{𝔼 ×_{𝔹} 𝔼^{fop} ×_{𝔹} 𝔼^{fop} ×_{𝔹} 𝔼 \ar[rr] \ar[dr] &  & 𝔼 \ar[dl] \\  & 𝔹}

For example, in the case of a PILL_{Y} -model, the interpretation of any inductively constructed type α, β ⊢ σ(α, β) with α occurring only negatively and β only positively induces a strong fibred functor, since as described in [Birkedal et al., 2006], for each such type we can define a closed term

t: ∏α, β, α′, β′. (α′ ⊸ α) → (β ⊸ β′) → σ(α, β) ⊸ σ(α′, β′)

The object part of the functor F is then defined as

F (A, B) = [[σ(A, B)]]

and the strength s of the functor is defined as

(s_{K})_{A,A′,B,B′} = [[K | −; − ⊢ t A A′ B B′]].

The morphism part of the functor is induced by the strength.

In fact, in a sense these are the only strong fibred functors on PILL-models.

5.6. Lemma. Suppose

\xymatrix{LinType^{fop} ×_{Kind} LinType \ar[rr]^{F} \ar[dr] &  & LinType \ar[dl] \\  & Kind}

is a strong fibred functor on a PILL-model. Then there exists a type α, β ⊢ σ and a closed term

t: ∏α, β, α′, β′. (α′ ⊸ α) → (β ⊸ β′) → σ(α, β) ⊸ σ(α′, β′)

in the internal language of LinType → Kind inducing F.

Proof. Let O: LinType_{Ω} denote the generic object of the fibration LinType → Kind. For each type A: LinType_{K} there exists a map K → Ω, which we will denote Â such that Â^{∗}O = A.

Define σ = F ([[α, β ⊢ α]], [[α, β ⊢ β]]). Then

F (A, A′) = F (⟨Â, Â′⟩^{∗}([[α, β ⊢ α]], [[α, β ⊢ β]])) = ⟨Â, Â′⟩^{∗}σ

for any pair of types (A, A′) ∈ (LinType^{fop} ×_{Kind} LinType)_{K}, since F is fibred. In the internal language K ⊢ σ(A, A′) is interpreted as ⟨Â, Â′⟩^{∗}σ and so indeed σ induces the action of F on objects.

Let s denote the strength of the fibred functor F. Consider the component

(s_{Ω^{4}})_{[[α,β,α′,β′⊢α]],[[α,β,α′,β′⊢β]],[[α,β,α′,β′⊢α′]],[[α,β,α′,β′⊢β′]]}

and denote it by t′. In the internal language, t′ is a term, and we can consider the polymorphic term

− ⊢ t = Λα. Λβ. Λα′. Λβ′. t′: ∏α, β, α′, β′. (α′ ⊸ α) → (β ⊸ β′) → (σ(α, β) ⊸ σ(α′, β′)).

We just need to show that the strength induced by the term t is in fact s, but

[[K ⊢ t A A′ B B′]] = ⟨Â, Â′, B̂, B̂′⟩^{∗}t′ = (s_{K})_{A,A′,B,B′}

since s is preserved by reindexing.

5.7. Theorem. In a parametric LAPL structure, for any strong fibred functor F there exists a closed type rec α. F (α, α) such that

F (rec α. F (α, α), rec α. F (α, α)) ≅ rec α. F (α, α)

in LinType_{1} for 1 the terminal object of Kind. The isomorphism is an initial dialgebra for the functor F_{1} : LinType_{1}^{op} × LinType_{1} → LinType_{1}.

Moreover, for any object K in Kind,

F (!_{K}^{∗}(rec α. F (α, α)),!_{K}^{∗}(rec α. F (α, α))) ≅!_{K}^{∗}(rec α. F (α, α)),

where !_{K} is the unique map K → 1 in Kind, holds in LinType_{K} and is an initial dialgebra for F_{K}.

Proof. Since by Lemma 5.6 we can express F in the internal language, the construction of solutions to recursive domain equations and the proofs of correctness in [Birkedal et al., 2006] goes through in the internal language of the LAPL structure, if we substitute the functorial interpretation of types as constructed in PILL_{Y} by the polymorphic term provided by Lemma 5.6. This gives the closed type rec α. F (α, α) and the isomorphism F (rec α. F (α, α), rec α. F (α, α)) ≅ rec α. F (α, α) provable in LAPL. Finally, by very strong equality the isomorphism F (rec α. F (α, α), rec α. F (α, α)) ≅ rec α. F (α, α) not only holds in LAPL but also in the category LinType_{1}.

The rest of the theorem can be proved likewise.

5.8. Parametrized recursive type equations. An inductively constructed type α_{1}, β_{1}, …, α_{n}, β_{n} ⊢ σ with 2n free type variables, in which the variables α⃗ occur only negatively and the variables β⃗ only positively induces a fibred functor

\xymatrix{(LinType^{fop} ×_{Kind} LinType)^{n} \ar[rr]^{F} \ar[dr] &  & LinType \ar[dl] \\  & Kind.}

On the other hand Definition 5.5 can easily be extended to define what it means that a functor F as above is strong fibred, and Lemma 5.6 extends to show that such strong fibred functors correspond to types σ as above and closed polymorphic terms of type

∏α⃗, β⃗, α′, β⃗′. (α′_{1} ⊸ α_{1}) → (β_{1} ⊸ β′_{1}) → … → (α′_{n} ⊸ α_{n}) → (β_{n} ⊸ β′_{n}) → σ(α⃗, β⃗) ⊸ σ(α′, β⃗′)

in the internal language. The following theorem is then the corresponding extension of Theorem 5.7 obtained using the analysis of [Birkedal et al., 2006].

5.9. Theorem. In a parametric LAPL structure, for any strong fibred functor

\xymatrix{(LinType^{fop} ×_{Kind} LinType)^{n+1} \ar[rr]^{F} \ar[dr] &  & LinType \ar[dl] \\  & Kind.}

there exists a strong fibred functor

\xymatrix{(LinType^{fop} ×_{Kind} LinType)^{n} \ar[rr]^{FixF} \ar[dr] &  & LinType \ar[dl] \\  & Kind.}

and a fibred natural isomorphism

F (A_{1}, B_{1}, …, A_{n}, B_{n}, FixF (B_{1}, A_{1}, …, B_{n}, A_{n}), FixF (A_{1}, B_{1}, …, A_{n}, B_{n}))
≅ FixF (A_{1}, B_{1}, …, A_{n}, B_{n}).

Moreover, if G is a strong fibred functor

\xymatrix{(LinType^{fop} ×_{Kind} LinType)^{m} \ar[rr]^{G} \ar@{-->}[dr] &  & (LinType^{fop} ×_{Kind} LinType)^{n} \ar[dl] \\  & Kind.}

then Fix(F ∘ (G × id)) = FixF ∘ G.

The universal condition satisfied by the functor FixF is a parametrized version of dinaturality. It has been described in [Birkedal et al., 2006], but for completeness we repeat it here in a semantic formulation.

For any object K ∈ Kind, all objects A_{1}, … A_{n}, B_{1}, …, B_{n}, C, C′ in the fibre LinType_{K} and all morphisms

\begin{matrix}g: F (A_{1}, B_{1}, …, A_{n}, B_{n}, C′, C) ⊸ C \\ g′: C′ ⊸ F (B_{1}, A_{1}, …, B_{n}, A_{n}, C, C′) \end{matrix}

also in the fibre LinType_{K}, there exist unique maps h, h′ making the diagrams

F (A_{1}, B_{1}, …, FixF (B_{1}, A_{1}, …), FixF (A_{1}, B_{1}, …))_{F (A_{1},B_{1},...,A_{n},B_{n},h′,h)}_{∘}  ^{≅} ^{∘}FixF (A_{1}, B_{1}, …, A_{n}, B_{n})_{h}_{∘} F (A_{1}, B_{1}, …, A_{n}, B_{n}, C, C)  _{g}  _{∘}C

C′  ^{g′}  ^{∘}_{h′} _{∘}  F (B_{1}, A_{1}, …, B_{n}, A_{n}, C, C′)_{F (B_{1},A_{1},...,B_{n},A_{n},h,h′)}_{∘} F (B_{1}, A_{1}, …, FixF (A_{1}, B_{1}, …), FixF (B_{1}, A_{1}, …)) _{≅} _{∘}FixF (B_{1}, A_{1}, …, B_{n}, A_{n})

commute in the fibre category LinType_{K}.

6. Conclusions

We have defined the category-theoretic notion of LAPL structure, and proved that this is a sound and complete notion of model for LAPL, a logic for parametricity and domain theory. We propose that parametric LAPL structures be used as a notion of domain theoretic models of parametric polymorphism. This notion is useful, because, as we have showed, semantic versions of the consequences for parametricity provable logically hold in parametric LAPL structures.

In forthcoming papers we show that the notion of parametric LAPL structure is also a general notion of domain theoretic models of parametricity, by giving a series of examples of parametric LAPL structures. These examples include a model constructed using partial equivalence relations over a domain theoretic model of the untyped lambda calculus, Simpson and Rosolini’s construction of models in intuitionistic set theory, a model constructed using the syntax of Lily and a general parametric completion process as in [Robinson and Rosolini, 1994]. In all these cases the notion of admissible relation is interpreted differently, and a central part of each of these verifications, is to show that the concrete notions of admissible relations satisfy the axioms of [Birkedal et al., 2006].

Acknowledgments

We gratefully acknowledge discussions with Shin-ya Katsumata, Milly Maietti, Gordon Plotkin, John Reynolds, Pino Rosolini and Alex Simpson. Thanks also to the two anonymous referees for helpful suggestions.

References

Barber, A. (1997). Linear Type Theories, Semantics and Action Calculi. PhD thesis, Edinburgh University.

Benton, P. (1995). A mixed linear and non-linear logic: Proofs, terms and models (preliminary report). Technical report, University of Cambridge.

Bierman, G. M., Pitts, A. M., and Russo, C. V. (2000). Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Fourth International Workshop on Higher Order Operational Techniques in Semantics, Montréal, volume 41 of Electronic Notes in Theoretical Computer Science. Elsevier.

Birkedal, L. and Møgelberg, R. E. (2005). Categorical models of Abadi-Plotkin’s logic for parametricity. Mathematical Structures in Computer Science, 15(4):709–772.

Birkedal, L., Møgelberg, R. E., and Petersen, R. L. (2006). Linear Abadi & Plotkin logic. Logical Methods in Computer Science, 2.

Birkedal, L., Møgelberg, R. E., and Petersen, R. L. (2007). Domain-theoretical models of parametric polymorphism. Theor. Comput. Sci, 388(1-3):152–172.

Freyd, P. (1990a). Algebraically complete categories. In Carboni, A., Pedicchio, M. C., and Rosolini, G., editors, Category Theory. Proceedings, Como 1990, volume 1488 of Lecture Notes in Mathematics, pages 95–104. Springer-Verlag.

Freyd, P. (1990b). Recursive types reduced to inductive types. In Proceedings of the fifth IEEE Conference on Logic in Computer Science, pages 498–507.

Freyd, P. (1991). Remarks on algebraically compact categories. In Fourman, M. P., Johnstone, P., and Pitts, A. M., editors, Applications of Categories in Computer Science. Proceedings of the LMS Symposium, Durham 1991, volume 177 of London Mathematical Society Lecture Note Series, pages 95–106. Cambridge University Press.

Huwig, H. and Poigné, A. (1990). A note on inconsistencies caused by fixpoints in a cartesian closed category. Theoretical Computer Science, 73:101–112.

Jacobs, B. (1993). Comprehension categories and the semantics of type dependency. Theoretical Computer Science, 107:169–207.

Jacobs, B. (1999). Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Publishers B.V.

Ma, Q. and Reynolds, J. (1992). Types, abstraction, and parametric polymorphism, part 2. In Brookes, S., Main, M., Melton, A., Mislove, M., and Schmidt, D., editors, Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 1–40. Springer-Verlag.

Maietti, M. E., Maneggia, P., de Paiva, V., and Ritter, E. (2005). Relating categorical semantics for intuitionistic linear logic. Applied Categorical Structures, 13(1):1–36.

Maneggia, P. (2004). Models of linear polymorphism. PhD thesis, University of Birmingham.

Møgelberg, R. E. (2005a). Category theoretic and domain theoretic models of parametric polymorphism. PhD thesis, IT University of Copenhagen.

Møgelberg, R. E. (2005b). Parametric completion for models of polymorphic intuitionistic / linear lambda calculus. Technical Report TR-2005-60, IT University of Copenhagen.

Møgelberg, R. E., Birkedal, L., and Petersen, R. L. (2005). Categorical models of PILL. Technical Report TR-2005-58, IT University of Copenhagen.

O’Hearn, P. W. and Tennent, R. D. (1995). Parametricity and local variables. Journal of the ACM, 42(3):658–709.

Pitts, A. M. (2000). Parametric polymorphism and operational equivalence. Mathematical Structures in computer Science, 10:321–359.

Plotkin, G. (1993a). Second order type theory and recursion. Notes for a talk at the Scott Fest.

Plotkin, G. and Abadi, M. (1993). A logic for parametric polymorphism. In Typed lambda calculi and applications (Utrecht, 1993), volume 664 of Lecture Notes in Comput. Sci., pages 361–375. Springer, Berlin.

Plotkin, G. D. (1993b). Type theory and recursion (extended abstract). In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, page 374, Montreal, Canada. IEEE Computer Society Press.

Reynolds, J. (1983). Types, abstraction, and parametric polymorphism. Information Processing, 83:513–523.

Robinson, E. and Rosolini, G. (1994). Reflexive graphs and parametric polymorphism. In Abramsky, S., editor, Proc. 9th Symposium in Logic in Computer Science, pages 364–371, Paris. I.E.E.E. Computer Society.

Rosolini, G. and Simpson, A. (2004). Using synthetic domain theory to prove operational properties of a polymorphic programming language based on strictness. Manuscript.

Tse, S. and Zdancewic, S. (2004). Translating dependency into parametricity. In ICFP ’04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming, pages 115–125. ACM Press.

A. Fibrations of opposite fibres

This appendix describes how the construction taking a fibration p: 𝔼 → 𝔹 producing a fibration of opposite fibres p^{fop} : 𝔼^{fop} → 𝔹^{fop}, defined in the text for split fibrations only, can be extended to general fibrations. (The construction of 𝔼^{fop} depends not only on 𝔼 but also on p, but we leave p implicit in notation.) Recall that since split fibrations p as above correspond to functors p̂: 𝔹^{op} → Cat (where Cat is the category of categories) via the Grothendieck construction, we could define p^{fop} in this special case to be the fibration corresponding to (−)^{op} ∘ p̂, where (−)^{op} : Cat → Cat is the functor mapping a category to its opposite.

Suppose now p: 𝔼 → 𝔹 is a fibration which is not assumed to be split. Recall that any map f: A → B in 𝔼 can be written as a composition g ∘ h where g is cartesian and h is vertical. This composition is not unique, but for any given two such compositions g ∘ h, g′ ∘ h′ there exists an isomorphism k such that g′ ∘ k = g and h′ = k ∘ h. Note that k is necessarily vertical. This information tells us, that we can construct an isomorphic copy of 𝔼 which has the same objects as 𝔼 but with morphisms from A to B being equivalence classes of triples (C, h: A → C, g: C → B) where h is vertical and g is cartesian, under the equivalence relation relating (C, h, g) to (C′, h′, g′) if there exists an isomorphism k: C → C′ such that g′ ∘ k = g and h′ = k ∘ h.

Using this we can define 𝔼^{fop} by just reversing the vertical arrows, defining it to be:

Objects: Objects of 𝔼

Morphisms: A morphism from A to B is an equivalence class of triples (C, h: C → A, g: C → B) where h is vertical and g is cartesian, under the equivalence relation relating (C, h, g) and (C′, h′, g′) if there exists an isomorphism k: C → C′ such that g = g′ ∘ k and h = h′ ∘ k.

Composition in 𝔼^{fop} is defined as follows: given a map from A to B represented by (D, h, g) and a map from B to C represented by (D′, h′, g′) we define the composition of the two to be the map represented by (D′′, h ∘ h′′, g′ ∘ g′′) as in the diagram

\xymatrix{A \\ D \ar[u]^{h} \ar[r]^{g} & B \\ D′′ \ar[u]^{h′′} \ar[r]^{g′′} & D′ \ar[u]_{h′} \ar[r]^{g′} & C}

where g′′ is a cartesian lift of p(g) and h′′ is the unique vertical map making the square commute. The functor p^{fop} : 𝔼^{fop} → 𝔹 is defined to map a morphism represented by (C, h, g) to p(g). The next theorem tells that all this structure is well defined. The proof is omitted.

A.1. Theorem. The above defines a category 𝔼^{fop} and a fibration p^{fop} : 𝔼^{fop} → 𝔹. Moreover, (−)^{fop} extends to an endofuntor on the category Fib(𝔹) of fibrations over 𝔹.

Lars Birkedal and Rasmus E. Møgelberg IT University of Copenhagen Rued Langgaardsvej 7 DK–2300 Copenhagen S Denmark

Rasmus L. Petersen Department of Computer Science Queen Mary, University of London London E1 4NS UK

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/20/7/20-07.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Georgia Southern University: gseal@georgiasouthern.edu

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown (at) btinternet.com Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca