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
Sum[Zero, N]reduces to
Sum[M, Zero]is stuck and doesn’t reduce, as it is not known whether
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.
In order to remedy this, the addition of a new reduction rule for match types is proposed.
Here are the objectives:
- Reduction should remain sound (and deterministic).
- Enhanced reduction should be compatible with current match type reduction.
- 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
Nis fully reduced. In that case, the new rule should not change the reduction.
Nis not fully reduced. In that case, if
Rwith the new rule, then
Nalso has to reduce to
Rwith 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.
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.