Quote pattern matching runtime spec #8687

nicolasstucki · 2020-04-07T15:30:27Z

A first draft of the evaluation semantics of quote pattern matching.

liufengyun

I left some open discussion points:

about the semantics of wildcard pattern
about the semantics of local definitions
about whether we should allow pattern matching inside quoted code patterns

/cc : @biboudis @OlivierBlanvillain @anatoliykmetyuk

liufengyun · 2020-04-08T07:58:28Z

docs/docs/reference/metaprogramming/quote-matching.md

+
+## Evaluation sematics
+
+Bellow we provide an informal description of the pattern evailatuion.


Suggested change

Bellow we provide an informal description of the pattern evailatuion.

Some short summary is probably a good idea, and apart from typos this seems good?

docs/docs/reference/metaprogramming/quote-matching.md

liufengyun · 2020-04-08T08:07:01Z

docs/docs/reference/metaprogramming/quote-matching.md

+* `&&&` matches if both sides match. Concatenates the extracted expressions of both sides.
+
+```scala
+'{ e } =?= '{ $x }  &&  typeOf('{e}) <:< typeOf('{$x}) && isColosedUnder()('{e})  ===>   matched('{e})


This looks like to be a wildcard pattern, the type checking looks redundant.

The condition isColosedUnder()('{e}) is a little controversial. I see the motivation is for safety. The question is:

whether it is indeed safe

potentially high usability penalty here, which may out-weigh the concern of safety

matched('{e}) probably also means "match x to e", right?

Actually $ should not be part of this part of the specification, here we deal with hole[T] which is the thing that is generated after typing the quote pattern.

liufengyun · 2020-04-08T08:08:17Z

docs/docs/reference/metaprogramming/quote-matching.md

+
+```scala
+'{ e } =?= '{ $x }  &&  typeOf('{e}) <:< typeOf('{$x}) && isColosedUnder()('{e})  ===>   matched('{e})
+'{ e } =?= '{ $y(x1, ..., xn) }  &&  isColosedUnder(x1, ... xn)('{e})  ===>   matched(lift(x1, ..., xn)('{e}))


This quoted pattern is a little counter-intuitive, both syntactically and semantically. I'm not sure how useful and usable it is in practice.

It's a higher-order pattern variable (see https://dl.acm.org/doi/10.1145/3136040.3136043, section 5.7). I think it's quite intuitive in actual examples. But it's a pretty limited pattern, and as was discussed before in the group meeting, it could be better to go with a scope-tracking type system instead.

liufengyun · 2020-04-08T08:32:11Z

docs/docs/reference/metaprogramming/quote-matching.md

+'{ val x: T = e1; e2 } =?= '{ val y: P = p1; p2 }   ===>   withEnv(x -> y)('[T] =?= '[P] &&& '{e1} =?= '{p1} &&& '{e2} =?= '{p2})
+'{ def x0(x1: T1, ..., xn: Tn): T0 = e1; e2 } =?= '{ def y0(y1: P1, ..., yn: Pn): P0 = p1; p2 }   ===>   withEnv(x0 -> y0, ..., xn -> yn)('[T0] =?= '[P0] &&& ... &&& '[Tn] =?= '[Pn] &&& '{e1} =?= '{p1} &&& '{e2} =?= '{p2})
+
+'{ e1; e2 } =?= '{ p1; p2 }   ===>   '{e1} =?= '{p1} &&& '{e2} =?= '{p2}


Seems it can be removed, it's a special case of the block.

docs/docs/reference/metaprogramming/quote-matching.md

liufengyun · 2020-04-08T08:34:34Z

docs/docs/reference/metaprogramming/quote-matching.md

