Add match type

[odersky]

Add matching on types as a full-blown type.

• syntax and parsing
• type-checking
• basic type representation
• reduction of match types

[dottybot]

Hello, and thank you for opening this PR! 🎉

All contributors have signed the CLA, thank you! ❤️

Commit Messages

We want to keep history, but for that to actually be useful we have
some rules on how to format our commit messages (relevant xkcd).

Please stick to these guidelines for commit messages:

1. Separate subject from body with a blank line
2. When fixing an issue, start your commit message with Fix #<ISSUE-NBR>:
3. Limit the subject line to 72 characters
4. Capitalize the subject line
5. Do not end the subject line with a period
6. Use the imperative mood in the subject line ("Add" instead of "Added")
7. Wrap the body at 80 characters
8. Use the body to explain what and why vs. how

adapted from https://chris.beams.io/posts/git-commit

Have an awesome day! ☀️

[odersky]

test performance please

[dottybot]

performance test scheduled: 1 job(s) in queue, 0 running.

[dottybot]

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/4964/ to see the changes.

Benchmarks is based on merging with master (1d24eaa)

[odersky]

So, this looks good from an expressiveness and performance perspective. There are for me two open questions, which are interlinked:

Do we have the right criterion for discarding a case in a match type? Right now this is implemented by comparing scrutinee with all abstract types and type parameters mapped to wildcards with pattern type. If that match fails, the case can be discarded and reduction proceeds to the following cases. The test seems a bit ad hoc, and there are conditions which it does not cover. For instance,

final class A
final class B
type T[X] = X match { case A => 0 case B => 1 }
def f[Y <: B]: T[Y]

Here, we know that for all instances of Y only the second pattern matches because the classes are final, but our test does not capture that, and would refuse to reduce the match type.

How can match expressions get match types? We would like a typing rule stating when a match expression has a match type (to keep things simple, let's assume the match type will be given explicitly). What's the right rule? Again, the problem of negative information is the hard one to crack. How do we know that a type reduction clause cannot be fired for a scrutinee?

EDIT: I think it would be good to put forward and discuss concrete type-systematic rules for both questions. I would be very interested in everyone's input on this.

[odersky]

9897d22 contains a new informal spec for match types, which arose from our discussion at LAMP yesterday. The current implementation does not yet cover this new spec.

[odersky]

@OlivierBlanvillain @gsps @AleksanderBG @smarter Checking that a match term has a match type is harder than first thought. 22e08f8 contains a revised description.

[odersky]

Current status:

• works: syntax, subtyping & reduction rules, termination handling
• do be done:
  • variance checking. This needs variance checking for hk types in general, see Variance checking for higher-kinded types #5100.
  • GADT-style typing rules for term scrutinees
  • detection of non-overlapping patterns
  • type checking match expressions against match types.

[odersky]

There are still a lot of things to do, but many of those steps are independent from this PR. Since on the other hand this PR is by now the reference implementation for generic tuples I propose to work on merging it, so that we have something to base next steps on.

Otherwise, we'd be stuck with the rewrite method based version of tuples, which is harder to fix, and there is less motivation to fix anything because rewrite methods are likely to be dropped.

To be clear: The version of tuples in this PR still uses rewrite methods, but does not rely on the fact that rewrite methods can change types. So it should continue to work in a more standard inlining setting.

[OlivierBlanvillain]

@odersky Yesterday you mentioned bumping into cases that require type aliases and would be cumbersome with dependent method. Are those example part of this PR?

As far as I can see all the type functions in library/src-scala3/scala/Tuple.scala are always called with with something.type arguments, so they would be perfect candidate for the TypeOf approach.

If we try to keep type-level parts of Tuple.scala, it comes down to the following:

sealed trait Tuple extends Any {
  rewrite def ++(that: Tuple): Concat[this.type, that.type] = ...
  rewrite def size: Size[this.type] = ...
}

object Tuple {
  type Concat[+X <: Tuple, +Y <: Tuple] <: Tuple = X match {
    case Unit => Y
    case x1 *: xs1 => x1 *: Concat[xs1, Y]
  }

  type Size[+X] <: Int = X match {
    case Unit => 0
    case x *: xs => S[Size[xs]]
  }

  type Elem[+X <: Tuple, +N] = X match {
    case x *: xs =>
      N match {
        case 0 => x
        case S[n1] => Elem[xs, n1]
      }
  }
}

abstract sealed class NonEmptyTuple extends Tuple {
  rewrite def apply(n: Int): Elem[this.type, n.type] = ...
}

The same could be expressed with dependent methods:

sealed trait Tuple extends Any {
  rewrite def ++(that: Tuple): { concat(this, that) } = ...
  rewrite def size: { size(this) } = ...
}

object Tuple {
  dependent def concat(x: Tuple, y: Tuple): Tuple = x match {
    case () => y
    case x1 *: xs1 => x1 *: concat(xs1, y)
  }

  dependent def size(x: Tuple): Int = x match {
    case () => 0
    case x *: xs => size(xs) + 1
  }

  dependent def elem(x: Tuple, n: Int): Any = x match {
    case x *: xs =>
      n match {
        case 0 => x
        case n => elem(xs, n - 1)
      }
  }
}

abstract sealed class NonEmptyTuple extends Tuple {
  rewrite def apply(n: Int): { elem(this, n) } = ...
}

I think one clear advantage of the dependent def version is that it doesn't require an extra contract and deconstruct integers since +1 and -1 are already part of the expression language.

[odersky]

@OlivierBlanvillain I also think there are many similarities between the two approaches, and that there are advantages to both. But let me stress that match types are much more conservative than typeof. In fact we could probably do without match types altogether by adding the right type member structure to Tuple. E.g.

type Tuple
  type Append[Ys]
}
class *: [+X, +Xs] extends Tuple {
  type Append[Ys] = X *: Append[Xs, Ys]
}
class Unit extends Tuple {
  type Append[Ys] = Ys
}

