Lean 学习笔记——4. 模块、类型类、Monad 与 IO

Some content in this article was created with AI assistance. Please verify as needed.

Lean 用命名空间管理名称，用结构体保存数据，用类型类描述多个类型共享的接口。mathlib 中许多看似自动的参数补全，实际来自类型类搜索。

模块、命名空间与作用域

命名空间

命名空间避免全局名称冲突：

namespace Text

def surround (left right value : String) : String :=
  left ++ value ++ right

def quote (value : String) : String :=
  surround "\"" "\"" value

end Text

#eval Text.quote "Lean"

open Text 会让当前作用域可以省略前缀：

section
open Text

#eval quote "Lean"

end

section 只创建作用域，不会成为名称的一部分；namespace 会成为全名的一部分。

可以用 open scoped 开启某个局部记号系统，用 open 导入普通名称。两者解决的问题不同。

模块与导入

Lean 文件路径对应模块名。例如项目中的：

MyProject/
├── Text/
│   └── Format.lean
└── Text.lean

MyProject/Text/Format.lean 的模块名为 MyProject.Text.Format，其他文件可以写：

1	import MyProject.Text.Format

import 导入整个模块及它传递导入的环境，不等同于把源代码文本直接复制进当前文件。

结构体组合

结构体可以扩展已有结构：

structure Named where
  name : String
  deriving Repr

structure User extends Named where
  id : Nat
  active : Bool
  deriving Repr

def ada : User where
  name := "Ada"
  id := 1
  active := true

#eval ada.name

这里的扩展更接近字段组合，不应该直接套用面向对象继承的全部语义。Lean 的函数通常仍然独立定义，数据也默认不可变。

类型类

类型类声明某种类型支持哪些操作：

class Summary (α : Type) where
  summarize : α → String

def summary {α : Type} [Summary α] (value : α) : String :=
  Summary.summarize value

方括号中的 [Summary α] 表示调用时需要找到一个实例。为 User 提供实例：

instance : Summary User where
  summarize user :=
    s!"#{user.id} {user.name}"

#eval summary ada

类型类不是运行时的“类对象”。实例通常在 elaboration 阶段通过类型类搜索补全，随后作为参数传给定义。

带参数的实例

实例也可以依赖其他实例。只要元素可转换为字符串，列表就可以获得摘要：

instance {α : Type} [ToString α] : Summary (List α) where
  summarize xs :=
    "[" ++ String.intercalate ", " (xs.map toString) ++ "]"

#eval summary [1, 2, 3]

类型类搜索会先尝试构造 Summary (List Nat)，然后继续寻找 ToString Nat。

实例冲突会让推断结果难以理解。常用设计是一个类型对一个规范实例；确实存在多种行为时，可以创建包装类型：

structure ReversedList (α : Type) where
  values : List α

instance {α : Type} [ToString α] : Summary (ReversedList α) where
  summarize xs :=
    summary xs.values.reverse

deriving

简单实例可以让 Lean 自动派生：

structure Version where
  major : Nat
  minor : Nat
  deriving Repr, BEq, Hashable

#eval Version.mk 4 33
#eval Version.mk 4 33 == Version.mk 4 32

常见派生项：

类型类	用途
`Repr`	供 `#eval` 等显示内部表示
`BEq`	使用 `==` 进行布尔比较
`Hashable`	计算哈希值
`Inhabited`	提供默认值

BEq 的结果是 Bool，它和数学命题中的相等 = 不同。前者用于计算，后者属于 Prop。

强制转换

Coe α β 类型类描述从 α 到 β 的强制转换。下面让用户名可以出现在需要字符串的位置：

structure UserName where
  value : String

instance : Coe UserName String where
  coe name := name.value

def welcome (name : UserName) : String :=
  "Welcome, " ++ name

#eval welcome ⟨"Ada"⟩

强制转换适合语义明确、不会造成信息丢失的转换。若转换可能失败，应该返回 Option 或 Except；若转换成本很高，则使用显式函数通常更清楚。

变量与作用域

