Lean基本类型
简介[编辑 | 编辑源代码]
Lean基本类型是Lean 4定理证明器/编程语言中构建复杂类型系统的基石。作为依赖类型语言，Lean的类型系统既是程序正确性的验证工具，也是数学形式化的表达框架。本章将系统介绍Lean内置的基本类型、它们的特性及实际应用。
类型层级[编辑 | 编辑源代码]
Lean的类型系统遵循类型层级（Type Universe）机制，用Type u表示不同层级的类型宇宙，其中u是宇宙层级参数：
数学表达为：
基础数据类型[编辑 | 编辑源代码]
布尔类型[编辑 | 编辑源代码]
Bool是最简单的命题类型，包含两个构造子：
inductive Bool where
| true : Bool
| false : Bool
示例操作：
#eval true && false -- 输出: false
#eval not true -- 输出: false
数值类型[编辑 | 编辑源代码]
| 类型 | 描述 | 示例 |
|---|---|---|
Nat |
无符号自然数 | 42
|
Int |
整数 | -3
|
Float |
浮点数 | 3.14
|
类型转换示例：
#check (42 : Nat) -- Nat
#check (42 : Int) -- Int
#eval Float.ofNat 5 -- 5.0
字符与字符串[编辑 | 编辑源代码]
Char：UTF-16编码字符String：不可变字符串
#eval "Lean".length -- 4
#eval "a" ++ "b" -- "ab"
结构化类型[编辑 | 编辑源代码]
乘积类型[编辑 | 编辑源代码]
表示有序对（笛卡尔积），语法糖为×：
#check (Nat × Bool) -- Type
def pair : Nat × String := (42, "answer")
#eval pair.1 -- 42
和类型[编辑 | 编辑源代码]
通过Sum表示不相交联合：
#check Sum Nat Bool -- Type
def example : Sum Nat Bool := Sum.inr true
依赖类型基础[编辑 | 编辑源代码]
依赖函数类型[编辑 | 编辑源代码]
参数类型可依赖值的函数：
def depFun (n : Nat) : Fin n → Nat :=
fun i => i.val
其中Fin n表示小于n的自然数集合。
依赖乘积类型[编辑 | 编辑源代码]
即Σ类型，第二分量类型依赖第一分量：
def sigmaExample : (n : Nat) × Fin n := ⟨3, 2⟩
类型推导[编辑 | 编辑源代码]
Lean强大的统一算法支持自动类型推导：
def autoType := 42 -- 推导为Nat
def autoFun x := x + 1 -- Nat → Nat
实际应用案例[编辑 | 编辑源代码]
案例：安全向量索引
def safeGet (v : Vec α n) (i : Fin n) : α :=
v.get i -- 保证不会越界
案例：长度保持操作
def zipWith (f : α → β → γ)
(v1 : Vec α n) (v2 : Vec β n) : Vec γ n :=
match v1, v2 with
| nil, nil => nil
| cons x xs, cons y ys => cons (f x y) (zipWith f xs ys)
类型类系统[编辑 | 编辑源代码]
Lean通过类型类实现特设多态：
instance : Add Nat where
add := Nat.add
#eval 1 + (2 : Nat) -- 3
常见问题[编辑 | 编辑源代码]
Q: 如何选择Nat和Int？
A: 当需要非负整数语义（如长度、索引）时使用Nat，需要完整整数运算时用Int。
Q: 为什么需要类型宇宙？
A: 避免罗素悖论，通过层级限制Type : Type这样的不一致陈述。
进阶说明[编辑 | 编辑源代码]
对于高级用户，Lean支持通过axiom和unsafe突破部分类型限制，但会丧失严格验证保证。例如：
unsafe def unsafeCast (x : α) : β :=
unsafeCast x