Archive for July, 2005

Roman Containers

Saturday, July 2nd, 2005

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

\begin{array}{ll@{}l} \mathsf{fz}\; & : \Pi n:\mathbb{N}. & \mathsf{Fin}\:(\mathsf{suc}\:n) \\ \mathsf{fs}\; & : \Pi n:\mathbb{N}. \mathsf{Fin}\:n \rightarrow & \mathsf{Fin}\:(\mathsf{suc}\:n) \\ \end{array}

The Roman (\mathbb{N},\mathbb{N})-container of which this is the least fixed point can be read off directly from this.

\begin{array}{ll} \mathrm{data}\: S \begin{array}[t]{rl} =& \mathsf{FZ}\:\mathbb{N} \\ |& \mathsf{FS}\:\mathbb{N} \\ \end{array} &\mbox{constructors, non-payload args} \end{array}

\begin{array}{l} P\:(\mathsf{FZ}\:n) = 0 \quad\mbox{enumeration of payload args}\\ P\:(\mathsf{FS}\:n) = 1\\ \end{array}

q\:(\mathsf{FZ}\:n) = \mathsf{suc}\:n   output indices per constructor
q\:(\mathsf{FS}\:n) = \mathsf{suc}\:n

r\:(\mathsf{FS}\:n,()) = n   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 (S_0,P_0,q_0,r_0) and (S_1,P_1,q_1,r_1) is given by

  • a container morphism (f:S_0\rightarrow S_1, u:\Pi s:S_0.P_1\:(f\: s)\rightarrow P_0\:s)
  • a proof that q_0\:s = q_1\: (f\:s)
  • a proof that r_1\:(f\:s,p) = r_0\:(s,u\:s\:p)

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?

Posted in General | 3 Comments »