Monad 与 do 记法

Functor/Applicative/Monad 层次、do 记法的脱糖、IO 与 Option/Except，以及 Lean 特有的 do 扩展。

从一个重复模式说起

def f1 (x : Nat) : Option Nat := if x > 0 then some (x * 2) else none
def f2 (x : Nat) : Option Nat := if x < 100 then some (x + 1) else none

-- 想连起来用，只能层层判断
def chain (x : Nat) : Option Nat :=
  match f1 x with
  | none   => none
  | some y =>
    match f2 y with
    | none   => none
    | some z => some (z * 10)

嵌套 match 且到处重复「是 none 就传播」。Monad 就是把这个模式抽象出来：

def chain' (x : Nat) : Option Nat := do
  let y ← f1 x
  let z ← f2 y
  return z * 10

← 读作「取出」——如果是 none 就直接返回 none，否则把值绑定给变量继续。

三层抽象

Functor      → map     (<$>)
  ↓
Applicative  → pure, seq  (<*>)
  ↓
Monad        → bind    (>>=)

类	核心方法	能力
`Functor`	`map : (α → β) → f α → f β`	对包裹的值做变换
`Applicative`	`pure : α → f α`、`seq`	把普通值放进去；应用包裹的函数
`Monad`	`bind : m α → (α → m β) → m β`	后续计算可以依赖前面的结果

Monad 比 Applicative 强的地方就在最后一句：bind 的第二个参数是函数，能拿到前一步的值再决定做什么。

#eval (· + 1) <$> some 3          -- some 4      Functor
#eval some 3 >>= fun x => some (x + 1)   -- some 4  Monad
#eval (pure 3 : Option Nat)       -- some 3

do 记法的脱糖

do 块本质是 >>= 的语法糖：

-- 这段
do
  let x ← ma
  let y ← mb
  return f x y

-- 等价于
ma >>= fun x =>
mb >>= fun y =>
pure (f x y)

do 里的写法	含义
`let x ← e`	取出 `e` 的结果绑定给 `x`（`>>=`）
`let x := e`	普通绑定，不涉及 monad
`e` 单独一行	执行并丢弃结果（`>>`）
`return e`	`pure e`

← 与 := 的区别是最常见的困惑点。

let x ← readLine      -- x : String       取出了 IO 里的值
let y := readLine     -- y : IO String    y 是那个动作本身，没执行

写错的典型症状是类型错误里出现多一层的 monad（IO (IO String) 之类）。

常用 Monad

Option：可能失败

def safeDiv (a b : Nat) : Option Nat :=
  if b = 0 then none else some (a / b)

def calc (x : Nat) : Option Nat := do
  let a ← safeDiv 100 x
  let b ← safeDiv a 2
  return b + 1

任何一步 none，整个结果就是 none——不用写传播逻辑。

Except：带错误信息

def safeDiv' (a b : Nat) : Except String Nat :=
  if b = 0 then .error "division by zero" else .ok (a / b)

def calc' (x : Nat) : Except String Nat := do
  let a ← safeDiv' 100 x
  return a + 1

#eval calc' 0     -- Except.error "division by zero"

比 Option 多了失败原因。

IO：副作用

def main : IO Unit := do
  IO.println "What's your name?"
  let name ← (← IO.getStdin).getLine
  IO.println s!"Hello, {name.trim}!"

IO α 表示「执行后会产生副作用并返回 α」。

注意那个嵌套的 ←：(← IO.getStdin).getLine——Lean 允许在表达式中间用 ←，它会被提升到最近的 do 里。这是 Lean 相对 Haskell 的一个便利扩展。

StateM：可变状态

def counter : StateM Nat Nat := do
  modify (· + 1)
  modify (· + 1)
  get

#eval counter.run 0        -- (2, 2)

用纯函数模拟可变状态：get 读、set 写、modify 改。

Lean 特有的 do 扩展

Lean 4 的 do 比 Haskell 强不少，支持命令式风格的控制流。

可变局部变量

def sumTo (n : Nat) : Nat := Id.run do
  let mut total := 0
  for i in [0:n+1] do
    total := total + i
  return total

#eval sumTo 10       -- 55

let mut 声明可变变量！这仍然是纯函数——Lean 把它脱糖成 StateT，只是写起来像命令式。

Id.run do 用于在纯函数里跑 do 块（Id 是恒等 monad）。

for 与 break/continue

def firstEven (xs : List Nat) : Option Nat := Id.run do
  for x in xs do
    if x % 2 == 0 then
      return some x
  return none

for ... in ... 遍历任何 ForIn 实例（List、Array、范围 [0:10] 等）。支持 break、continue、提前 return。

if 不带 else

def check (n : Nat) : IO Unit := do
  if n > 100 then
    IO.println "big"
  IO.println "done"

do 里的 if 可以省 else（隐含 pure ()）。

try/catch

def risky : IO Unit := do
  try
    let content ← IO.FS.readFile "maybe-missing.txt"
    IO.println content
  catch e =>
    IO.println s!"error: {e}"

IO 有异常机制，try/catch 捕获。纯 monad 用 Except 更合适。

Monad 变换器

abbrev MyApp := StateT Nat (ExceptT String IO)

def action : MyApp Unit := do
  let n ← get                      -- StateT 的能力
  if n > 10 then throw "too big"   -- ExceptT 的能力
  IO.println s!"n = {n}"           -- IO 的能力（自动提升）
  set (n + 1)

变换器把多个 monad 的能力叠起来。注意 IO.println 直接就能用——MonadLift 类型类自动把内层 monad 的操作提升到外层。

常用变换器：

变换器	加了什么
`StateT σ m`	可变状态
`ReaderT ρ m`	只读环境
`ExceptT ε m`	错误
`OptionT m`	可能无值

自定义 Monad

structure Logger (α : Type) where
  value : α
  logs  : List String

instance : Monad Logger where
  pure a := ⟨a, []⟩
  bind m f :=
    let r := f m.value
    ⟨r.value, m.logs ++ r.logs⟩

def logged (msg : String) : Logger Unit := ⟨(), [msg]⟩

def program : Logger Nat := do
  logged "start"
  logged "computing"
  return 42

#eval program.logs    -- ["start", "computing"]

只要给出 pure 与 bind，do 记法就能用。

严格来说还应该证明 monad 律（左单位元、右单位元、结合律）。Lean 有 LawfulMonad 类型类来记录这些证明：

instance : LawfulMonad Logger := by
  constructor <;> intros <;> simp [·] <;> sorry

日常写程序不强制，但库代码应该提供——很多通用引理依赖 LawfulMonad。这是 Lean 相对其他语言的独特之处：抽象的数学性质可以被真正证明，而不只是文档里的约定。

常见问题

「类型对不上，多了一层 monad」 → 检查是不是把 ← 写成了 :=。

「do 块里想用普通值」 → let x := e 而非 let x ← e。

「纯函数里想用 do」 → Id.run do。

「不同 monad 混用」 → 需要 monad 变换器或显式转换（如 IO.ofExcept）。

下一篇进入第 2 部分：依值类型。

本页目录