Skip to content

Commit

Permalink
Allow representing a zipper as a context "list"
Browse files Browse the repository at this point in the history 
Instead of having an inductive datatype for representing a zipper, we
can also use a "list" of the various fragments. Due to the type indexes,
we can't use a standard list but we need something fancier.

To show that we got this right, "prove" the equivalence of the two
representations by defining an isomorphism between the two.

I must say, I am positively amazed by how well GHC supported me in this
task. Agda has still the upper hand with its better tool support, but
writing this code was too much fun.
  • Loading branch information
@Blaisorblade
Blaisorblade committed Oct 5, 2014
1 parent 6e8f451 commit cf2f6f5
Showing 1 changed file with 29 additions and 0 deletions.
29 changes: 29 additions & 0 deletions src/Zippers.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,35 @@ data ASTZipper dom (sigHoles :: HList) sig where
-- argument type for the given left sibling.
ZRight :: AST dom (a :-> sig) → ASTZipper dom (sig ::: sigs) sigTot -> ASTZipper dom (Full a ::: sig ::: sigs) sigTot

-- Instead of having a type representing the complete zipper, we
-- can also have separate individual contexts. The only downside is that we
-- need a specialized list type for that.

data ASTZipperF dom sigTop sigNext sig where
FZLeft :: AST dom (Full a) → ASTZipperF dom (a :-> sig) sig sigTot
FZRight :: AST dom (a :-> sig) → ASTZipperF dom (Full a) sig sigTot

This comment has been minimized.

Sign in to view

Copy link
@Toxaris

Toxaris Oct 6, 2014

I would call this a context frame (as in: "stack frame"). Then a context is a list of context frame, just like a stack is a list of stack frames. I think I picked up this terminology from Danvy.

-- The same structure essentially appears in Agda's standard library (it's a
-- reflexive transitive closure IIRC), except for the extra `sig` parameter.

This comment has been minimized.

Sign in to view

Copy link
@Toxaris

Toxaris Oct 6, 2014

You mean Data.Star?
data ASTZipperL dom (sigHoles :: HList) sig where
LNil :: ASTZipperL dom (sig ::: HNil) sig
LCons :: ASTZipperF dom sigTop sigNext sig → ASTZipperL dom (sigNext ::: sigs) sig → ASTZipperL dom (sigTop ::: sigNext ::: sigs) sig

-- Let's "prove" (as far as possible in Haskell) that these structures are
-- essentially isomorphic.
zipperIsoL :: ASTZipperL dom sigHoles sig → ASTZipper dom sigHoles sig
zipperIsoR :: ASTZipper dom sigHoles sig → ASTZipperL dom sigHoles sig

zipperIsoL LNil = ZHole
zipperIsoL (LCons (FZLeft arg) zips) = ZLeft (zipperIsoL zips) arg
zipperIsoL (LCons (FZRight f) zips) = ZRight f (zipperIsoL zips)

zipperIsoR ZHole = LNil
zipperIsoR (ZLeft rest arg) = LCons (FZLeft arg) (zipperIsoR rest)
zipperIsoR (ZRight f rest) = LCons (FZRight f) (zipperIsoR rest)


-- Functions for "normal" zippers.
goLeft :: ASTLocation dom (Full a ::: sig ::: sigs) sigTot → ASTLocation dom (a :-> sig ::: sig ::: sigs) sigTot
goLeft (Loc arg (ZRight f parent)) = Loc f (ZLeft parent arg)

Expand Down

10 comments on commit cf2f6f5

@Blaisorblade
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Toxaris, WDYT?

@Blaisorblade
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the comments, but do you like it? It was relatively quick for me (after reimplementing syntactic and having studied zippers in detail recently), but I feel that this couple of days were simply more productive than usual.

@Blaisorblade
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See also emilaxelsson/syntactic#19.
And emilaxelsson/syntactic#16, on pattern synonyms.

I care about all of this because I realized syntactic is a (possibly much cooler) variant of the encoding of constant we use in ILC in Scala, and is probably superior to what we use in Agda for constants. Constants are applied to arguments one at a time (as in currying), but you can distinguish a fully applied constant (because constants have signatures param1 :-> param2 :-> ... :-> Full result, a bit like CBPV).

