Search code examples
scalatype-systemsalgebraic-data-types

How does the Scala type system know that cons + Nil is exhaustive?


I just wrote this function, wondering what would happen if I omitted the Nil case, and noticed that scalac gives me a warning:

def printList[String](list: List[String]) {
    list match {
        case head :: tail => {
            println(head)
            printList(tail)
        }
        //case Nil => println("Done")
    }
}

Warning: match may not be exhaustive. It would fail on the following input: Nil

I'm having trouble pinning down exactly what's going on here. I get the general idea of pattern matching on a recursive data type until you exhaust the cases, but it's not clear to me how that maps to the Scala type system. Specifically, I'm looking at the source code of the Scala standard library and wondering:

  1. Where exactly in the code is Scala getting the idea that a base case is required to complete a match statement for an instance of the List class? One could certainly imagine an algebraic data type that "just keeps going" with no base case.
  2. Where exactly in the code is scala.collection.immutable.Nil in particular designated as the base case for the List class?

Solution

  • You can see the source code for List here. There's nothing special going on to do with base cases, it's just that List is declared as sealed, and then there are only two classes extending it:

    sealed abstract class List[+A] ...
    case object Nil extends List[Nothing] { ... }
    final case class ::[B](override val head: B, private[scala] var tl: List[B]) extends List[B] { ... }
    

    The Scala compiler can pretty easily determine if a sealed trait or abstract class is exhaustively matched, since it can determine the universe of possible matches in a single file. Section 8.4 of the Scala specification says:

    If the selector of a pattern match is an instance of a sealed class, the compilation of pattern matching can emit warnings which diagnose that a given set of patterns is not exhaustive, i.e. that there is a possibility of a MatchError being raised at run-time.