variable 可以为一段代码预先声明参数：

section

variable {α : Type} [Summary α]

def duplicateSummary (x : α) : String :=
  summary x ++ " | " ++ summary x

end

这些变量只会出现在实际用到它们的定义中。section 结束以后，变量声明失效，定义本身仍然保留。

效果、Monad 与 IO

纯函数相同输入总是得到相同输出。文件、终端和时间等操作依赖外部世界，可能失败，还要求固定执行顺序。Lean 使用 IO 等带上下文的类型把这些效果显式写进函数签名。

Option 的 do 语法

多个可能失败的步骤可以用 do 串起来：

def parseDigit (c : Char) : Option Nat :=
  if c.isDigit then some (c.toNat - '0'.toNat)
  else none

def addTwoDigits (a b : Char) : Option Nat := do
  let x ← parseDigit a
  let y ← parseDigit b
  pure (x + y)

#eval addTwoDigits '4' '2' -- some 6
#eval addTwoDigits '4' 'x' -- none

← 从上下文中取出成功值；任何一步得到 none，整个计算都会直接得到 none。pure 把普通值放回当前上下文。

Except

Option 只能表示失败，Except ε α 还会携带错误信息：

def checkedDivide (a b : Int) : Except String Int :=
  if b == 0 then
    throw "division by zero"
  else
    pure (a / b)

def halfThenAdd (x y : Int) : Except String Int := do
  let half ← checkedDivide x 2
  pure (half + y)

#eval checkedDivide 42 2
#eval checkedDivide 42 0

构造器分别是 Except.ok 和 Except.error，pure 与 throw 是更适合 do 块的通用写法。

可以用 try/catch 在局部恢复：

def divideOrZero (a b : Int) : Except String Int := do
  try
    checkedDivide a b
  catch _ =>
    pure 0

do 的本质

do 不是只为 IO 提供的命令式语法。它是 bind、pure 等操作的语法糖，只要类型提供相应实例就能使用。

例如下面两个定义完全等价：

def next (x : Nat) : Option Nat :=
  some (x + 1)

def action : Option Nat := some 41

def viaDo : Option Nat := do
  let x ← action
  next x

def viaBind : Option Nat :=
  action >>= fun x => next x

前一种形式更接近逐步执行，后一种形式更直接展示函数组合。复杂流程通常使用 do 可读性更好。

IO

IO α 表示执行外部操作以后产生一个 α。最常见的 IO Unit 只关心效果，不关心返回数据：

1 2	def sayHello (name : String) : IO Unit := do IO.println s!"Hello, {name}!"

读取一行并再次输出：

def echo : IO Unit := do
  IO.print "input> "
  let stdin ← IO.getStdin
  let line ← stdin.getLine
  IO.println s!"echo: {line.trimAscii.toString}"

入口函数是一个名为 main 的 IO 值：

def main (args : List String) : IO Unit := do
  match args with
  | [] => IO.println "Hello, Lean!"
  | name :: _ => sayHello name

构建为可执行目标以后可以通过 lake exe <target> -- Ada 传入参数。

文件操作

文件读取会失败，因此底层仍然可能抛出 IO.Error：

def showFile (path : System.FilePath) : IO Unit := do
  try
    let content ← IO.FS.readFile path
    IO.println content
  catch error =>
    IO.eprintln s!"cannot read {path}: {error}"

对业务错误通常使用 Except，对真实外部操作使用 IO。两者可以组合成 IO (Except ε α)，但嵌套层数增加以后，可以考虑使用专门的转换器封装。

for 循环

支持遍历的值可以在 do 中使用 for：

def printLines (lines : List String) : IO Unit := do
  for line in lines do
    IO.println line

def printRange (n : Nat) : IO Unit := do
  for i in [0:n] do
    IO.println i

循环体仍然是一个 IO 计算。需要聚合纯数据时，map、filter 和 foldl 通常更合适。

可变变量

do 块内部可以使用 let mut 和赋值：

def countChars (lines : List String) : IO Nat := do
  let mut total := 0
  for line in lines do
    total := total + line.length
  pure total