I believe we can appeal to an encoding like this to argue soundness of match types. That's what the corresponding Haskell paper does. By contrast, typeof seems to need a lot more machinery. I still need to see a convincing argument why this would not roll in all the complexity of dependent types.

If typeof is reduced in scope to be essentially the same as match types, then I would argue that match types are still clearer. typeof has the somewhat strange mixing of terms and types. It just feels less clear to say "the type of applying this function" than to state the type directly. And since type is Scala's way to abstract over types, it just muddles the waters to now propose def - unless you go to full dependent types, where there is no difference between the two! That's a usability concern, not a technical one.

[smarter]

type Append[Ys] = X *: Append[Xs, Ys]

Given that Append is defined as a type member, I guess this should be:

type Append[Ys] = X *: Xs#Append[Ys]

But then we have a projection on an abstract type, so how do we justify soundness ?

[OlivierBlanvillain]

unless you go to full dependent types, where there is no difference between the two!

@odersky I think there is some confusion about what are dependent types. In my view, dependent types are types that dependent on a value, and that's all there is to it. Other things like:

• having types as first class values
• lifting every value to a type (that is, making no difference between the two)

are orthogonal concerns to dependent types, and clearly out of scope of Scala. Having these things on top of dependent types is useful for theorem proving, but it's also perfectly fine to be conservative and stick the essence of dependent types: types that depend on value.

So, according to this definition, match types clearly qualify as dependent types:

type M[X] = X match {
  case A => Int
  case B => String
}
def m(x: Any): M[x.type] = ...

Here the return type of m can be either Int or String, and that type depends on the value of x. Therefore, m is dependently typed.

I still need to see a convincing argument why this would not roll in all the complexity of dependent types.

Can you give an example where TypeOf bring more complexity than match types? Things are reversed for me, I would like to see a convincing argument why match types are any simpler than TypeOf. I feel than increasing the gap between types and values makes things trickier, not simpler:

1. Type-checking functions with match-types as return types become a hard problem. Are we going to need additional typing rules? If so, will these rules be any simpler than what we have for TypeOf?

2. With the match-type scheme, using any value-level functions at the type-level requires new primitive type operator (such as S[N]) and corresponding changes to TypeComparer. S is enough to do +1 and -1 on Int, but is this enough to cover everything we want from integers? How many primitive type operators would we need to write interesting type functions over java.lang.String singletons?

[LPTK]

@OlivierBlanvillain would you consider TypeScript to be dependently typed? Because your example can be done in TypeScript:

function m<T extends "A"|"B">(x: T): T extends "A" ? number : T extends "B" ? string : never {
  return m(x)
}
let x: number = m("A") // ok
let y: number = m("B") // Type 'string' is not assignable to type 'number'.
let z: string = m("A") // Type 'number' is not assignable to type 'string'.
let w: string = m("B") // ok

Sure, the TypeScript version uses a type parameter, but I really don't think this is an essential difference. Ultimately, what you match on in both the Scala and TypeScript versions is the type of what's passed into the function, not the value itself.

[OlivierBlanvillain]

@LPTK Yes, I would call that some form of dependent typing. I don't know much about the advanced type features of typescript, is it possible to do structural induction on types?

We can also do all that in today in Scala thought implicits. Whether or not that enough to call TypeScript and Scala 2.x dependently typed languages is up for debate, but in the case of Scala I would certainly argue that implicits are enough to write dependently typed programs.

Ultimately, what you match on in both the Scala and TypeScript versions is the type of what's passed into the function, not the value itself.

I agree, and this is also what's happening in the TypeOf version. Given the following definition:

dependent def size(x: Tuple): Int = x match {
  case () => 0
  case x *: xs => size(xs) + 1
}

When using size as a type ({ size(...) }), then x in x match { ... } is a type. More precisely, it's the type of what's passed into the size function.

[LPTK]

@OlivierBlanvillain I like the TypeOf proposal; it seems very natural to me. In fact, it already exists (in a more primitive form) in other languages, such as C++ with the decltype(expression) form.

It seems to me that while TypeOf is similar to match types for type-level programming, it would additionally be useful in its own right (sans dependent definitions), for expressing complex types succinctly (as in C++'s decltype), but also for 'applicative functor'-style types.

As we've talked about before, it'd allow to distinguish TreeMap[List[Int], {listOrd(intOrd)}] from TreeMap[List[Int], {listOrd(revIntOrd)}] so as to statically prevent those two from being merged. I think that would actually remove the main reason for wanting global type class coherence (AFAIK).

[nicolasstucki]

Shouldn't this check be performed in TypeBounds?

[odersky]

We don't have a constructor in TypeBounds. Maybe we need a refactoring, I am not sure. Anyway at the moment MatchType as whole needs more work but this will be in future PRs.

[nicolasstucki]

The implementation of the match types LGTM