How to navigate up inside a HUET Zipper

Question

I'm reading Huet Zipper, I cannot understand the go_up method:

let go_up (Loc(t,p)) = match p with
Top -> failwith "up of top"
| Node(left,up,right) -> Loc(Section((rev left) @ (t::right)),up);;

The full source of other types definitions can be found in the linked paper, if you understand Zipper, I think that doesn't matter to answer my question.

From what I know about Zipper, a Location contains the current node and its Path or the so called Context. The Path has everything other than the current node and its subnodes, or some people called it a one-hole-context.

Well, moving the focus up, means the parent node of the current node will become the new current node. But here, the author concatenates the current nodes and its siblings. But that's not a parent node, just the children of the parent node. I am stuck at here when implementing my own moveUp method in Scala, and failed to correctly represent the parent node of the current node.

Edacity

You might get inspiration from a former n-ary zipper implementation of mine: gist.github.com/3477576 – Nonfulfillment

@Nonfulfillment Your context always holds a reference to the parent node data, the context from this paper doesn't. I've seen others, instead of holding a parent context, they hold a parent location, which also gives you the chance to access parent node. – Edacity

You may not care if porting to another language, but rev foo @ bar would benefit from being written List.rev_append foo bar, which will traverse foo once instead of twice. – Holter

Answer 1

The zipper here is for the following tree datatype:

type tree =
   Item of item
 | Section of tree list;;

And the path datatype from the paper is this:

type path =
   Top
 | Node of tree list * path * tree list;;

The Node contains three components. The children of the parent node that are to the left of the hole (left), the path further up (up), and the children of the parent node that are to the right of the hole (right).

When moving up, in order to produce the actual parent node, we have to plug in the old tree t at the right position in between left and right. As the children to the left are stored in reverse order, we have to reverse them first.

Tiemannite

in order to produce the actual parent node, we have to plug in the old tree t at the right position in between left and right. but plugin t into the right position between left and right, only produce a children of parent, not the parent. I know Section is type of tree, but that doesn't mean if you navigate down from a single parent node, and then you navigate up, you got a Section of nodes as the parent node. – Edacity

@Edacity if you down then up you do get a Section, because the only other choice would be Item, but Item has no children so you couldn't have gone down in the first place. – Holter

@Edacity As gasche says in his other answer, there's nothing more to a node in this definition of tree than its list of children. If we can reconstruct the list of children of the parent node, we can also reconstruct the parent node itself by applying Section to it. (Note that this happens in a functional setting; there's no object identity.) – Tiemannite

Answer 2

the author concatenates the current nodes and its siblings. But that's not a parent node, just the children of the parent node

With the paper definition cited by kosmikus, a non-leaf node Section is defined by nothing other than its children. If you have added additional information, you must add it to the definition of the zipper.

Holter