A categorical model for HM(X)

Martin Wehr and Martin Sulzmann

28. August 1997

1 Introduction

Motivation and results of the work.

2 Background

This article uses results from the area for categorical logic. The aim of categorical logic is to identify the algebraical structures for models for various logics. Our motivation is the axiomatisation of constraint type theories. We hope that by making use of the vast body of results in categorical logic we reach a clean and convincing axiomatisation of constraint type theories.

Lambek and Scott [LP86] wrote an introduction into categorical logic. They made use of cartesian closed categories and topoi. Further categorical structures we may need are doctrines, hyperdoctrines, indexed categories and the new applications of fibrations. Categorical logic in condensed form with focus on modelling type theories can also be found in Pitts [Pit] handbook article. The two handbook articles [Fou77] and [Rey77] reveal the logical meaning of doctrines and topoi The latest textbook on topoi and sheaves is [Moe92].

Roy Croles book [Cro93] describes categorical models of type theories. He uses the technique of indexed categories to model second and higher order polymorphism. His slogan “type judgements as morphisms and substitution as composition” is one of the guide lines of categorical logic which we will follow.

The textbook of Barr-Wells [Bar90] offers the definition of fibrations and the Grothendieck construction. Phoa [Pho92] gives an introduction in the connections between fibrations and topoi used in categorical logic. It appears as Pavlovic [Pav90] was the first work to use fibrations for modelling type theory. in Jacobs thesis [Jac91] (short form [Jac93])includes an introduction to fibrations and its connections to indexed categories. Jacobs work is the main inspiration for our approach. Jacobs extends the fibrational approach for modelling type theories to the full lambda cube [Jac95b] and to subtyping [Jac95a].

Moggi’s monadic models for the λ-calculi [Mog89, Mog91] may be used to analyse first order polymorphism which is our goal.

To finish our modelling task modelling types is not enough we have to model constraints and have to glue both models together to gain models of constraint type theories. constraints are explained informally by examples in the frame of constraint logic programming CLP(X) [Coh90, JM94].

The work of concurent constraints is the basis for our adaption of the axiomatization for constraints. Saraswat et. al. [Sar90, SRP91] uses constraints in the computation method of concurent constraints and offers an algebraic definition and an operational definition.

The connection to categorical logic was made in cooperation with Seely et. al. [PSSS94, MPSS95].

3 Overview

For the full categorical setting of HM(X) there is a sequence of categories to consider. Each of the categories are obtained by adding some more structure to the previous category.

We start with the category S modelling substitutions. The category S can be seen as the free cartesian category over the syntactic types. On top of that we build the category L of the simply typed lambda calculus. L can be seen as an indexed category or a fibration where the base category is S. By quotienting of L we have to build the the category L_{i} of implicitly typed lambda calculus. By enriching L with polymorphic term variables we get the category F of first order polymorphic lambda calculus. Via a similar (but extended on first order polymorphism) quotienting as for category L_{i} we get the category H corresponding to the Hindley Milner system of first order implicit polymorphism.

Parallel to the fibration L which is the hyperdoctrine over the substitutions S we need a doctrine C over the same base category S representing the predicates or constraints over the substitutions. Logicaly the meaning of the three categories (S, C, L) can be understood as given a propositional logic (corresponding to S) we can extend this logic by including new parameters in two ways, either with predicates to a first order logic (corresponding to C) or with propositional variables to second order logic (corresponding to L). The quantifiers are then given by adjoints to the reindexing functor of projections. This is the core of categorical logic.

Now the final construction has to connect the two fibrations the one related to type theory (in our development L, L_{i}, F, H) and the other related to constraints over types (i.e C) to one fibration modelling constrained type theories. The connection of H and C can then recognized as the categorical model of HM(X) where the constraint parameter X is the category C.

3.1 Intuition

We start our development with an overview on the intuition behind the several categories. For every category we have clearly to understand the objects and morphisms but also the closure properties are interesting and finaly some categories are constructed by quotienting so we should understand the equivalence relation used.

Substitutions S objects Finite sets Δ of type variables α, β.

morphisms Types τ, τ′ and substitutions S, U

closure properties The category is free cartesian where the singelton set I = {α} generates every object Δ = I^{n}. So every type τ is is a morphism τ : tv(τ) → I and every substitution can be seen as a tuple of types.

S =< τ_{1}, …, τ_{n} >: cod(S) → dom(S) iff S = {α_{1} ↦ τ_{1}, …, α_{n} ↦ τ_{n}}

Further unification corresponds to the existence of equalizers and antiunification correponds to the coproduct in the slice category S ↓ I

simply typed lambda calculus L objects Types τ or contexts Γ.

morphisms Typed term Γ ⊢ e : τ corespond to morphisms e : Γ → τ in this category

closure properties The category is cartesian closed. The fine structure is given by the fibration to the base category S implicit typed lambda calculus L_{i}

objects Types τ or contexts Γ. morphisms Tuples (Γ, e) with a typotheses and and implicit typed term

SΓ ⊢ e : τ. equivalence relation Instantiations of typed terms. closure properties The same closure properties as as in category L but

there is a minimal morphism in L representing the equivalence class of a morphism in L_{i}. So there is an order induced on the set of morphisms of L by the instatiation (that is the reindexing functor associated with a substitution). The property of a minimal morphism representing the equivalence class is the principal type property in type theory. The fine structure of the category L_{i} can be given by observing three fibrations. The quotienting of the type fibration L leads to the fibration of type instatiations and substitutions. Further there are two obvious projection fibrations associated with the tuple (Γ, e) where the fiber L_{i}_{Γ} is the type theory with instantiable assumptions Γ and the fiber L_{i}_{e} is the poset of possible typings for term e.

first order polymorphism F

