编辑“︁Lean基本类型”︁

{{DISPLAYTITLE:Lean基本类型}}

== 简介 ==
'''Lean基本类型'''是Lean 4定理证明器/编程语言中构建复杂类型系统的基石。作为依赖类型语言，Lean的类型系统既是程序正确性的验证工具，也是数学形式化的表达框架。本章将系统介绍Lean内置的基本类型、它们的特性及实际应用。

== 类型层级 ==
Lean的类型系统遵循'''类型层级'''（Type Universe）机制，用<code>Type u</code>表示不同层级的类型宇宙，其中<code>u</code>是宇宙层级参数：

<mermaid>
graph TD
    Type 0 -->|居住于| Type 1
    Type 1 -->|居住于| Type 2
    Type u -->|居住于| Type (u+1)
</mermaid>

数学表达为：
<math>\mathtt{Type}\_0 : \mathtt{Type}\_1,\quad \mathtt{Type}\_1 : \mathtt{Type}\_2,\quad \ldots</math>

== 基础数据类型 ==

=== 布尔类型 ===
<code>Bool</code>是最简单的命题类型，包含两个构造子：
<syntaxhighlight lang="lean">
inductive Bool where
  | true : Bool
  | false : Bool
</syntaxhighlight>

'''示例操作'''：
<syntaxhighlight lang="lean">
#eval true && false  -- 输出: false
#eval not true       -- 输出: false
</syntaxhighlight>

=== 数值类型 ===

{| class="wikitable"
|+ Lean数值类型对比
! 类型 !! 描述 !! 示例
|-
| <code>Nat</code> || 无符号自然数 || <code>42</code>
|-
| <code>Int</code> || 整数 || <code>-3</code>
|-
| <code>Float</code> || 浮点数 || <code>3.14</code>
|}

'''类型转换示例'''：
<syntaxhighlight lang="lean">
#check (42 : Nat)    -- Nat
#check (42 : Int)    -- Int
#eval Float.ofNat 5  -- 5.0
</syntaxhighlight>

=== 字符与字符串 ===
* <code>Char</code>：UTF-16编码字符
* <code>String</code>：不可变字符串

<syntaxhighlight lang="lean">
#eval "Lean".length  -- 4
#eval "a" ++ "b"     -- "ab"
</syntaxhighlight>

== 结构化类型 ==

=== 乘积类型 ===
表示有序对（笛卡尔积），语法糖为<code>×</code>：
<syntaxhighlight lang="lean">
#check (Nat × Bool)  -- Type
def pair : Nat × String := (42, "answer")
#eval pair.1         -- 42
</syntaxhighlight>

=== 和类型 ===
通过<code>Sum</code>表示不相交联合：
<syntaxhighlight lang="lean">
#check Sum Nat Bool  -- Type
def example : Sum Nat Bool := Sum.inr true
</syntaxhighlight>

== 依赖类型基础 ==

=== 依赖函数类型 ===
参数类型可依赖值的函数：
<syntaxhighlight lang="lean">
def depFun (n : Nat) : Fin n → Nat := 
  fun i => i.val
</syntaxhighlight>
其中<code>Fin n</code>表示小于<code>n</code>的自然数集合。

=== 依赖乘积类型 ===
即Σ类型，第二分量类型依赖第一分量：
<syntaxhighlight lang="lean">
def sigmaExample : (n : Nat) × Fin n := ⟨3, 2⟩
</syntaxhighlight>

== 类型推导 ==
Lean强大的统一算法支持自动类型推导：
<syntaxhighlight lang="lean">
def autoType := 42      -- 推导为Nat
def autoFun x := x + 1  -- Nat → Nat
</syntaxhighlight>

== 实际应用案例 ==

'''案例：安全向量索引'''
<syntaxhighlight lang="lean">
def safeGet (v : Vec α n) (i : Fin n) : α :=
  v.get i  -- 保证不会越界
</syntaxhighlight>

'''案例：长度保持操作'''
<syntaxhighlight lang="lean">
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)
</syntaxhighlight>

== 类型类系统 ==
Lean通过类型类实现特设多态：
<syntaxhighlight lang="lean">
instance : Add Nat where
  add := Nat.add

#eval 1 + (2 : Nat)  -- 3
</syntaxhighlight>

== 常见问题 ==

'''Q: 如何选择<code>Nat</code>和<code>Int</code>？'''<br>
A: 当需要非负整数语义（如长度、索引）时使用<code>Nat</code>，需要完整整数运算时用<code>Int</code>。

'''Q: 为什么需要类型宇宙？'''<br>
A: 避免罗素悖论，通过层级限制<code>Type : Type</code>这样的不一致陈述。

== 进阶说明 ==
对于高级用户，Lean支持通过<code>axiom</code>和<code>unsafe</code>突破部分类型限制，但会丧失严格验证保证。例如：
<syntaxhighlight lang="lean">
unsafe def unsafeCast (x : α) : β := 
  unsafeCast x
</syntaxhighlight>

== 参见 ==
* [[Lean命题即类型原则]]
* [[Lean依赖类型编程]]
* [[Lean类型类系统详解]]

[[Category:Lean类型系统]]
[[Category:编程基础]]

[[Category:计算机科学]]
[[Category:Lean]]