Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Examples using pattern synonyms? #16

Open
Blaisorblade opened this issue Oct 2, 2014 · 1 comment
Open

Examples using pattern synonyms? #16

Blaisorblade opened this issue Oct 2, 2014 · 1 comment

Comments

@Blaisorblade
Copy link

It seems that pattern synonyms are perfect for scenarios like using the syntactic library, so, in case you don't know them already, you might want to take a look at Blaisorblade/learning-syntactic@a209c3c is an (improvable) example.

This is mainly a comment; the only actual "issue" is that examples should probably suggest this usage. GitHub search on this code didn't find any example though.

Reading your ICFP 2012 paper and searching "Combining Deep and Shallow Embedding for EDSL" found no hint about that (probably because pattern synonyms are newer than these papers). Your ICFP2012 paper (in Sec. 3.2) explicitly discusses the overheads with pattern matching that pattern synonyms arguably solve.
Blaisorblade referenced this issue in Blaisorblade/learning-syntactic Oct 2, 2014
@Blaisorblade
Showcase pattern synonyms + view patterns
a209c3c 
Compare optAddTop and optAddRule: the latter looks comparable to a
standard pattern matching, and the encoding overhead is reduced to the
occurrences of :$ and to using yet another identifier referring to the
`ADD` and `NUM` constructors. Bidirectional patterns could simplify even
that, I guess.
Blaisorblade referenced this issue in Blaisorblade/learning-syntactic Oct 6, 2014
@Blaisorblade
Allow representing a zipper as a context "list"
cf2f6f5 
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.
@emilaxelsson
Copy link
Owner

Thanks for the suggestion!

I've looked very quickly at pattern synonyms before, but haven't tried to use them in Syntactic. I like your example. I wasn't aware that they could be combined with view patterns in the way that you do. Very nice!

If you want, you could add a file under examples demonstrating pattern synonyms. Pull requests are welcome!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Blaisorblade @emilaxelsson