objects Objects of L that is contexts of monomorphic term variables are extended with polymorphic term variables. The type fibration L relates to each object Γ the set of used type variables Δ. Each polyvariable is a tuple (τ, Δ′) where Δ′ is disjunct to Δ and represents the bound type variables of τ

morphisms Polyvariables can only be used in the calculus if instantiated. So they correpond to elements from the equivalence class of morphisms in L_{i} which is representeted by an idendity in L. If instatiated then polyvariables can be abstracted in F.

closure properties We have again a cartesian closed category. Maybe the operation of “instantiation-only-on-polyvariables” can be represented as a monad. Then F should be constructed as the Kleisli category with use of the instantiation monad and the L category. This should lead to a monadic semantic in Moggi’s style and would give new insights in the categorical modeling of implicit polymorphism.

implicit first order polymorphism H this category should result through quotienting from category F in the similar way as category L_{i} was obtained from category L. The equivalence relation used in the earlier construction should be refined. In the first quotienting we needed the implicit qoutient of a monotype theory which was done by globaly instantiating. In the quotient contruction for category H we need instantiation quotient of the polytype theory F so there is localy instantiation neccesary at each use of an polyvariable.

closure properties Again we have a fine structure given by the three fibrations similar to category L_{i}. And further the principal type property of the Hindley Milner system (we can identify category H with the HMsystem) should give a minimal representant property for the equivalence classes related to morphisms in H

4 categorical semantic of HM(X)

In the following we describe the subsystems of HM(X) in order to construct the full system. Along with the description of the parts of HM(X) we develop the categorical semantic of the parts and connect them to the full system.

4.1 Analysis of the substitution category

Given a set S and a natural number n ∈ ℕ_{0} the S^{n} denotes the set of n-tuples with elements of S as entries. In this case () is the unique element of S^{0} and S^{∗} is the set of finite tuples.

Given a finite set Δ = {α_{1}, …, α_{n}} of type variables we define Ty(Δ) to be the set of types defined recursively by

• α ∈ Ty(Δ) if α ∈ Δ

• τ ⇒ τ′ ∈ Ty(Δ) if τ, τ′ ∈ Ty(Δ)

We also use ⇒ to denote the exponential in categories not to confuse it with the arrow → used in morphisms.

So the objects of S can be seen as the elements of ℕ (the set of natural numbers). For every 1 ≤ i ≤ n there is a projection π_{i}^{n} : n → 1 corresponding to the type variable α_{i} ∈ V_{n} = {α_{1}, …, α_{n}} for V_{n} the finite set of n distinct type variables. Further there exists a cartesian product in S to represent substitutions. So < τ_{1}, …, τ_{m} >: n → m is the substitution S = {τ_{1}/α_{1}, …, τ_{m}/α_{m}} for tv(τ_{i}) ∈ V_{m} or the other way round |S| : cod(S) → dom(S) is the morphism in S related to the substitution. Notice that in case cod(S) ⊆ V_{n} \ V_{m} the substitution S is idempotent.

Given types τ, τ′ with type variable condition tv(τ) ⊆ V_{n} and tv(τ′) ⊆ V_{n}. If we look a the associated morphisms τ, τ′ : n → 1 we can identfy the most general unifier of these morphisms a the categorical notion of an equalizer g : m → n.

[figure: m; g; n; τ; τ′; 1; k; s; u]

The definition of most general unifier gives the following characterisation (in morphism notation):

∃g : m → n ∀u : k → n. (τ′ ∘ u = τ ∘ u ⟹ ∃s : k → m u = g ∘ s)

that is g is mgu iff every unifier u of the types τ, τ′ factorizes through g (i.e ∃s.u = g ∘ s). The equalizer is defined up to isomorphism that is relative to renaming substitutions (where a renaming is a permutation of type variables).

A type τ′ is a generalisation of type τ in short τ′ ≤ τ iff there exists a substitution S such that Sτ′ = τ. We say also that τ is an instance of τ′. The categorical notion of an type instance in category S is an arrow in the comma category S ↓ 1

\begin{matrix}τ′ ≤ τ ⇔ ∃S.Sτ′ = τ ⇔ \begin{matrix}τ′ : m → 1 \\ τ : n → 1 \\ ∃S : n → m \\ τ′ ∘ S = τ : n → 1 \end{matrix} \\ ⇔ [figure: n; S; τ; m; τ′; 1] in S ⇔ S : τ → τ′ in S ↓ 1 \end{matrix}

Antiunification of two types τ, τ′ is defined as the most specialized generalisation τ′′ of the two types. So the antiunifier τ′′ of two types τ, τ′ is the greatest lower bound in the preorder ≤ of instantiation. The following two condition are fullfilled for τ′′:

(lower bound) τ′′ ≤ τ and τ′′ ≤ τ′.

(greatest lower bound) (τ_{3} ≤ τ ∧ τ_{3} ≤ τ′) ⟹ τ_{3} ≤ τ′′.

Taking that ingredients together we get a coproduct diagram in the category S ↓ 1

\xymatrix{ & τ_{3} \\ τ \ar[ur] \ar[r] & τ′′ \ar@{-->}[u] & τ′ \ar[ul] \ar[l]}

The empty Variable set ∅ is the terminal object of S. There is only one unique morphism from every type variable set to ∅ t.i. the empty morphism. Further the singelton type variable set I = V_{1} = {α} has the property that for every object Δ exists a number n ∈ ℕ_{0} with Δ = I^{n} and for every morphism s : Δ′ → Δ exist morphism τ_{i} : Δ′ → I (for 1 ≤ i ≤ n) with s =< τ_{1}, …, τ_{n} >. So S is the free cartesian category generated by I and the function symbol ⇒ of arity 2.