这是局部的命令式接口，Lean 会把它 elaboration 成合适的状态传递。它不会让普通纯值变成全局可变对象。

并发任务

Task α 表示可并行计算并最终得到 α 的任务。IO 中可以创建任务并等待结果：

def parallelDemo : IO Unit := do
  let task ← IO.asTask (pure (List.range 1000 |>.foldl (· + ·) 0))
  let result ← IO.ofExcept task.get
  IO.println result

实际并发还要考虑计算粒度、共享资源和异常传播。类型只保证效果被显式表达，并不会自动保证程序具有良好并行性能。

模块系统的边界

命名机制的边界

这三个概念经常同时出现，但作用不同：

module 以文件为单位，由 import 组成依赖图；
namespace 改变声明的全名，用于组织 API；
section 只影响局部变量和选项，不进入声明名称。

namespace Geometry

section Plane

variable (scale : Float)

def scaleLength (x : Float) : Float :=
  scale * x

end Plane

end Geometry

#check Geometry.scaleLength

虽然 scaleLength 写在 section Plane 中，它的名称不是 Geometry.Plane.scaleLength，而是 Geometry.scaleLength。section 只是让一段声明共享局部上下文。

文件名也不会自动成为 namespace。模块 MyProject.Geometry.Point 中完全可以声明任意名称，只是按照模块路径建立同名 namespace 是最容易维护的约定。

导入机制

C/C++ 的 #include 基本上是预处理器文本替换；Lean 的 import 导入已经 elaboration 并序列化的模块环境。

模块构建以后会产生 .olean，其中包含：

声明名称与类型；
定义体或其可用信息；
定理；
实例；
属性；
宏和语法扩展；
环境扩展数据。

因此导入模块不等于重新解析全部依赖源码。它更接近 Rust crate metadata、C++ module 或编译器的预编译接口。

不过 Lean 的导入具有传递性：若 A 导入 B，再导入 A 时通常也能看到 B 中声明。为了控制编译时间，库代码仍应按需导入，而不是处处 import Mathlib。

open

open Namespace 只是改变未限定名称的解析候选，不创建新定义：

namespace Colors

def red := "#ff0000"

end Colors

section
open Colors

#eval red
#eval Colors.red

end

若两个打开的命名空间都包含同名声明，名称可能歧义。公共代码中适当保留限定前缀往往更容易阅读。

open scoped Foo 则开启由 scoped attribute 注册的记号、实例等局部环境。mathlib 的 BigOperators、Topology 常用这种机制，避免所有记号全局生效。

protected 声明

protected 声明通常不通过普通 open 暴露，而是借助类型信息或限定名查找：

namespace Account

structure Account where
  name : String

protected def Account.label (account : Account) : String :=
  "user:" ++ account.name

end Account

它适合 Nat.rec、某个类型的专属定理等不应该污染常用名称空间的声明。

结构体与类型类的原理

structure 的双重角色

结构体既可以是普通记录，也可以包含性质：

structure Port where
  value : Nat
  valid : value < 65536

def httpPort : Port :=
  ⟨80, by decide⟩

value 位于 Type，运行时需要保存；valid 位于 Prop，编译器通常可以擦除。于是结构体可以把数据和不变量绑在一起，而不一定为证明付出运行时空间。

与 Rust newtype 加私有构造器相比，两者都能阻止无效值。Lean 还能在类型层面保存并组合正确性证明；Rust 通常在构造时动态检查，此后依靠模块封装维持不变量。

构造器、投影与 eta

声明结构体后，Lean 自动生成构造器和字段投影：

structure Size where
  width : Nat
  height : Nat

#check Size.mk
#check Size.width
#check Size.height

对单构造器结构，值通常由其所有投影唯一决定。下面的重建在定义上就能化简：

1 2	def rebuildSize (s : Size) : Size := { width := s.width, height := s.height }

结构更新：

1 2	def Size.withWidth (s : Size) (width : Nat) : Size := { s with width := width }

仍然创建一个新值；表面“更新”不会改变原对象。

