Match Types
A match type reduces to one of a number of right hand sides, depending on a scrutinee type. Example:
type Elem[X] = X match {
case String => Char
case Array[t] => t
case Iterable[t] => t
}
This defines a type that, depending on the scrutinee type X
, can reduce to one of its right hand sides. For instance,
Elem[String] =:= Char
Elem[Array[Int]] =:= Int
Elem[List[Float]] =:= Float
Elem[Nil.type] =:= Nothing
Here =:=
is understood to mean that left and right hand sides are mutually subtypes of each other.
In general, a match type is of the form
S match { P1 => T1 ... Pn => Tn }
where S
, T1
, ..., Tn
are types and P1
, ..., Pn
are type patterns. Type variables
in patterns start as usual with a lower case letter.
Match types can form part of recursive type definitions. Example:
type LeafElem[X] = X match {
case String => Char
case Array[t] => LeafElem[t]
case Iterable[t] => LeafElem[t]
case AnyVal => X
}
Recursive match type definitions can also be given an upper bound, like this:
type Concat[+Xs <: Tuple, +Ys <: Tuple] <: Tuple = Xs match {
case Unit => Ys
case x *: xs => x *: Concat[xs, Ys]
}
In this definition, every instance of Concat[A, B]
, whether reducible or not, is known to be a subtype of Tuple
. This is necessary to make the recursive invocation x *: Concat[xs, Ys]
type check, since *:
demands a Tuple
as its right operand.
Representation of Match Types
The internal representation of a match type
S match { P1 => T1 ... Pn => Tn }
is Match(S, C1, ..., Cn) <: B
where each case Ci
is of the form
[Xs] =>> P => T
Here, [Xs]
is a type parameter clause of the variables bound in pattern Pi
. If there are no bound type variables in a case, the type parameter clause is omitted and only the function type P => T
is kept. So each case is either a unary function type or a type lambda over a unary function type.
B
is the declared upper bound of the match type, or Any
if no such bound is given.
We will leave it out in places where it does not matter for the discussion. Scrutinee, bound and pattern types must be firstorder types.
Match type reduction
We define match type reduction in terms of an auxiliary relation, canreduce
:
Match(S, C1, ..., Cn) canreduce i, T'
if Ci = [Xs] =>> P => T
and there are minimal instantiations Is
of the type variables Xs
such that
S <: [Xs := Is] P
T' = [Xs := Is] T
An instantiation Is
is minimal for Xs
if all type variables in Xs
that appear
covariantly and nonvariantly in Is
are as small as possible and all type variables in Xs
that appear contravariantly in Is
are as large as possible. Here, "small" and "large" are understood with respect to <:
.
For simplicity, we have omitted constraint handling so far. The full formulation of subtyping tests describes them as a function from a constraint and a pair of types to
either success and a new constraint or failure. In the context of reduction, the subtyping test S <: [Xs := Is] P
is understood to leave the bounds of all variables
in the input constraint unchanged, i.e. existing variables in the constraint cannot be instantiated by matching the scrutinee against the patterns.
Using canreduce
, we can now define match type reduction proper in the reducesto
relation:
Match(S, C1, ..., Cn) reducesto T
if
Match(S, C1, ..., Cn) canreduce i, T
and, for j
in 1..i1
: Cj
is disjoint from Ci
, or else S
cannot possibly match Cj
.
See the section on overlapping patterns for an elaboration of "disjoint" and "cannot possibly match".
Subtyping Rules for Match Types
The following rules apply to match types. For simplicity, we omit environments and constraints.
The first rule is a structural comparison between two match types:
Match(S, C1, ..., Cm) <: Match(T, D1, ..., Dn)
if
S <: T, m >= n, Ci <: Di for i in 1..n
I.e. scrutinees and corresponding cases must be subtypes, no case reordering is allowed, but the subtype can have more cases than the supertype.
The second rule states that a match type and its redux are mutual subtypes
Match(S, Cs) <: T
T <: Match(S, Cs)
if
Match(S, Cs) reducesto T
The third rule states that a match type conforms to its upper bound
(Match(S, Cs) <: B) <: B
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).
Typing Rules for Match Expressions
Typing rules for match expressions are tricky. First, they need some new form of GADT matching for value parameters. Second, they have to account for the difference between sequential match on the term level and parallel match on the type level. As a running example consider:
type M[+X] = X match {
case A => 1
case B => 2
}
We'd like to be able to typecheck
def m[X](x: X): M[X] = x match {
case _: A => 1 // type error
case _: B => 2 // type error
}
Unfortunately, this goes nowhere. Let's try the first case. We have: x.type <: A
and x.type <: X
. This tells
us nothing useful about X
, so we cannot reduce M
in order to show that the right hand side of the case is valid.
The following variant is more promising:
def m(x: Any): M[x.type] = x match {
case _: A => 1
case _: B => 2
}
To make this work, we'd need a new form of GADT checking: If the scrutinee is a term variable s
, we can make use of
the fact that s.type
must conform to the pattern's type and derive a GADT constraint from that. For the first case above,
this would be the constraint x.type <: A
. The new aspect here is that we need GADT constraints over singleton types where
before we just had constraints over type parameters.
Assuming this extension, we can then try to typecheck as usual. E.g. to typecheck the first case case _: A => 1
of the definition of m
above, GADT matching will produce the constraint x.type <: A
. Therefore, M[x.type]
reduces to the singleton type 1
. The right hand side 1
of the case conforms to this type, so the case typechecks.
Typechecking the second case hits a snag, though. In general, the assumption x.type <: B
is not enough to prove that
M[x.type]
reduces to 2
. However we can reduce M[x.type]
to 2
if the types A
and B
do not overlap.
So correspondence of match terms to match types is feasible only in the case of nonoverlapping patterns (see next section about overlapping patterns)
For simplicity, we have disregarded the null
value in this discussion. null
does not cause a fundamental problem but complicates things somewhat because some forms of patterns do not match null
.
Overlapping Patterns
A complete defininition of when two patterns or types overlap still needs to be worked out. Some examples we want to cover are:
 Two classes overlap only if one is a subtype of the other
 A final class