4.2 The category L

For every type variable set Δ we define the free cartesian closed category L_{Δ} generated by the set Ty(Δ). The objects of L_{Δ} are elements Γ ∈ Ty(Δ)^{∗} called typotheses.

For every object Γ = (τ_{1}, …, τ_{n}) there exist n projections π_{i} : Γ → τ_{i} which are the projections of the cartesian product. For any two morphisms e_{1} : Γ → τ_{1} and e_{2} : Γ → τ_{2} there exists a morphism < e_{1}, e_{2} >: Γ → τ_{1} × τ_{2} such that π_{i}∘ < e_{1}, e_{2} >= e_{i}.

To each morphism e : Γ.τ → τ′ there exists a unique morphism Λ(e) : Γ → τ ⇒ τ′. Further there exists a natural transformation ev_{τ,τ′} : τ ⇒ τ′ × τ → τ′ such that ev_{τ,τ′}∘ < Λ(e) ∘ π_{1}, π_{2} >= e where π_{2} : Γ.τ → τ and π_{1} : Γ.τ → Γ are the two projections related to the product Γ.τ.

The category S of substitutions interconnects the L_{Δ} categories. For every typotheses Γ ∈ L_{Δ} and morphism S : Δ′ → Δ in S (i.e. a substitution with cod(S) = Δ′ and dom(S) = Δ) we get by instantiation a new typoheses S^{∗}Γ ∈ L_{Δ′} Further for every morphism e : Γ → τ in L_{Δ} we get a morphism S^{∗}e : S^{∗}Γ → S^{∗}τ in the category L_{Δ′}. By preservation of composition and identity we see that every substitution S : Δ′ → Δ operates as a functor S^{∗} : L_{Δ} → L_{Δ′}. Notice the reversing of the type variable sets.

Now we put this altogehter by the Grothendieck construction to get a sum category L and a fibration 𝕃 : L → S. The objects of L are tuples (Δ, Γ) with typotheses Γ an object of L_{Δ}. the morphisms of L are tuples (S, e) : (Δ, Γ) → (Δ′, Γ′) such that S : Δ → Δ′ is a morphism of S and e : Γ → S^{∗}Γ′ is a morphism of L_{Δ}. Composition of (S, e) : (Δ_{1}, Γ_{1}) → (Δ_{2}, Γ_{2}) and (S′, e′) : (Δ_{2}, Γ_{2}) → (Δ_{3}, Γ_{3}) is given by (S′, e′) ∘ (S, e) = (S′ ∘ S, S^{∗}e′ ∘ e). So the fibration 𝕃 is given by the first projection and the fibers are the categories L_{Δ}. For a typotheses Γ ∈ L_{Δ} and a substitution S : Δ′ → Δ the cartesian arrow is given by \overline{S}(Γ) : (Δ′, S^{∗}Γ) → (Δ, Γ)

proof: \overline{S}(Γ) is cartesian. Assume a given morphism (S′, e′) : (Δ′′, Γ′) → (Δ, Γ) this is to have a typed term Γ′ ⊢ e : S′Γ in L_{Δ′′}. Further we assume that S′ factorizes to S′ = S ∘ R for a morphism R : Δ′′ → Δ′ in S. So clearly the composition of morphism (R, e′) : (Δ′′, Γ′) → (Δ′, S^{∗}Γ) that is the same typed term represented as Γ′ ⊢ e : RSΓ and the second projection of \overline{S}(Γ) which is the instantiation of the idendity derivation SΓ ⊢ SΓ in L completes the diagramm for cartesian morphisms. □

4.3 The category C

The category C of constraints is build similar to category L. Let Σ be a signature of predicates with given arity so that Ω(Δ) is the set of tokens build by a predicate symbol of Σ and types τ ∈ Ty(Δ) as arguments. Now we can either introduce the binary operation ∧ on tokes which is commutative, associative and absorbtive, or introduce equvialently the set of constraints as P(Δ) ⊆ P^{f}Ω(Δ) where P^{f}A denotes the finite subsets of a set A.

Let ⊢^{e} ⊆ P(Δ) × Ω(Δ) be an entailment relation with C, D denoting sets of tokens and the following axioms :

(Ax1) C ⊢^{e} t if t ∈ C

(Ax2) (∀t ∈ D.C ⊢^{e} t) and D ⊢^{e} t′ ⟹ C ⊢^{e} t′

We extend ⊢^{e} to a relation P(Δ) × P(Δ) by defining C ⊢^{e} D iff (∀t ∈ D.C ⊢^{e} t). With this ingredients we build the free catesian category C_{Δ} of constraints. The objects are constraint sets C, D ∈ P(Δ). The morphisms are judements C ⊢^{e} D. Every substitution induces a reindexing functor S^{∗} : C_{Δ′} → C_{Δ}. Again we construct a sum category C and a fibration ℂ : C → S. The objects of C are tuples (Δ, C) with C ∈ C_{Δ}. The morphism (S, m) : (Δ, C) → (Δ′, D) are given by a substitution S : Δ → Δ′ and a judgement m : C ⊢^{e} S^{∗}D in C_{Δ} cartesian morphisms are given by instantiation \overline{S}(C) = (S, SC ⊢^{e} SC) : (SC, Δ′) → (C, Δ) i.e. for a constraint C ∈ C_{Δ} and a substitution S : Δ′ → Δ we get an instantiation of the identical constraint derivation.

4.3.1 Operational semantic of constraints

Now lets have a closer look on the presentation of decidable constraints. The decision algorithm will be given by a term reduction system. The confluence and normalisation property of the term reduction system gives the decision procedure. We describe the ingredients for such a term reduction system by definition of its parts and by illustration with the example of the unification constraint system.

