Here’s a story I’ve had on the go for a while.
It’s an experiment in managing the multitudinous variations on the theme of a datatype, inspired by this overlay from a talk I gave ten years ago. If you squint hard at it, you can see that it shows the difference between lists and vectors. Let’s see how to formalize that notion as a big pile of Agda. The plan, of course, is to do something very like this for real on Epigram’s built in universe of datatypes.
I’ll need some bits and bobs like Sigma-types (Sg). Step one. Build yourself a little language describing indexed functors.
Descriptions
data Desc (I : Set) : Set1 where
say : I -> Desc I
sg : (S : Set)(D : S -> Desc I) -> Desc I
ask_*_ : I -> Desc I -> Desc I
What do these things mean?
[_] : forall {I} -> Desc I -> (I -> Set) -> (I -> Set)
[ say i' ] X i = i' == i
[ sg S D ] X i = Sg S \ s -> [ D s ] X i
[ ask i' * D ] X i = X i' * [ D ] X i
Here, [ D ] X i is the set of D-described data which say they have index i; everywhere the description asks for some index i’, the corresponding set has an X i’. Meanwhile sg just codes for ordinary Sg-types, allowing nodes of datatypes to be built like dependent records. The X marks the spot for recursive data. Our next move is to take a fixpoint.
data Data {I : Set}(D : Desc I)(i : I) : Set where
<_> : [ D ] (Data D) i -> Data D i
I guess I’d better give you an example. Let’s have natural numbers. First, I define a datatype of constructor tags with a snazzy dependent eliminator, designed to make higher-order programming look first-order.
data ZorS : Set where
ze su : ZorS
ze->_su->_ : forall {a}{P : ZorS -> Set a} ->
P ze -> P su -> (c : ZorS) -> P c
ze->_su->_ pz ps ze = pz
ze->_su->_ pz ps su = ps
And now I can write down a description for Nat.
NatD : Desc One
NatD = sg ZorS (
ze-> say _
su-> ask _ * say _ )
Now define
Nat : Set
Nat = Data NatD _
zero : Nat
zero = < ze , refl >
suc : Nat -> Nat
suc x = < su , x , refl >
map and fold
We can build data, but can we compute with them? You’ll find you can work on individual datatypes just fine by pattern matching. But we get generic patterns, too. Here’s map (I said [ D ] was a functor, didn’t I?).
_-:>_ : {I : Set} -> (I -> Set) -> (I -> Set) -> Set
X -:> Y = {i : _} -> X i -> Y i
infix 40 _-:>_
map : forall {I X Y}(D : Desc I) ->
(X -:> Y) -> [ D ] X -:> [ D ] Y
map (say i) f q = q
map (sg S D) f (s , xs) = s , map (D s) f xs
map (ask i * D) f (x , xs) = f x , map D f xs
And here’s fold: the termination checker doesn’t like it, so the Desc file also contains an annoyingly specialised workaround.
fold : forall {I X}{D : Desc I} ->
([ D ] X -:> X) -> Data D -:> X
fold {D} phi < ds > = phi (map D (fold phi) ds)
That ([ D ] X -:> X) is a D-algebra, explaining how to build X values the same way we build Data D values. Let’s check that we can still add. I define addition as a fold, where (adda y) is the algebra which adds y.
adda : Nat -> [ NatD ] (k Nat) -:> k Nat
adda y (ze , refl) = y
adda y (su , z , refl) = suc z
_+_ : Nat -> Nat -> Nat
x + y = fold {X = k Nat} (adda y) x
Ornaments
We know what a theme is. What is a variation? Let’s see how to ornament a description. For starters, we can replace a boring index type, I, with a fancy index type, J, provided we have a function f : J -> I which forgets the fancy stuff. We’ll often need to pick elements of J which fit with a given i : I. We need the inverse image:
data _^-1_ {I J : Set}(f : J -> I) : I -> Set where
ok : (j : J) -> f ^-1 (f j)
Now we can explain how to scribble over a plain old Desc I, turning it into a fancy Desc J. The key points
- Everywhere the plain description has an i, we need some j which maps back to i, so we demand an element of (f ^-1 i)
- Anywhere we like, we can insert a demand for an extra non-recursive field.
data Orn {I}(J : Set)(f : J -> I) : Desc I -> Set1 where
say : {i : I} -> f ^-1 i ->
Orn J f (say i)
sg : (S : Set) {D : S -> Desc I} ->
((s : S) -> Orn J f (D s)) ->
Orn J f (sg S D)
ask_*_ : {i : I} -> f ^-1 i ->
{D : Desc I} -> Orn J f D ->
Orn J f (ask i * D)
insert : (S : Set)
{D : Desc I} -> (S -> Orn J f D) ->
Orn J f D
Of course, we had better be able to read off the fancy description from the ornament which gives its difference from the plain. We just drop the new fancy J indices in place of the old plain I’s and turn the insertions into fields.
ornD : forall {I J f}{D : Desc I} ->
Orn J f D -> Desc J
ornD (say (ok j)) = say j
ornD (sg S O) = sg S \ s -> ornD (O s)
ornD (ask (ok j) * O) = ask j * ornD O
ornD (insert S O) = sg S \ s -> ornD (O s)
Let’s have a nice simple example: making List X from Nat. Note that the indexing stays trivial.
ListO : Set -> Orn One _ NatD
ListO X = sg ZorS (
ze-> say (ok _)
su-> insert X \ _ -> ask (ok _) * say (ok _) )
See? In the successor case, we stuff in an extra field of type X. Lists are labelled Nats! Just to check.
ListD : Set -> Desc One
ListD A = ornD (ListO A)
List : Set -> Set
List X = Data (ListD X) _
[l] : forall {X} -> List X
[l] = < ze , refl >
_:l:_ : forall {A} -> A -> List A -> List A
x :l: xs = < su , x , xs , refl >
Ornamental Algebras
What have we bought with this more nuanced presentation of List X? What connection with Nat have we established? Given that we know what extra we have added, the least we can expect is to rub the extras out. Every ornament induces a forgetful function from fancy data back to plain. Moreover, this function is a fold by the ornamental algebra.
forget : forall {I J f}{D : Desc I}(O : Orn J f D) ->
(Data (ornD O)) -:> Data D o f
forget O = fold (ornAlg O)
The carrier of the ornamental algebra has to be a J-indexed set, but plain Data D : I -> Set, so we compose with our forgetful f : J -> I to get (Data D o f) : J -> Set. We turn fancy records with index i into plain Data D (f i), by packing up plain records…
ornAlg : forall {I J f}{D : Desc I}(O : Orn J f D) ->
[ ornD O ] (Data D o f) -:> Data D o f
ornAlg D ds = < ornAlgHelp D ds >
…so we need to turn fancy records into plain records just by deleting fields which arose by insert.
ornAlgHelp : forall {I J f}{D : Desc I}
{R : I -> Set} ->
(O : Orn J f D) ->
[ ornD O ] (R o f) -:> [ D ] R o f
ornAlgHelp (say (ok j)) refl = refl
ornAlgHelp (sg S O) (s , rs) =
s , ornAlgHelp (O s) rs
ornAlgHelp (ask (ok j) * O) (r , rs) =
r , ornAlgHelp O rs
ornAlgHelp (insert S O) (s , rs) =
ornAlgHelp (O s) rs
See? It acts like the identity in all but the last case! Of course, we get
length : forall {A} -> List A -> Nat
length {A} = forget (ListO A)
Phew!
Algebraic Ornaments
Breath back? Well then! We’ve seen how to make an algebra from an ornament, but we can also go the other way around. If we have an algebra (a structural way to compute values from data), we can use it statically to enforce compatibility of data with the algebra. We get a fancier kind of indexed data by an algebraic ornament.
algOrn : forall {I J}(D : Desc I) ->
([ D ] J -:> J) -> Orn (Sg I J) fst D
algOrn (say i) phi = say (ok (i , phi refl))
algOrn (sg S D) phi =
sg S \ s -> algOrn (D s) (phi o _,_ s)
algOrn {J = J} (ask i * D) phi =
insert (J i) \ j ->
ask (ok (i , j)) * algOrn D (phi o _,_ j)
We start with D : Desc I, but we have an algebra phi which computes J’s. That means we can glue on an extra J-index. The idea is that we copy our way along D, feeding fields to phi. When we reach the end, phi tells us what J to say (along with the i : I we said before). But whenever D asks for recursive data, we need to know which J to ask for in the fancy version, so we insert an extra J field. We can have any indices we like in recursive positions, and phi will use them to compute the index we deliver at the end.
We’d better have a concrete example. What ornament is induced by the (adda y) algebra? It’s just the number-like thing whose indices are guaranteed to be in the image of adding y: we get the ≥ relation.
GeD : Nat -> Desc (One * Nat)
GeD y = ornD (algOrn NatD (adda y))
Ge : Nat -> Nat -> Set
Ge x y = Data (GeD y) (_ , x)
geq : {y : Nat} -> Ge y y
geq {y} = < ze , refl >
ges : {x y : Nat} -> Ge x y -> Ge (suc x) y
ges p = < su , _ , p , refl >
Just checking:
trans : forall {x y z} -> Ge x y -> Ge y z -> Ge x z
trans < ze , refl > q = q
trans < su , _ , p , refl > q =
< su , _ , trans p q , refl >
The Algebraic Ornament from the Ornamental Algebra
I’ve shown you how to make (List X) from Nat. In fact, that tells us exactly how to make (Vec n X) from (List X). The ornamental algebra for lists tells us their length: the corresponding algebraic ornament indexes lists by their length.
VecO : (X : Set) -> Orn (One * Nat) fst (ListD X)
VecO X = algOrn (ListD X) (ornAlg (ListO X))
VecD : (X : Set) -> Desc (One * Nat)
VecD X = ornD (VecO X)
Vec : Nat -> Set -> Set
Vec n X = Data (VecD X) (_ , n)
[] : forall {X} -> Vec zero X
[] = < ze , refl >
_::_ : forall {X n} -> X -> Vec n X -> Vec (suc n) X
x :: xs = < su , x , _ , xs , refl >
So there you are! Vectors emerge for free when you make lists by ornamenting lengths.
Loose Ends
There are lots of things I haven’t said, mostly because I don’t know what exactly to say.
- What does algorn D <_> give you? Ornamenting by the initial algebra gives you a structure you can use to pack up the inductive hypotheses in a proof by induction. I’ve proved an induction principle this way, but it’s annoying to use.
- I’ve proved a less pretty but more ergonomic induction principle for Desc I.
- An algebraic ornament comes with a ‘remember’ operation which takes plain data to fancy data, using the algebra to compute the extra index information. That’s definable by induction. E.g., remember takes a list to a vector with the list’s length.
- If you take some fancy data in an algebraically ornamented type, forget its index, then recompute it using the algebra, (GASP!) you get the index you started with.
- Here’s a very cheeky proof of compiler correctness for Hutton’s Razor. Summary: an expression e should compile to code compatible with e’s meaning; oh look; it does.
- I suspect something highly amusing happens when we try to ornament the more sophisticated universe in The Gentle Art of Levitation. There, we pay much closer attention to the flow of index information, and we correspondingly avoid a lot of mucking about with equality. My guess is that the work will get easier (but a wee bit longer).
- It’d be lovely to figure out how to lift ornaments to functions over data (how to get ++ from + ?). To do that, we really need to build a universe of ornaments for algebras, compatible with these ornaments for functors.
- It’s time I finished the paper.