Lean 语言参考手册

20.9. 单元类型🔗

单元类型是恰好具有一个元素的规范类型，该元素名为 unit，并由空元组 () 表示。 它只描述单个值，该值由上述不带参数的构造子构成。

Unit 类似于 C 语言及其派生语言中的 void：尽管 void 没有任何可以被命名的元素，但它表示从函数返回的控制流，而不包含额外信息。 在函数式编程中，Unit 是那些“什么都不返回”的事物的返回类型。 在数学上，这由一个完全不包含任何信息的单一值来表示，这与 Empty 这样的空类型相反，后者表示不可达的代码。

当使用 单子编程时，Unit 特别有用。 对于任何类型 α，m α 表示一个具有副作用并返回类型 α 的值的操作。 类型 m Unit 表示一个具有某些副作用但不返回值的操作。

单元类型有两种变体：

在幕后，Unit 实际上被定义为 PUnit.{1}。 可能的情况下，应优先使用 Unit 而不是 PUnit，以避免不必要的宇宙参数。 如有疑问，请使用 Unit 直到出现宇宙层级的错误。

🔗定义
Unit : Type
Unit : Type

只有一个元素的规范类型。该元素写作 ()。

Unit 有多种用途：

  • 可用于表示从函数调用返回、但不提供其他信息的控制流。

  • 返回 Unit 的单子操作只产生副作用而不计算值。

  • 在多态类型中，可用它表示某个字段不存储数据。

🔗定义
Unit.unit : Unit
Unit.unit : Unit

单元类型的唯一元素。

它可以写成空元组：()。

🔗归纳类型
PUnit.{u} : Sort u
PUnit.{u} : Sort u

只有一个元素的规范宇宙多态类型。

当上下文要求类型是宇宙多态的、因而不能使用 Unit 时，应使用此类型。

构造子

PUnit.unit.{u} : PUnit

宇宙多态单元类型的唯一元素。

20.9.1. 定义等价🔗

类单元类型 是一种只有一个构造子的归纳类型，且该构造子不接受非证明参数。 PUnit 就是这样一种类型。 类单元类型的所有元素都与所有其他元素 定义等价。

Unit 的定义等价

具有 Unit 类型的每个项都与具有 Unit 类型的每个其他项定义等价：

example (e1 e2 : Unit) : e1 = e2 := rfl
在线查看 ↪
类单元类型的定义等价

CustomUnit 和 AlsoUnit 都是类单元类型，具有不带参数的单一构造子。 这两种类型中的任意一对项都是定义等价的。

inductive CustomUnit where | customUnit example (e1 e2 : CustomUnit) : e1 = e2 := rfl structure AlsoUnit where example (e1 e2 : AlsoUnit) : e1 = e2 := rfl

带有参数的类型（例如 WithParam）如果是具有不接受参数的单一构造子，那么它们也是类单元类型。

inductive WithParam (n : Nat) where | mk example (x y : WithParam 3) : x = y := rfl

具有非证明参数的构造子不是类单元类型，即使参数全部是类单元类型也是如此。

inductive NotUnitLike where | mk (u : Unit) example (e1 e2 : NotUnitLike) : e1 = e2 := Type mismatch rfl has type ?m.3 = ?m.3 but is expected to have type e1 = e2rfl 
Type mismatch
  rfl
has type
  ?m.3 = ?m.3
but is expected to have type
  e1 = e2

类单元类型的构造子可以接受证明作为参数。

inductive ProofUnitLike where | mk : 2 = 2 → ProofUnitLike example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl
在线查看 ↪