set of tokens Ω(Δ) The unification tokens are equations on Ty(Δ) denoted as < τ = τ′ >

set of constraints P(Δ) = P^{f}Ω(Δ)

set of normal tokens nΩ(Δ) The normal tokens are occurence free variable bindings. So normal tokes have form < α = τ > with α ∉ tv(τ).

set of redex tokens rΩ(Δ) = Ω(Δ) \ nΩ(Δ)

set of redex constraints rP(Δ) with rΩ(Δ) ⊆ rP(Δ) ⊆ P(Δ). A unification redex constraint is of form < α = τ > ∧ t where variable binding tokens is normal.

set of normalised constraints nP(Δ) = {C ∈ P(Δ)|P^{f}(C) ∩ rP(Δ) = ∅} so in a normalised constraint there appears no redex constraint.

set of reduction rules R(Δ) = {C → D|C ∈ rP(Δ) and D ∈ P(Δ×Δ′)}. Notice that the reduct constraint D may extend the set of used type variables by Δ′. There are two reduction rules for the unification :

(congruence) < τ_{1} → τ′_{2} = τ′_{1} → τ′_{2} > ⟶ < τ_{1} = τ′_{1} > ∧ < τ_{2} = τ′_{2} >
(subst)  < α = τ > ∧t  ⟶ < α = τ > ∧[τ/α]t

The rule for unifying two variable bindings

(unify) < α = τ > ∧ < α = τ′ > ⟶ < τ = τ′ >

is an instance of rule (subst).

reduction relation of constraint is defined as C′ ∧ C → C′ ∧ D if C → D ∈ ⋃_{Δ} R(Δ).

inconsistent constraints iP(Δ) = {C|C →^{∗} false }

Now we can use the term reduction as a semantics for constraints. We need the reductiuon system to be confluent and normalising. In that case we use a normalisation procedure to compute for every constraint C ∈ P(Δ) a normalised constraint \underline{C} ∈ nP(Δ×Δ′). All the constraint systems used in HM(X) will be extensions of the unification system. Further the the normal form \underline{C} will be one of the four following forms :

inconsistency \underline{C} = false in this case inconsistent constraints are implied by C. We will denote this as C ↑.

satisfaction \underline{C} = true we will denote this in short as C ↓.

solution \underline{C} =< α_{1} = τ_{1} > ∧ ⋯ ∧ < α_{n} = τ_{n} > whith \{α_{1}, …, α_{n}\} = Δ and tv(τ_{i}) ⊆ Δ′. So the normalised constraint presents a idempotent substitution S_{C} : Δ′ → Δ. This case states that every satisfying substitution S : Δ′′ → Δ with SC ↓ can be factorised by S_{C} t.i ∃S′ : Δ′′ → Δ′.S = S′; S_{C}. The term reduction system has the principal constraint property if S_{C} is the smallest possible solution substitution.

refinement \underline{C} =< α_{1} = τ_{1} > ∧ ⋯ ∧ < α_{n} = τ_{n} > ∧D with D ∈ nP(Δ′). So \underline{C} can be seen as a constrained substitution (D, S_{C}) : Δ′ → Δ which states that every satisfying substitution S : Δ′′ → Δ with SC ↓ can be factorised by (D, S_{C}) t.i ∃S′ : Δ′′ → Δ′.S = S′; S_{C} and S′D ↓. There is a obvious ordering on constraint subtitutions. For (C, S) : Δ′ → Δ and (D, S′) : Δ′′ → Δ we define :

(C, S) ≤ (D, S′) iff ∃S′′ : Δ′′ → Δ′.S′ = S′′; S and D ⊢^{e} S′′C

The term reduction system has the principal refinement property if (D, S_{C}) is the smallest possible refinement substitution.

4.3.2 Structure of constraint systems

Now we go one step back to rethink the structure of a constraint system. Assume we are given the set of constraints P(Δ) for every type variable set Δ. To have a structure on the constraints we have to introduce an entailment relation. We can introduce this entailment relation axiomatically. In the following we will construct entailment relations by use of adding structure.

Definition 1 We call iP(Δ) ⊂ P(Δ) a set of inconsistent constraints if

∀C ∈ P(Δ).D ∈ iP(Δ) ⟹ C ∧ D ∈ iP(Δ)

Given this inconsistency predicate we can interpret a constraint C ∈ P(Δ) by the non-inconsistent constraints related to C.

⟦C⟧_{I} = {D|C ∧ D ∉ iP(Δ)}

We use the interpretation to define an entailment relation C ⊢^{i} D iff ⟦C⟧_{I} ⊆ ⟦D⟧_{I}.

We add some more structure to the constraint sets by denoting a subset of constraints behaving like maps.

Definition 2 For type variable sets Δ and Δ′ we call the elements M of the set M(Δ′, Δ) ⊂ P(Δ × Δ′) map constraints if there is a map M^{∗} : P(Δ × Δ′) → P(Δ′) satisfying the following laws:

(id) true ∈ M(Δ′, Δ)
(map) ∀C ∈ P(Δ × Δ′).M ∧ C ∈ iP(Δ × Δ′) ⇔ M^{∗}(C) ∈ iP(Δ′)

Using the law (id) we introduce ∃_{Δ′}C ∈ P(Δ′) as notational convention for true^{∗}(C) with C ∈ P(Δ × Δ′). Using absorbtion of ∧ and (map) we get idempotentence M^{∗}(C) ∈ iP(Δ′) ⇔ M^{∗}(M^{∗}(C)) ∈ iP(Δ′). Using down closedness of inconsistency D ∈ iP(Δ) ⟹ C ∧ D ∈ iP(Δ) and (map) we get antimonotony C ∈ iP(Δ′) ⟹ M^{∗}(C) ∈ iP(Δ′). We define the set of all maps as Map = ⋃_{Δ,Δ′} M(Δ′, Δ). Given the map constraints we can interpret a constraint C ∈ P(Δ) by the non-inconsistent map constraints related to C.

