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 form the first number class, the countable Brouwer-ordinals
form the second, and you can push on further into the so-called `finite’ number classes in the obvious way, by chucking in a to the functor whose gave you the previous number class . (You can think of these sets as `aleph numbers’ .)
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 `‘ one takes the union of the finite number classes, and then presses on as in the step from to . In type theory, the theory of the finite number classes is quite interesting (there are some well-cool `collapsing functions’ )), 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.
The initial algebras of these chaps are, successively,
(Now you can maybe see why I wrote rather than .)
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 .
And of course, these functors are given by containers: ,
Moreover, it is obvious that there are natural transformations from to all the way up. Taking the colimit of this series (the formalisation requires a universe to `recurse into’), we get a functor whose is , and whose value at 0 is .
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.