+
+'{ {e0; e1; ...; en}; em } =?= '{ {p0; p1; ...; pm}; em }   ===>   '{ e0; {e1; ...; en; em} } =?= '{ p0; {p1; ...; pm; em} }
+'{ val x: T = e1; e2 } =?= '{ val y: P = p1; p2 }   ===>   withEnv(x -> y)('[T] =?= '[P] &&& '{e1} =?= '{p1} &&& '{e2} =?= '{p2})
+'{ def x0(x1: T1, ..., xn: Tn): T0 = e1; e2 } =?= '{ def y0(y1: P1, ..., yn: Pn): P0 = p1; p2 }   ===>   withEnv(x0 -> y0, ..., xn -> yn)('[T0] =?= '[P0] &&& ... &&& '[Tn] =?= '[Pn] &&& '{e1} =?= '{p1} &&& '{e2} =?= '{p2})


The semantics for local definitions is surprising. I see the intention is to avoid scope extrusion, but it seems to be a big usability penalty here.

@liufengyun What alternative semantics are you thinking about?

The original comment is actually about the following rule:

'{ e } =?= '{ $x } && typeOf('{e}) <:< typeOf('{$x}) && isColosedUnder()('{e}) ===>
matched('{e})

From my limited meta-programming experience, I like quoted pattern matching on terms and types a lot, it's a big productivity booster. In particular, it saves a lot of boilerplate when pattern matching on known methods and types. This makes developing macro-based DSLs a joyful experience. Previously, they have to be performed via low-level reflect API in a tedious way or doing it in an unsafe way via string comparison. @nicolasstucki has done a great job here for Scala meta-programmers👍

However, I'm not sure that making it safer and feature-complete will help much in practice, in particular when it comes at the price of usability. By usability, I mean simple API, natural and precise semantics, stability, debuggability, a clear-cut boundary of what is supported (accountable & trustable) and what is not.

For example, maybe it is safe drop the support for quoted code patterns of pattern matches and definitions, and leave them to reflect API?

docs/docs/reference/metaprogramming/quote-matching.md

Blaisorblade · 2020-04-08T14:24:38Z

docs/docs/reference/metaprogramming/quote-matching.md

+'{ e: T } =?= '{ p: P }   ===>   '{e} =?= '{p} &&& '[T] =?= '[P]
+'{ e } =?= '{ p: P }   ===>   '{e} =?= '{p}
+'{ e.x } =?= '{ p.x }   ===>   '{e} =?= '{p}
+'{ x } =?= '{ x }   ===>   matched


~~Should this be somewhere next with '{{ x}} =?= '{{y }} , and maybe merged together?~~
NOPE, that's a pattern.

I now suspect I agree with this rule, but it took me a while to see why '{ x } =?= '{ y } is illegal (because alpha-equivalence is handled when checking local binders). Some explanation would help. (Who writes it is another question).

BTW, I'd hope Selects encoded as Idents (per desugarIdent) show up as Select here. I see they do not in Tasty reflection... does at least -Ycheck ensure that they're represented consistently so it's well-defined what you have to write to match Int (as opposed to needing Int, scala.Int or _root_.scala.Int depending on, say, what the user wrote)?

docs/docs/reference/metaprogramming/quote-matching.md

Blaisorblade · 2020-04-08T14:48:50Z

Hi! I hope it's okay, I took the liberty of leaving a few review comments, also because this relates to #8600 (and I hope I can contribute a bit here).
And to be clear, it's very cool you're sketching this!

docs/docs/reference/metaprogramming/quote-matching.md

smarter · 2020-04-08T14:58:34Z

docs/docs/reference/metaprogramming/quote-matching.md

+
+'[T] =?= '[P] && T <:< P   ===>   matched
+'[ T0[T1, ..., Tn] ] =?= '[ P0[P1, ..., Pn] ]   ===>   '[T0] =?= '[P0] &&& ... &&& '[Tn] =?= '[Pn]
+'[T @annot] =?= '[P]   ===>   '[T] =?= '[P]


Annotations should be handled by subtyping rules already (and some annotations can create proper subtype, see https://github.com/lampepfl/dotty/blob/4253708ee22265959b6768547169c330244bf9cb/compiler/src/dotty/tools/dotc/core/Types.scala#L4589)

smarter · 2020-04-08T15:02:55Z

docs/docs/reference/metaprogramming/quote-matching.md

+'{ e.super[T] } =?= '{ p.super[T] }   ===>   '{e} =?= '{p}
+'{ Seq(e0, ..., en): _* } =?= '{ Seq(p0, ..., pn): _* }   ===>   '{e0} =?= '{p0} &&& ... &&& '{en} =?= '{pn}
+
+'[T] =?= '[P] && T <:< P   ===>   matched


This seems to contradict the fact that scala.quoted.Type is invariant in its type parameter. I guess this is needed for #8695 to work, but as I noted there, I tihnk the proper thing to do is to create quoted type variable instead of doing type inference -> picking "Any" -> relying on this rule to get other types to match.

LPTK

I understand that this is an informal spec, but it is still missing the whole aspect about checking subtyping while extracting pattern type variables. The tricky part is that you'd need to specify a big part of Dotty's subtyping algorithm. But this is important and significant: there are tough questions to answer, especially when dealing with matching GADT types.

LPTK · 2020-04-14T15:59:35Z

docs/docs/reference/metaprogramming/quote-matching.md

+'{ Seq(e0, ..., en): _* } =?= '{ Seq(p0, ..., pn): _* }   ===>   '{e0} =?= '{p0} &&& ... &&& '{en} =?= '{pn}
+
+'[T] =?= '[P] && T <:< P   ===>   matched
+'[ T0[T1, ..., Tn] ] =?= '[ P0[P1, ..., Pn] ]   ===>   '[T0] =?= '[P0] &&& ... &&& '[Tn] =?= '[Pn]


Does Dotty do higher-order subtyping (cc @smarter)? As in, will it successfully check List <: Seq, i.e., [+X] => List[X] <: [+Y] => Seq[Y]? What happens if the variances differ?
Moreover, it should be possible to match types which do not align in their parameters. For example, type pattern Iterable[$t] should be able to match type Map[K,V].

As in, will it successfully check List <: Seq

Yes.

What happens if the variances differ?

We take variance into account: https://github.com/lampepfl/dotty/blob/63ee630044b5555df691de02e59fb6d43d121a6d/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L594-L595 (but note that type lambdas themselves have inferred variance now: #8082)

LPTK · 2020-04-14T17:01:25Z

On the same topic, since it's related: I stumbled upon the flops-rewrite tests in tests/run-macros/ and noticed that their encoding of safe term transformations, based on quote-matching, is unsound.

For instance, in tests/run-macros/flops-rewrite-3/Macro_1.scala, if we try:

  val rewriter = Rewriter().withFixPoint.withPost(
    Transformation.safe[Any] {
      case _ => '{"oops"}
    }

We get a match error in the inner match of:

  def apply[T: Type](e: Expr[T])(using QuoteContext): Expr[T] = {
    e match {
      case '{ $e: U } => transform.applyOrElse(e, identity) match { case '{ $e2: T } => e2 }
      case e => e
    }

Indeed, the transformation may rewrite to something that's larger than the expected type, in which case it should not be deemed applicable. There is a U <: T check missing.

This is an important gotcha to watch out for, if a rewrite primitive is ever added to the reflection API.

nicolasstucki · 2020-04-15T10:00:26Z

I've moved the spec to the Matcher class to make it easier to maintain in sync with the implementation. I also named the rules and added references to the rules in the implementation.

I improved the readability of the rules based on the feedback (still to be improved) as well as fixing some rules that were not in line with the implementation. The current state represented the current implementation.

For actual semantic issues, I did not fix the rules but added some TODOs in the code. Once we have this spec in we can fix those while updating the spec at the same time.

I suggest merging this and have any discussion on semantics on new issues that reference the spec.

Thank you for all the feedback.

nicolasstucki · 2020-04-15T10:01:47Z

@liufengyun, could you re-review this. We should just make sure that the current spec is inline with the current implementation for this PR.

liufengyun

LGTM

library/src/scala/internal/quoted/Matcher.scala

Co-Authored-By: Fengyun Liu <[email protected]>

nicolasstucki requested a review from liufengyun April 7, 2020 15:30

nicolasstucki assigned liufengyun Apr 7, 2020

nicolasstucki marked this pull request as ready for review April 8, 2020 06:54

nicolasstucki mentioned this pull request Apr 8, 2020

Fix #8600: Match trough type ascription #8684

Merged

liufengyun reviewed Apr 8, 2020

View reviewed changes

Blaisorblade mentioned this pull request Apr 8, 2020

Match fails using quasiquotes #8600

Closed

Blaisorblade reviewed Apr 8, 2020

View reviewed changes

docs/docs/reference/metaprogramming/quote-matching.md Outdated Show resolved Hide resolved

Blaisorblade reviewed Apr 8, 2020

View reviewed changes

docs/docs/reference/metaprogramming/quote-matching.md Outdated Show resolved Hide resolved

Blaisorblade reviewed Apr 8, 2020

View reviewed changes

docs/docs/reference/metaprogramming/quote-matching.md Outdated Show resolved Hide resolved

smarter reviewed Apr 8, 2020

View reviewed changes

docs/docs/reference/metaprogramming/quote-matching.md Outdated Show resolved Hide resolved

smarter reviewed Apr 8, 2020

View reviewed changes

LPTK suggested changes Apr 14, 2020

View reviewed changes

nicolasstucki force-pushed the add-quote-matching-spec branch from 52b16dd to b7f0b51 Compare April 15, 2020 09:49

Quote pattern matching runtime spec

b48ca44

nicolasstucki force-pushed the add-quote-matching-spec branch from b7f0b51 to b48ca44 Compare April 15, 2020 09:51

liufengyun approved these changes Apr 15, 2020

View reviewed changes

library/src/scala/internal/quoted/Matcher.scala Outdated Show resolved Hide resolved

Update library/src/scala/internal/quoted/Matcher.scala

7473077

Co-Authored-By: Fengyun Liu <[email protected]>

nicolasstucki merged commit c811957 into scala:master Apr 15, 2020

nicolasstucki deleted the add-quote-matching-spec branch April 15, 2020 11:09

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Quote pattern matching runtime spec #8687

Quote pattern matching runtime spec #8687

nicolasstucki commented Apr 7, 2020

liufengyun left a comment

liufengyun Apr 8, 2020

Blaisorblade Apr 8, 2020

liufengyun Apr 8, 2020

Blaisorblade Apr 8, 2020

nicolasstucki Apr 15, 2020

liufengyun Apr 8, 2020

LPTK Apr 14, 2020

liufengyun Apr 8, 2020

liufengyun Apr 8, 2020

LPTK Apr 14, 2020

liufengyun Apr 14, 2020

Blaisorblade Apr 8, 2020 •

edited

Loading

Blaisorblade Apr 8, 2020

Blaisorblade commented Apr 8, 2020 •

edited

Loading

smarter Apr 8, 2020

smarter Apr 8, 2020 •

edited

Loading

LPTK left a comment

LPTK Apr 14, 2020 •

edited

Loading

smarter Apr 14, 2020

LPTK commented Apr 14, 2020 •

edited

Loading

nicolasstucki commented Apr 15, 2020

nicolasstucki commented Apr 15, 2020

liufengyun left a comment


		## Evaluation sematics

		Bellow we provide an informal description of the pattern evailatuion.

Quote pattern matching runtime spec #8687

Quote pattern matching runtime spec #8687

Conversation

nicolasstucki commented Apr 7, 2020

liufengyun left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Blaisorblade Apr 8, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Blaisorblade commented Apr 8, 2020 • edited Loading

Choose a reason for hiding this comment

smarter Apr 8, 2020 • edited Loading

Choose a reason for hiding this comment

LPTK left a comment

Choose a reason for hiding this comment

LPTK Apr 14, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

LPTK commented Apr 14, 2020 • edited Loading

nicolasstucki commented Apr 15, 2020

nicolasstucki commented Apr 15, 2020

liufengyun left a comment

Choose a reason for hiding this comment

Blaisorblade Apr 8, 2020 •

edited

Loading

Blaisorblade commented Apr 8, 2020 •

edited

Loading

smarter Apr 8, 2020 •

edited

Loading

LPTK Apr 14, 2020 •

edited

Loading

LPTK commented Apr 14, 2020 •

edited

Loading