⟦C⟧_{M} = {M|C ∧ M ∉ iP(Δ) and M ∈ Map}

We use the interpretation to define a entailment relation C ⊢^{m}D iff ⟦C⟧_{M} ⊆ ⟦D⟧_{M}.

Assume the set of constraints P(Δ) is given with a term reduction system as described above. Further this system is an extension of the unification system.

Definition 3 (entailment reduction) The reduction on constraints (further denoted as →^{c}) can be extended as a reduction on entailments. We define the reduction C ⊢ D →^{e} C′ ⊢ D′ by the following rules:

(redl) C →^{c} C′ ⟹ C ⊢ D ⟶^{e} C′ ⊢ D
(redr) D →^{c} D′ ⟹ C ⊢ D ⟶^{e} C ⊢ D′
(entail) C ∧ C′ ⊢ D ∧ C′ ⟶^{e} C ∧ C′ ⊢ D if C′ is no unification constraint
(substl) C∧ < τ = τ′ > ⊢ D ⟶^{e} C∧ < τ = τ′ > ⊢ D∧ < τ = τ′ >
(substr) C ⊢ D∧ < τ = τ′ >⟶^{e} C∧ < τ = τ′ > ⊢ D∧ < τ = τ′ >

If the reduction system on constraints is strongly normalising then we denote by \underline{C} ⊢ \underline{D} the normalform of C ⊢ D. The normalform can be used to define a entailment relation :

C ⊢^{t}D iff \underline{C} ⊢ \underline{D} and \underline{D} = false ⟹ \underline{C} = false

A constraint system given with a term reduction system has a natural notion of inconsictency iP(Δ) = {C|C →^{∗} false }. Using this incosistency predicate we get a by above construction a entailment relation ⊢^{i} . The term reduction system is called extensional if ⊢^{t} ⊆ ⊢^{i} .

A constraint system which is an extension of the unification system has a natural notion of map constraints. A constraint M ∈ P(Δ × Δ′) is called a map constraint M ∈ M(Δ′, Δ) if it can be solved in form Δ′ × Δ t.i. its normalform \underline{M} has form < α_{1} = τ_{1} > ∧ ⋯ ∧ < α_{n} = τ_{n} > whith {α_{1}, …, α_{n}} = Δ and tvτ_{i} ⊆ Δ′. Now above we constructed a entailment ⊢^{m} for constraints with map constraitns. The term reduction system is called map extensional iff ⊢^{t} ⊆ ⊢^{m}.

A constraint system with an axiomatic defined entailment relation ⊢^{e} has a natural inconsistency predicate iP(Δ) = {C ∈ P(Δ)|C ⊢^{e} false}. By use of (Ax1) we get ⊢^{e} ⊆ ⊢^{i} . The construction of the map entailment ⊢^{m} is a restriction of the constrauction for ⊢^{i} so obviously ⊢^{i} ⊆ ⊢^{m}.

4.3.3 Categorical normalisation

Given two categories C and D we call [C, D] the functor category, consisting of functors F : C → D as objects and natural transformations between these functors as morphisms of [C, D]. The category Ĉ = [C^{op}, Set] of contravariant setvalued functors is called the category of presheafs over C. If we restrict the morphisms between presheafs to inclusions that is for F̂, Ĝ ∈ Ĉ we define F̂ → Ĝ if F̂(C) ⊆ Ĝ(C) for every C ∈ C then we call this restricted category Ĉ_{s} the category of subpresheafs and denote the inclusion map as relation F̂ ⊆ Ĝ.

Given a small category C (t.i. every homset is a set), then we get for every C ∈ C a presheaf C( , C) : C^{op} → Set called the hom-functor. The object part of C( , C) is defined as D ↦ C(D, C) and the morphism part maps every mophism f : D → D′ to the map of homsets C(f, D) : C(D′, C) → C(D, C) by the operation ∘ f taking g ∈ C(D′, C) to g ∘ f ∈ C(D, C). The map taking C ∈ C to the homfunctor C( , C) and every morphism f : C → D to the natural transformation C( , f) = f ∘ : C( , C) → C( , D) is called the yoneda functor Y_{C} : C → Ĉ. We call functors F, G : D → Ĉ presheaf representations. We call F a subsheaf representation of G in short F ⊆ G if F (C) ⊆ G(C) for every C ∈ C.

Let’s recall the operational model of constraints. The hom set S(Δ′, Δ) is the set of all substitutions S : Δ′ → Δ. The map interpretation ⟦ ⟧_{M} is a map from constraints to a subset of substitutions. We name this map the normalisation (or non-inconsistency) functor.

Proposition 1 To every map extensional constraintsystem we get a functor N : C → Ŝ_{s} defined by the map (C, Δ) ↦ Ĉ with Ĉ : C → Set the instantiation presheaf associated to a constraint C ∈ P(Δ)

Ĉ : Δ′ ↦ S_{C}(Δ′, Δ) = {SΔ′ → Δ | SC ∉ iP(Δ′)}

Given the fibration ℂ : C → S and the yoneda functor Y_{S} : S → Ŝ then N is a sub presheaf representations of Y_{S} ∘ ℂ : C → Ŝ.

proof: To complete the proof we have to construct the morphism part of the map and check functoriality. A morphism m : (C, Δ) → (D, Δ′) in C is given by a substitution S : Δ → Δ′ which is a morphism in S and an entailment C ⊢^{e} SD.

