## Roman Containers

Hank and I whiled away a Friday afternoon, musing on dependent containers. Yet another formulation of them emerged from the flotsam, which we christened *Roman* containers (after an old joke on our part), but should probably call *annotated* containers or even *refined* containers. I’ll stick with Roman for now.

Given sets (I,O) of ‘input and output sorts’, a Roman (I,O)-container, (S,P,q,r) is given by a container (S,P) and a pair of functions q:S→O, r:ΣP→I. The idea is just that q explains which output sort each shape delivers and r explains which input sort each position in each shape requests.

The extension of such a thing inhabits (I→Set) → (O→Set) and is computed thus

[(S,P,q,r)] T o := Σs:S. o = q s × Πp:P s. T (r (s,p))

(Aside, for a differentiable container F, we can just say that q : F 1 -> O and r : dF 1 -> I.)

Allow me to present a little example. The finite sets, when defined inductively are given by

The Roman -container of which this is the least fixed point can be read off directly from this.

output indices per constructor

input index for payload arg

(For years now, Hank and I have been referring to these Alf/Epigram datatype families as ‘Catholic’, with Agda/Haskell’s more austere notion being ‘Presbyterian’. The difference between the two is that Catholics believe in a general transubstantiative equality. Catholic families are the fixpoints of Roman containers.)

It is now blatantly obvious what a morphism between two Roman (I,O)-containers should be: a container morphism which preserves sorts.

A morphism between and is given by

- a container morphism
- a proof that
- a proof that

Moreover, it is now clear how to generalise this to a *container driver*: the presentation of a ’master‘ (I,O)-container as an interface to a ’slave‘ (I’,O’)-container. Simply replace the equalities above with a pair of relations Q:I→I’→Prop, R:O’→O→Prop which characterise the intended simulation between sorts. The conditions now ensure that the driver correctly implements a command-response interface which respects this simulation.

Can we get away with that?

July 2nd, 2005 at 11:05 am

That’s an excellently McBridic summary.

Lest one thinks that there is a unique way to skin a cat, there are dozens.

Here’s another approach to defining the family of finite sets.

First, let 0 be the empty container, and (C+1) the successor of container

C with shapes S+1 and positions P’(inl(s)) = P(s), P(inr(_)) = S. Now form

the least fixed point (mu X:Cont. 0 + (X+1)). The shapes in this container are

effectively the natural numbers n, and the positions Fin(n).

July 2nd, 2005 at 1:23 pm

is just a low categorical trick for a dependent family

.

S(o) is actually

Likewise

is just the same low categorical trick.

It seems to me there is a systematic to-ing and fro-ing between the Trinity of Roman, Presbyterian and Thorstenic containers, by use of low categorical tricks.

July 12th, 2005 at 12:33 pm

A further conversation with Conor revealed that there are (prima facie at least) 4 notions of dc. Usings and

, they can be tabulated:

The typical objects of these types have the forms (respectively):

[Unparseable or potentially dangerous latex formula. Error 5 : 527x40]

What is going on here? Part of it has to do with the different analyses we can give of the concept of binary relation in type theory.

The types in the first row are isomorphic (by Currying/uncurrying). The bottom left-hand entry is more-or-less a notion of *span* between A and B. The bottom right-hand entry is what I have been calling a transition structure from A to B.

A monotone predicate transformer is, modulo isomorphism a relation between O and Pow(I) which is monotone

in the second argument. If we ring the permutations of Fam and Pow, we get the 4 entries in the table with which I started.

It may be worth observing that the top entry in the left-hand column is positive in both O and I. Were we to localise Fam to a given universe/family of sets (A,B) (ie. define , then we can look at the least-fixed-points of the functor with respect to O, I (separately), and in the homogeneous case .

The top-left notion is Conor’s. The top-right is mine. The bottom right is Thorsten’s. As far as I know, no-one has yet espoused the bottom left notion.

[Apologies of the latex stuff above doesn't compile. I don't think one can edit/repair comments in this blog...]