[experimental feature] Support HOAS pattern with type variables for quote pattern matching #18271

zeptometer · 2023-07-23T05:44:05Z

This PR extends higher-order patterns inside quote patterns to allow type parameters. When this PR is merged, we'll be able to write quote patterns like the following example with an experimental flag experimental.quotedPatternsWithPolymorphicFunctions.

def decomposePoly(x: Expr[Any])(using Quotes): Expr[Int] =
  x match
    case '{ [A] => (x: List[A]) => $y[A](x) : Int } =>
      '{ $y[Int](List(1, 2, 3)) }
    case _ => Expr(0)

You can see that the higher-order pattern $y[A](x) carries an type parameter A. It states that this pattern matches a code fragment with occurrences of A, and y is assigned a polymorphic function type [A] => List[A] => x.

This PR mainly changes two parts: type checker and quote pattern matcher. Those changes are based on the formalized type system defined in Nicolas Stucki's thesis, and one can expect the soundness of the implementation.

Type Dependency

If a higher-order pattern carries a value parameter with a type that has type parameters defined in the quoted pattern, those type parameters should also be captured in the higher-order pattern. For example, the following pattern will not be typed.

case '{ [A] => (x: List[A]) => $y(x) : Int } =>

In this case, x has the type List[A], which includes a type variable A that is defined in the pattern. However, the higher-order pattern $y(x) does not have any type parameters. This should be ill-typed. One can always avoid this kind of type errors by adding type parameters, like $y[A](x)

Implementation Restriction

Current implementation only allows type parameters that do not have bounds, because sound typing rules for such pattern is not clear yet.

case '{ [A] => (x: List[A]) => $y(x) : Int } => // Allowed
case '{ [A <: Int] => (x: List[A]) => $y(x) : Int } => // Disallowed

compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala

zeptometer · 2023-07-31T08:16:36Z

compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala

+           * (NOTE: Needs non-trivial extension to type system)
+           */
+          val bounds = ctx.gadt.fullBounds(typedTypearg.symbol)
+          if bounds != null && bounds != TypeBounds.empty then


We might want to move this logic to checkPattern because we have fully-typed tree.

Sync Aug 07: How to check type bounds with fully typed tree?

compiler/src/dotty/tools/dotc/quoted/QuotePatterns.scala

zeptometer · 2023-08-07T05:41:31Z

compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala

+           * (NOTE: Needs non-trivial extension to type system)
+           */
+          val bounds = ctx.gadt.fullBounds(typedTypearg.symbol)
+          if bounds != null && bounds != TypeBounds.empty then


Sync Aug 07: How to check type bounds with fully typed tree?

compiler/src/scala/quoted/runtime/impl/QuoteMatcher.scala

compiler/src/dotty/tools/dotc/quoted/QuotePatterns.scala

zeptometer

Add comment with "Implementation restriction"
Add test cases with and without experimental flags
(potentailly) improve performance of type comparison under an environment
update stdlibExperimentalDefinitions.scala
Add documentation

zeptometer · 2023-08-14T08:12:57Z

tests/neg-macros/hoas-pattern-with-type-params.scala

+  body match
+    case '{ [A] => (x : A) => $b[A] : (A => A) } => // error
+      Expr("A higher-order pattern must carry value params")
+    case '{ [A] => (x : A) => $b(x) : (A => A) } => // error


better to have: Show example of expected code $b[A](x) in this case

tests/run-macros/quote-match-poly-function/Macro_1.scala

compiler/src/scala/quoted/runtime/impl/QuoteMatcher.scala

tests/neg-macros/hoas-pattern-with-type-params.scala

nicolasstucki · 2023-10-16T08:47:09Z

I will rebase this PR to solve the small conflict in library/src/scala/runtime/stdLibPatches/language.scala.

Future proof for scala#18271.

Gedochao · 2024-07-10T15:16:16Z

This has been decided to be included in 3.6.0.

jchyb

Rebased to resolve conflicts (all very simple). Also added some (also very simple) changes to make it work on top of #17396

jchyb · 2024-07-22T11:30:22Z

tests/run-macros/quote-match-poly-function-1-regression/Test_2.scala

@@ -0,0 +1,5 @@
+//> using options -experimental


Added experimental here and in other tests

jchyb · 2024-07-22T11:33:49Z

compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala

-              assert(targs.isEmpty, "unexpected type arguments in SPLICEPATTERN") // `targs` will be needed for #18271. Until this fearure is added they should be empty.
-              SplicePattern(pat, args, patType)
+              SplicePattern(pat, targs, args, patType)


Adjusted pickling and unpicking of SplicePatterns as it was previously prepared for this PR by Nicolas

jchyb · 2024-07-22T11:34:02Z

compiler/src/dotty/tools/dotc/core/tasty/TreePickler.scala

-        case SplicePattern(pat, args) =>
-          val targs = Nil // SplicePattern `targs` will be added with #18271
+        case SplicePattern(pat, targs, args) =>


jchyb · 2024-07-22T11:41:16Z

Thank you so much @zeptometer! Fantastic work!

zeptometer · 2024-07-23T05:48:02Z

@jchyb I'm glad to hear that this feature is merged 😄 Thank you for your effort in merging this PR!

zeptometer force-pushed the hoas-with-tvar branch 2 times, most recently from 988087c to 6b345cc Compare July 24, 2023 07:09

nicolasstucki added the needs-minor-release This PR cannot be merged until the next minor release label Jul 25, 2023