Now if we assume that the entailment ⊢^{e} is map extensional then we get the implication C ⊢^{e} D ⟹ ⟦C⟧_{M} ⊆ ⟦D⟧_{M} the subset relation ⟦C⟧_{M} ⊆ ⟦D⟧_{M} implies for every type variable set Δ′′ the relation S_{C}(Δ′′, Δ) ⊆ S_{D}(Δ′′, Δ) this is the subpresheaf relation Ĉ ⊆ D̂ so we are done with the morphism part. Transitivity and reflexifity of ⊆ gives the functiorality of N. Because for every constraint C the construction S_{C} results a subset of the corresponding homset of S we get the sub presheaf representation relation N ⊆ Y_{S} ∘ ℂ □.

4.4 First order Polymorphism

Until now we managed to model simply typed lambda calculus in the category L. We had to care about two languages :

τ ::= α | τ → τ′
e ::= x | λx.e | ee′

The types τ and the expressions e. All this was organised in a three rule type system.

\begin{matrix}(T AUT) & Γ.x : τ ⊢ x : τ \\ (→ I) & \frac{Γ.x : τ ⊢ e : τ′}{Γ ⊢ λx.e : τ → τ′} \\ (→ E) & \frac{Γ ⊢ e : τ′ → τ Γ ⊢ e′ : τ′}{Γ ⊢ e e′ : τ} \end{matrix}

Now we want to extend the system to handle first order polymorphism. We will observe how this extension is done syntactically to proceed in categorically following these steps. This first step is an extension of the type language by allowing prefix quantification.

σ ::= τ | ∀α.σ

The new types σ are named polytypes while the old types τ will be named monotypes. Notice that all the monotypes are embedded in the collection of polytypes. The idea of quantification is to allow instantiations. Here we define instantiation as a relation between polytypes by :

∀α.σ ≤ [τ/α]σ

The crucial point is that instantiation of type variable α is possible only with monotypes τ. This restriction is the core of first order polymorphism. To extend the system the typotheses Γ are now extended to hold polytyped entries x : σ

The first step to extend the rule system is to exchange the (T AUT) for dealing with polytypes:

(pT AUT) Γ.x : σ ⊢ x : τ ( if σ ≤ τ)

Notice that in this system with the new (pT AUT) rule all consequences e : τ of judgements Γ ⊢ e : τ are still typed by monotypes as in the simply typed lambda calculus. The only new feature is the instantiation of one polytyped variable x : σ to several maybe different instance monotypes τ.

Now the final step to reach full first order polymorphism is to allow quantification and instantiation on every typed term.

(∀I) \frac{Γ ⊢ e : σ  (α ∉ tv(Γ))}{Γ ⊢ e : ∀α.σ}  (∀E) \frac{Γ ⊢ e : ∀α.σ}{Γ ⊢ e : [τ/α]σ}

It is a well known fact that type derivations with appearance of rule application (∀I) followed by (∀E) can be reduced. Notice that in this system application and abstraction is still typed only by monotypes. Finally Roy Croles slogan “morphism as judgements and composition as substitution” for categorical models of type systems leads to the following simplification of the instantiation rule.

(p∀E) \frac{Γ ⊢ e : σ  σ ≤ τ}{Γ ⊢ e : τ}

Notice that no expressiveness is lost. Further this version of the (∀E) rule can be seen as a instantiation of the (pT AUT) rule by substituting the variable x by expression e.

4.4.1 Polytypes categorically

A polyvariable denoted by pτ : Δ → Δ′ is given by an identity morphism id : τ → τ in L_{Δ×Δ′} (equivalent would be a arrow τ : Δ × Δ′ → I in S). The instances of pτ are given for every substitution S : Δ → Δ′ as an morphism pτ\underline{S} : \underline{S}τ → \underline{S}τ in L_{Δ} where

\underline{S} =< id_{Δ}, S >^{∗}: L_{Δ×Δ′} ⟶ L_{Δ}

with use of the diagonal diag =< id_{Δ}, id_{Δ} >: Δ → Δ × Δ.

So Δ can be seen as the free type variables of τ and Δ′ as the set of bound type variables of τ (t.i. we model the type ∀Δ′.τ). Finally \underline{S} is the instantiation of a polyvariable.

To build the category of instantiations I we describe the set of polytypes Pty(Δ) over free type variables Δ by :

τ ∈ Ty(Δ × Δ′) ⟹ ∀Δ′.τ ∈ Pty(Δ)

Now we can define

Objects of I_{Δ} Objects are represented as instantiations i : P ⊢ Γ where P is a tuple of polytypes ∀Δ′.τ ∈ Pty(Δ) and Γ is a typotheses t.i. an object of L_{Δ}. The instantiation are build by the following rules:

(inst)  Sτ : ∀Δ′.τ ⊢ \underline{S}τ
(⅋)  \frac{i : P ⊢ Γ  i′ : P ⊢ Γ′}{i⅋i′ : P ⊢ Γ, Γ′}
(⊗) \frac{i : P ⊢ Γ  i′ : P′ ⊢ Γ′}{i ⊗ i′ : P, P′ ⊢ Γ, Γ′}

morphisms in I S : i → i′ is given for i ∈ I_{Δ} and i′ ∈ I_{Δ′} by a substitution S : Δ → Δ′ (i.e. a morphism in S) such that Si′ = i.

4.4.2 The category P

By extending the simply typed lambda calculus with instantiable polyvariables we extend the expressibility of the system. The category P is a categorical model of the modificated system through exchange of the the rule (T AUT) by the rule (pT AUT). As expected this category is an extension of category L.

objects of P_{Δ} are the objects of L_{Δ}.

morphisms of P_{Δ} are of form (e, i) : Γ → τ for an instantiation i : P ⊢ Γ′ in I_{Δ} and a morphism e : Γ, Γ′ → τ in L_{Δ}.

