Pre-SIP: Enhanced Match Type Reduction

Scala Improvement Process
1

Motivation

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

This prevents multiple base cases to be accessible. Consider the following code.

// Type-level natural numbers
sealed trait Nat
case class Zero() extends Nat
case class Succ[N <: Nat](n: N) extends Nat

// Type-level sum of natural numbers
type Sum[M <: Nat, N <: Nat] <: Nat = (M, N) match
  case (Zero, _) => N
  case (_, Zero) => M
  case (Succ[predM], _) => Succ[Sum[predM, N]]
  case (_, Succ[predN]) => Succ[Sum[M, predN]]

Sum has two base cases. However, the second cannot apply as generally. For M, N <: Nat:

  1. Sum[Zero, N] reduces to N.
  2. Sum[M, Zero] is stuck and doesn’t reduce, as it is not known whether M is Zero.

Below is an example illustrating how this limitation impacts expressivity.

// Uniform tuple with length encoded as part of the type
sealed trait Uniform[Length <: Nat, T]:
  def reversed: Uniform[Length, T] = reversedOnAcc(Empty())
  def reversedOnAcc[M <: Nat](acc: Uniform[M, T]): Uniform[Sum[Length, M], T]

// Empy uniform tuple
case class Empty[T]() extends Uniform[Zero, T]:
  def reversedOnAcc[M <: Nat](acc: Uniform[M, T]): Uniform[M, T] = acc

// Non-empty uniform tuple
case class Cons[PredL <: Nat, T](head: T, tail: Uniform[PredL, T]) extends Uniform[Succ[PredL], T]:
  def reversedOnAcc[M <: Nat](acc: Uniform[M, T]): Uniform[Succ[Sum[PredL, M]], T] =
    tail.reversedOnAcc(Cons(head, acc))

There doesn’t seem to be any way to rewrite Sum that can make this code compile, as the reduction of both base cases is needed.

Proposal

In order to remedy this, the addition of a new reduction rule for match types is proposed.

Here are the objectives:

  1. Reduction should remain sound (and deterministic).
  2. Enhanced reduction should be compatible with current match type reduction.
  3. Expressivity should be enhanced (by allowing code like the example above to compile).

Here is an elaboration of objective 2: for any current match type reduction M → N, either

  1. N is fully reduced. In that case, the new rule should not change the reduction.
  2. N is not fully reduced. In that case, if M → R with the new rule, then N also has to reduce to R with the new rule.

If the two first objectives are satisfied, disruption should be minimized. Code that currently compiles should still compile and keep the same semantics.

The new rule is currently expressed as an additional subtyping rule for System FM (as defined in the paper Type-Level Programming with Match Types). It is presented in the draft linked here, as I couldn’t find a way to include math directly here.

Concerns

One concern is how this would affect compile-time complexity. I do not think this is a fundamental issue for the proposal, as match types can already lead to arbitrary compile-time complexity for a project (family), including non-terminating.

To mitigate this concern further, a way could be added for the user to bound
the number of steps taken by the compiler during the match type reduction phase. This would already be useful now for current match type reduction.

1 Like