Fix #6709: Correlate match types and match expression #8024

OlivierBlanvillain · 2020-01-17T13:30:43Z

This PR adds a simple form of dependent typing by allowing match expressions to be typed as match types when their scrutinee type, pattern types, and body types align. Concretely, this means that we can define a value level counterpart to the LeafElem type from the match type documentation, and type check that expression with the match type:

type LeafElem[X] = X match {
  case String      => Char
  case Array[t]    => LeafElem[t]
  case Iterable[t] => LeafElem[t]
  case AnyVal      => X
}

def leafElem[X](x: X): LeafElem[X] =
  x match {
    case x: String      => x.charAt(0)
    case x: Array[t]    => leafElem(x(0))
    case x: Iterable[t] => leafElem(x.head)
    case _: AnyVal      => x
  }

This special mode of typing for match expressions is only used when the following conditions are met: (that logic is implemented by the isMatchTypeShaped function in Typer.scala)

The match expression patterns do not have guards
The match expression scrutinee's type is a subtype of the match type scrutinee's type
The match expression and the match type have the same number of cases
The match expression patterns are all Typed Patterns, and these types are =:= to their corresponding type patterns in the match type

Follow up work could potentially relax some of these conditions, for instance to support unapply patterns that are equivalent to typed patterns.

odersky

The implementation looks good, but we should not lose details in the docs.

docs/docs/reference/new-types/match-types.md

odersky · 2020-01-20T10:43:51Z

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

