Container Types

Archive for June, 2005

Container Drivers

Tuesday, June 28th, 2005

I’ve just got hold of The Fall Peel Sessions. Surely we can figure out what a container driver is…

Conor and I once talked about `Naperian’ containers, that so to speak work well with logarithms.
He reminds me that A Naperian container has one shape, and a set of positions.
So it represents an endofunctor $X \mapsto X^K$ .
The logarithm of this container is K.
Every container is a sum of Naperian containers.

To be Naperian is to be a multiplicative, unsummy kind of thing,
all products and exponentials, with no Sigma. Sheer testosterone. [The dependent counterpart is a monotone predicate transformer that commutes with all intersections. ]

Conor’s comment to this note dances the McBride with/out-of the subject,
and relates it to derivatives.

There is a connection between lambda abstraction
and some basic laws of logarithms, namely that in some respects
lambda-abstraction behaves like a logarithm, in that it satisfies
laws such as:
$\begin{array}[t]{l} log_x(a^k) = log_x(a) * k, \\ log_x(a*b) = log_x(a) + log_x(b), \;\;\; \mbox{Note: non-linear}\\ log_x 1 = 0, \;\;\;\;\;\; \mbox{Note: non-affine}\\ log_x(x) = 1, \\ x^{log_x a} = a. \end{array}$
Linear lambda-abstraction corresponds to the case where the logarithm is Naperian.
To handle log_x(k^x) you need a special constant (^) reflecting ^ in the sense that
b^a^(^) = a ^ b. Then log_x(k^x) is (k^) = k^(^).

As Conor pointed out, Naperian functors are closed under composition
(which when taking logarithms translates into ×). In some sense they are closed under
nu expressions, and he shows how to take the logarithm of these.

The weird similarity between lambda abstraction and logarithms was (according to a manuscript by Felice Cardone and Roger Hindley on the history of the lambda-calculus ) known to Böhm in the 1970’s. It really has to do with the combinatorial completeness for the untyped lambda calculus of 4 arithmetical combinators, with exponentiation
A^F reflecting application F(A). Lambda abstraction is the undoing of application in the same way as taking the logarithm is the undoing of exponentiation. You get combinatorial completeness for the linear lambda calculus by dropping
0 and +, and for affine lambda calculus by dropping only +.

Posted in General | 3 Comments »

Any mpt is iso to some dc.

Thursday, June 16th, 2005

mpt = monotone predicate transformer. A monotone predicate transformer is a function $$F of type $Set^I \to Set^O$ (for some sets or types $I,O : Set$ ) such that for all $U \subseteq V : I \to Set$ , we have $F(U) \subseteq F(V) : O \to Set$ . Here $U \subseteq V$ is the set of functions $(\Pi i : I)U(i) \to V(i)$ . When we are interested in equality between such functions the previous sentence actually means that $F$ is functorial.

dc = dependent container. There are two subtly different candidates for this title,
namely objects of the types
$\begin{array}[t]{l} O \to Fam(Pow(I)) \\ O \to Fam(Fam(I)) \end{array}$
Here
$\begin{array}[t]{l} Fam(X) = (\Sigma I : Set) I \to X \\ Pow(X) = X \to Set. \end{array}$
The types are slightly different, and amount to different presentations of the same information. The differences may be relevant to computing with these presentations.

In the FamFam one, we make a table where the sections are per output type, the subsections are per shape of the output sort, and the subsubsections are per position in that shape (and give an input sort).
In the FamPow one, the subsubsections are per input type, and give the set of positions in the shape which share that input port.

There is a choice between having $I,O$ fixed, or on the other hand having it the carrier set in our structure, in the same way that in the theory of groups the carrier set is not globally fixed: different groups, or different dependent containers can have different carrier sets.
I have explored this only for the case I = O.

Any mpt can be expressed in (Presbyterian) disjunctive normal form , which looks like
$U \mapsto \{ o : O | (\Sigma s : S(o) )(\Pi p : P(o,s))U(o[s/p]) \}$
for some (the following piece of latex compiles fine on my system).
[Unparseable or potentially dangerous latex formula. Error 2 ]
In the `Pow’ variant we have a slightly different `Episcopelian’ structure
(The following compiles fine on my system…)
[Unparseable or potentially dangerous latex formula. Error 2 ]

If the powerset of a set is a set, ie Pow and/or Fam : Set $\to$ Set, then any monotone predicate transformer is extensionally equal to a predicate transformer in disjunctive normal form. (Extensional equality
between predicate transformers F and G means that each includes the other. That F is included in G means that for all $U, V \subseteq S$ , $U \subseteq V$ implies $F(U) \subseteq G(V)$ .

The proof is a piece of vacuous impredicative bollocks, where the idea is that you have an intermediate set which is actually the set of subsets of S.

I think this is interesting, because it means that impredicatively, dependent containers are a complete representation `at the level of objects’. (NB, if you have impredicativity, you can define Leibnitz equality.)

