Club polymorphism

Martin Wehr

11. März 1999

1 A categorical axiomatisation of adt’s

Let I be the category of lower natural number intervals. The objects of I are the sets [n] := {1, …, n} for a natural number n ∈ ℕ. The morphisms of I are the functions on intervals. Note that I is the skeleton of the category F inSet of finite sets and functions.

In the following we take a set S which elements we will call sorts. We are interested in S^{∗} the free monoid on the sorts. The elements u, v ∈ S^{∗} will be called strings. We denote by |u| = n ∈ ℕ the length of an string.

The comma category S−Rep := I^{op} ↓ S is the category of string representations. The object are of form \overline{u} : [n] → S where the natural number n is the length of the represented string. The morphisms \overline{m} : [|v|] → \overline{[}|u|] are called representation of string morphisms with short notation m : u → v. The morphism have to satisfy the equation \overline{v} = \overline{u} ∘ \overline{m}.

The category S − Sig := S ↓ (Set ↓ (I^{op} ↓ S)) is the category of S-sorted signatures. The construction of the free S-sorted terms is a monad on this category. We give the monad the name T m : S −Sig → S −Sig. The unit of the monad is the injection of variables. The multiplication of the monad is defined by substituting variables by terms. Each object of the category comes with a carrier C ∈ Set. The elements of the carrier f ∈ C come equipped with a typing (u, s) with an argument string u ∈ S^{∗} and a result sort s ∈ S. If the carrier C is finite we call the object Σ a signature.

The free S-sorted Lawvere theory T_{Σ} generated by a S-sorted signature is a free cartesian category. The objects of this category are the strings on the sort set. The morphisms of the category are the strings of terms where the terms coincide on there argument strings.

\underline{m} : u → v ∈ T_{Σ}  iff m : u → v is a morphism in S − Rep
t : u → s ∈ T_{Σ} iff t : (u, s) is a term in T m(Σ)
t_{1}t_{2} : u → v_{1}v_{2} ∈ T_{Σ} iff t_{1} : u → v_{1} ∈ T_{Σ} and t_{2} : u → v_{2} ∈ T_{Σ}

By an abuse of notion we call morphisms of the theory T_{Σ} terms, even if we should distinguish between terms t ∈ T m(Σ) and strings of terms t ∈ T_{Σ}. We denote the composition of terms by t • t′. This category is finitary cartesian and has finite equalisers. So it has pullbacks as well. We will denote the pullback by t˜⊔t′ for two morphisms t, t′ ∈ T_{Σ} ↓ u. This pullback is the cartesian product of the factors

(t ⊔^{⊲} t′)(t ⊔^{⊳} t′) = t˜⊔t′.

We denote by □t the domain of an Lawvere term and by t□ we denote its codomain.

1.1 free variables

To each term t ∈ T_{Σ} there is a typing t : u ⊢ v. Further there is an universal relevant term r(t) : u′ ⊢ v with a string morphism fv(t) : u → u′ Such that t = r(t) ∘ \underline{fv(t)}. The universal property gives for each factorisation t = t′′ ∘ \underline{m} with a string morphism m a unique factorisation. So there exists an unique string morphisms m′ with fv(t) = m′ ∘ m and t′′ = r(t) ∘ \underline{m′}. A term t is relevant iff the free variable string morphism fv(t) is an isomorphism.

1.2 Two dimensional free Lawvere theories

A S-sorted free Lawvere theory has strings of sorts as object. A two dimensional S-sorted Theory V al has the morphisms of a S-sorted free Lawvere theory T yp as objects. We will call the morphisms v of V al the values and the morphisms τ of T yp the types. We will denote a value as an arrow v : τ ⊢ τ′ so the codomain is the type □v = τ and the domain is the type v□ = τ′.

We need the axiom □□v = □(v□) to define predicative polymorphic types for a valuev. This axiom allows to define instantiation as an action of types on values. Instantiation is a a operation v ⊲ τ which is defined iff □□v = τ□. In case of definedness the types of a value v : τ ⊢ τ′ change accordingly to v ⊲ τ′′ : τ • τ′′ ⊢ τ • τ′′. Further the action laws are (v ⊲ τ) ⊲ τ′ = v ⊲ (τ • τ′) and interchange (v • v′) ⊲ τ = (v ⊲ τ) • (v′ ⊲ τ).

Given a relevant value v the principle value with typing is denoted as ṽ: ˜□v ⊢ v ˜□ with an instantiation type τ^{v} such that we get a universal factorisation v = ṽ ⊲ τ^{v}.

So the composition of values v • v′ is determined by the composition of their principal values.

\begin{aligned}τ^{v•v′} & = & τ^{({ \atop v•v′})} • (v ˜□˜⊔˜□v′) \\ { \atop v • v′} & = & (ṽ ⊲ •(v ˜□ ⊔^{⊲} ˜□v′)) • (ṽ′ ⊲ (v ˜□ ⊔^{⊳} ˜□v′)) \\ □({ \atop v • v′}) & = & (□ṽ) • (v ˜□ ⊔^{⊲} ˜□v′) \\ ({ \atop v • v′})□ & = & (ṽ′□) • (v ˜□ ⊔^{⊳} ˜□v′) \end{aligned}

The operation ∥ ∥ is a cartesian functor from the values to untyped prevalues which are morphisms of a S-sorted free Lawvere theory. A typed value v is sent to a S-sorted term ∥ v ∥: (□v)□ ⊢ □□v. Functoriality gives the law ∥ v • v ∥=∥ v ∥ • ∥ v′ ∥.