类型类与隐式参数

普通结构参数必须手动传递：

structure Encoder (α : Type) where
  encode : α → String

def encodeWith {α : Type} (encoder : Encoder α) (x : α) : String :=
  encoder.encode x

改成 class 和方括号参数后：

class EncoderClass (α : Type) where
  encode : α → String

def encodeAuto {α : Type} [EncoderClass α] (x : α) : String :=
  EncoderClass.encode x

[EncoderClass α] 会触发实例搜索；这里的差别在参数解析方式，不在对象布局。

类型类可以按编译期字典传递来理解：

源代码：
  encodeAuto value

概念上的显式形式：
  encodeAuto selectedEncoder value

Haskell 类型类采用类似字典传递；Rust trait 常通过静态单态化或 trait object 实现；C++ concepts 主要约束模板匹配。Lean 类型类不仅用于程序接口，还承担代数结构、可判定性、记号解释和证明搜索等工作。

实例搜索

假设目标是：

1	Summary (List Nat)

而环境中有：

1 2	instance {α : Type} [ToString α] : Summary (List α) where summarize xs := String.intercalate "," (xs.map toString)

搜索过程大致为：

发现实例结论 Summary (List α) 可以与目标统一；
得到 α := Nat；
产生新的实例子目标 ToString Nat；
找到标准实例；
构造完整实例项。

实例搜索是递归的。循环实例、过深链条或输出参数不明确，都可能导致 failed to synthesize、typeclass instance problem is stuck 等错误。

调试时可以：

1 2	#synth ToString Nat #synth Repr (List Nat)

复杂问题还可以临时开启 trace：

1 2	-- set_option trace.Meta.synthInstance true in -- #synth SomeClass SomeType

trace 输出非常多，只适合缩小后的示例。

默认实例与局部实例

实例是全局搜索环境的一部分，随 import 传播。若同一类型存在多个同等合理的实例，导入顺序和优先级可能影响结果。

可以把实例限制在 section 中：

section

local instance : ToString Bool where
  toString b := if b then "yes" else "no"

#eval toString true

end

局部实例不会进入其他模块。对于“升序还是降序”“JSON 精简还是美化”这类没有唯一答案的行为，可以采用：

显式传入配置；
使用包装类型；
使用局部实例；
不要注册多个全局规范实例。

操作与定律

程序接口可能只声明操作：

1 2	class Resettable (α : Type) where reset : α → α

数学结构则经常同时包含操作和定律。例如群不仅有乘法、单位元、逆元，还要求结合律、单位律和逆元律。

若只提供操作而没有定律，下游无法可靠推理；若所有普通程序接口都把行为规范写成证明字段，使用成本又可能过高。

一般原则：

需要形式化推理的抽象结构，应携带必要定律；
只用于运行时替换实现的工程接口，可以先保持轻量；
定律应尽量正交，避免存储能由其他字段推导的冗余证明。

mathlib 的代数结构层级采用了这种做法：基础结构只保存少量操作和定律，更强的结构在其上扩展。

强制转换原则

只为不会失败、语义基本唯一的转换提供强制转换实例：

structure Celsius where
  value : Float

instance : Coe Celsius Float where
  coe c := c.value

从包装类型取底层值通常没有歧义。反方向 Float → Celsius 则未必适合强制转换，因为它可能需要验证范围或单位语义。

以下转换通常不适合隐式完成：

可能失败；
丢失精度；
成本高；
有多种合理解释；
改变单位或坐标系。

强制转换链过长时，错误信息会出现大量 Coe.coe。此时显式写转换函数反而更清晰。

Functor、Applicative 与 Monad

Option、Except、IO 虽然用途不同，但都表示“带某种上下文的值”。可以从三层接口理解：

1
2
3

Functor      : 把普通函数作用到上下文中的值
Applicative  : 组合相互独立的上下文计算
Monad        : 后一步计算依赖前一步产生的值

Functor 的核心操作是 map：

1 2	#eval (some 41).map (fun n => n + 1) #eval (none : Option Nat).map (fun n => n + 1)

