Skip to content

Fix #10994: align typed pattern syntax with Scala 2 #11023

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

Closed
wants to merge 5 commits into from

Conversation

liufengyun
Copy link
Contributor

@liufengyun liufengyun commented Jan 7, 2021

Fix #10994: align typed pattern syntax with Scala 2

In Scala 2, a typed pattern p: T restricts that p can only be a
pattern variable.

In Dotty, #6919 allows p to be any pattern, in order to support
pattern matching on generic number literals.

This PR aligns the syntax with Scala 2 by stipulating that in a typed
pattern p: T, either

  • p is a pattern variable, or
  • p is a number literal

@liufengyun liufengyun changed the title Fix #10994: align typed pattern syntax to Scala 2 Fix #10994: align typed pattern syntax with Scala 2 Jan 7, 2021
In Scala 2, a typed pattern `p: T` restricts that `p` can only be a
pattern variable.

In Dotty, scala#6919 allows `p` to be any pattern, in order to support
 pattern matching on generic number literals.

This PR aligns the syntax with Scala 2 by stipulating that in a typed
pattern `p: T`, either

- `p` is a pattern variable, or
- `p` is a number literal
The test case `tests/explicit-nulls/neg/strip.scala` specify that null
unions inside intersection types should work.  After changing the
scrutinee type of the extractor `OrNull` it is no longer the case.

Changing the scrutinee type is still justified because it agrees with
the name as well as the usage in `Types.scala`.

In contrast, in `Typer.scala`, the logic is more clear without using `OrNull`.
@som-snytt
Copy link
Contributor

TIL. But this seems useful:

