Read on Twitter
how to put this picture in a bottle?
choose a node and a sector from which to start
construct a spanning tree, depth first; working anticlockwise, follow edges if they lead to somewhere you haven’t been yet
when you meet an edge that’s new to you, but it leads to somewhere you’ve been, jump *over* it
when you get back to where you came in, go back where you came from
when you meet the other end of an edge you’ve already jumped over, duck under it
and keep on going...
...until you’re back to your starting node and sector
now, erase the interior of the black loop and deform it into a single node; the remaining edges are exactly those which were *not* part of the spanning tree; they’re the ones you went over then under
I deformed it some more; note that we started planar if and only if we’re still planar
walk anticlockwise round the node; record your reconnection debt; i.e., remember which edges you’ve seen exactly *once*; the graph is planar if and only if this debt obeys the *stack* discipline; last in first out
stack discipline is locally enforceable by indexing...
stacks are snoc-lists of edge labels; I write -, for snoc and ,- for cons; I consider both : and :: too symmetrical
besides which, : is sacred
construct the free category, as cons-lists; aka reflexive-transitive closure
we can generate a free category from valid stack transitions
to get spanning trees, we can add one last generator, allowing us to visit a subtree by following an edge; we record the label of the vertex we visit; ez’ is the stack of edges we visit once in that subtree that we must complete after we get back; i.e., we go depth first
note that this definition is not in conflict with “rotation systems”: it is rotation systems! it’s just that I happen to be storing the rotations around each node in a tree, which happens to be a spanning tree
so here’s the picture, rendered data with intrinsic validity; I drew out the spans as edges and joined the pushes to their pops; it’s visibly planar
BUT not all is well...
DON’T TOUCH THE GREEN SLIME!
remember this? what if we wanted to be somewhere else?
what sort of a thing was a “here”? not just a node, but a *sector*; let’s play spot-the-sector
before we do that, I just spotted a typo; that * should have been there all along
I drew a blue box in each sector; we’re always in one of them, but we should be able to move to any other; spot the off-by-one error in the making? all but one vertex in the spanning tree has a parent
now imagine turning this into a parametrized data structure Planar X, where there is an X stored in each blue box; Planar is a comonad; the counit projects out the X where you are; the comultiplication labels each sector with the graph refocused from that sector
here’s what the comultiplication does (for every sector, not just the one which was handily near a blank bit of board): it replaces each sector’s payload by a local copy of the original graph, rooted instead at *that* sector; same graph, different spanning tree
the key to implementing the comultiplication is rotation; rotating these stack-safe sequences denormalizes them: if I move a push from the start to the end, it might end up after its pop, in which case I need to swap which is which
if you have any sequence of stack transitions and you pick a stack entry, you can tell which of two ways the sequence decomposes; either it stays firmly above the entry, or it eventually gets down to the entry and pops it, then does whatever else it likes
computing which of those two decompositions we get and grabbing the components is easy; proving that the original sequence can be recovered from the components is harder; it would be easy if I had only push and pop, but... span has deadly green slime
the typechecker doesn’t internalize the equational theory of ++ (or monoids, more generally), so I have a lot of repair work to do; that a sequence stays above a given stack level is also characterized in terms of ++
adding a “skyhook” edge by which you hold the root gets rid of the off-by-one error (or commits it, depending on your point of view)
we can allow a spanning subtree to have initial and final stacks of connection debt; by doing so, we no longer commit to exploring depth-first; is this redundancy good or bad? yes, I guess
and with fewer colour errors; every edge takes us to another sector
and there was no green slime; the span g is an excursion along g’s skyhook, popping some old connection debt, but pushing new
there’s an operation which allows us to add more connection debt to the global end of input and output stacks, extending to a functor on transition sequences; it looks a lot like the identity function; it ought to be subsumptive subtyping
Stack is not just a set but a monoid; we’re not only indexing over stacks; we’re appropriately functorial; stack transitions monkey about at the near end, so we can shove extra stuff at the far end; our current dependent datatypes give no way to give functoriality by construction
