Scala 3's Type System, Part 10: GADTs, Variance, and the Frontier
Two questions close out this series. Why is List[Dog] a List[Animal] while
Array[Dog] is emphatically not an Array[Animal], and why does a single
eval function get to return Int for one case and Boolean for another
without a cast? The answers are variance and GADTs, and both are things you want
to be able to predict rather than look up.
🔗The problem: a container that lies
Java made covariant arrays a language rule. This compiles:
Object[] arr = new String[1];
arr[0] = Integer.valueOf(42); // ArrayStoreException at runtime
Every Java array store carries a runtime type check to catch that, and the
failure is an ArrayStoreException thrown from an assignment that the compiler
approved. Scala refuses the program instead, because Array is invariant:
// scala-check: expect-error
class Animal
class Dog extends Animal
class Cat extends Animal
@main def demo(): Unit =
val dogs: Array[Dog] = Array(new Dog)
val animals: Array[Animal] = dogs // rejected here
animals(0) = new Cat-- [E007] Type Mismatch Error --------------------------------------------
8 | val animals: Array[Animal] = dogs
| ^^^^
| Found: (dogs : Array[Dog])
| Required: Array[Animal]
The rule underneath: a container you can only read from may be covariant; a container you can also write to may not.
🔗Covariance, contravariance, and predicting the error
Mark a type parameter +A and F[Dog] <: F[Animal]. Mark it -A and the
subtyping flips: F[Animal] <: F[Dog]. Producers are covariant, consumers are
contravariant.
class Animal
class Dog extends Animal
final class Box[+A](val value: A) // produces A
trait Sink[-A]: // consumes A
def send(a: A): Unit
@main def demo(): Unit =
val animalBox: Box[Animal] = Box(new Dog) // covariance
val anySink: Sink[Animal] = a => println(a)
val dogSink: Sink[Dog] = anySink // contravariance
dogSink.send(new Dog)
Sink[Dog] = anySink reads oddly until you say it out loud: something that
accepts any animal is a perfectly good place to send dogs.
Function types combine both — Function1[-T, +R] — which is why this is legal:
class Animal
class Dog extends Animal
val f: Dog => String = (a: Animal) => a.toString
A function that handles all animals can stand in wherever one that handles dogs is expected, and its return type can be more specific.
Now the rule that lets you predict the compiler’s complaint. Every occurrence of a type parameter sits in a position, and positions flip:
Where A appears | Position |
|---|---|
Method result type, val type | covariant |
| Method parameter type | contravariant |
Inside a +X type argument | keeps the surrounding position |
Inside a -X type argument | flips the surrounding position |
| Inside an invariant type argument | invariant — nothing is allowed |
var field type | invariant |
A +A may appear only in covariant positions, a -A only in contravariant
ones. Flips compose, which is why this whole trait is fine despite A sitting
inside function parameters:
trait Source[+A]:
def head: A // covariant: fine
def foreach(f: A => Unit): Unit // param of a param: flipped twice
def fold[B](z: B)(op: (B, A) => B): B // same, fine
And why this one is not:
// scala-check: expect-error
import scala.collection.mutable.ListBuffer
trait Source[+A]:
def collectInto(buffer: ListBuffer[A]): Unitcovariant type A occurs in invariant position in type ListBuffer[A]
of parameter buffer
ListBuffer is invariant, so once A is under it, no amount of position
flipping helps.
🔗The lower-bound fix
The canonical failure is a covariant collection with an “add” method:
// scala-check: expect-error
final class Stack[+A](items: List[A]):
def push(a: A): Stack[A] = Stack(a :: items)covariant type A occurs in contravariant position in type A
of parameter a
The fix is not to drop the +. It is to accept a wider element and return a
wider stack — exactly what List.:: and List.:+ do:
final class Stack[+A](private val items: List[A]):
def push[B >: A](b: B): Stack[B] = Stack(b :: items)
def top: Option[A] = items.headOption
class Animal
class Dog extends Animal
class Cat extends Animal
@main def demo(): Unit =
val dogs: Stack[Dog] = Stack(List(new Dog))
val animals: Stack[Animal] = dogs.push(new Cat) // widens to the LUB
println(animals.top)
B is a fresh parameter, so it occupies a contravariant position legally, and
the result type honestly reports that you now have a stack of something more
general. Pushing a Cat onto a Stack[Dog] gives you a Stack[Animal] rather
than a lie.
The standard library is not uniformly variant.
Ordering[T]is a pure consumer and yet is invariant —Ordering[Animal]will not be accepted whereOrdering[Dog]is wanted. That is a historical artifact of itsComparator/PartialOrderingancestry, not a principle. Check before you assume.
🔗GADTs: an evaluator that type-checks
Here is the motivating case. A small expression language where the type parameter records what each expression evaluates to:
enum Expr[A]:
case Lit(i: Int) extends Expr[Int]
case Bool(b: Boolean) extends Expr[Boolean]
case Add(l: Expr[Int], r: Expr[Int]) extends Expr[Int]
case Eq[B](l: Expr[B], r: Expr[B]) extends Expr[Boolean]
case If[A](c: Expr[Boolean], t: Expr[A], e: Expr[A]) extends Expr[A]
import Expr.*
def eval[A](e: Expr[A]): A = e match
case Lit(i) => i
case Bool(b) => b
case Add(l, r) => eval(l) + eval(r)
case Eq(l, r) => eval(l) == eval(r)
case If(c, t, f) => if eval(c) then eval(t) else eval(f)
@main def demo(): Unit =
println(eval(If(Eq(Lit(1), Lit(1)), Add(Lit(2), Lit(3)), Lit(0))))
Look at the first branch. The declared result type is A, and the branch
returns an Int. That is only sound because of what the match taught the
compiler: Lit extends Expr[Int], so if this value is a Lit and its static
type is Expr[A], then A must be Int in this branch and nowhere else.
That is the whole idea of GADT reasoning: matching a case introduces a local
type equality about the type parameter. The compiler records A =:= Int for
the duration of that branch, uses it to accept i, and discards it at the next
case. In the Bool branch it has A =:= Boolean instead. There is no
runtime tag inspection and no cast — the constructor already carried the
evidence.
Scala 2 could declare that same Expr, but its inference could not exploit the
equality, so the standard workaround was to cast:
// scala-check: skip
// Scala 2 — the shape everyone wrote
def eval[A](e: Expr[A]): A = (e match {
case Lit(i) => i
case Bool(b) => b
}).asInstanceOf[A]
That works and is unsatisfying: the cast is doing no work at runtime, it exists only to silence the compiler, and it silences genuinely wrong branches too. Scala 3 removes the need.
🔗Where GADT inference still gives up
Two limits are worth knowing, because both produce errors that look like the compiler being obtuse.
Omitting the result type disables the payoff. GADT constraints refine each branch, but with no declared result type the branches are joined into a union:
// scala-check: expect-error
enum Expr[A]:
case Lit(i: Int) extends Expr[Int]
case Bool(b: Boolean) extends Expr[Boolean]
import Expr.*
def eval[A](e: Expr[A]) = e match // no `: A`
case Lit(i) => i
case Bool(b) => b
@main def demo(): Unit =
val n: Int = eval(Lit(1)) // Found: Int | Boolean
Always annotate the result type of a GADT match. This is not a style preference; it is what turns the constraint on.
Type members do not get GADT refinement — only type parameters do. If you model the same evaluator with the path-dependent style from Part 9, it does not work:
// scala-check: expect-error
trait Expr:
type Value
case class Lit(i: Int) extends Expr:
type Value = Int
case class Bl(b: Boolean) extends Expr:
type Value = Boolean
def eval(e: Expr): e.Value = e match
case Lit(i) => i // Found: (i : Int) Required: e.Value
case Bl(b) => b
Matching on Lit tells the compiler the value e is a Lit, but it does not
propagate that into the abstract type projection e.Value. The workaround is
mechanical and slightly annoying: convert the type member into a type parameter
(trait Expr[A]) and the enum-style code above starts working. If you need the
type-member formulation for other reasons, you are back to a cast.
Beyond these, GADT constraint solving gets weaker as the relationship between the case’s parent type and the scrutinee’s type gets more indirect — nesting under abstract type constructors, or type parameters that occur in multiple positions. When it fails, the message is a plain type mismatch with no hint that a constraint was expected, which is the frustrating part.
🔗The frontier
Everything in this section is experimental. It requires nightly builds,
-experimental, or a specificimport language.experimental.*, and the syntax has already changed at least once for most of these. Do not build a production codebase on any of it. All snippets below are illustrative only.
Safer exceptions turns checked exceptions into an implicit capability. A
throws clause introduces a required CanThrow[E], and try/catch provides
one:
// scala-check: skip
import language.experimental.saferExceptions
class InsufficientFunds extends Exception
def withdraw(balance: Long, amount: Long): Long throws InsufficientFunds =
if amount > balance then throw InsufficientFunds() else balance - amount
@main def demo(): Unit =
try println(withdraw(100, 500))
catch case _: InsufficientFunds => println("declined")
Calling withdraw outside a catch for that exception is a compile error.
Java’s checked exceptions with the ergonomics fixed, essentially, though the
interaction with higher-order functions is where the hard parts live.
Capture checking is the ambitious one: tracking which capabilities a value
holds, so the compiler can tell you a resource escaped the scope that owns it.
The ^ suffix marks a type as capturing something:
// scala-check: skip
import language.experimental.captureChecking
// `logger` is valid only inside `op`; the ^ says the type captures a capability
def withLogger[T](path: String)(op: Logger^ => T): T = ???
// Rejected: the logger escapes, and would be used after close.
val leaked = withLogger("app.log")(logger => logger)
If this lands, use-after-close and leaked Iterators over closed streams become
compile errors, and effect tracking gets a foundation that does not require
wrapping everything in a monad. It is also the largest change to Scala’s typing
rules since 3.0 and is still moving.
Named tuples give tuples labeled fields, so a query result or a small record needs no case class:
// scala-check: skip
type Order = (id: String, total: Long)
val o: Order = (id = "A-1", total = 1250L)
val cheap = o.total < 500
This one has progressed furthest — it graduated out of the experimental import in 3.7 — but treat the surrounding tooling and library support as young.
into and the conversion rework narrows implicit conversions from a global
hazard to an opt-in at a specific parameter. The callee declares where a
conversion may fire; nowhere else:
// scala-check: skip
import language.experimental.into
case class Route(segments: List[String])
given Conversion[String, Route] = s => Route(s.split("/").toList)
def handle(r: into Route): String = r.segments.mkString("/")
handle("orders/1") // conversion allowed here, and only here
The spelling of into has already changed once between releases. The direction
— conversions become a property of the API rather than of the import scope — is
the part to remember.
🔗Retrospective: ten parts
The arc was the three jobs from Part 1.
Model data so illegal states cannot be built. Enums and ADTs, union and intersection types, and opaque types. This is the part with an immediate payoff and essentially no cost. Every application codebase should be using all three.
Abstract over behavior. Given/using and type classes and derivation pay off around the third caller. Higher-kinded types and type lambdas are mostly a library concern — reach for them when you are writing the abstraction, not when you are consuming one.
Compute at compile time. Match types, dependent and structural types, and GADTs. These are where compile times go and where error messages get long. They earn their place in a library that thousands of call sites depend on, and rarely in application code.
If I had to compress the practical advice into one table:
| Feature | Application code | Library code |
|---|---|---|
| Enums / ADTs | Yes, everywhere | Yes |
| Opaque types | Yes, for identifiers and units | Yes |
| Union types | Yes, for error channels | Sparingly |
Type classes (given/using) | Yes, once you have three callers | Core tool |
| Derivation | Consume it | Write it |
| Higher-kinded types | Rarely | Yes |
| Match types | No | Yes, with care |
| Literal / dependent types | For a typed config, maybe | Yes |
| Structural types | Only at dynamic edges | At dynamic edges |
| GADTs | If you have an interpreter | Yes |
| Variance annotations | On your own collections | Always think about it |
The failure mode I see most often is not underusing these features. It is a codebase where someone reached for match types and inline resolution to solve something a sealed trait handled fine, and now the compile takes four minutes and nobody wants to touch that module. The type system is good enough now that restraint is the skill worth practicing.
Thanks for reading all ten.