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.
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
Untyped Template Haskell quotes as patterns #529
base: master
Are you sure you want to change the base?
Untyped Template Haskell quotes as patterns #529
Conversation
Can flush out with quick summaries later
A few questions about the interpretation of quotation patterns: Would you allow any of the following, and would they recognize precisely the lambda expressions?
Is Given that the language in the module that invokes the metaprogram that uses a quotation pattern may be using different GHC extensions than the module in which it occurs, what happens if there's e.g. |
Returns
Returns
I assume you meant Those would not be equivalent because the syntax being matched is different even though syntax has the same semantics. (It would be interesting to do macros that respect various equational theories on syntax, but that is a huge leap from what we have today with Template Haskell. I think it is better to leave that out of scope.) Instead, I rather create new splicing forms that allow one to e.g. splice (in positive and negative position) a list of parameters. e.g. suppose we could could do isLambda [| \$(x) $..(_) -> $(_) |] = True and that would match both \(Pat foo) -> ignored
\(Pat foo) ignored -> ignored in both cases binding My brief experience with @int-index exploring converting Still, this too I think is best left as future work. We can nail down the core feature now, and then with a good foundation open the floodgates to much more quoting/splicing flexibility, I think that will work better. |
WRT the related work in Racket, the gold standard is no longer The relevant paper is "Fortifying Macros" by Culpepper and Felleisen, and there's a Haskell implementation of its core as part of Crucible's concrete syntax. |
Thanks to @th-quotes-as-patterns; I am basically just including his comment at ghc-proposals#529 (comment)
Updated to properly distinguish Scheme and Racket :), thanks @david-christiansen |
@Ericson2314, are you by any chance attending Haskell Symposium? If so, would you like to present this proposal at the GHC Proposals session? |
@nomeata I unfortunately am not going to ICFP --- and feeling some regret right now for sure! |
Hmm I guess I forgot to submit this to the committee? |
Looks like it :-). Is it ready fonr submission? |
@nomeata I think so! I mean to submit it. |
Good idea, thanks!
And clarify declaration pattern matching.
48f23b4
to
6788cba
Compare
As far as terminology is concerned, I'd like to suggest to make a distinction between "pattern quotes" and "quote patterns". Pattern quote: a Template Haskell quote that constructs a pattern, i.e. Based on this terminology, |
I like that, @int-index. But moreover I would love to wash my hands of all name bike-shedding, purely following the consensus of others on this one :). So I hope you and @adamgundry can come to a decision on that! |
@adamgundry I believe I have addressed most of the issues, except for the naming issue, and expanding the Related Work section. Perhaps some sort of interactive discussion in what sort of topics would be useful to discuss, so I know what I should delve into. Maybe a good starting point is also that the Scheme family macros work fundamentally differently, in that that the binding structure is unknown because the syntax is sexpression of unknown meaning until the final splice. Whereas we quote actual Haskell expressions and thus the quote-internal binding structure is known from the get-go, before manipulation. Perhaps therefore the most important one to investigate is Rust, since it is very Racket inspired but does allow quotes of expression etc. (rather than mere "token tree", it's s-expression equivalent) like us. I am not at all familiar with what Idris and Lean do. |
I get the general motivation but lots of things are unclear here.
|
The examples point out that binding a name inside a quote-as-pattern is disallowed, so this is rejected because of the binding occurrence of f [| \x -> x |] = ... There is a bit more discussion of this in the Alternatives, section 6.2. The point is that picking the right semantics for such bindings seems nontrivial, so the proposal defers committing to a semantics. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Shepherd here. I've reviewed the updates and made a few more suggestions. Once @Ericson2314 has had a chance to look at these and @simonpj's comments, I'm inclined to recommend acceptance to the committee.
One other broad point: I'm a little worried that the implementation effort required for this proposal might be nontrivial. The Motivation section is clear when it comes to quotes of expressions, but could more clearly motivate support for quotes of other syntactic categories (notably declarations, where the restrictions on binding names seem to bite hard, and the fact that there may be more than one declaration needs thought). I can see that symmetry and consistency is one motivation, but are there motivating examples involving the other syntactic categories?
Note we do have quotes *of patterns* today (``[p| ... |]``), but that is orthogonal. | ||
This is quotes *as patterns*, the type of syntax being quoted doesn't matter and could be anything. | ||
The point is the quotes are in negative position. | ||
|
||
With this change put together, the hope is that a significant portion of TH out in the wild is going to be more stable across GHC versions. | ||
This is all accomplished without trying to minimize TH AST changes, which is quite a hopeless task and also a perverse incentive for the rest of language development. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My point wasn't that quasiquotes make this proposal superfluous: rather, quasiquotes can already generate patterns (quotePat
returns a Q Pat
) so it makes sense to extend this to TH quoters. (This is Simon's point 3 in #529 (comment).)
|
||
- https://arxiv.org/pdf/2001.10490.pdf | ||
|
||
Future Work |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I thought about this some more, and realised that ideally we would want TExp
to be a GADT, so that pattern-matching a TExp a
with [|| \ $(x) -> $(y) ||]
would refine a
to be a function type. This seems hard. But it's fine to have this proposal be about Untyped TH and leave TTH for future work. 😁
Relax the rules so that TH Quotes only impose a ``Quote`` constraint when ``newName`` is in fact needed. | ||
Otherwise, merely impose a ``Monad`` constraint. | ||
|
||
[This was a `alaternative that was rejected <./0246-overloaded-bracket.rst#alternatives>` of Proposal #246, but now we have additional movation for it (as detailed in "Effectas and Interactions") below.] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
[This was a `alaternative that was rejected <./0246-overloaded-bracket.rst#alternatives>` of Proposal #246, but now we have additional movation for it (as detailed in "Effectas and Interactions") below.] | |
[This was an `alternative that was rejected <./0246-overloaded-bracket.rst#alternatives>`_ of Proposal #246, but now we have additional motivation for it (as detailed in "Effects and Interactions") below.] |
- ``[| ... |]`` or ``[e| ... |]``, where "..." is an expression, is a pattern that matches ``Exp`` | ||
- ``[p| ... |]``, where "..." is a pattern, is a pattern that matches ``Pat`` | ||
- ``[t| ... |]``, where "..." is a type, is a pattern that matches ``Type`` | ||
- ``[d| ... |]``, where "..." is a top-level declaration, is a pattern that matches a ``List Dec`` with a single item. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm wondering about this restriction to a single item. Why is that needed? It seems a bit inconsistent with the fact that that quotes of declarations as expressions (and quasiquotes yielding declarations) may have multiple declarations.
For example, De Bruijn indices encode actions in a way that makes equality between the actions *themselves*, rather than their results, easily decidable. | ||
This would be a less hacky solution. | ||
|
||
Note that without this alternative, we still don't have to full back completely on not using our new feature for this use-case. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Note that without this alternative, we still don't have to full back completely on not using our new feature for this use-case. | |
Note that without this alternative, we still don't have to fall back completely on not using our new feature for this use-case. |
The third and final difference is that names in quotes must all be uses, never bindings. | ||
The semantics of matching a name, either standalone, or inside a larger quote, is name equality. | ||
This is formalized on the deguaring of a case alternative below:: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The third and final difference is that names in quotes must all be uses, never bindings. | |
The semantics of matching a name, either standalone, or inside a larger quote, is name equality. | |
This is formalized on the deguaring of a case alternative below:: | |
The third and final difference is that names in quotes must all be uses, never bindings. | |
The semantics of matching a name, either standalone, or inside a larger quote, is name equality. | |
This is formalized by the desugaring of a case alternative below:: |
Quotes as patterns | ||
~~~~~~~~~~~~~~~~~~ | ||
|
||
With the new extension ``TemplateHaskellQuotesAsPatterns``, slightly modified quotes are usable in pattern position. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I see that @int-index also had a suggestion in #529 (comment), although my inclination is still to have explicit prepositions rather than relying on word order to distinguish "pattern quote" from "quote pattern". I'm happy to leave the bikeshed colour to be resolved later once the substance of the proposal is agreed, though.
I still think it would be helpful to have some explicit definitions, something like (with the current terminology):
- A quote is said to be of the syntactic category being quoted, for example
[e| ... |]
is a quote of an expression and[p| ... |]
is a quote of a pattern. Template Haskell already supports quotes of expressions, patterns, types and declarations, plus quotes of arbitrary syntax via quasiquotes. - A quote is said to be used as the syntactic category in which it occurs, for example
x = [...| ... |]
includes a quote as an expression whereasf [...| ... |] = ...
includes a quote as a pattern. Template Haskell currently supports quotes as expressions and quasiquotes as all four categories; this proposal adds quotes as patterns. - Thus in
f [t| Bool |] = [d| data T |]
we have a quote of a type as a pattern and a quote of a declaration as an expression.
Should we mark this as “needs revision”? |
Yes please. And I had written it for HF consideration but it is now pretty far down in the future work on the draft proposal I am working on so it feels less urgent (perhaps I shouldn't have submitted it to the committee). I am glad I wrote it, I am thankful @adamgundry reviewed it, but I feel less urgency pushing it to completion until the lower hanging fruit we can do re |
Thanks for this @Ericson2314, I'm happy to label this as "needs revision" for now and wait for you or another willing volunteer to decide to pick it up and get it over the line. As I indicated I think this is basically a solid idea, albeit a nontrivial one to implement and with a few interesting corners to discuss. 😄 |
As we discussed on Sunday (Ben's notes) and as the proposal states, writing such "quote patterns" is a great way for users that use TH for the macros/grammar use case (as opposed to the staging/code gen use case) to define their macros in a way that is far less susceptible to churn in the TH AST, plus it is far more ergonomically to use. Perhaps the discussion on Sunday would re-ignite @Ericson2314's interest on the matter? As far as bike-shedding is concerned, I'd like to throw "Quotes in matches" or "matching quotes" into the ring. That expresses that these things must occur in a meta level pattern match, in "negative" position. There is no risk of confusing that with "Quote patterns" or "pattern quotes" where which is which I already forgot since I started this post. Unfortunately, a match is already a name describing the syntactic construct that encompasses a pattern and its GRHSs so that name isn't optimal either. Perhaps we should take strong inspiration in https://docs.racket-lang.org/guide/pattern-macros.html (Edit: Or even the more closely related foo :: Int -> Int
f [| foo (2*$(x)) |] = [| 2 * foo $(x) |] (I hope I got that right.) Here, Template Haskell used to have template quotes only, now it also got pattern quotes. (Makes you wonder if the name still flies.) I don't think it makes sense to call Rather, as @david-christiansen points out in #529 (comment), this proposal is quite similar to foo :: Int -> Int
f [| foo (2*$(x :: VarP)) |] = [| 2 * foo $(x) |] Which certainly is a potential extension to this proposal. Edit: Clarification on |
|
||
Quotes as Patterns | ||
~~~~~~~~~~~~~~~~~~ | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Empty subsection. Intended?
|
||
because matching on lists of multiple declarations is left as future work. | ||
|
||
Optional: Fine-grained Quotation constraints |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this can and should be a separate proposal. Perhaps move to Future Work instead?
Effect and Interactions | ||
----------------------- | ||
|
||
``TemplateHaskell`` will not imply ``TemplateHaskellQuotesAsPatterns``, though it does imply ``TemplateHaskellQuotes``. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think I'd prefer something like -XPatternQuotes
after my reflection in #529 (comment). No need to include the then misnomer TemplateHaskell
.
~~~~~~~~~~~~~~~~ | ||
|
||
The lack of symmetry where expression create actions but patterns only bind plain AST values is annoying. | ||
But the fixes for this might be too radical? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I didn't understand what you meant here at first. IMO, give examples or move to Future Work!
Pattern match on actions(!) | ||
~~~~~~~~~~~~~~~~~~~~~~~~~~~ | ||
|
||
I hypothesize that we could do better than the proposed actions vs no action asymmetry by meditating on the ways pattern matching relates to optics. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is this an alternative? Can't we have both? I'm not convinced that we want, though; seems confusing and almost no benefit (could just write the traverse
form). Future Work?
Support local variables | ||
~~~~~~~~~~~~~~~~~~~~~~~ | ||
|
||
Quotes that bind local variables do in fact have an interpretation as non-linear patterns:: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this section is confusing for these reasons:
- It discusses an extension to this proposal, namely binding constructs in patterns, that would be reasonable to implement in the future. So it belongs in Future Work.
- It calls these matches "non-linear", but of course the resulting desugaring is not non-linear in the meta language, as you readily point out.
- If this really were about non-linear matches, I'd totally expect
__x1 == __x3
to hold.
Besides, I think the semantics you describe is very reasonable, because it allows for the expected round-tripping property: If I define
f [| (\x -> x, \x -> x) |] =...
... $(f [| (\x -> x, \x -> x) |] ...
... $(f [| (\z -> z, \z -> z) |] ...
... $(f [| (\a -> a, \b -> b) |] ...
Then I would expect all uses of f
to match. Is that how it works in Racket and Lean, @david-christiansen @Kha?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In macro systems like Racket's and Lean's, you cannot distinguish between bindings and uses in quotations because scoping is discovered only during expansion. So "quotes that bind local variables" is not even something we can detect in those systems.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I presume "discovered only during expansion" is an artifact of the fact that Racket-style macros will not get a name-resolved TH AST as input (where we know the binding structure but limit ourselves to macro syntax expressible in Haskell) but rather just a concrete syntax tree. Perhaps let me rephrase in terms of the example in https://school.racket-lang.org/2019/plan/tue-mor-lecture.html:
(define-syntax (robust-for/list5 stx)
(syntax-parse stx
[(_ ([elem-name:id seq]) computation)
#'(map (λ (elem-name) computation) seq)]))
This macro will expand (robust-for/list5 ([x (list 1 2)]) (add1 x))
to (map (λ (x) (add1 x)) (list 1 2))
, matching [elem-name :-> x, seq :-> (list 1 2)]
. Note that elem-name
is ultimately spliced into a binding occurrence and that computation
may refer to the instantiation of elem-name
, thus its syntax class is specified to be id
, which is what elem-name:id
does. (This is somewhat like pushing an expected type for the AST node to match inside the pattern, I guess, where "type" in Racket really means a user-definable non-terminal of the extensible syntax. See 5.6 in the link above.) But the pattern (_ ([elem-name:id seq]) computation)
does not know about binding structure at all; rather the macro equips the pattern with a binding structure post-hoc when it generates the template (map (λ (elem-name) computation) seq)]))
for the pattern, thus intentionally capturing occurrences of elem-name
in computation
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's exactly right. It's the same reason I mentioned in the ZuriHac discussion why our macros are untyped (on the level of the quoted language) but core-level transformations can optionally be typed (which is done by https://github.com/gebner/quote4 btw).
f [|| $$(x) $$(y) ||] = ... :: delta | ||
|
||
``x`` would be bound as ``x :: Code m (beta -> alpha)``, and | ||
``y`` would be bound as ``y :: Code m beta``. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Tricky, and good thinking. Perhaps you need Monad m =>
or Applicative m =>
to have access to pure
.
@mpickering probably knows what to do here; altough typed macros are probably not a priority to TTH (which focuses on staging).
|
||
None at this time. | ||
|
||
Related Work |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Correct me if I'm wrong, but since the proposal currently does not allow matching on binding constructs, we can't make hygiene better or worse. Judging from an hour worth reading, I also don't think we lock ourselves out with this proposal to more modern approaches such as syntax-parse
because the stated semantics should be a subset of whatever advanced stuff we will happen to want in the future.
The Template Haskell AST is inherently unstable. Let's make that less of an issue. We can do that by allowing Quotes to be used instead of Template Haskell AST data constructors in patterns.
Rendered