By: Dale Wijnand and Fengyun Liu
History
Date | Version |
---|---|
May 18th 2021 | Submitted |
Introduction
Exhaustivity checking is one of the safety belts for using pattern matching in functional programming. However, if one wants to partition values of an existing type to reason about them in separate cases of a match or as separate types this requires wrapping the values in new classes, which incurs a boxing cost.
As an alternative, one may define custom extractors and use them as the case patterns. However, there is no way in Scala to declare that these extractors are complementary, i.e. the match is exhaustive when the complete set of extractors are used together.
Similarly, one can define TypeTest
s for matching abstract types, but there is no way to determine
if a match on an abstract type exhausts all its subtypes.
This SIP solves these three problems by introducing sealed types.
Motivating Examples
We’ve identified several real world use cases that calls for enhancing exhaustivity checking, and used them to stress the design proposed here. You can find them here, but we’ll present an example below.
Using the opaque types and custom extractors we can work safely with positive integers and negative integers:
opaque type Pos <: Int = Int
opaque type Neg <: Int = Int
object Pos { def unapply(x: Int): Option[Pos] = if (x > 0) Some(x) else None }
object Neg { def unapply(x: Int): Option[Neg] = if (x < 0) Some(x) else None }
(n: Int) match
case 0 =>
case Pos(x) =>
case Neg(x) =>
With the above, when we get a Pos
value, it’s guaranteed to be a positive number. The same goes
for Neg
. Sadly the match is reported as not exhaustive because the two extractors and the value
0
aren’t known to be complementary.
Design
We identify two root causes:
- You can’t define a type, that isn’t a class, as
sealed
- You can’t define a mapping from values to types
The sealed type, proposed by this SIP, allow partitioning of value of a given type into a sealed type hierarchy. Here you can find how sealed types address the issues faced by all the motivating examples, but we’ll present here how it fixes the number example above.
In order to partition int into positive, zero, and negative numbers we’ll define a new sealed
type
Num
and how to distinguish its subtypes with match syntax:
sealed type Num = Int {
case 0 => val Zero
case n if n > 0 => type Pos
case _ => type Neg
}
This sealed type definition desugars into the following type and value definitions:
type Num = Int
val Zero: Num = 0
opaque type Pos <: Num = Num
opaque type Neg <: Num = Num
The match desugars into an ordinal method, that reuses the logic to associate an ordinal for each case:
extension (n: Num):
def ordinal: Int = (n: Int) match {
case 0 => 0
case n if n > 0 => 1
case _ => 2
}
Finally a series of TypeTest
s are defined, allowing for values of both the underlying type Int
and the sealed type Num
to be tested against the subtypes and singleton subtypes Pos
,
Zero.type
, and Neg
, using the ordinal
method:
given TypeTest[Int, Zero.type] = (n: Int) => if ((n: Num).ordinal == 0) Some(n) else None
given TypeTest[Int, Pos] = (n: Int) => if ((n: Num).ordinal == 1) Some(n) else None
given TypeTest[Int, Neg] = (n: Int) => if ((n: Num).ordinal == 2) Some(n) else None
given TypeTest[Int, Num] = (n: Int) => Some(n)
given [T <: Num](using t: TypeTest[Int, T]): TypeTest[Num, T] = (n: Num) => t.unapply(n)
Given the above, one can either change the usage from extractors to types:
(n: Int) match
case 0 =>
case x: Pos =>
case x: Neg =>
Or we can keep the usage the same by redefining the extractors (using a value class name-based
extractors PosExtractor
and NegExtractor
to avoid allocating):
object Pos { def unapply(x: Pos): PosExtractor = new PosExtractor(x) }
object Neg { def unapply(x: Neg): NegExtractor = new NegExtractor(x) }
class PosExtractor(private val x: Pos) extends AnyVal { def isEmpty: false = false ; def get = x }
class NegExtractor(private val x: Neg) extends AnyVal { def isEmpty: false = false ; def get = x }
(n: Int) match
case 0 =>
case Pos(x) =>
case Neg(x) =>
Syntax
The existing syntax is enhanced as follows:
TypeDcl ::= `sealed` [`opaque`] `type` id [TypeParamClause]
TypeDef ::= `sealed` [`opaque`] `type` id [TypeParamClause] [`>:` Type] [`<:` Type] `=` Type `{`
`case` Pattern [Guard] `=>` (`type` id [TypeParamClause] | `val` id [`:` Type])
`}`
Specifically:
- the
sealed
modifier becomes available for type definitions and declarations - on the right-hand side of definitions is the underlying type of the sealed type
- following the underlying type is a match that operates on a value of the underlying type and defines the type or singleton type associated to that case.
- the type is defined using the
type
keyword and singleton types are defined usingval
Desugaring
Using the example
sealed [opaque] type T[X..] [bounds] = U {
case p1 => type C[X..]
case p2 => val S
}
That desugars into:
- a type alias
type T[X..] [bounds] = U
,opaque
if the sealed type isopaque
(see Restrictions) - opaque type definitions,
opaque type C[X..] <: T[Y..] = T[Y..]
, for each non-singleton type case- any type argument
Y
that isn’t defined fromX..
will be:- its lower bound, if the type parameter is covariant
- its upper bound, if the type parameter is contravariant
- a wildcard type, with the type parameter’s bounds, if the type parameter is invariant
- any type argument
- val definitions,
val S: T[Y..] = p
, for singleton type cases, using the same type argument rules - an ordinal method,
extension (t: T): def ordinal: Int = (t: U) match { case p1 => 0 p2 => 1 .. }
- each of the sealed type’s cases is associated with a unique ordinal
- ordinals starts from 0 and increase for each case, in the order of their definition
- the ordinal method adds a
case _ => -1
default case, if the sealed type’s match is inexhaustive - such an ordinal method may only be defined by the compiler, to preserve exhaustivity guarantees
- a series a
TypeTest
s, defined in terms of the ordinal method- a
TypeTest
betweenU
and each caseA
, having ordinalordA
:given TypeTest[U, C] = (u: U) => if ((u: T).ordinal == $ordA) Some(u) else None
given TypeTest[U, S.type] = (u: U) => if ((u: T).ordinal == $ordA) Some(u) else None
- a type test between the underlying type and the sealed type:
given TypeTest[U, T] = (u: U) => if ((u: T).ordinal == -1) None else Some(u)
- a generic type test between
T
and each caseA
, defined in terms of the above type tests:given [A <: T](using t: TypeTest[U, A]): TypeTest[T, A] = (x: T) => t.unapply(x)
- a
Restrictions
- If the match on the value of the underlying type is not exhaustive, then the sealed type must be
declared
opaque
, in order to preserve the fact that the sealed type represents only a subset of the values of the underlying type (e.g. positive integers) - No other type may be declared to subtype the opaque type
T
- For singleton types, the pattern
p
must be a stable value, e.g. aval
, acase object
, or a literal - Each case must define a new type or singleton type
Alternative Design
An alternative design is to introduce an annotation @complete
to specify that
a type can be partitioned into a list of subtypes.
For example, given the following definition:
opaque type Nat <: Int = Int
opaque type Neg <: Int = Int
@complete[(Nat, Neg)] // Num decomposes to `Nat` and `Neg`
type Num = Int
given TypeTest[Int, Neg] = (n: Int) => if (x < 0) Some(n) else None
given TypeTest[Int, Nat] = (n: Int) => if (x >= 0) Some(n) else None
The user now can write code as follows:
def foo(n: Num) =
n match
case x: Neg =>
case x: Nat =>
Knowing that the type Num
can be decomposed to Neg
and Nat
, the compiler
can verify that the pattern match above is exhaustive.
This approach, however, is relatively low-level and the compiler does not provide any guarantee that the annotation is actually correct.
You can find more examples here
Related Work
Haskell has a COMPLETE
pragma which allows patterns and type constructors to be
defined to be a complete set, relying on the programmer getting it right.
data Choice a = Choice Bool a
pattern LeftChoice :: a -> Choice a
pattern LeftChoice a = Choice False a
pattern RightChoice :: a -> Choice a
pattern RightChoice a = Choice True a
{-# COMPLETE LeftChoice, RightChoice #-}
foo :: Choice Int -> Int
foo (LeftChoice n) = n * 2
foo (RightChoice n) = n - 2
References
- Opaque types
- Forum discussion about Opt[T]
- Github discussion about enhancing exhaustivity check
- Lightweight static capabilities, Oleg Kiselyov, Chung-chieh Shan, 2007
- TypeTest documentation
- https://github.com/lampepfl/dotty/issues/10961 False “match may not be exhaustive warning”
- https://github.com/lampepfl/dotty/pull/11186 Implement @covers annotation for partial irrefutable specification
- https://downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/exts/pragmas.html#complete-pragma
- https://downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/exts/pattern_synonyms.html
- https://dotty.epfl.ch/docs/reference/other-new-features/opaques.html