Lean 语言参考

20.10. 空的Type🔗

空类型 Empty 表示不可能的值。 它是一个没有任何构造函数的归纳类型。

虽然普通类型 Unit（具有不带参数的单个构造函数）可用于对结果不想要或无趣的计算进行建模，但 Empty 可用于根本不可能进行计算的情况。 使用 Empty 实例化多态类型可以将其某些构造函数（具有相应类型的参数的构造函数）标记为不可能； this can rule out certain code paths that are not desired.

类型为 Empty 的术语的存在表示已到达不可能的代码路径。 由于缺乏构造函数，这种类型永远不会有值。 在不可能的代码路径上，没有理由编写更多代码；函数 Empty.elim 可用于逃离不可能的路径。

Empty 的宇宙多态等价物是 PEmpty。

🔗inductive type
Empty : 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
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

函数 f 的类型签名表明它可能会抛出异常，但允许异常类型为任何类型：

def f (n : Nat) : Except ε Nat := pure n

使用 Empty 实例化 f 的异常类型利用了 f 实际上从未抛出异常的事实，将其转换为类型指示不会抛出异常的函数。 特别是，它允许使用 Empty.elim 来避免处理不可能的异常值。

def g (n : Nat) : Nat := match f (ε := Empty) n with | .error e => Empty.elim e | .ok v => v
Live ↪

20.10.1. API 参考🔗

🔗def
Empty.elim.{u} {C : Sort u} : Empty → C
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.{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.