类型与项

一切皆项、类型宇宙层级、Type 与 Prop 的分工，以及为什么需要宇宙。

一切皆项

Lean 里只有一种东西：项（term）。每个项都有一个类型，而类型本身也是项，也有类型。

#check 42          -- 42 : Nat
#check Nat         -- Nat : Type
#check Type        -- Type : Type 1
#check Type 1      -- Type 1 : Type 2

读这条链：

42     的类型是 Nat
Nat    的类型是 Type
Type   的类型是 Type 1
Type 1 的类型是 Type 2
...无穷

没有「顶层类型」——这是刻意的。

为什么需要宇宙层级

朴素的想法是让 Type : Type。但那会导致罗素悖论的类型论版本（Girard 悖论），使系统不一致——一旦不一致，任何命题都能被「证明」，整个系统失去意义。

解法是宇宙层级（universe hierarchy）：

Type 0 (写作 Type)  : Type 1
Type 1              : Type 2
Type 2              : Type 3
...

每一层的类型住在更高一层，永远没有自己包含自己的情况。

日常写代码几乎不用关心层级——Lean 自动推断。只在写通用库代码时才需要显式处理：

universe u

def myId {α : Type u} (a : α) : α := a

universe u 声明宇宙变量，Type u 表示「某一层」。这让 myId 能作用于任意层级的类型，而不必为每层写一遍。

宇宙多态（universe polymorphism）通常是自动的：写 {α : Type _} 或 {α : Sort _}，Lean 会推断出所需的层级参数。

报错里出现 universe 字样时，通常是把不同层级的东西混用了——比如试图让一个 Type 的集合包含 Type 自身。

Sort、Type、Prop

Lean 的宇宙有一个统一形式 Sort：

Sort 0     = Prop        命题的宇宙
Sort 1     = Type 0 = Type
Sort 2     = Type 1
Sort (n+1) = Type n

所以 Prop 是第 0 层宇宙，Type 是 Type 0 的简写。

#check Prop         -- Prop : Type
#check (2 = 2)      -- 2 = 2 : Prop
#check Nat          -- Nat : Type

Prop 与 Type 的分工

	`Prop`	`Type`
住在里面的是	命题	数据类型
它的项是	证明	值
例子	`2 = 2`、`p ∧ q`、`∀ n, n + 0 = n`	`Nat`、`String`、`List α`
项之间是否相关	无关（proof irrelevance）	相关
编译后	被擦除	保留

Proof irrelevance（证明无关性） 是 Prop 的关键特性：同一个命题的任意两个证明被认为相等。

example (p : Prop) (h1 h2 : p) : h1 = h2 := rfl

这在 Type 上不成立——(1 : Nat) 与 (2 : Nat) 显然不等。

为什么这样设计：我们关心「命题是否成立」，不关心「怎么证的」。这让编译器可以把所有证明完全擦除——形式化验证过的代码，运行时不带任何证明开销。

Proof irrelevance 有个实际后果：不能对 Prop 里的项做模式匹配把信息带回 Type（除少数受限的消去规则）。

想在数据层面区分情况，命题要放进 Type，或者用可判定性（Decidable），见类型类。

函数类型

#check Nat → Nat            -- Nat → Nat : Type
#check (fun n => n + 1)     -- fun n => n + 1 : Nat → Nat

→ 是右结合的：

#check Nat → Nat → Nat      -- 等价于 Nat → (Nat → Nat)

所以多参数函数实际是返回函数的函数（柯里化）：

def add (a b : Nat) : Nat := a + b

#check add        -- Nat → Nat → Nat
#check add 3      -- Nat → Nat      ← 部分应用，合法
#eval  add 3 4    -- 7

add 3 是一个「还差一个参数」的函数。这是函数式语言的标准行为，在 Lean 里用得非常多。

基本类型速览

#check (42 : Nat)                  -- 自然数（0, 1, 2, ...），无负数
#check (-5 : Int)                  -- 整数
#check (true : Bool)
#check ("hi" : String)
#check ('a' : Char)
#check ([1, 2, 3] : List Nat)
#check ((1, "a") : Nat × String)   -- 积类型
#check (some 5 : Option Nat)

两个必须立刻注意的点。

Nat 是任意精度且不会下溢

#eval (3 : Nat) - 5       -- 0   不是 -2

Nat 上的减法是截断减法：结果小于 0 时变 0。这不是 bug，是 Nat 的定义——它没有负数。

需要负数用 Int：

#eval (3 : Int) - 5       -- -2

这是初学者最常踩的坑之一。 涉及减法的证明里，Nat 的截断行为会让很多「显然成立」的等式不成立——比如 a - b + b = a 在 a < b 时左边是 b 而非 a。

正确的形式需要前提 b ≤ a（Mathlib 里对应 Nat.sub_add_cancel）。写涉及 Nat 减法的命题时，先问自己「会不会下溢」。

Bool 与 Prop 是不同的东西

#check true          -- Bool     ← 一个【值】
#check True          -- Prop     ← 一个【命题】
#check (2 == 2)      -- Bool
#check (2 = 2)       -- Prop

	`Bool`	`Prop`
是什么	数据类型，有 `true`/`false` 两个值	命题的宇宙
相等判断	`==`（`BEq` 类型类）	`=`（命题相等）
用于	`if` 条件、可计算判断	定理陈述

两者靠 Decidable 连接——可判定的命题能自动转成 Bool：

#eval (2 = 2 : Bool)     -- true，通过 Decidable 实例转换

if 的条件需要是 Bool 或可判定的 Prop。详见类型类。

variable 与 section

section
variable (n : Nat)

def addN (m : Nat) : Nat := m + n     -- n 自动成为参数

end

variable 声明「后续定义可能用到的参数」——只有实际用到时才会被加进签名。写一组共享参数的定义时非常省事。

section ... end 限定作用域；namespace ... end 则同时加名字前缀：

namespace MyLib
def helper : Nat := 42
end MyLib

#check MyLib.helper

open MyLib in
#check helper          -- open 之后可省略前缀

类型即规格

最后回到 Lean 的核心思想。看这个签名：

def myId {α : Type} (a : α) : α

这个类型几乎唯一地确定了实现：对任意类型 α，给一个 α 造一个 α——除了返回参数本身无事可做（这叫参数性 / 自由定理）。

类型携带的信息越多，实现的自由度越小、正确性保证越强。依值类型把这一点推到极致——那时类型可以精确表达「返回长度为 n 的列表」这种规格。

下一篇：函数。

本页目录