I spent some time the other day thinking about zippers and structural editors and I wanted to share some of the ideas, because they were interesting, so this is going to be a thread about that
Discussion
this is basically an insertion zipper for a text editing string, which is a neat fact
perhaps we can make some larger unification of these ideas to understand how to get insertion editing operations for trees!
the observation to make is that if we view a text insertion zipper as a normal tree overtype zipper on a string, rather than a true insertion zipper, we can analyze insertion and overtype as follows:
a string-with-insertion-cursor, such as
fo|o
corresponds to the tree zipper
"o" @ "fo_"
where the LHS of @ is the thing in focus, the RHS is the one-hold context (with an _ representing the hole)
the act of typing a character, such as 't' should produce the string-with-insertion-cursor
fot|o
which is
"o" @ "fot_"
which is equivalent to updating the zipper to
"to" @ "fo_"
and then navigating to the next recursive tree position
but when we view these tree contexts through McBride's tube view, where a one hole context is a stack of frames of local subtrees, we get this:
fo|o
is the tube-y zipper
"o" @ [ 'o':_, 'f':_ ]
and
fot|o
is
"o" @ [ 't':_, 'o':_, 'f':_ ]
from this perspective, we can describe the insertion operation as follows:
1. we have a whole subtree "o" to operate on
2. we want to insert a single character 't'
3. we find the unique list/string constructor that has a single char arg and a single list arg: cons (`:`)
4. we partially apply cons (`:`) to the single char 't', and form a one hole zipper 't':_
5. we push that onto the tube-y context stack
now, we could view key presses as complex commands, which specifically mean that precise thing. and that's fine. but i want to generalize this and think about something a bit more eh.. rich?
i phrased the above sequence of operations the way i did because i want to consider the possibility that our tree structure isn't as simple as lists
instead, lets imagine that its some arbitrary tree type that has many constructors some of them with char args
for instance, i dunno, something like
data Tree = Z | O Char Tree | T Char Tree Tree
now when we press a single key, we look at step 3 and say, well, there is a unique constructor `O` that takes a char and a recursive tree, yes, indeed, so we can push `O 't' _` to the stack
but there's ALSO a constructor `T` that takes two recursive trees
we obviously can't use that right? i mean, which subtree gets the hole? and what do we put in for the other subtree?
well if we have a way of representing an as of yet un-filled portion of a tree (also called a "hole" but this type a different sort, so i'll just call it a "gap" for clarity), we can say this:
we can also add either of
T 'f' _ ?
and
T 'f' ? _
to the stack as well
here i'm using ? to represent gaps that must be filled in eventually
so here we have a situation where a single key press can reasonably suggest edits that "insert" three different kinds of tree nodes:
an O node, that's like a string insertion
a T node with a gap on the right
a T node with a gap on the left
from a UI perspective, we have an ambiguity here, in terms of what is intended by the user with the single keypress
this could be resolved with different modes selected prior to the keypress, or by offering up the different options with one selected as a default