20.10. 空类型🔗

空类型 Empty 表示不可能的值。它是一个完全没有构造子的归纳类型。

平凡类型 Unit 只有一个不接受参数的构造子，可用于为不需要或不关心结果的计算建模；而 Empty 可用于根本不应有任何计算发生的情形。用 Empty 实例化多态类型，可以将该类型的某些构造子——即带有相应类型参数的构造子——标记为不可能，从而排除某些不希望出现的代码路径。

出现类型为 Empty 的项，表示程序已经到达一条不可能的代码路径。由于没有构造子，这种类型绝不会有值。在不可能的代码路径上没有理由继续编写代码；可使用函数 Empty.elim 脱离这条不可能的路径。

Empty 的宇宙多态对应物是 PEmpty。

归纳类型

Empty : Type
Empty : Type

空类型。它没有构造子。

当作用域中有一个类型为 Empty.elim 所消去的 Empty 值时使用它。

构造子

归纳类型

PEmpty.{u} : Sort u
PEmpty.{u} : Sort u

宇宙多态的空类型，没有构造子。

PEmpty 可用于任意宇宙，但这种灵活性可能导致较差的错误消息，并使宇宙层级统一更具挑战。可能时应优先使用类型 Empty 或命题 False。

构造子

不可能的代码路径

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

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

将 f 的异常类型实例化为 Empty，便可利用 f 实际上从不抛出异常这一事实，将其转换为一个类型表明不会抛出异常的函数。具体而言，这样便可使用 Empty.elim，避免处理不可能存在的异常值。

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

在线查看 ↪

20.10.1. API 参考🔗

定义

Empty.elim.{u} {C : Sort u} : Empty → C
Empty.elim.{u} {C : Sort u} : Empty → C

Empty.elim : Empty → C 表示可以从 Empty 构造任何类型的值。这可以被认为是编译器检查的断言，即代码路径无法访问。

定义

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 表示可以从 PEmpty 构造任何类型的值。这可以被认为是编译器检查的断言，即代码路径无法访问。