@Blaisorblade
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When I asked for comments, I forgot to say the main point: zippers are not in the paper on syntactic, nor in the package itself, so the whole Zippers.hs is novel.

@Toxaris
Copy link

@Toxaris Toxaris commented on cf2f6f5 Oct 9, 2014

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I don't really understand what you want feedback about. Are you asking about this commit or these files in general? Maybe you can show me what's going on here in person next week?

Is syntactic the library based on Emil Axelsson's 2012 paper? I think that's almost the same thing as what we do in the ilc-agda codebase, just that in Agda, one can encode it in a more light-weight and more obvious way. As you say, in syntactic, the static type of a constant includes information of the form param1 :-> param2 :-> ... :-> Full result. This is just an encoding of a list of types [param1, param2, ...] and another type result. In ilc-agda, the static type of a constant includes a list of types and the result type as type tags. So the difference appear to be:

  • ilc-agda uses a universe construction, syntactic uses types directly.
  • ilc-agda uses standard lists, syntactic uses an encoding of lists.

I think these different choices come from the differences between Agda and Haskell.

@Blaisorblade
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I don't really understand what you want feedback about. Are you asking about this commit or these files in general? Maybe you can show me what's going on here in person next week?

Let's talk in person, yes. (Also about my other points below).
But basically, I reimplemented Axelsson's syntactic (yes, it's the library from his ICFP 2012 paper), then added two forms of zippers to it more or less overnight (the paper mentions that as possible future work), and I wonder how cool these zippers are.

Is syntactic the library based on Emil Axelsson's 2012 paper? I think that's almost the same thing as what we do in the ilc-agda codebase, just that in Agda, one can encode it in a more light-weight and more obvious way. As you say, in syntactic, the static type of a constant includes information of the form param1 :-> param2 :-> ... :-> Full result. This is just an encoding of a list of types [param1, param2, ...] and another type result. In ilc-agda, the static type of a constant includes a list of types and the result type as type tags. So the difference appear to be:

ilc-agda uses a universe construction, syntactic uses types directly.
ilc-agda uses standard lists, syntactic uses an encoding of lists.

That's fine for the types, but what about the applied constants themselves? What's the AST for + 1 in ilc-agda? There's no such thing :-(. I suspect this is a bad smell, but I don't get it well enough for DSLDI.

I think these different choices come from the differences between Agda and Haskell.

I think there's more. With ilc-agda you only have fully applied constants as parts of the AST, unlike with Syntactic or ilc-scala. We had our reasons for this choice, but Syntactic addresses these as well.
Let me give a teaser: I believe with Syntactic, I wouldn't have need to come up with this kind of type signatures (note take and drop) for doing recursion on the argument list:

https://github.com/inc-lc/ilc-agda/blame/573930b7dfef998446b5cfac86d34434385bd338/Parametric/Syntax/Term.agda#L384-L388

(I also punted on that). Syntactic would have been better at the task, because there is an AST for + 1 (and partially applied constants in general).

I don't claim there is no better solution for what I wanted to do, but I do believe that ilc-agda made the task complicated enough to allow failure.

@Toxaris
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the AST for + 1 in ilc-agda? There's no such thing :-(

What's the AST for + 1 on the whiteboard? There is no such thing.

@Blaisorblade
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the AST for + 1 on the whiteboard? There is no such thing.

It depends. If + is a curried infix operator (as in Haskell), you have an AST for + 1, and I believe that's useful.

@Toxaris
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, and the ilc-agda encoding supports this, doesn't it? But here, you're asking for an AST for + 1 even if + is not curried.

@Blaisorblade
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yep: Syntactic provides that AST, whether or not you have functions in your language. (So I'm confused how useful this is, if you do have abstraction and application; but that's a separate story). I'll need to see whether this structure simplifies writing the transformations I have in mind (the one to CBPV). (In fact, I need to process arguments left-to-right, but maybe I can use Danvy's "There And Back Again" (TABA) pattern).

Please sign in to comment.