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


\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?

3 Responses to “Roman Containers”

  1. Hank Says:

    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).

  2. Hank Says:

     $ q : S \to  O $
    is just a low categorical trick for a dependent family
     $ \{ S(o) | o : O \} $ .
    S(o) is actually  $ S^{-1} \{ o \} $

    Likewise
     $ r : \Sigma(S,P) \to  I $
    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.

  3. Hank Says:

    A further conversation with Conor revealed that there are (prima facie at least) 4 notions of dc. Usings  $ Fam(X) = (\Sigma I : Set)X^I $ and
     $ Pow(X) = Set^X $ , they can be tabulated:
    
\[
\begin{array}[t]{l|l} 
Fam(O \times Fam(I)) & O \to Fam(Fam(I)) \\
Fam(O \times Pow(I)) & O \to Fam(Pow(I)) 
\end{array}
\]
    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.
    
\[
\begin{array}[t]{ll}
Pow(A \times B) & A \to Pow(B) \\
Fam(A \times B) & A \to Fam(B) 
\end{array}
\]
    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  $ Pow(I) \to Pow(O) $ 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  $ Fam’(X) = (\Sigma a : A) X^{B(a)} $ , then we can look at the least-fixed-points of the functor  $ O,I \mapsto Fam’(O \times Fam’(I)) $ with respect to O, I (separately), and in the homogeneous case  $ I \mapsto Fam’( I \times Fam’(I) ) $ .

    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...]