18.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

The empty type. It has no constructors.

Use Empty.elim in contexts where a value of type Empty is in scope.

Constructors

inductive type

PEmpty.{u} : Sort u

The universe-polymorphic empty type, with no constructors.

PEmpty can be used in any universe, but this flexibility can lead to worse error messages and more challenges with universe level unification. Prefer the type Empty or the proposition False when 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

18.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.

def

PEmpty.elim.{u_1, u_2} {C : Sort u_1} :
  PEmpty → C

PEmpty.elim : Empty → C says that a value of any type can be constructed from PEmpty. This can be thought of as a compiler-checked assertion that a code path is unreachable.