Parallel match types

Language Design
1

Currently, match type reduction stalls once a case is encountered that doesn’t match but cannot be shown to be disjoint either.

I often find myself in situations where that prevents my code from type-checking.

For value-level matches, the sequentiality of the matching process is not an issue, since it never stalls on a case. However, at the type level, it significantly reduces expressivity.

I wonder if there is any accessible (backwards-compatible) Scala 3 language change that would allow parallel match types to be expressed (where any case that matches could be used to reduce the match type, regardless of case order).

Here is an example where I think parallel match types would be necessary (and sufficient) to get the code to compile. If there were parallel match types, then Sum could be written as

type Sum[M <: NatT, N <: NatT] <: NatT = (M, N) parallel match
  case (_, Zero) => M
  case (Zero, _) => N
  case (_, Succ[predN]) => Sum[Succ[M], predN]

Of course, one would have to decide on the semantics of when multiple cases match. But several acceptable solutions seem to exist in that case.

2

are you using only sealed/final types? compile time operations such as match types are really only useful with those, because no unknown runtime types can pollute the match

1 Like
3

Are you aware of compiletime.ops?
You can just utilize those operations for sum etc. Much better than match types for this use-case.

1 Like
4

Did you look at my example?

5

I was not fully aware of them. Thank you! However, I’m not sure how they would apply in my example, where I define a tuple-like type that keeps track of its size at the type level.

6

Look at how it’s implemented for Tuple:

  type Size[X <: Tuple] <: Int = X match {
    case EmptyTuple => 0
    case x *: xs => S[Size[xs]]
  }
7

The thing is that I want the size to be part of the type of ScalarTuple. This way, I could write things like

def foo[L <: NatT, S](t1: ScalarTuple[L, S], t2: ScalarTuple[L, S]): t1: ScalarTuple[L, S] = ???

or

trait A[S]:
  type D <: NatT
  type T = ScalarTuple[D, S]
8

I feel like the order is necessary to remove ambiguity, for example:

type Test[X] = X match
  case Int => String
  case Int => Int

What does Test[Int] evaluate to ?

9

Yes. For parallel match types, some new semantics would have to be decided in these cases.

I haven’t thought much about it, but one of the easiest solutions might be to pick the first match in these cases.

A more advanced solution could be to check whether all the matching branches eventually evaluate to the same type, and throw a compiler error if not. But that could lead to exponential complexity in some cases.

Memoization probably would reduce the set of such possibilities, but wouldn’t get rid of it altogether. Nevertheless, I don’t think it’s a fundamental issue, as it’s already possible to write match types that blow up, and the compiler could simply time out after a (flag-)set amount of time.

10

@Stephane just FYI there’s an open SIP which may be relevant for your use case: https://github.com/scala/improvement-proposals/pull/43

11

@gabro Thanks! As far as I can see, there is no overlap, but it’s interesting nonetheless.

12

If I’m not mistaken, that’s what’s being done currently, and is the reason we need disjunct cases !

Int match
  case MaybeMatchesInt[t] => Int
  case Int => String

You (the compiler) want to take MaybeMatchesInt if you can, since you do earliest first, but you don’t know, so what do you do ?
If you do it anyways, that introduces unsoundness
If you take the second case, then maybe by the user introducing new types, or refactoring MaybeMatchesInt, the match will evaluate to a different type !

13

Early on in the design of match types we played with a parallel version, where the result of a match would be the union (with |) of all cases that could possibly match the scrutinee. But that’s incompatible with match expressions, and also does not support niceties such as catch-alls at the end and user-defined errors. So it was not followed up on.

1 Like
14

We definitely woudn’t want that. What I meant is take the first case where we know it matches.

Is that so bad? If so, then what about my other suggestion, where all possible paths should be compatible?

For MaybeMatchesInt I cannot comment, as I dont’ know its definition, and I don’t have a fully formal strategy yet. But for Sum:

type Sum[M <: NatT, N <: NatT] <: NatT = (M, N) parallel match
  case (_, Zero) => M
  case (Zero, _) => N
  case (_, Succ[predN]) => Sum[Succ[M], predN]

For Sum[Zero, N] the compiler doesn’t know if it matches the first case.

But if it does, then N has to be Zero. In that case, Sum[Zero, N] would evaluate to Zero. This is consistent with the second case, where if N is Zero, the result is also Zero. The third case is not applicable if N is Zero.

If N is not Zero, then the two other cases both match. They can again be (inductively) shown to always evaluate to the same type.

So the compiler would accept this parallel match type definition, and there doesn’t seem to be any room for issues. Of course, this would have to be formalized, which would take some effort. Anyways. It doesn’t seem likely to make its way into Scala any time soon, even if a formal strategy were at hand.

15

I think this might be more complicated that we might expect, as equivalence is in practice a very hard problem, for example:

X parallel match
  case (4,1) => 65533
  case (m,n) => Ackermann[m,n]

Where Ackermann[m,n] is a matchtype translation of the 2ary Ackermann function

The above should technically compile !

16

Would a new (not-too-complicated) semantics for match types have a chance of being included in Scala, if they always reduced in the same way as match types currently do, except that they might reduce further when matching currently gets stuck?

Or would it still lead to compatibility issues?

For example, in my Sum example, Sum[Zero, N] could reduce to N, while @Sporarum 's example would remain stuck.

17

The compiler already takes virtually forever to terminate on such cases. For example:

summon[Ackermann[4,1] =:= 65533]
18

I would be surprised if you can do that and stay sound. According to my understanding, you’d get M | N, which is not all that helpful. You can’t simply skip to the second case for arguments (Zero, M), M might turn out to be Zero later, in which case the first case would match.

19

But assuming I could? I don’t want to think about it more unless there is a chance it gets used…

20

That’s the crux of the issue, I am doubtful a parallel match could work as you’d like, so it is on you to convince me, and the community at large, that it can work ^^’

1 Like