zeptometer force-pushed the hoas-with-tvar branch 4 times, most recently from 282e4ad to fc15089 Compare July 31, 2023 07:51

zeptometer commented Jul 31, 2023

View reviewed changes

compiler/src/dotty/tools/dotc/typer/QuotesAndSplices.scala Show resolved Hide resolved

zeptometer commented Jul 31, 2023

View reviewed changes

compiler/src/dotty/tools/dotc/quoted/QuotePatterns.scala Outdated Show resolved Hide resolved

zeptometer commented Jul 31, 2023

View reviewed changes

compiler/src/dotty/tools/dotc/quoted/QuotePatterns.scala Outdated Show resolved Hide resolved

zeptometer commented Jul 31, 2023

View reviewed changes

compiler/src/dotty/tools/dotc/quoted/QuotePatterns.scala Outdated Show resolved Hide resolved

dwijnand assigned nicolasstucki Aug 1, 2023

zeptometer force-pushed the hoas-with-tvar branch 2 times, most recently from 49c0cca to 6764d5e Compare August 7, 2023 05:36

zeptometer commented Aug 7, 2023

View reviewed changes

compiler/src/dotty/tools/dotc/quoted/QuotePatterns.scala Show resolved Hide resolved

zeptometer force-pushed the hoas-with-tvar branch from dc7be2b to f8764b6 Compare August 14, 2023 04:55

zeptometer commented Aug 14, 2023

View reviewed changes

zeptometer force-pushed the hoas-with-tvar branch from 3b44c95 to 61f4b7f Compare August 18, 2023 14:03

nicolasstucki self-requested a review August 22, 2023 07:46

nicolasstucki added the area:experimental label Aug 22, 2023

zeptometer force-pushed the hoas-with-tvar branch from 11fdce9 to ab8a613 Compare August 27, 2023 01:26

zeptometer marked this pull request as ready for review August 27, 2023 01:27

zeptometer changed the title ~~WIP: Support HOAS pattern with type variables for quote pattern matching~~ [experimental feature] Support HOAS pattern with type variables for quote pattern matching Aug 28, 2023

nicolasstucki approved these changes Oct 16, 2023

View reviewed changes

nicolasstucki force-pushed the hoas-with-tvar branch from e53c7e6 to 02b60bf Compare October 16, 2023 08:49

nicolasstucki mentioned this pull request Apr 19, 2024

Add quote ASTs to TASTy #20165

Merged

nicolasstucki added a commit to dotty-staging/dotty that referenced this pull request Apr 22, 2024

Add type argument encoding to SPLICEPATTERN

3d8aca6

Future proof for scala#18271.

nicolasstucki added a commit to dotty-staging/dotty that referenced this pull request Apr 22, 2024

Add type argument encoding to SPLICEPATTERN

743cc0b

Future proof for scala#18271.

Kordyjan unassigned nicolasstucki Jul 3, 2024

Kordyjan requested a review from jchyb July 3, 2024 15:04

Kordyjan assigned jchyb Jul 3, 2024

Generalize HOAS patterns to take type parameters (experimental feature)

41e2d52

jchyb force-pushed the hoas-with-tvar branch from 02b60bf to 41e2d52 Compare July 22, 2024 10:00

jchyb reviewed Jul 22, 2024

View reviewed changes

jchyb approved these changes Jul 22, 2024

View reviewed changes

jchyb merged commit 4c9cf0a into scala:main Jul 22, 2024
28 checks passed

WojciechMazur added this to the 3.6.0 milestone Oct 8, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[experimental feature] Support HOAS pattern with type variables for quote pattern matching #18271

[experimental feature] Support HOAS pattern with type variables for quote pattern matching #18271

zeptometer commented Jul 23, 2023 •

edited

Loading

zeptometer Jul 31, 2023

zeptometer Aug 7, 2023

zeptometer Aug 7, 2023

zeptometer left a comment •

edited

Loading

zeptometer Aug 14, 2023

nicolasstucki commented Oct 16, 2023

Gedochao commented Jul 10, 2024

jchyb left a comment

jchyb Jul 22, 2024

jchyb Jul 22, 2024

jchyb Jul 22, 2024

jchyb commented Jul 22, 2024

zeptometer commented Jul 23, 2024

[experimental feature] Support HOAS pattern with type variables for quote pattern matching #18271

[experimental feature] Support HOAS pattern with type variables for quote pattern matching #18271

Conversation

zeptometer commented Jul 23, 2023 • edited Loading

Type Dependency

Implementation Restriction

zeptometer Jul 31, 2023

Choose a reason for hiding this comment

zeptometer Aug 7, 2023

Choose a reason for hiding this comment

zeptometer Aug 7, 2023

Choose a reason for hiding this comment

zeptometer left a comment • edited Loading

Choose a reason for hiding this comment

zeptometer Aug 14, 2023

Choose a reason for hiding this comment

nicolasstucki commented Oct 16, 2023

Gedochao commented Jul 10, 2024

jchyb left a comment

Choose a reason for hiding this comment

jchyb Jul 22, 2024

Choose a reason for hiding this comment

jchyb Jul 22, 2024

Choose a reason for hiding this comment

jchyb Jul 22, 2024

Choose a reason for hiding this comment

jchyb commented Jul 22, 2024

zeptometer commented Jul 23, 2024

zeptometer commented Jul 23, 2023 •

edited

Loading

zeptometer left a comment •

edited

Loading