**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 using`val`

## 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 is`opaque`

(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 from`X..`

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`

between`U`

and each case`A`

, having ordinal`ordA`

:`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 case`A`

, 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. a`val`

, a`case 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