4.4.3 Construction of polytypes in L

Application of rule (∀I) is allowed only if side condition α ∉ tv(Γ) holds. Here we will look at the categorical synonym of this side condition. Before looking a the situation in category L lets recall some equivalences in the category S of substitutions. There is are isomorphisms between the tuples of types, the substitutions, typotheses and map constraints. Given a sequence of types τ_{i} ∈ Ty(Δ) for 1 ≤ i ≤ n with Δ′ = V_{n} = {α_{1}, …, α_{n}} the set on n type variables there is the obvious isomorphisms :

(τ_{1}, …, τ_{n})  < τ_{1}, …, τ_{n} > morphism in S (tupel)
⇔ S = [τ_{1}/α_{1}, …, τ_{n}/α_{n}]  S : Δ → Δ′ morphism in S (subst)
⇔ {x_{1} : τ_{1}, …, x_{n} : τ_{n}} Γ ∈ L_{Δ} with |dom(Γ)| = n (typo)
⇔ M =< α_{1} = τ_{1} > ∧ ⋯ ∧ < α_{n} = τ_{n} > M ∈ M(Δ′, Δ) ⊆ Pr(Δ′ × Δ) (map)

So to every morphism S : Δ → Δ′ in S corresponds a typotheses Γ_{S} ∈ L_{Δ} where the size of the codomain of S and the size of domain of Γ coincide |Δ′| = |dom(Γ_{S})|. Now the property tv(Γ_{S}) ⊆ Δ′′ ⊂ Δ can be simply categorically presented in S. The meaning is that type variable set Δ can be represented as Δ = Δ′′ × Δ_{3} such that the substitution S can be represented as S = S′π_{1} with S′ : Δ′′ → Δ′ and use of first projection π_{1} : Δ = Δ′′ × Δ_{3} → Δ′′. We will note this situation in short Γ ⊂ Δ′′ for Γ ∈ L_{Δ=Δ′′×Δ_{3}}.

Given a morphism e : Γ → τ in L_{Δ} where we assume Γ ⊂ Δ′′ for Δ = Δ′ × Δ′′ then we can type morphism e with a polytype e : Γ → ∀Δ′.τ. Notice that this typing lives in Δ′′ (t.i. ∀Δ′.τ ∈ Pty(Δ′′)) such that for every instantiation \underline{S}τ ∈ L_{Δ′′} we get a unique morphism \underline{S}e : Γ → \underline{S}τ in L_{Δ′′}. A technical problem is that morphisms of form e : Γ → ∀Δ′.τ can’t compose in category L because typotheses hold only monotyped variables.

4.4.4 The category F

Now we have the material to model first order polymorphism. Category I gives the notion of polytypes and instantiation. Category P models the simply typed calculus with instantiated polyvariables. The construction above gives the hint how to model the (∀I) rule. Finally taking the composition with matching polytypes leads naturally to the interpretation of the general instantiation rule (p∀E).

We define the category P of first order polymorphism fiberwise by :

objects of F_{Δ} are poly typotheses P with P (x) ∈ Pty(Δ) for x ∈ dom(P).

morphisms of F_{Δ} A morphism (e, i) : P → P′ can be constructed by the following 3 cases:

1. Either a morphism of form (e, i) : P → ∀Δ′.τ that is a morphism (e, i) : Γ → τ in P_{Δ×Δ′} with an instantiation i : P ⊢ Γ such that Γ ⊂ Δ in L_{Δ×Δ′}.

2. or a morphism e⅋e′ : P → P_{1}, P_{2} for morphisms e : P → P_{1} and e′ : P → P_{2} in F_{Δ}.

3. or e ⊗ e′ : P_{1}, P_{2} → P′_{1}, P′_{2} for e : P_{1} → P_{1} and e′ : P_{2} → P_{2} in F_{Δ}.

4.5 Constrained type systems

Now that we defined categorical models of constraints and categorical models of type theories we can fullfill the task of gluing these categories together. Let’s recall that all type theories were modelled as fibration on the substitution category S. We had the simple type theory 𝕃 : L → S. First order polymorphism needed a fibration 𝕀 : I → S for modelling polytypes on which was used to build the fibration 𝔽 : F → S for modelling the type theory. The fact that all fibrations used the same base category S reflects the property that in these theories application of all substitution lead to new consistent judgement. In short instantiation is always allowed.

Now modelling constraints gives a categorical notion of restricted instantiations. This was done syntactical by the fibration ℂ : C → S stating that every instantiation of an entailment leads to another valid but maybe nonsensical entailment. The notion of decidable non-inconsistency was cover by the presheaf representation N : C → Ŝ_{S}. Simplified functor N yields for every constraint C the set Ĉ allowed instantiations. This observation opens the way to model constrained type theories.

Technically the new models are build by exchanging the base category S allowing all instantiations by the category C allowing only non-inconsistent instantiations.

In the simple type theory 𝕃 : L → S every morphism (t.i every judgement of the theory) could be instantiated by applying reindexing functor S^{∗} : L_{Δ} → L_{Δ′} for every morphism of base category S. In the corresponding constrained simple type theory 𝕃^{C} : L → C instantiation by reindexing functor S^{∗} : L_{C} → L_{SC} is only allowed for the non-inconsistent substitutions S ∈ Ĉ.

In the same way full instantiation of polytypes related to fibration 𝕀 : I → S is restricted to non-inconsistent instantiation in constrained polytypes modelled by fibration 𝕀^{C} : I → C.

4.6 Constraint Parametricity

Idea of uniform behaviour informal by Stracey in [Str67]

Reynolds idea of relational parametricity in [Rey83]. Categorical account on relational parametricity in [MR91] by Reynolds and Ma.