对于 Option，map 只在 some 中应用函数；对于 Except，它跳过错误；对于 IO，它在执行 IO 后变换结果。

Monad 的核心操作是 bind：

def halfIfEven (n : Nat) : Option Nat :=
  if n % 2 = 0 then some (n / 2) else none

def quarterIfPossible (n : Nat) : Option Nat :=
  halfIfEven n >>= halfIfEven

第二次 halfIfEven 的输入依赖第一次成功得到的值，因此需要 bind，而不只是 map。

do 语法展开

下面的代码：

def optionProgram (n : Nat) : Option Nat := do
  let half ← halfIfEven n
  let quarter ← halfIfEven half
  pure (quarter + 1)

可以粗略展开为：

def optionProgramExpanded (n : Nat) : Option Nat :=
  halfIfEven n >>= fun half =>
  halfIfEven half >>= fun quarter =>
  pure (quarter + 1)

因此 do 不会把函数式语言变成隐式共享状态的命令式语言。它只是把嵌套 lambda 和 bind 排成顺序形式。

与 Python async/await 相比，两者都有“展开为组合操作”的味道，但 Lean do 并不特指异步；Option、状态计算、解析器和 IO 都可以使用。

Monad 与异常

不同 Monad 表达的上下文不同：

类型	上下文含义
`Option α`	可能没有结果
`Except ε α`	可能带错误失败
`StateM σ α`	读取并更新状态 `σ`
`ReaderT ρ m α`	读取共享环境 `ρ`
`IO α`	与外部世界交互
`Task α`	异步计算结果

共同接口允许 do 复用，但不会消除语义差异。看到 m α 时，仍然必须知道具体 m 表示什么效果。

StateM

状态计算可以理解为函数：

1	σ → (α × σ)

输入旧状态，返回结果和新状态。StateM 封装这套传递：

def nextCounter : StateM Nat Nat := do
  let current ← get
  set (current + 1)
  pure current

def runCounter : Nat × Nat :=
  (do
    let a ← nextCounter
    let b ← nextCounter
    pure (a + b)).run 10

#eval runCounter

代码看起来在修改变量，语义上仍可解释为显式传入并返回状态。这比全局可变变量更容易组合和测试。

Monad transformer

真实程序经常同时需要环境、状态、错误和 IO。直接嵌套：

1	ReaderT Config (StateT Cache (ExceptT Error IO)) Result

可以精确表达效果，但类型会很长。transformer 的作用是把一种上下文叠加到另一种 Monad 上。

层级顺序会影响语义。例如“错误发生时是否保留已经更新的状态”，取决于 StateT 与 ExceptT 的组合顺序。它们不是随意排列的装饰器。

小程序不必一开始使用复杂栈。一个实用策略是：

纯函数返回 Except Error α；
最外层使用 IO 负责文件和终端；
确实出现大量共享上下文后，再引入 transformer。

IO、状态与并发

IO 边界

函数：

1 2	def loadConfig (path : System.FilePath) : IO String := IO.FS.readFile path

本身仍是一个普通 Lean 值，它描述了一个 IO 计算。只有运行时系统执行这个值时才真正读取文件。

这与 Haskell 的 IO 思路接近：不是假装外部世界是纯的，而是把与外部世界交互的顺序放进类型和组合接口。

相比之下，C、Python 的函数签名通常看不出是否读取文件、修改全局状态或打印终端，只能依赖文档和约定。

IO.Error 与业务错误

文件不存在、权限不足等系统失败由 IO 机制报告。配置字段非法、用户输入不符合业务规则则更适合自定义错误：

inductive ConfigError where
  | empty
  | invalidPort (text : String)
  deriving Repr

def validateConfig (text : String) : Except ConfigError String :=
  if text.isEmpty then
    .error .empty
  else
    .ok text

把两类错误分开有几个好处：

纯验证逻辑不依赖 IO，容易测试；
业务错误可以穷尽匹配；
最外层统一决定怎样打印或映射退出码；
不会把所有失败都压缩成无法区分的字符串。