-        val result = typedMatchFinish(tree, sel1, selType, tree.cases, pt)
+
+        /** Extractor for match types hidden behind an AppliedType/MatchAlias */
+        object MatchTypeInDisguise {


This is interesting. Are there opportunities to use this extractor elsewhere?

I haven't found any, is it ok to leave it nested in here until we found another use of it?

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

odersky · 2020-01-20T10:46:58Z

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

+                // To check that pattern types correspond we need to type
+                // check `pat` here and throw away the result.
+                val gadtCtx: Context = ctx.fresh.setFreshGADTBounds
+                val pat1 = typedPattern(pat, selType)(gadtCtx)


Is there a way to avoid the repeated typing of the patterns? It would be nice if there was but maybe that's too complicated.

I think that would be too much spaghetti, we should need pass these GADT contexts and the typed patterns around inside typedMatchFinish, typedCases, and zip them with the cases before finally passing them to typedCase where they are needed...

OlivierBlanvillain · 2020-01-23T17:07:45Z

I agree the commit updating the docs was unreviewable, I've just splitted it into 6 smaller commits with some explanations in the commit message to justify the changes. I will wait for your input on which part of the delete text you would like to preserve before thinking about creating a more details docs page.

odersky

I believe we need to talk about variable instantiation and termination - these are difficult but central topics. Otherwise the changes look good to me.

odersky · 2020-01-30T09:47:42Z

docs/docs/reference/new-types/match-types.md

@@ -118,7 +118,6 @@ if
 Match(S, C1, ..., Cn)  can-reduce  i, T
 ```
 and, for `j` in `1..i-1`: `Cj` is disjoint from `Ci`, or else `S` cannot possibly match `Cj`.
-See the section on [overlapping patterns](#overlapping-patterns) for an elaboration of "disjoint" and "cannot possibly match".


Agree we should remove this. But we should nevertheless investigate whether we would gain something interesting if we also analyzed patterns for overlap. If none of the patterns overlap then we can presumably relax or drop the scrutinee / pattern overlap test. Would that gives us more expressivity in practice?

odersky · 2020-01-30T10:00:36Z

docs/docs/reference/new-types/match-types.md

-```
-if `Ci = [Xs] => P => T` and there are minimal instantiations `Is` of the type variables `Xs` such that
-```
-S <: [Xs := Is] P


The problem is that the rewritten version only talks about subtyping, not about type variable instantiation. But instantiation is crucial for understanding what goes on in more complicated examples. Maybe the existing text is not clear enough. Then it needs to be improved, but it should not be dropped outright.

odersky · 2020-01-30T10:02:50Z

docs/docs/reference/new-types/match-types.md

@@ -143,55 +143,6 @@ The third rule states that a match type conforms to its upper bound

 Within a match type `Match(S, Cs) <: B`, all occurrences of type variables count as covariant. By the nature of the cases `Ci` this means that occurrences in pattern position are contravarant (since patterns are represented as function type arguments).

-## Handling Termination
-


Agree that the tone of the description is more like an issue and not like a spec. But a spec still has to talk about termination. So the info needs to be given, just formulated differently.

LPTK · 2020-04-06T15:35:11Z

docs/docs/reference/new-types/match-types.md

+
+## Variance Laws for Match Types
+
+Within a match type `Match(S, Cs) <: B`, all occurrences of type variables count as covariant. By the nature of the cases `Ci` this means that occurrences in pattern position are contravarant (since patterns are represented as function type arguments).


@OlivierBlanvillain this formulation does not make any sense to me.

I think you wanted to say something along the lines of:

The type S and each type Ci occur positively in match type Match(S, Cs) <: B — i.e., the match type is covariant in S and Ci.

Furthermore, I imagine that the match type is contravariant in B , right?

This paragraph was not modified by PR, not sure why it shows up in the overall diff... But it appears to be outdated, so thanks for pointing it out!

Furthermore, I imagine that the match type is contravariant in B , right?

The bound isn't used when doing subtyping between two match types, so Match(S, Cs) <: B1 is =:= to Match(S, Cs) <: B2 forall B1, B2

Sure!

The bound isn't used when doing subtyping between two match types

It still needs to be considered during variance checks, no? Otherwise I think it could lead to unsoundness.

I don't see how, do you have an example?

I think I could come up with examples, but there does not seem to be an easy way to get a type with mismatched variance into the bound of a match type, at least from user code:

scala> class C[+T] { type A[X] <: T = X match { case Int => Nothing } } 1 |class C[+T] { type A[X] <: T = X match { case Int => Nothing } } | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | covariant type T occurs in invariant position in type [X] = | X match { | case Int => Nothing | } <: T of type A

Is there any other way for match type bounds to get picked up, other than by using and upper bound on an abstract type? If not, then I guess there is no soundness problem. But I'd be wary of corner cases.

PS: weirdly, this one works:

class C[+T] { type A[X] <: T = X match { case _ => Nothing } }

Is there any other way for match type bounds to get picked up, other than by using and upper bound on an abstract type?

No, that's the only syntax we have (which is kind of limiting, for example there is no way to specify bounds of nested match types).

Well, of you ever add a first-class syntax for match type bounds, you should remember to check their variance too :^P

The first sentence was wrong, stating that MT reduce to "a number of RHS", whereas the implementation only reduces to a single RHS. This commit also remove the covariant annotation in the Concat example as it's outdated (trying to compile that snippet on master results in "covariant type parameter Xs occurs in invariant position").

That section was a preliminary descrition of what's implemented in this PR, and is essentially subsumed by the section on Dependent typing.

This information is all outdated, the current implementation doesn't check for overlap between patterns. Instead it's looking at how the overlap between the scrutinee type and each pattern, sequentially.

I didn't understand that section on MT reduction, the rewritten version seams to correspond more closely to what's implemented in the compiler. I didn't get to review that text when it was first added to the docs, but here are the parts that are giving me trouble: - Which part of the code implements the "minimal instantiation" as described in the text? - What is `i` in the two "can-reduce" code blocks? Is it related to T/T'? - The "cannot possibly match" relation, which is central to the algorithm, isn't defined anywhere.

"we should investigate whether..." -> doesn't belong to a spec page. Maybe that text should go into an issue?

See https://github.com/lampepfl/dotty/blob/9982f0dced80d96cf5ca01f89ad68d969b9516ba/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L814-L816 Where we check for equality of scrutinees And https://github.com/lampepfl/dotty/blob/9982f0dced80d96cf5ca01f89ad68d969b9516ba/library/src/scala/internal/MatchCase.scala#L5 Where the pattern of a match case is invariant, meaning we also use equality for those.

OlivierBlanvillain requested a review from odersky January 17, 2020 13:30

OlivierBlanvillain assigned odersky Jan 17, 2020

odersky requested changes Jan 20, 2020

View reviewed changes

odersky assigned OlivierBlanvillain and unassigned odersky Jan 20, 2020

OlivierBlanvillain force-pushed the fix-6709 branch 2 times, most recently from db77ff4 to 4cb631d Compare January 23, 2020 17:02

odersky requested changes Jan 30, 2020

View reviewed changes

odersky added this to the 0.22 Tech Preview milestone Jan 30, 2020

anatoliykmetyuk removed this from the 0.22 Tech Preview milestone Feb 3, 2020

OlivierBlanvillain mentioned this pull request Mar 11, 2020

Match typing with trait types doesn't work #8493

Closed

OlivierBlanvillain force-pushed the fix-6709 branch from 872d052 to 613ca2d Compare April 6, 2020 09:01

LPTK reviewed Apr 6, 2020

View reviewed changes

OlivierBlanvillain added 11 commits April 6, 2020 21:53

Add test cases

030eab9

Special case typing matches w/ match type protos

e48a574

Docs: Add section on dependent typing (impl in this PR)

de26f46

Docs: Remove section on typing rules for Match expr

4c4ae84

That section was a preliminary descrition of what's implemented in this PR, and is essentially subsumed by the section on Dependent typing.

Docs: Remove mentions of overlapping patterns

c519cd7

This information is all outdated, the current implementation doesn't check for overlap between patterns. Instead it's looking at how the overlap between the scrutinee type and each pattern, sequentially.

Docs: Remove discussion on termination: future work

fae6e63

"we should investigate whether..." -> doesn't belong to a spec page. Maybe that text should go into an issue?

Restore text on termination

fec431c

Restore text on instantiation in type patterns

60cfa2d

OlivierBlanvillain force-pushed the fix-6709 branch from 613ca2d to 60cfa2d Compare April 9, 2020 15:00

OlivierBlanvillain merged commit f64e879 into scala:master Apr 9, 2020

OlivierBlanvillain deleted the fix-6709 branch April 9, 2020 16:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix #6709: Correlate match types and match expression #8024

Fix #6709: Correlate match types and match expression #8024

OlivierBlanvillain commented Jan 17, 2020

odersky left a comment

odersky Jan 20, 2020

OlivierBlanvillain Jan 23, 2020

odersky Jan 20, 2020

OlivierBlanvillain Jan 23, 2020 •

edited

Loading

OlivierBlanvillain commented Jan 23, 2020

odersky left a comment

odersky Jan 30, 2020

odersky Jan 30, 2020

odersky Jan 30, 2020

LPTK Apr 6, 2020

OlivierBlanvillain Apr 7, 2020

LPTK Apr 7, 2020

OlivierBlanvillain Apr 9, 2020

LPTK Apr 9, 2020 •

edited

Loading

OlivierBlanvillain Apr 9, 2020

LPTK Apr 9, 2020

		@@ -143,55 +143,6 @@ The third rule states that a match type conforms to its upper bound

		Within a match type `Match(S, Cs) <: B`, all occurrences of type variables count as covariant. By the nature of the cases `Ci` this means that occurrences in pattern position are contravarant (since patterns are represented as function type arguments).

		## Handling Termination


		## Variance Laws for Match Types

		Within a match type `Match(S, Cs) <: B`, all occurrences of type variables count as covariant. By the nature of the cases `Ci` this means that occurrences in pattern position are contravarant (since patterns are represented as function type arguments).

Fix #6709: Correlate match types and match expression #8024

Fix #6709: Correlate match types and match expression #8024

Conversation

OlivierBlanvillain commented Jan 17, 2020

odersky 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

OlivierBlanvillain Jan 23, 2020 • edited Loading

Choose a reason for hiding this comment

OlivierBlanvillain commented Jan 23, 2020

odersky 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

LPTK Apr 9, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

OlivierBlanvillain Jan 23, 2020 •

edited

Loading

LPTK Apr 9, 2020 •

edited

Loading