C
overlaps with a traitT
only ifC
extendsT
directly or indirectly.  A class overlaps with a sealed trait
T
only if it overlaps with one of the known subclasses ofT
.  An abstract type or type parameter
A
overlaps with a typeB
only ifA
's upper bound overlaps withB
.  A union type
A1  ...  An
overlaps withB
only if at least one ofAi
fori
in1..n
overlaps withB
.  An intersection type
A1 & ... & An
overlaps withB
only if all ofAi
fori
in1..n
overlap withB
.  If
C[X1, ..., Xn]
is a case class, then the instance typeC[A1, ..., An]
overlaps with the instance typeC[B1, ..., Bn]
only if for every indexi
in1..n
, ifXi
is the type of a parameter of the class, thenAi
overlaps withBi
.
The last rule in particular is needed to detect nonoverlaps for cases where the scrutinee and the patterns are tuples. I.e. (Int, String)
does not overlap (Int, Int)
since
String
does not overlap Int
.
Handling Termination
Match type definitions can be recursive, which raises the question whether and how to check that reduction terminates. This is currently an open question. We should investigate whether there are workable ways to enforce that recursion is primitive.
Note that, since reduction is linked to subtyping, we already have a cycle dectection mechanism in place. So the following will already give a reasonable error message:
type L[X] = X match {
case Int => L[X]
}
def g[X]: L[X] = ???
 val x: Int = g[Int]
 ^^^^^^
 found: Test.L[Int]
 required: Int
The subtype cycle test can be circumvented by producing larger types in each recursive invocation, as in the following definitions:
type LL[X] = X match {
case Int => LL[LL[X]]
}
def gg[X]: LL[X] = ???
In this case subtyping enters into an infinite recursion. This is not as bad as it looks, however, because
dotc
turns selected stack overflows into type errors. If there is a stackoverflow during subtyping,
the exception will be caught and turned into a compiletime error that indicates
a trace of the subtype tests that caused the overflow without showing a full stacktrace.
Concretely:
 val xx: Int = gg[Int]
 ^
Recursion limit exceeded.
Maybe there is an illegal cyclic reference?
If that's not the case, you could also try to increase the stacksize using the Xss JVM option.
A recurring operation is (inner to outer):

 subtype Test.LL[Int] <:< Int
 subtype Test.LL[Int] <:< Int
 ...
 subtype Test.LL[Int] <:< Int
(The actual error message shows some additional lines in the stacktrace).
Related Work
Match types have similarities with closed type families in Haskell. Some differences are:
 Subtyping instead of type equalities.
 Match type reduction does not tighten the underlying constraint, whereas type family reduction does unify. This difference in approach mirrors the difference between local type inference in Scala and global type inference in Haskell.
 No apriori requirement that cases are nonoverlapping. Uses parallel reduction instead of always chosing a unique branch.
Match types are also similar to Typescript's conditional types. The main differences here are:
 Conditional types only reduce if scrutinee and pattern are ground, whereas match types also work for type parameters and abstract types.
 Match types can bind variables in type patterns.
 Match types support direct recursion.
Conditional types in Typescript distribute through union types. We should evaluate whether match types should support this as well.