The empty type. It has no constructors. The Empty.rec
eliminator expresses the fact that anything follows from the empty type.
12.10. The Empty Type
Planned Content
Tracked at issue #170
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
The universe-polymorphic empty type. Prefer Empty or False where
possible.
Constructors
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
12.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.