Consider adding zippers?

[Blaisorblade]

@emilaxelsson , your paper mentions that adding generic zippers based on Syntactic seems possible. It turns out that you're right, at least on a modern GHC (I've used 7.8.3, mostly because of pattern synonyms) and type-level lists (I've also done it without, but the resulting API has less precise types):

https://github.com/Blaisorblade/learning-syntactic/blob/master/src/Zippers.hs

• What do you think about it? This is not particularly refined yet, but it should be highly typesafe and I've tested some basic examples.
• Would you be interested in having this code in the library?
  If compatibility with older GHC is interesting, one could probably avoid DataKinds by doing the desugaring by hand, and maybe also other features.
  Also, I just realized I picked the MIT license instead of the BSD license, but that's not a problem (and I could even relicense the code).

BTW, I'm a PhD student in the area, so should you think this is worth writing about, I'd be interested. Right now it does not seem so interesting to deserve a paper on its own, but it seems like it would belong in a revised version of your paper.

[emilaxelsson]

Looks, nice! I'm snowed under with teaching at the moment, so I'll have to wait with taking a closer look. Are you using the same approach as in Scrap-Your-Zippers, or is it something else?

In any case, I would definitely like to have it in the library. Older GHC compatibility is not so important now that GHC 7.8.3 is in the Platform. (There are also things in the library that could be modernized; e.g. some type classes with fundeps that could be rewritten using closed type families.)

[Blaisorblade]

Happy you're interested!

Are you using the same approach as in Scrap-Your-Zippers, or is it something else?

I didn't read that paper yet (and I'm snowed under with moving, so I shouldn't read it so quickly), but it might well be. I was inspired by your related work section (in the ICFP 2012 paper), in particular this paragraph:

Another use of a spine data type is found in Adams’ Scrap Your Zippers [1], which defines a generic zipper data structure. The Left data type—similar to our AST—holds the left siblings of the current position. Just like for AST, its type parameter specifies what arguments it is missing. The Right data type—reminiscent of our Args—holds the right siblings of the current position, and its type parameter specifies what arguments it provides. This similarity suggests that it might be possible to implement a similar generic zipper for the AST type.

However, I treat AST as a binary tree to derive a zipper, so each "zipper piece" (ASTZipperF) contains one left or right sibling, not siblings as in the above.

[emilaxelsson]

Ah, I see. I suppose that can be useful, but one probably also wants zippers where one can only focus fully applied symbols, as that's what corresponds to nodes in a normal data type. (OTOH I don't really have a usecase for either version.)

But please send a pull request for your zipper implementation when it's ready.

[Blaisorblade]

I see your point — I'll take a look at it, and at a pull request, when I next have time. (Semester's starting here :-( ). I have some use cases in mind where this kind of zipper might be useful.

[Blaisorblade]

It seems that each "fragment" of "your zipper" (i.e., only focusing on fully applied symbols) is one of "my zippers", where both sides of the zippers have type Full t (a bit like ASTF); one just needs a list which requires this constraint on signatures, and allows composing compatible zippers (this second point is the same of ASTZipperL — both lists create a free category of zippers).

See ASTZipperLF for what seems an implementation (not sure yet).
Blaisorblade/learning-syntactic@bb1db93...9984a2f

[emilaxelsson]

Now that I think about it, what I was after was probably just to be able to navigate through fully applied trees -- it doesn't really matter what the internal representation is.

I played with your code, and came to the following functions for navigating horizontally:

goLeftFull
    ∷ ASTLocation dom (Full a ::: sig ::: sigs) sigTot
    → (∀ b. ASTLocation dom (Full b ::: (a :→ sig) ::: sig ::: sigs) sigTot → c) → c
goLeftFull l = goSecond (goLeft l)

goRightFull
    ∷ ASTLocation dom (Full b ::: ((a :→ sig) ::: (sig ::: sigs))) sigTot
    → ASTLocation dom (Full a ::: (sig ::: sigs)) sigTot
goRightFull l = goRight (goUp l)

It seems harder to implement goFirstFull and goUpFull. For these you'd need to generate evidence to know how many times to go left or up. But that should be doable.

[Blaisorblade]

Makes sense, though I'm not sure of the details and can't fully get in (should find a 4-hour block for looking at this properly). Here's what I figured in less than that:

For these you'd need to generate evidence to know how many times to go left or up.

The real problem is for typing the operations. With some thought, I believe that the runtime evidence for running the operation is in the data structures themselves, though I'm not 100% sure.
For typing, there's some design space: sigs in the output type doesn't depend so easily on the input type, but on the input value, so one has to return an existential (encoded via CPS). Optionally, one can write a first function (with an existential type) that looks at the tree and produces evidence of how many steps one has to walk left/up, and a second function that does the walking based on the evidence. The only advantage of the split seems that the second function has a more precise type, but that seems only useful if you can produce your evidence statically (so that it has a non-existential type).

But if goUpFull returns ASTLocation dom (Full a ::: sigs) sigTot (where I just replaced sig with Full a in goUp's signature), then you are getting either to an ZRight argument or to the top (I verified this on the ASTLocationL variant by case splitting on ASTLocationL dom (Full a ::: sigs) sigTot — I think I did by hand what Agda would do automatically if you keep case-splitting).

goFirstFull can't get to something with a Full type (because it gets to the head of an application, which has a :→ type), but it seems it just needs to get to a left-most Sym-node, so again you know by pattern-matching where to stop.