局部可变性

let mut 提供命令式表面语法：

def sumArray (xs : Array Nat) : Nat := Id.run do
  let mut total := 0
  for x in xs do
    total := total + x
  return total

#eval sumArray #[1, 2, 3, 4]

它的作用域局限在 do 块，外部仍然看到一个纯函数。编译器可以将其优化成高效循环。

Lean 不是要求所有算法都写成低效链表递归。纯接口、局部命令式实现和唯一性优化可以共存，这一点与现代函数式语言的实践一致。

引用与共享可变状态

IO 中确实需要共享可变单元时，可以使用 IO.Ref：

def refDemo : IO Nat := do
  let counter ← IO.mkRef 0
  counter.modify (fun n => n + 1)
  counter.modify (fun n => n + 1)
  counter.get

引用的可变性被限制在 IO 类型中，纯函数无法直接观察它。并发修改还需要考虑原子性与同步；IO.Ref 本身不自动解决所有数据竞争设计问题。

Task 与线程

Task α 表示最终产生 α 的异步任务。它关注依赖和结果，不要求用户直接管理系统线程生命周期。

1
2
3

def taskDemo : IO Nat := do
  let task ← IO.asTask (pure 42)
  IO.ofExcept task.get

多个 task 可能由运行时调度到工作线程。细粒度任务的调度开销可能超过计算收益，因此并行并不是加一个 asTask 就必然更快。

与 C++ std::thread 相比，Task 更接近 future；与 Python asyncio.Task 相比，Lean Task 可以用于运行时调度的计算任务，而 Python asyncio 主要围绕单线程事件循环中的协作式 IO。

资源安全

打开文件、锁或网络连接以后，即使中途异常也必须释放。Lean 的 IO API 提供 bracket/finally 风格组合，应优先使用保证清理动作执行的接口，而不是只在正常路径末尾手动关闭。

概念上：

acquire
  ↓
use resource
  ↓ 无论成功或失败
release

这对应 C++ RAII、Rust Drop、Python with 和 Java try-with-resources。差异在于 Lean 将整个过程放在 IO 计算中组合。

错误与 panic

Lean 程序中可以出现 panic，但它不应该代替正常错误建模：

调用者可能合理恢复：返回 Option/Except；
系统操作失败：在 IO 中处理；
真正违反内部不变量：才考虑 panic；
逻辑上不可能的分支：最好由类型和证明排除。

动态语言常把所有问题都交给异常机制；Lean 允许在类型层面区分缺失、业务错误、IO 错误与不可能状态，接口信息更丰富，但也要求设计者提前决定失败语义。

宏与抽象层次

宏扩展

Lean 自身可以扩展 parser、命令和 tactic 语法，这也是 mathlib 能提供丰富 DSL 的原因。最简单的记号可以写成：

syntax "twice!" term : term

macro_rules
  | `(twice! $x) => `($x + $x)

#eval twice! 21

宏操作语法，不直接证明展开结果正确。展开后代码仍要正常 elaboration 并由内核检查。

自定义语法会增加阅读和工具维护成本。以下条件同时满足时再考虑宏：

某种结构反复出现且普通函数无法表达；
新语法显著接近问题领域记号；
错误位置和编辑器支持仍然可接受；
团队愿意维护这套局部语言。

普通函数、高阶函数或 do 已经足够时，宏没有带来额外信息。

抽象层次

Lean 同时提供很多组织机制：

需求	首选机制
避免名称冲突	namespace
文件级依赖与增量构建	module/import
共享局部变量或选项	section
固定字段的数据	structure
多种构造情况	inductive
一个规范的重载接口	typeclass
多种策略并存	显式参数或包装类型
可能失败	Option/Except
外部效果	IO
局部状态	StateM 或 `let mut`
共享可变状态	IO.Ref 等受控接口
特殊领域语法	最后再考虑 macro

类型类是由 elaborator 搜索的结构参数；Monad 规定带上下文计算的组合方式。选用哪种机制，取决于需要自动补参数、组织数据，还是显式描述效果。