There is also `the level of morphisms’, where you define a notion of morphism between
predicate transformers, which may be given in disjunctive normal form. There are 3 interesting notions of
mapping between mpts and dcs, corresponding to the types
DC -> DC, DC -> MPT, and MPT -> MPT. In the case
DC -> DC, when both isotopes of DC are presbyterian (FamFam),
we have something very concrete.
Impredicatively, all these notions of mapping coincide.

With dependent containers, it seems that the statement of the representation theorem in your paper(s?)
(that there is a full and faithful functor from DC -> MPT essentially, ie. something which is at the level of morphisms,), can be strengthened to say there is actually there is even a functor which is surjective on objects.

The moral I take to be be that if you want concrete representations for mpts, you are looking for some variant
among slightly different notions of dc’s.

Posted in General | No Comments »

Containers for number-classes

Thursday, June 9th, 2005

The following is an example of an operation on (non-dependent) containers that may be of interest to those (me and Dr Altenkirch) of us with an interest in constructive versions of the higher `number classes’.

What’s a number class? Well, the notion and terminology comes from Cantor. Traditionally, the natural numbers $Nat = (\mu X)X + 1$ form the first number class, the countable Brouwer-ordinals
$BO = (\mu X)X + 1 + X^{Nat}$ form the second, and you can push on further into the so-called `finite’ number classes in the obvious way, by chucking in a $+ X^{NC_n}$ to the functor whose $\mu$ gave you the previous number class NC_n . (You can think of these sets as `aleph numbers’ $\aleph_0, \aleph_1, \ldots$ .)

Computable versions of these blighters were defined by Church and Kleene in 1937-1938, and by Markwald and Spector in 1954-1955. In fact they extended the series into the transfinite: at ` $\omega$ ‘ one takes the union of the finite number classes, and then presses on as in the step from $\aleph_n$ to $\aleph_{n+1}$ . In type theory, the theory of the finite number classes is quite interesting (there are some well-cool `collapsing functions’ $\aleph_{n+1} \to \aleph_n$ )), but somewhat hindered by being full of `dot dot dots’. Moreover, as far as I know, there is no decent development of transfinite number-classes in type-theory. (One wants in the first place to get up to the first inaccessible ordinal, this being, for those of you who know what `regular’ means, a regular
ordinal closed under the step to the next regular. )

Anyway. The best way to approach the finite number classes is via the endofunctors of which they are the initial algebras. And the most natural way to do it is as follows.
$\begin{displaymath} \begin{array}[t]{l} F_0(X) = X \\ F_{n+1}(X) = F_n(X) + X^{\mu(F_{n})} \end{array} \end{displaymath}$
The initial algebras of these chaps are, successively,
$\begin{array}[t]{lclclcl} 0 &=& (\mu F_0) &=& (\mu X)X \\ Nat &=& (\mu F_1) &=& (\mu X)X + X^0 &=& (\mu X) X + 1\\ BO &=& (\mu F_2) &=& (\mu X)X + 1 + X^{Nat}\\ \ldots& & \end{array}$
(Now you can maybe see why I wrote $X + 1$ rather than $1 + X$ .)
Funnily enough, the empty set comes out as the first `number-class’, the naturals as the second, etc., so we’re off-by-one from the conventional terminology, but who cares. The point is by working with the endo-functors rather than their initial algebras, we get a nice closed-form description of the step to the next number-class, without any `dot dot dots’ as in $\aleph_{n+1} = (\mu X)1 + X + X^{\aleph_0} + \ldots + X^{\aleph_n}$ .

