在 Lean 4 里手推一遍 Monad：从 Option 到 do 语法
来源：eli.thegreenplace.net — 2026-11-10
📋 概述
Eli Bendersky 用一个表达式求值器讲清 monad 的来路：先是每个分支都要手写 none 检查的嵌套 match，再抽成 withSome 辅助函数，然后重载成运算符，最后发现这正是 Monad 类型类的 pure 与 bind，而 do 记法不过是 bind 的语法糖。
🔑 核心要点
- 求值器支持整数、加法与除法，除零用 Option 显式表达失败，失败要一层层向上传递
- bind 的心智模型：取一个带副作用的包装值，接上一个可能再产生副作用的计算，合成最终的包装值
- monad 把「计算做什么」与「如何串联」解耦，串联的记账交给 bind 的实现
- 同样的结构换到 Except String Int，就能把失败原因一并带出，思路接近 Rust 的 Result
- 文章顺带指出这与 continuation-passing style 的亲缘关系，续延本身也能用 monad 建模
💡 金句
monad 把计算做什么与它们如何被串联解耦。
← 返回 Lobsters 首页