### Roman Containers

Saturday, July 2nd, 2005Hank 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?