Proof theory to parametricity by Mairson [Mai91]. Presented as a logical system in [PA93] by Plotkin Abadi and they extended it to include subtyping [PAC94]. We extend to general X constraints theirs is an instance.

Use of parametricity to prove program transformations Wadler [Wad93] or more general to prove program equivalences [Pit95]

Categories, realisability and polymorphism are analysed by Freyd et.al[PJF77]. The previous work leads to a new categorical approach to model polymorphism [BFSS90] which is generalised in [Fre93].

5 Appendices

5.1 fibrations

definition of cartesian arrows. definition of fibrations. definition of indexed categories. The Grothendieck construction.

5.2 categorical logic

cartesian fibrations. Correspondence between cartesian fibration and symbolic logic. modelling quantifiers as adjoints of reindexing by projection doctrines and hyper doctrines topoi

Literatur

[Bar90] Ch. Wells M. Barr. Fibrations. [BW90], pages 252–270, 1990.

[BFSS90] E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P. J. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35–64, 1990.

[BW90] Michael Barr and Charles Wells. Category Theory for Computing Science. prentice hall, 1990.

[Coh90] Jaques Cohen. Constraint logic programming languages. Communications of the ACM, 33(7):54–68, 1990.

[Cro93] Roy L. Crole. Categories for Types. Cambridge University Press, 1993.

[Fou77] Michael P. Fourman. The logic of topoi. In J. Barwise, editor, Handbook of Mathematical Logic, pages 1053–1090. North Holland, 1977.

[Fre93] P. Freyd. Structural polymorphism. Theoretical Computer Science, 115:107–129, 1993.

[Jac91] Bart Jacobs. Categorical Type Theory. PhD thesis, catholic University of Nijmegen, September 1991.

[Jac93] Bart Jacobs. Comprehension categories and the semantics of type dependency. Theoretical Computer Science, 107:169–207, 1993.

[Jac95a] B. P. F. Jacobs. Subtypes and bounded quantification from a fibered perspective. Electronic Notes in Theoretical Computer Science, 1, 1995.

[Jac95b] Bart Jacobs. On cubism. Journal of Functional Programming, 1995.

[JM94] Joxan Jaffar and Michael Maher. Constraint logic programming: A survey. Journal of Loagic Programming, 19,20:503–581, 1994.

[LP86] J. Lambek and P.J.Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1986.

[Mai91] Harry G. Mairson. Outline of a proof theory of parametricity. In J. Hughes, editor, Functional Programming Languages and Computer Architechture, pages 311–327, LNCS 523, August 1991. ACM, Springer Verlag.

[Moe92] S. Mac Lane Ieke Moerdijk. Sheaves in Geometry and Logic. Springer Verlag, 1992.

[Mog89] Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 14–23, Asilomar Conference Center, Pacific Grove, California, June 1989. IEEE Computer Society Press.

[Mog91] Eugenio Moggi. Notions of computations and monads. Information and Computation, 93:55–92, 1991.

[MPSS95] Max P. Mendler, Prakash Panangaden, P. J. Scott, and R. A. G. Seely. A logical view of concurrent constraint programming. Nordic Journal of Computing, 2:182–221, 1995.

[MR91] QingMing Ma and John C. Reynolds. Types, abstraction and parametric polymorphism, part 2. In 7^{th} Conf. on Mathematical Foundations of Programming Semantics, pages 1–40, LNCS 598, 1991. Springer Verlag.

[PA93] Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In Typed Lambda Calculi and Applications TLCA ‘93, pages 361–375, LNCS 664, March 1993. Springer Verlag.

[PAC94] Gordon Plotkin, Martin Abadi, and Luca Cardelli. Subtyping and parametricity. In LICS ‘94, pages 310–319, Paris, France, July 1994. IEEE Press.

[Pav90] Dusko Pavlovic. Predicates and Fibrations. PhD thesis, Rijksuniversiteit te Utrecht, November 1990.

[Pho92] Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. University of Edinburgh ECS-LFCS-92-208, April 1992.

[Pit] Andrew M. Pitts. Categorical Logic, volume 6 of Handbook of Logic in Computer Science. Oxford University Press.

[Pit95] Andrew M. Pitts. Operationally-based theories of program equivalences. In Summer School on Semantics and Logics of Computation, Cambridge, September 1995. ESPRIT CLICS-II.

[PJF77] A. Scedrov A. Carboni P. J. Freyd. A categorical approach to realizability and polymorphic types. In D. Schmidt M. Main A. Melton, M. Nistore, editor, Mathematical Foundations of Programing Language Semantics LNCS 298, pages 23–42. Springer Verlag, 1977.

[PSSS94] P. Panangaden, V. Saraswat, P. J. Scott, and R. A. G. Seely. A hyperdoctrinal view of concurrent constraint programminig. 1994.

[Rey77] A. Kock G. E. Reyes. Doctrines in categorical logic. In J. Barwise, editor, Handbook of Mathematical Logic, pages 284–313, 1977.

[Rey83] John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513–523. Elsevier Science (North Holland), 1983.

[Sar90] Martin Rinard Vijay A. Saraswat. Concurent constraint programming. In POPL ’90, pages 232–242. ACM, 1990.

[SRP91] Vijay Saraswat, Martin Rinard, and Prakash Panagaden. The semantic foundation fo concurent constraint programming. In POPL ‘91, pages 333–352, Orlado, FL, USA, January 1991. ACM, ACM press.

[Str67] Christopher Strachey. Fundamental concepts in programming languages. In unpublished, editor, International Summer School in Programming Languages, Copenhagen, August 1967.

[Wad93] Philip Wadler. Theorems for free! In Proc. of FPCA ’89, pages 347–359. ACM, 1993.