scala> Array(1,2,3.14) match { case Array(1,2,3.14): Array[Int] => }
scala.MatchError: [D@6f36267d (of class [D)
  ... 27 elided

or

scala> Array(1,2,3.0) match { case Array(1,2,3): Array[Double] => }

scala>   

OK I glanced at the ticket but I don't know what a fork pattern is. 🍴

@bishabosha
Copy link
Member

bishabosha commented Jan 8, 2021

OK I glanced at the ticket but I don't know what a fork pattern is. 🍴

I assume it meant using a custom extractor, like the following:

scala> object Fork { def unapply[T](x: T): (x.type, x.type) = (x,x) }
// defined object Fork

scala> List(23, 47) match { case Fork(List(a, _), List(_, b)) => println(s"it works! $a, $b") }
it works! 23, 47

or for your example:

scala> Array(1,2,3.0) match { case Fork(Array(1,2,3), _: Array[Int]) => } // MatchError

@liufengyun
Copy link
Contributor Author

But this seems useful:

scala> Array(1,2,3.14) match { case Array(1,2,3.14): Array[Int] => }
scala.MatchError: [D@6f36267d (of class [D)
  ... 27 elided

This seems to be a marginal use case because

  • if the array is defined locally, we would not care about the type of the elements
  • if the array is created elsewhere, it's typed is usually known through method parameters.

The use cases found in the compiler seem to be an abuse of the feature. There is concern that the feature might lead to more difficult to understand code. Meanwhile, the feature gives rise to problems like lampepfl/dotty-feature-requests#159. Therefore, I think it's better to align with Scala 2 syntax.

Copy link
Member

@bishabosha bishabosha left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code change looks good to me.

cc/ @odersky @sjrd

the change to enable nested patterns within a typetest came from the generic number literals feature, which has been suspended until after 3.0.

The ability to use destructuring patterns inside a typetest pattern could be desirable in general but is probably a significant enough change on its own to require a full language proposal, what do you think?

Merging this will still support generic number literal patterns.

@bishabosha bishabosha assigned sjrd and odersky and unassigned bishabosha Jan 8, 2021
@sjrd sjrd removed their assignment Jan 8, 2021
Co-authored-by: Jamie Thompson <bishbashboshjt@gmail.com>
Copy link
Contributor

@odersky odersky left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why should we change this? It makes the language more complicated and less powerful?

@odersky odersky removed their assignment Jan 11, 2021
@liufengyun
Copy link
Contributor Author

Why should we change this? It makes the language more complicated and less powerful?

The reason is to make sure pattern match code is always simple and easily understandable.

So far we have seen no valid usage of this feature, and the use cases found in the compiler show that it only complicates the code and hide refactoring opportunities in the code.

@bishabosha
Copy link
Member

bishabosha commented Jan 16, 2021

This syntax can be useful for assistance with extracting phantom types, but that is probably a symptom of unapply patterns not having the syntax to extract the relevant type variable:

enum Ev[F <: AnyKind]:                                                                                           
  case HK() extends Ev[List]

def f[F <: AnyKind](ev: Ev[F]): Unit = ev match {
  case Ev.HK(): Ev[f] =>
    val m: f[Int] = List(1,2,3)
    ()
}

@liufengyun
Copy link
Contributor Author

liufengyun commented Jan 18, 2021

This syntax can be useful for assistance with extracting phantom types, but that is probably a symptom of unapply patterns not having the syntax to extract the relevant type variable:

enum Ev[F <: AnyKind]:                                                                                           
  case HK() extends Ev[List]

def f[F <: AnyKind](ev: Ev[F]): Unit = ev match {
  case Ev.HK(): Ev[f] =>
    val m: f[Int] = List(1,2,3)
    ()
}

In this example, it seems we already know f = List, an overkill to use the typed pattern 😄

Suppose there are cases where we do need to use typed pattern to extract a phantom type. I'd like to argue that such use cases can be misleading.

The reason is that usually in patmat, the inferred type comes from the scrutinee. In the case above, the concrete type of f does not come from the scrutinee type Ev[F], but from the sub-patterns via GADT constraints. This can have dangerous consequences (see #5077).

@bishabosha
Copy link
Member

bishabosha commented Jan 18, 2021

In this example, it seems we already know f = List, an overkill to use the typed pattern 😄

The reason i used this example is because extracting f with the typed pattern was necessary, F was not known to be List in that case, (with just case Ev.HK() =>) perhaps that is a bug

@liufengyun
Copy link
Contributor Author

In this example, it seems we already know f = List, an overkill to use the typed pattern 😄

The reason i used this example is because extracting f with the typed pattern was necessary, F was not known to be List in that case, (with just case Ev.HK() =>) perhaps that is a bug

It seems related to kind checking. The following code compiles:

enum Ev[F[_]]:
  case HK() extends Ev[List]

def f[F[_]](ev: Ev[F]): Unit = ev match {
  case Ev.HK(): Ev[F] =>
    val m: F[Int] = List(1,2,3)
    ()
}

@LPTK
Copy link
Contributor

LPTK commented Jan 18, 2021

@liufengyun there are many situations in more advanced use cases, relating to dependent typing, where specifying the names of types that are being matched is very useful. It's not just for phantom types either. The fact you have not found such patterns in the compiler does not imply these are not useful. It's more likely that:

  • there is just not that much type-level code in the compiler;

  • the support for this feature is relatively recent (it's not in Scala 2), and many people did not even know of its existence, which was my case until recently.

@liufengyun
Copy link
Contributor Author

liufengyun commented Jan 18, 2021

@LPTK Thanks for the feedback. We discussed it today, we need more careful evaluation and feedback about

  • whether to keep the feature, and
  • how to handle it in type checking, GADT, exhaustivity check, and type-test warnings

As one example of type checking, look at the code below:

enum Ev[F<:AnyKind]:
  case EvInt() extends Ev[Int]
  case EvStr() extends Ev[String]

// works
def f[F](ev: (F, Ev[F])): Int = ev match {
  case (x: F,  _: Ev[Int]) => x
  case _ => 0
}

// works
def g[F](ev: (F, Ev[F])): Int = ev match {
  case (x: F,  Ev.EvInt()) => x
  case _ => 0
}

// Does not work
def h[F](ev: (F, Ev[F])): Int = ev match {
  case (x: F,  Ev.EvInt(): Ev[Int]) => x            // error
  case _ => 0
}

Both the pattern _: Ev[Int] and Ev.EvInt() work, but the pattern Ev.EvInt(): Ev[Int] gets the following error:

-- [E007] Type Mismatch Error: examples/A.scala:19:39 --------------------------
19 |  case (x: F,  Ev.EvInt(): Ev[Int]) => x            // error
   |                                       ^
   |               Found:    (x : F)
   |               Required: Int
   |
   |               where:    F is a type in method h with bounds >: (?1 : F)

which is counter-intuitive. It suggests type checking needs to be enhanced to avoid surprising behavior.

@LPTK
Copy link
Contributor

LPTK commented Jan 18, 2021

@liufengyun this just sounds like a missing case in the GADT reasoning code. Maybe the assumption of the person who wrote the code was that there was no more type info to get on the LHS of a type pattern. Maybe @abgruszecki can tell us more.

At any rate, there's no reason that it should behave differently than the following, which works:

  case (x: F,  _: (Ev.EvInt &  Ev[Int])) => x

@abgruszecki
Copy link
Contributor

I agree that in principle nested typecase patterns behave the same as intersection types. It's clear what GADT logic should do with patterns like that, it just was never tested with them. The idea that "the assumption of the person who wrote the code was that there was no more type info to get on the LHS of a type pattern" is a good one, that'd be my hunch as well.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

nested named irrefutable typetest pattern causes exhaustivity warning
7 participants