# Monad 与 do 记法

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

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/monads
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## 从一个重复模式说起

```lean
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 就是把这个模式抽象出来**：

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

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

## 三层抽象

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

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

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

```lean
#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` 块本质是 `>>=` 的语法糖：

```lean
-- 这段
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` |

<Callout type="warn">
  **`←` 与 `:=` 的区别是最常见的困惑点。**

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

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

## 常用 Monad

### Option：可能失败

```lean
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：带错误信息

```lean
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：副作用

```lean
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：可变状态

```lean
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 强不少，支持命令式风格的控制流。

### 可变局部变量

```lean
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

```lean
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

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

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

### try/catch

```lean
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 变换器

```lean
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

```lean
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` 记法就能用。

<Callout type="info">
  **严格来说还应该证明 monad 律**（左单位元、右单位元、结合律）。Lean 有 `LawfulMonad` 类型类来记录这些证明：

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

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

## 常见问题

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

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

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

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

下一篇进入第 2 部分：[依值类型](https://daiw.org/manual/lean4/dependent-types)。