The empty type. It has no constructors. The Empty.rec
eliminator expresses the fact that anything follows from the empty type.
14.10. The Empty Type
The empty type Empty represents impossible values.
It is an inductive type with no constructors whatsoever.
While the trivial type Unit, which has a single constructor that takes no parameters, can be used to model computations where a result is unwanted or uninteresting, Empty can be used in situations where no computation should be possible at all.
Instantiating a polymorphic type with Empty can mark some of its constructors—those with a parameter of the corresponding type—as impossible; this can rule out certain code paths that are not desired.
The presence of a term with type Empty indicates that an impossible code path has been reached.
There will never be a value with this type, due to the lack of constructors.
On an impossible code path, there's no reason to write further code; the function Empty.elim can be used to escape an impossible path.
The universe-polymorphic equivalent of Empty is PEmpty.
inductive type
Empty : Type
inductive type
PEmpty.{u} : Sort u
Impossible Code Paths
The type signature of the function f indicates that it might throw exceptions, but allows the exception type to be anything:
def f (n : Nat) : Except ε Nat := pure n
Instantiating f's exception type with Empty exploits the fact that f never actually throws an exception to convert it to a function whose type indicates that no exceptions will be thrown.
In particular, it allows Empty.elim to be used to avoid handing the impossible exception value.
def g (n : Nat) : Nat :=
match f (ε := Empty) n with
| .error e =>
Empty.elim e
| .ok v => v
14.10.1. API Reference
def
Empty.elim.{u} {C : Sort u} : Empty → C
Empty.elim : Empty → C says that a value of any type can be constructed from
Empty. This can be thought of as a compiler-checked assertion that a code path is unreachable.
This is a non-dependent variant of Empty.rec.