And of course, these functors are given by containers: $S_0 = 1, P_0(0) = 1$ ,
$S_{n+1} = S_{n} + 1, P_{n+1}(inL(s)) = P_{n}(s), P_{n+1}(inR(0)) = \mu(S_n \rhd P_n)$ .
Moreover, it is obvious that there are natural transformations from $F_n$ to $F_{n+1}$ all the way up. Taking the colimit of this series (the formalisation requires a universe to `recurse into’), we get a functor $F_\omega$ whose $\mu$ is $\aleph_{\omega + 1}$ , and whose value at 0 is $\aleph_{\omega}$ .

In other words, the theory of (non-dependent) containers seems to provide quite a bit of the apparatus one needs to make a type-theoretic development of number-classes beyond the finite ones, whose absence (till now) constitutes a minor scandal in type-theory.

Some further thoughts along/beyond these lines can be found here, and here.

Posted in General | No Comments »

What are dependent containers (for)?

Wednesday, June 8th, 2005

I am trying to write some kind of paper about dependent containers.
A reasonably up to date version may be found here.
(The sources are nearby in “cp.tar.gz”.)

There’s a couple of roughly similar structures that one might call (unary) `dependent containers’, to wit:

$I \to (\Sigma A : Set) A \to J \to Set$ , with typical element $(\lambda i) \langle a (i),(\lambda a,j)B(i,a,j) \rangle$ , where
$A : I \to Set$ , and $B : (\Pi i : I)A(i) \to J \to Set$ .
In the case (which I’d call the homogeneous case), these have been used to represent cover-relations between neighbourhoods in formal topology, among other things. (See for example this, section 3.1. . The notion of `axiom-set’ is due to Peter Aczel.) Dr. Altenkirch likes ‘em too, so I call them Episcopelian
$I \to (\Sigma A : Set)A \to (\Sigma B : Set)B \to J$ , with typical element $(\lambda i)\langle a (i), (\lambda a)\langle B(i,a),(\lambda b)n(i,a,b)\rangle \rangle$ ,
where $A : I \to Set$ , $B : (\Pi i : I)A(i) \to Set$ , and $n : (\Pi i : I, a : A(i))B(i,a) \to J$ .
Me’n'my pals have been using these things (particularly the homogenous variety) to represent imperative interfaces in type-theory. (For example NPS, chapter 16. I call them Presbyterian.

One can put these things in a more compact form with the aid of some definitions:
$Fam(X) = (\Sigma I : Set)X^I$ , and
$Pow(X) = X \to Set$ .
(Here $X$ is a type, by which I mean a `proper’, or `large’ type, such as for example $Set$ , $$Set \to Set$$ , $Fam(Set)$ , etc. .) Then the two types above are
$I \to Fam(Pow(J)$ , and $I \to Fam(Fam(J))$ .
[Concerning `Fam': one could call a family of X's a multiplicity (or even an array) of X's. There is no requirement that the function is mono. The same X could be listed again and again.]

[Dr. Altenkirch doesn't like `Pow'. The only alternative I know is `Pr', suggesting both PRedicate and PResheaf.
I suggest he installs some equi-expansive macro such as `Blam' in his head, and thinks of it as a tiny explosion. I never, ever use proof irrelevance, and am usually mindful of the implications of functoriality, naturality, and suchlike jazz.]

What are non-dependent containers for? It is to my mind a reasonable answer that they are representations of endo-functors on sets or rather endo-functors on Set which are given by algebraic signatures. As for the morphisms between them, they represent natural transformations between the relevant endo-functors. There may be other reasons to be interested in them, and there may be happier expressions of it, but that seems to be the killer application.

What then about morphisms between these mothers? What are they for? There’s a lot to say about this, but before getting into it, we can ask whether the $I$ and the $J$ are to be globally fixed, or whether they are to count as part of the structure. Furthermore, are we going to be interested particularly in the homogeneous case $I = J$ ?
Taking the homogeneous case, if we count $I$ as part of the structure, then our objects are really of type

$(\Sigma I : Set)I \to Fam(Pow(I))$ , or to put it another way $$(\Sigma I : Set)I \to (\Sigma A : Set)A \to I \to Set$
$(\Sigma I : Set)I \to Fam(Fam(I))$ , or to put it another way $(\Sigma I : Set) I \to (\Sigma A : Set) A \to (\Sigma B : Set) B \to I$ .

Both these things represent, to put it briefly, monotone predicate transformers on a set. To put it a little more exactly, they represent
pairs $I : Set, F : (I \to Set) \to I \to Set$ , where $F$ preserves inclusions $(\Pi i : I)U(i) \to V(i)$ between $U, V : I \to Set$ . They do so in essentially the same way:

$F(U) = \{i : I | (\Sigma a : A(i))(\Pi j : I)B(i,a,j) \to U(j)\}$ . Remember, $B : (\Pi i : I)A(i) \to I \to Set$
$F(U) = \{i : I | (\Sigma a : A(i))(\Pi b : B(i,a))U(n(i,a,b)\}$ . Remember, $B : (\Pi i : I)A(i) \to Set$ , and $n : (\Pi i : I, a : A(i))B(i,a) \to I$

Such an $F$ is a `monotone’ operator on $I$ -indexed families of sets; or to put it another way, a monotone relation $i \lhd U$ between $i : I$ and $U : I \to Set$ (`monotone’ in the argument $U$ ).

Now one thing I have figured out (in the One True logical assistant Agda), which Dr. Altenkirch already knew, is the following. Suppose we globally fix $I$ and $J$ , and regard $Pow(I)$ and $Pow(J)$ as categories. That is to say, we regard as having objects $U : I \to Set$ , and take for morphisms $m : hom(U,V)$ families of functions $f : (\Pi i : I)U(i) \to V(i)$ . Similarly for . Humour me, and call such $m$ inclusions, or shminclusions if you like. Then a functor from $Pow(I)$ to $Pow(J)$ is analogous to a monotone function from the powerset of $I$ to the powerset of $J$ . A natural transformation from $F : Pow(I) \to Pow(J)$ to (same type) $G$ is naught but a function having type $(\Pi U : Pow(I))F(U) \to G(U)$ , or to us (Scandinavian) type-theorists, a proof that the predicate transformer $F$ is `pointwise’ included in the predicate transformer $G$ . Oh, which satisfies the naturality condition.

Now, where $F$ and $G$ are represented by by objects of type $I \to Fam(Pow(J))$ , we can represent such a natural transformation by a pair of functions $\langle u, f \rangle$ , having types
$u : (\Pi i : I) A_F(i) \to A_G(i)$ , and
$f : (\Pi i : I, a : A_F(i) ) B_G(i, u(i,a)) \to B_F(i,a)$ ,
which is what Dr Altenkirch proposes as a morphism between type 1 objects.
Should you be interested, here is the Agda file. This doesn’t appear to work with the $Fam(Fam( ))$ version.

What if we take for objects in our category pairs of type $(\Sigma I : Set)I \to Fam(Fam(I))$ (as I have done with Anton and Pierre)? What should we take for morphisms? Below is the answer we arrived at.

Suppose our domain is the object $\langle I_h, A_h, B_h, n_h \rangle$ , and $\langle I_l, A_l, B_l, n_l \rangle$ is the codomain. (The subscripts stand for `high-level’ and `low-level’.) We then have a certain (monotone) relation-transformer, or if you like, monotone transformer of predicates (or set-valued functions) $Q$ over $I_h \times I_l$ , namely:
$Q \mapsto \{(i_h,i_l) | \begin{array}[t]{l} (\Pi a_h : A_h(i)) \\ \; (\Sigma a_l : A_l(i_l)) \\ \; (\Pi b_l : B_l(i_l,a_l)) \\ \;\;(\Sigma b_h : B_h(i_h,a_h)) \\ \;\;\;Q(n_h(i_h,a_h,b_h), n_l(i_l,a_l,b_l))\} \end{array}$$
For morphisms from $h$ to $l$ , one takes $Q$ which are post-fixed points (invariants) for the above operator.

Clearly, this is quite a mouthful. Its properties emerge only after a certain amount of study. It may be reassuring to know at the outset that these objects have been studied some decades. They are known as `downwards’, or `forwards’ simulations.

The first thing to observe is that by applying the (type-theoretic) axiom of choice, one can massage the relation-transformer into the form $I, A, B, n$ . Namely,
$I = I_h \times I_l$ ,
$A(\langle i_h, i_l \rangle) = \begin{array}[t]{l} (\Sigma f : A(i_h) \to A(i_l)) \\ (\Pi a_h : A_h(i_h))B_l(i_l,f(a_h)) \to B_h(i_h,a_h)\end{array}$ ,
$B(\langle i_h, i_l \rangle, \langle f, g \rangle) = (\Sigma a_h : A_h(i_h))B_l(i_l,f(a_h))$ , and
$n(\langle i_h, i_l \rangle, \langle f, g \rangle, \langle a_h, b_l \rangle ) = \langle n_h(i_h, a_h, g(a_h, b_l)), n_l(i_l, f(a_h), b_l) \rangle$ .

So here we have a binary operator on $I, A, B, n$ things. For reasons that will emerge, I use the notation $h\mathbin{\relbar\mskip-8mu\circ} l$ for this. You will immediately want to know what $\otimes$ is. I might as well write it down here:
$I = I_1 \times I_2$ ,
$A(\langle i_1, i_2 \rangle) = A_1(i_1) \times A_2(i_2)$ ,
$B(\langle i_1, i_2 \rangle, \langle a_1, a_2 \rangle) = B_1(i_1, a_1) \times B_2(i_2, b_2)$ ,
$n(\langle i_1, i_2 \rangle, \langle a_1, a_2 \rangle, \langleb_1, b_2 \rangle) = \langle n_1(i_1, a_1, b_1), n_2(i_2, a_2, b_2) \rangle$ .

OK, what does a morphism $h \mathbin{\relbar\mskip-8mu\circ} l$ represent? If we think of $h = \langle I_h, A_h, B_h, n_h \rangle$ as
representing $I_h : Set, |h| : Pow(I_h) \to Pow(I_h)$ , and similar for $l$ , then let’s say that a simulation of $\langle I_h,|h| \rangle$ by $\langle I_l, |l| \rangle$ is an $m : Pow(I_h) \to Pow(I_l)$ such that $m \cdot |h| \subseteq |l| \cdot m$ . (This stands for $(\Pi U : Pow(I_h),i_l : I_l) m(|h|(U),i_l) \to |l|(m(U),i_l)$ .)
Call a simulation downwards if it is a `left adjoint’, meaning that there is a $m^\ast : Pow(I_l) \to Pow(I_h)$ such that we have a Galois connection: $m(U) \subseteq V \Longleftrightarrow U \subseteq m^\ast(V)$ for all $U : Pow(I_h), V : Pow(I_l)$ . (Equivalently, $m$ commutes with arbitrary unions, or equivalently coincides with a relational union, or equivalently … .) Then: what $h\mathbin{\relbar\mskip-8mu\circ} l$ represents is a downwards simulation.

I should say straightaway that I don’t know if the lollipop gives a complete representation of downwards simulations, though I’d be flabbergasted if not. Hmm — maybe I should try to prove it… .

A certain amount is known about the category of (homogeneous) predicate transformers and downward simulations (though more by Pierre Hyvernat than me). In particular, there are a number of interesting monads and comonads, principally a monad for reflexive and transitive closure of a predicate transformer, and a comonad for a reflexive and transitive `interior’. Oh, and there’s a `bang’, and other paraphernalia of linear logic.

Having indicated a certain amount of maybe relevant technical stuff about our two basic structures, it’s high time to start some discussion of the question in the title of this note. On you go.

One thing I should have mentioned is that a structure $\langle I, A, B, n \rangle$ is a possible model for multi-sorted signatures:
$i : I$ models a sort.
$a : A(i) $ models an operator with target/output sort $i$ .
$b : B(i,a)$ models an operand of the operator $a$ with target sort $i$ .
$n(i,a,b)$ models the sort of operand $b$ of the operator $a$ with target sort $i$ .
The structure (and presumably the other variant of it) is remarkably rich in applications. (I mentioned above that it serves also as a model for command-response interfaces, with $I$ modelling a state space, $A$ commands, $B$ responses, and $n$ the next-state function. Or if I didn’t, I should have.)