-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[experimental feature] Support HOAS pattern with type variables for q…
…uote pattern matching (#18271) 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`. ```scala 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](https://github.com/nicolasstucki#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. ```scala case '{ [A] => (x: List[A]) => $y(x) : Int } => // Allowed case '{ [A <: Int] => (x: List[A]) => $y(x) : Int } => // Disallowed
- Loading branch information
Showing
38 changed files
with
624 additions
and
125 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.