Hello World!

置顶发表于 2023-10-28 更新于 2024-12-28 阅读次数：字数： 492 时间 ≈ 2 分钟

欢迎来到 lookeng.cn，博客定位是与数学关联的一切一切，这里是置顶博客，整理已写博文和计划展开的话题，欢迎交流~

阅读全文 »

Putnam 竞赛深度调研报告

发表于 2025-10-28 阅读次数：字数： 5.7k 时间 ≈ 21 分钟

深入调研 PutNam 数学竞赛的历史、规则、题目特点及其对数学教育的重要意义

阅读全文 »

Lean 元编程基础(一) | 全书概要

发表于 2025-10-17 更新于 2025-10-28 阅读次数：字数： 2.2k 时间 ≈ 8 分钟

英文原文：Metaprogramming in Lean 4

本书的目的

本书旨在教授 Lean 4 元编程，通过学习本书，你将掌握：

构建自己的元编程工具（定义新的 Lean 符号，如「∑」；构建新的 Lean 命令，如 #check；编写策略，如 use 等）
阅读和理解元编程 API，如 Lean 4 核心库和 Mathlib4 中的 API

我们并不打算对整个 Lean 4 元编程 API 进行详尽的解释，也不深入涉及单子（Monad）化编程的主题。我们希望示例足够简单，即使不太熟悉单子化编程的读者也能跟上。强烈推荐《Lean 中的函数式编程》作为这个主题的参考资料。

本书的结构

本书致力于为 DSL 和策略建立足够的上下文背景，帮助你理解它们。章节依赖关系如下：

「表达式」=> 「MetaM」
「语法」=> 「宏」
「语法」+「MetaM」=> 「繁饰」=> 「DSL」
「宏」+「繁饰」=> 「证明策略」

证明策略一章之后是包含关键概念和功能概述的备忘录。随后是一些额外章节，展示了 Lean 4 元编程的其他应用。大多数章节的末尾都有习题，书的最后提供习题答案。

本章的其余部分将简要介绍什么是元编程，并提供一些小示例作为开胃菜。

注意：代码片段不是自包含的。它们应该从每章的开头开始，以增量方式运行/阅读。

译注：本书一律将 Syntax 译为语法，Grammar 译为文法。

「元」是什么？

当我们使用 Python、C、Java 或 Scala 等大多数编程语言编写代码时，通常需要遵循预定义的语法，否则编译器或解释器将无法理解代码。在 Lean 中，这些预定义语法用于定义归纳类型、实现函数、证明定理等。然后，编译器必须解析代码，构建一个 AST（抽象语法树），并将其语法节点阐释为语言内核可以处理的项。我们说编译器执行的这些活动是在元层面中完成的，这正是本书的内容。我们还说，语法的常见用法是在对象层面中完成的。

在大多数系统中，元层面活动是用与我们当前用来编写代码的语言不同的语言完成的。在 Isabelle 中，元层面语言是 ML 和 Scala；在 Coq 中，它是 OCaml；在 Agda 中，是 Haskell。而在 Lean 4 中，元代码主要是用 Lean 本身编写的，还有一些用 C++ 编写的组件。

Lean 的一个很酷且方便的特性是，它允许我们用日常在对象层面编写 Lean 的方式来自定义语法节点，并实现元层面例程。例如，可以编写记号来实例化某种类型的项，并在同一个文件中立即使用它！这个概念通常被称为反射。我们可以说，在 Lean 中，元层面被「反射」到对象层面。

用 Ruby、Python 或 JavaScript 等语言做元编程的方式可能是使用预定义的元编程方法来即时定义一些东西。例如，在 Ruby 中你可以使用 Class.new 和 define_method 在程序执行时即时定义一个新类及其新方法（其中包含新代码！）。

在 Lean 中，我们通常不需要「即时地」定义新的命令或策略，但是在 Lean 元编程中能做类似的事，并且同样直接。例如，你可以使用简单的一行 elab "#help" : command => do ...normal Lean code...。

然而，在 Lean 中，我们经常想要直接操作 Lean 的 CST（具体语法树，Lean 的 Syntax 类型）和 Lean 的 AST（抽象语法树，Lean 的 Expr 类型），而不是使用「正常的 Lean 代码」，特别是当我们编写证明策略（Tactic）时。因此，Lean 元编程更难掌握。本书的大部分内容都是为了研究这些类型以及我们如何操作它们。

元编程示例

下面这些例子仅作为展示。如果您现在不了解细节，请不要担心。

引入符号（定义新语法）

通常，人们希望引入新的符号，例如更适合数学（某个分支）的符号。例如，在数学中，人们会将给一个自然数加 2 的函数写为 x : Nat ↦ x + 2 或简单地写为 x ↦ x + 2（如果可以推断出定义域是自然数）。相应的 Lean 定义 fun x : Nat => x + 2 和 fun x => x + 2 使用 =>，这在数学中表示蕴涵，因此可能会让一些人感到困惑。

import Lean

macro x:ident ":" t:term " ↦ " y:term : term => do
  `(fun $x : $t => $y)

#eval (x : Nat ↦ x + 2) 2 -- 4

macro x:ident " ↦ " y:term : term => do
  `(fun $x  => $y)

#eval (x ↦  x + 2) 2 -- 4

构建命令

构建一个辅助命令 #assertType，它检查给定的项是否属于某种类型。用法如下：

#assertType <term> : <type>

代码如下：

elab "#assertType " termStx:term " : " typeStx:term : command =>
  open Lean Lean.Elab Command Term in
  liftTermElabM
    try
      let tp ← elabType typeStx
      discard $ elabTermEnsuringType termStx tp
      synthesizeSyntheticMVarsNoPostponing
      logInfo "success"
    catch | _ => throwError "failure"

/-- info: success -/
#assertType 5 : Nat

-- don't display names of metavariables
set_option pp.mvars false in

/--
error: type mismatch
  []
has type
  List ?_ : Type _
but is expected to have type
  Nat : Type
-/
#assertType [] : Nat

elab 启动 command 语法的定义。当被编译器解析时，它将触发后续的计算。

此时，代码应该在单子 CommandElabM 中运行。然后我们使用 liftTermElabM 来访问单子 TermElabM，这使我们能够使用 elabType 和 elabTermEnsuringType 从语法节点 typeStx 和 termStx 构建表达式。

首先，我们繁饰预期的类型 tp : Expr，然后使用它来繁饰项表达式。该项应具有类型 tp，否则将引发错误。然后我们丢弃生成的项表达式，因为它对我们来说并不重要——我们调用 elabTermEnsuringType 作为健全性检查。

我们还添加了 synthesizeSyntheticMVarsNoPostponing，它强制 Lean 立即繁饰元变量。如果没有这一行，#assertType [] : ?_ 将导致 success。

如果到目前为止没有抛出任何错误，则繁饰成功，我们可以使用 logInfo 输出 success。相反，如果捕获到某些错误，则我们使用 throwError 并显示相应的消息。

构建 DSL 和语法

让我们解析一个经典文法，即带有加法、乘法、自然数和变量的算术表达式文法。我们将定义一个 AST（抽象语法树）来编码表达式的数据，并使用运算符 + 和 * 来构建算术 AST。以下是我们将要解析的 AST：

inductive Arith : Type where
  | add : Arith → Arith → Arith -- e + f
  | mul : Arith → Arith → Arith -- e * f
  | nat : Nat → Arith           -- 常量
  | var : String → Arith        -- 变量

现在我们声明一个语法类别（declare syntax category）来描述我们将要解析的文法。我们通过为 + 语法赋予比 * 语法更低的优先级权重来控制 + 和 * 的优先级，这表明乘法比加法绑定得更紧密（数字越高，绑定越紧密）。

declare_syntax_cat arith
syntax num                        : arith -- nat for Arith.nat
syntax str                        : arith -- strings for Arith.var
syntax:50 arith:50 " + " arith:51 : arith -- Arith.add
syntax:60 arith:60 " * " arith:61 : arith -- Arith.mul
syntax " ( " arith " ) "          : arith -- 带括号表达式

-- 将 arith 翻译为 term 的辅助符号
syntax " ⟪ " arith " ⟫ " : term

-- 我们的宏规则执行「显然的」翻译：
macro_rules
  | `(⟪ $s:str ⟫)              => `(Arith.var $s)
  | `(⟪ $num:num ⟫)            => `(Arith.nat $num)
  | `(⟪ $x:arith + $y:arith ⟫) => `(Arith.add ⟪ $x ⟫ ⟪ $y ⟫)
  | `(⟪ $x:arith * $y:arith ⟫) => `(Arith.mul ⟪ $x ⟫ ⟪ $y ⟫)
  | `(⟪ ( $x ) ⟫)              => `( ⟪ $x ⟫ )

#check ⟪ "x" * "y" ⟫
-- Arith.mul (Arith.var "x") (Arith.var "y") : Arith

#check ⟪ "x" + "y" ⟫
-- Arith.add (Arith.var "x") (Arith.var "y") : Arith

#check ⟪ "x" + 20 ⟫
-- Arith.add (Arith.var "x") (Arith.nat 20) : Arith

#check ⟪ "x" + "y" * "z" ⟫ -- 优先级
-- Arith.add (Arith.var "x") (Arith.mul (Arith.var "y") (Arith.var "z")) : Arith

#check ⟪ "x" * "y" + "z" ⟫ -- 优先级
-- Arith.add (Arith.mul (Arith.var "x") (Arith.var "y")) (Arith.var "z") : Arith

#check ⟪ ("x" + "y") * "z" ⟫ -- 括号
-- Arith.mul (Arith.add (Arith.var "x") (Arith.var "y")) (Arith.var "z")

编写我们自己的策略

让我们创建一个策略，将一个给定名称的新假设添加到语境中，并将其证明推迟到最后。它类似于 Lean 3 中的 suffices 策略，只是我们要确保新目标位于目标列表的底部。

它将被称为 suppose，用法如下：

suppose <name> : <type>

让我们看看代码：

open Lean Meta Elab Tactic Term in
elab "suppose " n:ident " : " t:term : tactic => do
  let n : Name := n.getId
  let mvarId ← getMainGoal
  mvarId.withContext do
    let t ← elabType t
    let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
    let (_, mvarIdNew) ← MVarId.intro1P $ ← mvarId.assert n t p
    replaceMainGoal [p.mvarId!, mvarIdNew]
  evalTactic $ ← `(tactic|rotate_left)

example : 0 + a = a := by
  suppose add_comm : 0 + a = a + 0
  rw [add_comm]; rfl     -- 证明主目标
  rw [Nat.zero_add]; rfl -- 证明 `add_comm`

我们首先将主要目标存储在 mvarId 中，并将其用作 withContext 的参数，以确保我们的繁饰能够适用于依赖于语境中其他变量的类型。

这次我们使用 mkFreshExprMVar 为 t 的证明创建一个元变量表达式，我们可以使用 intro1P 和 assert 将其引入语境。

为了要求将新假设的证明作为目标，我们调用 replaceMainGoal，并在头部传递一个带有 p.mvarId! 的列表。然后我们可以使用 rotate_left 策略将最近添加的顶部目标移到底部。

Lean 函数式编程(三) | 单子

发表于 2025-10-16 更新于 2025-10-19 阅读次数：字数： 23k 时间 ≈ 1:22

Monads

在 C# 和 Kotlin 中，?. 运算符是一种在可能为 null 的值上查找属性或调用方法的方式。如果 ?. 前的值为 null，则整个表达式为 null。否则，该非 null 值会被用于调用。多个 ?. 可以链接起来，在这种情况下，第一个 null 结果将终止查找链。像这样链接 null 检查比编写和维护深层嵌套的 if 语句方便得多。

类似地，异常机制比手动检查和传递错误码方便得多。同时，通过使用专用的日志记录框架（而不是让每个函数同时返回其日志结果和返回值）可以轻松地完成日志记录。链式的空值检查和异常通常要求语言设计者预先考虑这种用法，而日志记录框架通常利用副作用将记录日志的代码与日志的累积解耦。

所有这些功能以及更多功能都可以作为通用 API —— Monad 的实例在库代码中实现。Lean 提供了专门的语法，使此 API 易于使用，但也可能会妨碍理解幕后发生的事情。本章从手动嵌套空值检查的细节介绍开始，并由此构建到方便、通用的 API。在此期间，请暂时搁置你的怀疑。

检查`none`：避免重复代码

在 Lean 中，模式匹配可用于链式的空值检查。从列表中获取第一个元素可以使用可选的索引记号：

1 2	def first (xs : List α) : Option α := xs[0]?

结果必须是 Option 类型，因为空列表没有第一个元素。提取第一个和第三个元素需要检查每个元素都不为 none：

def firstThird (xs : List α) : Option (α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      some (first, third)

类似地，提取第一个、第三个和第五个元素需要更多检查，以确保这些值不是 none：

def firstThirdFifth (xs : List α) : Option (α × α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      match xs[4]? with
      | none => none
      | some fifth =>
        some (first, third, fifth)

而将第七个元素添加到此序列中则开始变得相当难以管理：

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
  match xs[0]? with
  | none => none
  | some first =>
    match xs[2]? with
    | none => none
    | some third =>
      match xs[4]? with
      | none => none
      | some fifth =>
        match xs[6]? with
        | none => none
        | some seventh =>
          some (first, third, fifth, seventh)

这段代码的根本问题在于它处理了两个关注点：提取数字和检查它们是否全部存在，但第二个关注点是通过复制粘贴处理 none 情况的代码来解决的。通常良好的编程风格是将重复的片段提取到辅助函数中：

def andThen (opt : Option α) (next : α → Option β) : Option β :=
  -- if opt 不存在，直接返回 none，else 返回 next x
  match opt with
  | none => none
  | some x => next x

该辅助函数类似于 C# 和 Kotlin 中的 ?.，用于传播 none 值。它接受两个参数：一个可选值和一个在该值非 none 时应用的函数。如果第一个参数是 none，则辅助函数返回 none。如果第一个参数不是 none，则该函数将应用于 some 构造器的内容。

现在，firstThird 可以使用 andThen 重写：

def firstThird (xs : List α) : Option (α × α) :=
  andThen xs[0]? fun first =>
  andThen xs[2]? fun third =>
  some (first, third)

在 Lean 中，作为参数传递时，函数不需要用括号括起来。以下等价定义使用了更多括号并缩进了函数体：

def firstThird (xs : List α) : Option (α × α) :=
  andThen xs[0]? (fun first =>
    andThen xs[2]? (fun third =>
      some (first, third)))

andThen辅助函数提供了一种让值流过的“管道”，具有特殊缩进的版本更能说明这一事实。改进 andThen的语法可以使其更容易阅读和理解。

中缀运算符

在 Lean 中，可以使用 infix、infixl 和 infixr 命令声明中缀运算符，分别用于非结合、左结合和右结合的情况。当连续多次使用时，左结合运算符会将（开）括号堆叠在表达式的左侧。加法运算符 + 是左结合的，因此 w + x + y + z 等价于 (((w + x) + y) + z)。指数运算符 ^ 是右结合的，因此 w ^ x ^ y ^ z 等价于 (w ^ (x ^ (y ^ z)))。比较运算符（如 <）是非结合的，因此 x < y < z 是一个语法错误，需要手动添加括号。

以下声明将 andThen 声明为中缀运算符：

1	infixl:55 " ~~> " => andThen

冒号后面的数字声明了新中缀运算符的优先级。在一般的数学记号中，x + y * z 等价于 x + (y * z)，即使 + 和 * 都是左结合的。在 Lean 中，+ 的优先级为 65，* 的优先级为 70。优先级更高的运算符应用于优先级较低的运算符之前。根据 ~~> 的声明，+ 和 * 都具有更高的优先级，因此会被首先计算。通常来说，找出最适合一组运算符的优先级需要一些实验和大量的示例。

在新的中缀运算符后面是一个双箭头 =>，指定中缀运算符使用的命名函数。Lean 的标准库使用此功能将 + 和 * 定义为指向 HAdd.hAdd 和 HMul.hMul 的中缀运算符，从而允许将类型类用于重载中缀运算符。不过这里的 andThen 只是一个普通函数。

通过为 andThen 定义一个中缀运算符，firstThird 可以被改写成一种，显化 none 检查的“管道”风格的方式：

def firstThirdInfix (xs : List α) : Option (α × α) :=
  xs[0]? ~~> fun first =>
  xs[2]? ~~> fun third =>
  some (first, third)

这种风格在编写较长的函数时更加精炼：

def firstThirdFifthSeventh (xs : List α) : Option (α × α × α × α) :=
  xs[0]? ~~> fun first =>
  xs[2]? ~~> fun third =>
  xs[4]? ~~> fun fifth =>
  xs[6]? ~~> fun seventh =>
  some (first, third, fifth, seventh)

错误消息的传递

像 Lean 这样的纯函数式语言并没有用于错误处理的内置异常机制，因为抛出或捕获异常超出了表达式逐步求值模型考虑的范围。然而函数式程序肯定需要处理错误。在 firstThirdFifthSeventh 的情况下，用户很可能需要知道列表有多长以及查找失败发生的位置。

这通常通过定义一个可以表示错误或结果的数据类型，并让带有异常的函数返回此类型来实现：

-- 和类型，两个构造子，error 存储 ε 类型的报错信息，ok 存储 α 数据类型
inductive Except (ε : Type) (α : Type) where
  | error : ε → Except ε α
  | ok : α → Except ε α
deriving BEq, Hashable, Repr

类型变量 ε 表示函数可能产生的错误类型。调用者需要处理错误和成功两种情况，因此类型变量 ε 的作用有点类似 Java 中需要检查的异常列表。

类似于 Option，Except 可用于指示在列表中找不到项的情况。此时，错误类型为 String：

def get (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => Except.ok x

查找未越界的值会返回 Except.ok：

def ediblePlants : List String :=
  ["ramsons", "sea plantain", "sea buckthorn", "garden nasturtium"]

#eval get ediblePlants 2

Except.ok "sea buckthorn"

查找越界的值会返回 Except.error：

1
2
3

#eval get ediblePlants 4

Except.error "Index 4 not found (maximum is 3)"

单个列表查找可以方便地返回值或错误：

1 2	def first (xs : List α) : Except String α := get xs 0

连续进行两次列表查找需要处理可能发生的失败情况：

def firstThird (xs : List α) : Except String (α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  -- 拿到正确的 first 后，继续查找 third
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      Except.ok (first, third)

向函数中添加另一个列表查找操作需要处理更多的错误：

def firstThirdFifth (xs : List α) : Except String (α × α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      match get xs 4 with
      | Except.error msg => Except.error msg
      | Except.ok fifth =>
        Except.ok (first, third, fifth)

再添加一个列表查找操作则开始变得相当难以管理：

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
  match get xs 0 with
  | Except.error msg => Except.error msg
  | Except.ok first =>
    match get xs 2 with
    | Except.error msg => Except.error msg
    | Except.ok third =>
      match get xs 4 with
      | Except.error msg => Except.error msg
      | Except.ok fifth =>
        match get xs 6 with
        | Except.error msg => Except.error msg
        | Except.ok seventh =>
          Except.ok (first, third, fifth, seventh)

同样，可以将通用模式提取为一个辅助函数。函数中的每一步都会检查错误，只有在成功的情况下才进行后续计算。可以为 Except 定义新版本的 andThen：

def andThen (attempt : Except e α) (next : α → Except e β) : Except e β :=
  match attempt with
  | Except.error msg => Except.error msg
  | Except.ok x => next x

与 Option 一样，这个版本的 andThen 允许更简洁地定义 firstThird：

def firstThird' (xs : List α) : Except String (α × α) :=
  andThen (get xs 0) fun first  =>
  andThen (get xs 2) fun third =>
  Except.ok (first, third)

在 Option 和 Except 的情况下，都有两个重复的模式：每一步都有对中间结果的检查，已提取为 andThen；还有最终的成功结果，分别是 some 或 Except.ok。为了方便起见，可以将成功的情况提取为辅助函数 ok：

1 2	-- 将 x 记录到 ok 中 def ok (x : α) : Except ε α := Except.ok x

类似地，可以将失败的情况提取为辅助函数 fail：

1 2	-- 将 err 记录到 error 中 def fail (err : ε) : Except ε α := Except.error err

使用 ok 和 fail 使得 get 的可读性更好：

def get (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => fail s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => ok x

在为 andThen 添加中缀运算符后，firstThird 可以和返回 Option 的版本一样简洁：

infixl:55 " ~~> " => andThen

def firstThird (xs : List α) : Except String (α × α) :=
  get xs 0 ~~> fun first =>
  get xs 2 ~~> fun third =>
  ok (first, third)

这种技术同样适用于更复杂的函数：

def firstThirdFifthSeventh (xs : List α) : Except String (α × α × α × α) :=
  get xs 0 ~~> fun first =>
  get xs 2 ~~> fun third =>
  get xs 4 ~~> fun fifth =>
  get xs 6 ~~> fun seventh =>
  ok (first, third, fifth, seventh)

Q：同样模式反复出现后，怎么归纳统一？

日志记录

当一个数字除以 2 时没有余数则称它为偶数：

1 2	def isEven (i : Int) : Bool := i % 2 == 0

函数 sumAndFindEvens 计算列表所有元素的和，同时记录沿途遇到的偶数：

def sumAndFindEvens : List Int → List Int × Int
  | [] => ([], 0)
  | i :: is =>
    let (moreEven, sum) := sumAndFindEvens is
    (if isEven i then i :: moreEven else moreEven, sum + i)

此函数是一个常见模式的简化示例。许多程序需要遍历一次数据结构，在计算一个主要结果的同时累积某种额外的结果。一个例子是日志记录：一个类型为 IO 的程序会将日志输出到磁盘上的文件中，但是由于磁盘在 Lean 函数的数学世界之外，因此对基于 IO 的日志相关的证明变得十分困难。另一个例子是同时计算树的中序遍历和所有节点的和的函数，它必须记录每个访问的节点：

def inorderSum : BinTree Int → List Int × Int
  | BinTree.leaf => ([], 0)
  | BinTree.branch l x r =>
    let (leftVisited, leftSum) := inorderSum l
    let (hereVisited, hereSum) := ([x], x)
    let (rightVisited, rightSum) := inorderSum r
    (leftVisited ++ hereVisited ++ rightVisited, leftSum + hereSum + rightSum)

sumAndFindEvens 和 inorderSum 都具有共同的重复结构。计算的每一步都返回一个对（pair），由数据列表和主要结果组成。在下一步中列表会被附加新的元素，计算新的主要结果并与附加的列表再次配对。通过对 sumAndFindEvens 稍微改写，二者共同的结构变得更加明显：

def sumAndFindEvens : List Int → List Int × Int
  | [] => ([], 0)
  | i :: is =>
    let (moreEven, sum) := sumAndFindEvens is
    let (evenHere, ()) := (if isEven i then [i] else [], ())
    (evenHere ++ moreEven, sum + i)

为了清晰起见，可以给由累积结果和值组成的对（pair）起一个专有的名字：

1
2
3

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α

同样，保存累积结果列表的同时传递一个值到下一步计算的过程，可以提取为一个辅助函数，再次命名为 andThen：

def andThen (result : WithLog α β) (next : β → WithLog α γ) : WithLog α γ :=
  let {log := thisOut, val := thisRes} := result
  let {log := nextOut, val := nextRes} := next thisRes
  {log := thisOut ++ nextOut, val := nextRes}

在 Except 的语境下，ok 表示一个总是成功的操作。然而在这里，它仅简单地返回一个值而不产生任何日志：

1	def ok (x : β) : WithLog α β := {log := [], val := x}

正如 Except 提供 fail 作为一种可能性，WithLog 应该允许将项添加到日志中。它不需要返回任何有意义的结果，所以返回类型为 Unit：

1 2	def save (data : α) : WithLog α Unit := {log := [data], val := ()}

WithLog、andThen、ok 和 save 可以将两个程序中的日志记录与求和关注点分开：

-- 计算列表元素的和，同时记录遇到的偶数
def sumAndFindEvens : List Int → WithLog Int Int
  | [] => ok 0  -- 空列表：返回和为0，无日志
  | i :: is =>
    -- 第一步：如果当前元素是偶数，则记录它；否则不记录任何内容
    andThen (if isEven i then save i else ok ()) fun () =>
    -- 第二步：递归处理剩余列表，获取它们的和
    andThen (sumAndFindEvens is) fun sum =>
    -- 第三步：返回当前元素与剩余元素和的总和
    ok (i + sum)

-- 计算二叉树所有节点的和，同时记录中序遍历的节点序列
def inorderSum : BinTree Int → WithLog Int Int
  | BinTree.leaf => ok 0  -- 叶子节点：返回和为0，无日志
  | BinTree.branch l x r =>
    -- 第一步：递归计算左子树的和
    andThen (inorderSum l) fun leftSum =>
    -- 第二步：记录当前节点的值（中序遍历的核心）
    andThen (save x) fun () =>
    -- 第三步：递归计算右子树的和
    andThen (inorderSum r) fun rightSum =>
    -- 第四步：返回左子树、当前节点和右子树的总和
    ok (leftSum + x + rightSum)

关键设计模式：

andThen 函数将计算步骤串联起来，自动处理日志的合并
ok 函数用于返回纯值，不产生任何日志
save 函数用于向日志中添加数据，返回 Unit 类型

同样地，中缀运算符有助于专注于正确的步骤：

infixl:55 " ~~> " => andThen

def sumAndFindEvens : List Int → WithLog Int Int
  | [] => ok 0
  | i :: is =>
    (if isEven i then save i else ok ()) ~~> fun () =>
    sumAndFindEvens is ~~> fun sum =>
    ok (i + sum)

def inorderSum : BinTree Int → WithLog Int Int
  | BinTree.leaf => ok 0
  | BinTree.branch l x r =>
    inorderSum l ~~> fun leftSum =>
    save x ~~> fun () =>
    inorderSum r ~~> fun rightSum =>
    ok (leftSum + x + rightSum)

对树节点编号

树的每个节点的中序编号指的是在中序遍历中被访问的次序。例如，考虑如下的 aTree：

open BinTree in
def aTree :=
  branch
    (branch
       (branch leaf "a" (branch leaf "b" leaf))
       "c"
       leaf)
    "d"
    (branch leaf "e" leaf)

它的中序编号结果为：

BinTree.branch
  (BinTree.branch
    (BinTree.branch (BinTree.leaf) (0, "a") (BinTree.branch (BinTree.leaf) (1, "b") (BinTree.leaf)))
    (2, "c")
    (BinTree.leaf))
  (3, "d")
  (BinTree.branch (BinTree.leaf) (4, "e") (BinTree.leaf))

虽然树用递归函数来处理最为自然，但树的常见递归模式并不适合计算中序编号。这是因为左子树中分配的最大编号将决定当前节点的编号，进而决定右子树编号的起点。在命令式语言中，可以使用一个保存下一个待分配编号的可变变量来解决此问题。以下 Python 程序使用可变变量计算中序编号：

class Branch:
    def __init__(self, value, left=None, right=None):
        self.left = left
        self.value = value
        self.right = right
    def __repr__(self):
        return f'Branch({self.value!r}, left={self.left!r}, right={self.right!r})'

def number(tree):
    num = 0
    def helper(t):
        nonlocal num
        if t is None:
            return None
        else:
            new_left = helper(t.left)
            new_value = (num, t.value)
            num += 1
            new_right = helper(t.right)
            return Branch(left=new_left, value=new_value, right=new_right)

    return helper(tree)

aTree 在 Python 中的等价定义是：

a_tree = Branch("d",
                left=Branch("c",
                            left=Branch("a", left=None, right=Branch("b")),
                            right=None),
                right=Branch("e"))

它的编号结果是：

1
2

>>> number(a_tree)
Branch((3, 'd'), left=Branch((2, 'c'), left=Branch((0, 'a'), left=None, right=Branch((1, 'b'), left=None, right=None)), right=None), right=Branch((4, 'e'), left=None, right=None))

尽管 Lean 没有可变变量，但存在一种解决方法。从外部观察者的角度来看，可变变量可以认为具有两个相关方面：函数调用时的值和函数返回时的值。换句话说，使用可变变量的函数可以看作是：将变量的起始值作为参数，返回变量的最终值和计算结果构成的元组的函数。然后可以将此最终值作为参数传递给下一步计算。

正如 Python 示例中使用定义可变变量的外部函数和更改变量的内部辅助函数一样，Lean 版本使用：提供变量初值并明确返回结果的外部函数，以及在计算编号树的同时传递变量值的内部辅助函数：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper (n : Nat) : BinTree α → (Nat × BinTree (Nat × α))
    | BinTree.leaf => (n, BinTree.leaf)
    | BinTree.branch left x right =>
      let (k, numberedLeft) := helper n left
      let (i, numberedRight) := helper (k + 1) right
      (i, BinTree.branch numberedLeft (k, x) numberedRight)
  (helper 0 t).snd

此代码与传递 none 的 Option 代码、传递 error 的 Except 代码以及累积日志的 WithLog 代码一样，混合了两个关注点：传递计数器的值和实际遍历树以查找结果。与那些情况一样，可以定义一个 andThen 辅助函数，在计算的各个步骤之间传递状态。第一步是为以下模式命名：将输入状态作为参数并返回输出状态和值的模式：

1 2	def State (σ : Type) (α : Type) : Type := σ → (σ × α)

在 State 的情况下，ok 函数保持输入状态不变，并返回提供的值：

1 2	def ok (x : α) : State σ α := fun s => (s, x)

在使用可变变量时，有两个基本操作：读取值和用新值替换它。读取当前值是通过一个函数实现的，该函数将输入状态原样放入输出状态，同时将其作为返回值：

1 2	def get : State σ σ := fun s => (s, s)

写入新值是指忽略输入状态，并将提供的新值放入输出状态：

1 2	def set (s : σ) : State σ Unit := fun _ => (s, ())

最后，可以通过将第一个函数的输出状态和返回值传递给下一个函数来实现两个使用状态的计算的顺序执行：

def andThen (first : State σ α) (next : α → State σ β) : State σ β :=
  fun s =>
    let (s', x) := first s
    next x s'

infixl:55 " ~~> " => andThen

使用 State 和它的辅助函数，可以模拟局部可变状态：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => ok BinTree.leaf
    | BinTree.branch left x right =>
      helper left ~~> fun numberedLeft =>
      get ~~> fun n =>
      set (n + 1) ~~> fun () =>
      helper right ~~> fun numberedRight =>
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

由于 State 只模拟单个局部变量，因此 get 和 set 不需要引用任何特定的变量名。

单子：一种函数式设计模式

以上每个示例都包含以下结构：

一个多态类型，例如 Option、Except ε、WithLog logged 或 State σ
一个运算符 andThen，用于处理具有此类型的程序的顺序组合和重复模式
一个运算符 ok，它（在某种意义上）是使用该类型最基本的方式
一系列其他操作，例如 none、fail、save 和 get，它们提供了使用相应类型的具体方式

这种风格的 API 称为单子（Monad）。虽然单子的思想源自数学分支范畴论，但在编程中使用它们并不需要理解范畴论。单子的核心思想是：每个单子都使用纯函数式语言 Lean 提供的工具来编码特定类型的副作用。例如，Option 表示可能通过返回 none 而失败的程序，Except 表示可能抛出异常的程序，WithLog 表示在运行时累积日志的程序，State 表示具有单个可变变量的程序。

Monad 类型类

无需为每个单子都实现 ok 或 andThen 这样的运算符，Lean 标准库包含一个类型类，允许它们被重载，以便相同的运算符可用于任何单子。单子有两个操作，分别相当于 ok 和 andThen：

1
2
3

class Monad (m : Type → Type) where
  pure : α → m α
  bind : m α → (α → m β) → m β

这个定义略有简化。Lean 标准库中的实际定义更复杂一些，稍后会介绍。

Option 和 Except 的 Monad 实例可以通过调整它们各自的 andThen 操作的定义来创建：

instance : Monad Option where
  pure x := some x
  bind opt next :=
    match opt with
    | none => none
    | some x => next x

instance : Monad (Except ε) where
  pure x := Except.ok x
  bind attempt next :=
    match attempt with
    | Except.error e => Except.error e
    | Except.ok x => next x

例如 firstThirdFifthSeventh 原本对 Option α 和 Except String α 类型分别定义。现在，它可以被定义为对任何单子都有效的多态函数。但是，它需要接受一个参数作为查找函数，因为不同的单子可能以不同的方式找不到结果。bind 的中缀运算符是 >>=，它扮演与示例中 ~~> 相同的角色。

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
  lookup xs 0 >>= fun first =>
  lookup xs 2 >>= fun third =>
  lookup xs 4 >>= fun fifth =>
  lookup xs 6 >>= fun seventh =>
  pure (first, third, fifth, seventh)

给定作为示例的 slowMammals 和 fastBirds 列表，该 firstThirdFifthSeventh 实现可与 Option 一起使用：

def slowMammals : List String :=
  ["Three-toed sloth", "Slow loris"]

def fastBirds : List String := [
  "Peregrine falcon",
  "Saker falcon",
  "Golden eagle",
  "Gray-headed albatross",
  "Spur-winged goose",
  "Swift",
  "Anna's hummingbird"
]

#eval firstThirdFifthSeventh (fun xs i => xs[i]?) slowMammals

none

#eval firstThirdFifthSeventh (fun xs i => xs[i]?) fastBirds

some ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

在将 Except 的查找函数 get 重命名为更具体的形式后，完全相同的 firstThirdFifthSeventh 实现也可以与 Except 一起使用：

def getOrExcept (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => Except.ok x

#eval firstThirdFifthSeventh getOrExcept slowMammals

Except.error "Index 2 not found (maximum is 1)"

#eval firstThirdFifthSeventh getOrExcept fastBirds

Except.ok ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

m 必须有 Monad 实例，这一事实意味着可以使用 >>= 和 pure 运算符。

通用的单子运算符

由于许多不同类型都是单子，因此对任何单子多态的函数非常强大。例如，函数 mapM 是 map 的另一个版本，它使用 Monad 将函数调用的结果按顺序连接起来：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM f xs >>= fun tl =>
    pure (hd :: tl)

函数参数 f 的返回类型决定了将使用哪个 Monad 实例。换句话说，mapM 可用于生成日志的函数、可能失败的函数、或使用可变状态的函数。由于 f 的类型直接决定了可用的效应 (Effects)，因此 API 设计人员可以对其进行严格控制。译者注：效应 (Effects) 是函数式编程中与 Monad 密切相关的主题，实际上对效应的控制比此处原文所述更复杂一些，但超出了本文的内容。另外副作用 (Side Effects) 也是一种效应。

As described in this chapter’s introduction, State σ α represents programs that make use of a mutable variable of type σ and return a value of type α. These programs are actually functions from a starting state to a pair of a value and a final state. The Monad class requires that its parameter expect a single type argument—that is, it should be a Type → Type. This means that the instance for State should mention the state type σ, which becomes a parameter to the instance:

如本章简介所介绍的，State σ α 表示使用类型为 σ 的可变变量，并返回类型为 α 的值的程序。这些程序实际上是从起始状态到值和最终状态构成的对 (pair) 的函数。Monad 类型类要求：类型参数期望另一个类型参数，即它应该是 Type → Type。这意味着 State 的实例应提及状态类型 σ，使它成为实例的参数：

instance : Monad (State σ) where
  pure x := fun s => (s, x)
  bind first next :=
    fun s =>
      let (s', x) := first s
      next x s'

这意味着在使用 bind 对 get 和 set 排序时，状态的类型不能更改，这是具有状态的计算的合理规则。运算符 increment 将保存的状态增加一定量，并返回原值：

def increment (howMuch : Int) : State Int Int :=
  get >>= fun i =>
  set (i + howMuch) >>= fun () =>
  pure i

将 mapM 和 increment 一起使用会得到一个计算列表元素累加和的程序。更具体地说，可变变量包含到目前为止的和，而作为结果的列表包含各个步骤前状态变量的值。换句话说，mapM increment 的类型为 List Int → State Int (List Int)，展开 State 的定义得到 List Int → Int → (Int × List Int)。它将初始值作为参数，应为 0：

1
2
3

#eval mapM increment [1, 2, 3, 4, 5] 0

(15, [0, 1, 3, 6, 10])

A logging effect can be represented using WithLog. Just like State, its Monad instance is polymorphic with respect to the type of the logged data:

可以使用 WithLog 表示日志记录效应。就和 State 一样，它的 Monad 实例对于被记录数据的类型也是多态的：

instance : Monad (WithLog logged) where
  pure x := {log := [], val := x}
  bind result next :=
    let {log := thisOut, val := thisRes} := result
    let {log := nextOut, val := nextRes} := next thisRes
    {log := thisOut ++ nextOut, val := nextRes}

saveIfEven is a function that logs even numbers but returns its argument unchanged:

saveIfEven函数记录偶数，但将参数原封不动返回：

def saveIfEven (i : Int) : WithLog Int Int :=
  (if isEven i then
    save i
   else pure ()) >>= fun () =>
  pure i

Using this function with mapM results in a log containing even numbers paired with an unchanged input list:

将 mapM 和该函数一起使用，会生成一个记录偶数的日志、和未更改的输入列表：

#eval mapM saveIfEven [1, 2, 3, 4, 5]



{ log := [2, 4], val := [1, 2, 3, 4, 5] }

The Identity Monad

恒等单子

Monads encode programs with effects, such as failure, exceptions, or logging, into explicit representations as data and functions. Sometimes, however, an API will be written to use a monad for flexibility, but the API’s client may not require any encoded effects. The identity monad is a monad that has no effects, and allows pure code to be used with monadic APIs:

单子将具有效应(Effects)的程序（例如失败、异常或日志记录）编码为数据和函数的显式表示。有时API会使用单子来提高灵活性，但API的使用方可能不需要任何效应。 恒等单子 (Identity Monad)是一个没有任何效应的单子，允许将纯(pure)代码与monadic API一起使用：

def Id (t : Type) : Type := t

instance : Monad Id where
  pure x := x
  bind x f := f x

The type of pure should be α → Id α, but Id α reduces to just α. Similarly, the type of bind should be α → (α → Id β) → Id β. Because this reduces to α → (α → β) → β, the second argument can be applied to the first to find the result.

pure的类型应为 α → Id α，但Id α 归约为 α。类似地，bind 的类型应为α → (α → Id β) → Id β。由于这归约为 α → (α → β) → β，因此可以将第二个参数应用于第一个参数得到结果。 译者注：此处归约一词原文为reduces to，实际含义为beta-reduction，请见类型论相关资料。

With the identity monad, mapM becomes equivalent to map. To call it this way, however, Lean requires a hint that the intended monad is Id:

"使用恒等单子时，mapM等同于map。但是要以这种方式调用它，Lean需要额外的提示来表明目标单子是Id：

#eval mapM (m := Id) (· + 1) [1, 2, 3, 4, 5]



[2, 3, 4, 5, 6]

Omitting the hint results in an error:

省略提示则会导致错误：

#eval mapM (· + 1) [1, 2, 3, 4, 5]

1 2	failed to synthesize instance HAdd Nat Nat (?m.9063 ?m.9065)

In this error, the application of one metavariable to another indicates that Lean doesn’t run the type-level computation backwards. The return type of the function is expected to be the monad applied to some other type. Similarly, using mapM with a function whose type doesn’t provide any specific hints about which monad is to be used results in an “instance problem stuck” message:

导致错误的原因是：一个元变量应用于另一个元变量，使得Lean不会反向运行类型计算。函数的返回类型应该是应用于其他类型参数的单子。类似地，将 mapM 和未提供任何特定单子类型信息的函数一起使用，会导致"instance problem stuck"错误：

#eval mapM (fun x => x) [1, 2, 3, 4, 5]



typeclass instance problem is stuck, it is often due to metavariables
  Monad ?m.9063

The Monad Contract

单子约定

Just as every pair of instances of BEq and Hashable should ensure that any two equal values have the same hash, there is a contract that each instance of Monad should obey. First, pure should be a left identity of bind. That is, bind (pure v) f should be the same as f v. Secondly, pure should be a right identity of bind, so bind v pure is the same as v. Finally, bind should be associative, so bind (bind v f) g is the same as bind v (fun x => bind (f x) g).

正如 BEq 和 Hashable 的每一对实例都应该确保任何两个相等的值具有相同的哈希值，有一些是固有的约定是每个 Monad 的实例都应遵守的。首先，pure应为 bind 的左单位元，即 bind (pure v) f 应与 f v 等价。其次，pure应为 bind 的右单位元，即 bind v pure 应与 v 等价。最后，bind应满足结合律，即 bind (bind v f) g 应与 bind v (fun x => bind (f x) g) 等价。

This contract specifies the expected properties of programs with effects more generally. Because pure has no effects, sequencing its effects with bind shouldn’t change the result. The associative property of bind basically says that the sequencing bookkeeping itself doesn’t matter, so long as the order in which things are happening is preserved.

这些约定保证了具有效应的程序的预期属性。由于 pure 不导致效应，因此用 bind 将其与其他效应接连执行不应改变结果。 bind满足的结合律则意味着先计算哪一部分无关紧要，只要保证效应的顺序不变即可。

Exercises

练习

Mapping on a Tree

映射一棵树

Define a function BinTree.mapM. By analogy to mapM for lists, this function should apply a monadic function to each data entry in a tree, as a preorder traversal. The type signature should be:

定义函数BinTree.mapM。通过类比列表的mapM，此函数应将单子函数应用于树中的每个节点，作为前序遍历。类型签名应为：

1	def BinTree.mapM [Monad m] (f : α → m β) : BinTree α → m (BinTree β)

The Option Monad Contract

Option单子的约定

First, write a convincing argument that the Monad instance for Option satisfies the monad contract. Then, consider the following instance:

首先充分论证 Option 的 Monad 实例满足单子约定。然后，考虑以下实例：

1
2
3

instance : Monad Option where
  pure x := some x
  bind opt next := none

Both methods have the correct type. Why does this instance violate the monad contract?

这两个方法都有正确的类型。但这个实例却违反了单子约定，为什么？

Example: Arithmetic in Monads

例子：利用单子实现算术表达式求值

Monads are a way of encoding programs with side effects into a language that does not have them. It would be easy to read this as a sort of admission that pure functional programs are missing something important, requiring programmers to jump through hoops just to write a normal program. However, while using the Monad API does impose a syntactic cost on a program, it brings two important benefits: 1. Programs must be honest about which effects they use in their types. A quick glance at a type signature describes everything that the program can do, rather than just what it accepts and what it returns. 2. Not every language provides the same effects. For example, only some language have exceptions. Other languages have unique, exotic effects, such as Icon’s searching over multiple values and Scheme or Ruby’s continuations. Because monads can encode any effect, programmers can choose which ones are the best fit for a given application, rather than being stuck with what the language developers provided.

单子是一种将具有副作用的程序编入没有副作用的语言中的范式。但很容易将此误解为：承认纯函数式编程缺少一些重要的东西，程序员要越过这些障碍才能编写一个普通的程序。虽然使用 Monad 确实给程序带来了语法上的成本，但它带来了两个重要的优点：

程序必须在类型中诚实地告知它们使用的作用（Effects）。因此看一眼类型签名就可以知道程序能做的所有事情，而不只是知道它接受什么和返回什么。
并非每种语言都提供相同的作用。例如只有某些语言有异常。其他语言具有独特的新奇作用，例如 Icon’s searching over multiple values以及Scheme 或Ruby的continuations。由于单子可以编码任何作用，因此程序员可以选择最适合给定程序的作用，而不是局限于语言开发者提供的作用。

One example of a program that can make sense in a variety of monads is an evaluator for arithmetic expressions.

对许多单子都有意义的一个例子是算术表达式的求值器。

Arithmetic Expressions

算术表达式

An arithmetic expression is either a literal integer or a primitive binary operator applied to two expressions. The operators are addition, subtraction, multiplication, and division:

一条算术表达式要么是一个字面量(Literal)，要么是应用于两个算术表达式的二元运算。运算符包括加法、减法、乘法和除法：

inductive Expr (op : Type) where
  | const : Int → Expr op
  | prim : op → Expr op → Expr op → Expr op


inductive Arith where
  | plus
  | minus
  | times
  | div

The expression 2 + 3 is represented:

表达式 2 + 3 表示为：

open Expr in
open Arith in
def twoPlusThree : Expr Arith :=
  prim plus (const 2) (const 3)

and 14 / (45 - 5 * 9) is represented:

而 14 / (45 - 5 * 9) 表示为：

open Expr in
open Arith in
def fourteenDivided : Expr Arith :=
  prim div (const 14) (prim minus (const 45) (prim times (const 5) (const 9)))

Evaluating Expressions

对表达式求值

Because expressions include division, and division by zero is undefined, evaluation might fail. One way to represent failure is to use Option:

由于表达式包含除法，而除以零是未定义的，因此求值可能会失败。表示失败的一种方法是使用 Option：

def evaluateOption : Expr Arith → Option Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateOption e1 >>= fun v1 =>
    evaluateOption e2 >>= fun v2 =>
    match p with
    | Arith.plus => pure (v1 + v2)
    | Arith.minus => pure (v1 - v2)
    | Arith.times => pure (v1 * v2)
    | Arith.div => if v2 == 0 then none else pure (v1 / v2)

This definition uses the Monad Option instance to propagate failures from evaluating both branches of a binary operator. However, the function mixes two concerns: evaluating subexpressions and applying a binary operator to the results. It can be improved by splitting it into two functions:

此定义使用 Monad Option 实例，来传播从二元运算符的两个分支求值产生的失败。然而该函数混合了两个问题：对子表达式的求值和对运算符的计算。可以将其拆分为两个函数：

def applyPrim : Arith → Int → Int → Option Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y => if y == 0 then none else pure (x / y)

def evaluateOption : Expr Arith → Option Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateOption e1 >>= fun v1 =>
    evaluateOption e2 >>= fun v2 =>
    applyPrim p v1 v2

Running #eval evaluateOption fourteenDivided yields none, as expected, but this is not a very useful error message. Because the code was written using >>= rather than by explicitly handling the none constructor, only a small modification is required for it to provide an error message on failure:

运行 #eval evaluateOption fourteenDivided 产生 none, 与预期一样, 但这个报错信息却并不十分有用. 由于代码使用 >>= 而非显式处理none，所以只需少量修改即可在失败时提供错误消息：

def applyPrim : Arith → Int → Int → Except String Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)


def evaluateExcept : Expr Arith → Except String Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateExcept e1 >>= fun v1 =>
    evaluateExcept e2 >>= fun v2 =>
    applyPrim p v1 v2

The only difference is that the type signature mentions Except String instead of Option, and the failing case uses Except.error instead of none. By making evaluate polymorphic over its monad and passing it applyPrim as an argument, a single evaluator becomes capable of both forms of error reporting:

唯一区别是：类型签名提到的是 Except String 而非 Option，并且失败时使用 Except.error 而不是 none。通过让 evaluate 对单子多态，并将对应的求值函数作为参数 applyPrim 传递，单个求值器就足够以两种形式报告错误：

def applyPrimOption : Arith → Int → Int → Option Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then
      none
    else pure (x / y)

def applyPrimExcept : Arith → Int → Int → Except String Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y =>
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def evaluateM [Monad m] (applyPrim : Arith → Int → Int → m Int): Expr Arith → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applyPrim e1 >>= fun v1 =>
    evaluateM applyPrim e2 >>= fun v2 =>
    applyPrim p v1 v2

Using it with applyPrimOption works just like the first version of evaluate:

将其与 applyPrimOption 一起使用作用就和最初的 evaluate 一样：

#eval evaluateM applyPrimOption fourteenDivided



none

Similarly, using it with applyPrimExcept works just like the version with error messages:

类似地，和 applyPrimExcept 函数一起使用时作用与带有错误消息的版本相同：

#eval evaluateM applyPrimExcept fourteenDivided



Except.error "Tried to divide 14 by zero"

The code can still be improved. The functions applyPrimOption and applyPrimExcept differ only in their treatment of division, which can be extracted into another parameter to the evaluator:

代码仍有改进空间。 applyPrimOption和 applyPrimExcept 函数仅在除法处理上有所不同，因此可以将它提取到另一个参数中：

def applyDivOption (x : Int) (y : Int) : Option Int :=
    if y == 0 then
      none
    else pure (x / y)

def applyDivExcept (x : Int) (y : Int) : Except String Int :=
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def applyPrim [Monad m] (applyDiv : Int → Int → m Int) : Arith → Int → Int → m Int
  | Arith.plus, x, y => pure (x + y)
  | Arith.minus, x, y => pure (x - y)
  | Arith.times, x, y => pure (x * y)
  | Arith.div, x, y => applyDiv x y

def evaluateM [Monad m] (applyDiv : Int → Int → m Int): Expr Arith → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applyDiv e1 >>= fun v1 =>
    evaluateM applyDiv e2 >>= fun v2 =>
    applyPrim applyDiv p v1 v2

In this refactored code, the fact that the two code paths differ only in their treatment of failure has been made fully apparent.

在重构后的代码中，两条路径仅在对失败情况的处理上有所不同，这一事实显而易见。

Further Effects

额外的作用

Failure and exceptions are not the only kinds of effects that can be interesting when working with an evaluator. While division’s only side effect is failure, adding other primitive operators to the expressions make it possible to express other effects.

在考虑求值器时，失败和异常并不是唯一值得在意的作用。虽然除法的唯一副作用是失败，但若要增加其他运算符的支持，则可能需要表达对应的作用。

The first step is an additional refactoring, extracting division from the datatype of primitives:

第一步是重构，从原始数据类型中提取除法：

inductive Prim (special : Type) where
  | plus
  | minus
  | times
  | other : special → Prim special

inductive CanFail where
  | div

The name CanFail suggests that the effect introduced by division is potential failure.

名称 CanFail 表明被除法引入的作用是可能发生的失败。

The second step is to broaden the scope of the division handler argument to evaluateM so that it can process any special operator:

第二步是将 evaluateM 的作为除法计算的参数扩展，以便它可以处理任何特殊运算符：

def divOption : CanFail → Int → Int → Option Int
  | CanFail.div, x, y => if y == 0 then none else pure (x / y)

def divExcept : CanFail → Int → Int → Except String Int
  | CanFail.div, x, y =>
    if y == 0 then

      Except.error s!"Tried to divide {x} by zero"
    else pure (x / y)

def applyPrim [Monad m] (applySpecial : special → Int → Int → m Int) : Prim special → Int → Int → m Int
  | Prim.plus, x, y => pure (x + y)
  | Prim.minus, x, y => pure (x - y)
  | Prim.times, x, y => pure (x * y)
  | Prim.other op, x, y => applySpecial op x y

def evaluateM [Monad m] (applySpecial : special → Int → Int → m Int): Expr (Prim special) → m Int
  | Expr.const i => pure i
  | Expr.prim p e1 e2 =>
    evaluateM applySpecial e1 >>= fun v1 =>
    evaluateM applySpecial e2 >>= fun v2 =>
    applyPrim applySpecial p v1 v2

No Effects

无作用

The type Empty has no constructors, and thus no values, like the Nothing type in Scala or Kotlin. In Scala and Kotlin, Nothing can represent computations that never return a result, such as functions that crash the program, throw exceptions, or always fall into infinite loops. An argument to a function or method of type Nothing indicates dead code, as there will never be a suitable argument value. Lean doesn’t support infinite loops and exceptions, but Empty is still useful as an indication to the type system that a function cannot be called. Using the syntax nomatch E when E is an expression whose type has no constructors indicates to Lean that the current expression need not return a result, because it could never have been called.

Empty类型没有构造子，因此没有任何取值，就像Scala或Kotlin中的 Nothing 类型。在Scala和Kotlin中，返回类型为 Nothing 表示永不返回结果的计算，例如导致程序崩溃、或引发异常、或陷入无限循环的函数。参数类型为 Nothing 表示函数是死代码，因为我们永远无法构造出合适的参数值来调用它。 Lean 不支持无限循环和异常，但 Empty 仍然可作为向类型系统说明函数不可被调用的标志。当 E 是一条表达式，但它的类型没有任何取值时，使用 nomatch E 向Lean说明当前表达式不返回结果，因为它永远不会被调用。

Using Empty as the parameter to Prim indicates that there are no additional cases beyond Prim.plus, Prim.minus, and Prim.times, because it is impossible to come up with a value of type Empty to place in the Prim.other constructor. Because a function to apply an operator of type Empty to two integers can never be called, it doesn’t need to return a result. Thus, it can be used in any monad:

将 Empty 用作 Prim 的参数，表示除了 Prim.plus、Prim.minus 和 Prim.times 之外没有其他情况，因为不可能找到一个 Empty 类型的值来放在 Prim.other 构造子中。由于类型为 Empty 的运算符应用于两个整数的函数永远不会被调用，所以它不需要返回结果。因此，它可以在任何单子中使用：

1 2	def applyEmpty [Monad m] (op : Empty) (_ : Int) (_ : Int) : m Int := nomatch op

This can be used together with Id, the identity monad, to evaluate expressions that have no effects whatsoever:

这可以与恒等单子 Id 一起使用，用来计算没有任何副作用的表达式：

open Expr Prim in
#eval evaluateM (m := Id) applyEmpty (prim plus (const 5) (const (-14)))



-9

Nondeterministic Search

非确定性搜索

Instead of simply failing when encountering division by zero, it would also be sensible to backtrack and try a different input. Given the right monad, the very same evaluateM can perform a nondeterministic search for a set of answers that do not result in failure. This requires, in addition to division, some means of specifying a choice of results. One way to do this is to add a function choose to the language of expressions that instructs the evaluator to pick either of its arguments while searching for non-failing results.

遇到除以零时，除了直接失败并结束之外，还可以回溯并尝试不同的输入。给定适当的单子，同一个 evaluateM 可以对不致失败的答案集合执行非确定性搜索。这要求除了除法之外，还需要指定选择结果的方式。一种方法是在表达式的语言中添加一个函数choose，告诉求值器在搜索非失败结果时选择其中一个参数。

The result of the evaluator is now a multiset of values, rather than a single value. The rules for evaluation into a multiset are: * Constants $ n $ evaluate to singleton sets $ \{n\} $. * Arithmetic operators other than division are called on each pair from the Cartesian product of the operators, so $ X + Y $ evaluates to $ \\{ x + y \\mid x ∈ X, y ∈ Y \\} $. * Division $ X / Y $ evaluates to $ \\{ x / y \\mid x ∈ X, y ∈ Y, y ≠ 0\\} $. In other words, all $ 0 $ values in $ Y $ are thrown out. * A choice $ \\mathrm{choose}(x, y) $ evaluates to $ \\{ x, y \\} $.

求值结果现在变成一个多重集合(multiset)，而不是一个单一值求值到多重集合的规则如下：

常量 ( n ) 求值为单元素集合 ( {n} )。
除法以外的算术运算符作用于两个参数的笛卡尔积中的每一对，所以 ( X + Y ) 求值为 ( \{ x + y \mid x ∈ X, y ∈ Y \} )。
除法 ( X / Y ) 求值为 ( \{ x / y \mid x ∈ X, y ∈ Y, y ≠ 0\} ). 换句话说，所有 ( Y ) 中的 ( 0 ) 都被丢弃。
选择 ( \mathrm{choose}(x, y) ) 求值为 ( \{ x, y \} )。

For example, $ 1 + \\mathrm{choose}(2, 5) $ evaluates to $ \\{ 3, 6 \\} $, $1 + 2 / 0 $ evaluates to $ \\{\\} $, and $ 90 / (\\mathrm{choose}(-5, 5) + 5) $ evaluates to $ \\{ 9 \\} $. Using multisets instead of true sets simplifies the code by removing the need to check for uniqueness of elements.

例如， ( 1 + \mathrm{choose}(2, 5) ) 求值为 ( \{ 3, 6 \} )， (1 + 2 / 0 ) 求值为 ( \{\} )，并且 ( 90 / (\mathrm{choose}(-5, 5) + 5) ) 求值为 ( \{ 9 \} )。使用多重集合而非集合，是为了避免处理元素重复的情况而使代码过于复杂。

A monad that represents this non-deterministic effect must be able to represent a situation in which there are no answers, and a situation in which there is at least one answer together with any remaining answers:

表示这种非确定性作用的单子必须能够处理没有答案的情况，以及至少有一个答案和其他答案的情况：

1
2
3

inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

This datatype looks very much like List. The difference is that where cons stores the rest of the list, more stores a function that should compute the next value on demand. This means that a consumer of Many can stop the search when some number of results have been found.

该数据类型看起来非常像List。不同之处在于，cons存储列表的其余部分，而 more 存储一个函数，该函数仅在需要时才会被调用来计算下一个值。这意味着 Many 的使用者可以在找到一定数量的结果后停止搜索。

A single result is represented by a more constructor that returns no further results:

单个结果由 more 构造子表示，该构造子不返回任何进一步的结果：

1	def Many.one (x : α) : Many α := Many.more x (fun () => Many.none)

The union of two multisets of results can be computed by checking whether the first multiset is empty. If so, the second multiset is the union. If not, the union consists of the first element of the first multiset followed by the union of the rest of the first multiset with the second multiset:

两个作为结果的多重集合的并集，可以通过检查第一个是否为空来计算。如果第一个为空则第二个多重集合就是并集。如果非空，则并集由第一个多重集合的第一个元素，紧跟着其余部分与第二个多重集的并集：

1
2
3

def Many.union : Many α → Many α → Many α
  | Many.none, ys => ys
  | Many.more x xs, ys => Many.more x (fun () => union (xs ()) ys)

It can be convenient to start a search process with a list of values. Many.fromList converts a list into a multiset of results:

对值列表搜索会比手动构造多重集合更方便。函数 Many.fromList 将列表转换为结果的多重集合：

1
2
3

def Many.fromList : List α → Many α
  | [] => Many.none
  | x :: xs => Many.more x (fun () => fromList xs)

Similarly, once a search has been specified, it can be convenient to extract either a number of values, or all the values:

类似地，一旦搜索已经确定，就可以方便地提取固定数量的值或所有值：

def Many.take : Nat → Many α → List α
  | 0, _ => []
  | _ + 1, Many.none => []
  | n + 1, Many.more x xs => x :: (xs ()).take n

def Many.takeAll : Many α → List α
  | Many.none => []
  | Many.more x xs => x :: (xs ()).takeAll

A Monad Many instance requires a bind operator. In a nondeterministic search, sequencing two operations consists of taking all possibilities from the first step and running the rest of the program on each of them, taking the union of the results. In other words, if the first step returns three possible answers, the second step needs to be tried for all three. Because the second step can return any number of answers for each input, taking their union represents the entire search space.

Monad Many实例需要一个 bind 运算符。在非确定性搜索中，对两个操作进行排序包括：从第一步中获取所有可能性，并对每种可能性都运行程序的其余部分，取结果的并集。换句话说，如果第一步返回三个可能的答案，则需要对这三个答案分别尝试第二步。由于第二步为每个输入都可以返回任意数量的答案，因此取它们的并集表示整个搜索空间。

def Many.bind : Many α → (α → Many β) → Many β
  | Many.none, _ =>
    Many.none
  | Many.more x xs, f =>
    (f x).union (bind (xs ()) f)

Many.one and Many.bind obey the monad contract. To check that Many.bind (Many.one v) f is the same as f v, start by evaluating the expression as far as possible:

Many.one和 Many.bind 遵循单子约定。要检查 Many.bind (Many.one v) f 是否与 f v 相同，首先应最大限度地计算表达式：

Many.bind (Many.one v) f
===>
Many.bind (Many.more v (fun () => Many.none)) f
===>
(f v).union (Many.bind Many.none f)
===>
(f v).union Many.none

The empty multiset is a right identity of union, so the answer is equivalent to f v. To check that Many.bind v Many.one is the same as v, consider that bind takes the union of applying Many.one to each element of v. In other words, if v has the form {v1, v2, v3, ..., vn}, then Many.bind v Many.one is {v1} ∪ {v2} ∪ {v3} ∪ ... ∪ {vn}, which is {v1, v2, v3, ..., vn}.

空集是 union 的右单位元，因此答案等同于f v。要检查 Many.bind v Many.one 是否与 v 相同，需要考虑 Many.one 应用于 v 的各元素结果的并集。换句话说，如果 v 的形式为 {v1, v2, v3, ..., vn}，则Many.bind v Many.one 为{v1} ∪ {v2} ∪ {v3} ∪ ... ∪ {vn}，即{v1, v2, v3, ..., vn}。

Finally, to check that Many.bind is associative, check that Many.bind (Many.bind bind v f) g is the same as Many.bind v (fun x => Many.bind (f x) g). If v has the form {v1, v2, v3, ..., vn}, then:

最后，要检查 Many.bind 是否满足结合律，需要检查 Many.bind (Many.bind bind v f) g 是否与 Many.bind v (fun x => Many.bind (f x) g) 相同。如果 v 的形式为{v1, v2, v3, ..., vn}，则：

1
2
3

Many.bind v f
===>
f v1 ∪ f v2 ∪ f v3 ∪ ... ∪ f vn

which means that

Many.bind (Many.bind bind v f) g
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g

Similarly,

与此类似，

Many.bind v (fun x => Many.bind (f x) g)
===>
(fun x => Many.bind (f x) g) v1 ∪
(fun x => Many.bind (f x) g) v2 ∪
(fun x => Many.bind (f x) g) v3 ∪
... ∪
(fun x => Many.bind (f x) g) vn
===>
Many.bind (f v1) g ∪
Many.bind (f v2) g ∪
Many.bind (f v3) g ∪
... ∪
Many.bind (f vn) g

Thus, both sides are equal, so Many.bind is associative.

因此两边相等，所以 Many.bind 满足结合律。

由此得到的单子实例为：

1
2
3

instance : Monad Many where
  pure := Many.one
  bind := Many.bind

An example search using this monad finds all the combinations of numbers in a list that add to 15:

利用此单子，下例可找到列表中所有加起来等于15的数字组合：

def addsTo (goal : Nat) : List Nat → Many (List Nat)
  | [] =>
    if goal == 0 then
      pure []
    else
      Many.none
  | x :: xs =>
    if x > goal then
      addsTo goal xs
    else
      (addsTo goal xs).union
        (addsTo (goal - x) xs >>= fun answer =>
         pure (x :: answer))

The search process is recursive over the list. The empty list is a successful search when the goal is 0; otherwise, it fails. When the list is non-empty, there are two possibilities: either the head of the list is greater than the goal, in which case it cannot participate in any successful searches, or it is not, in which case it can. If the head of the list is not a candidate, then the search proceeds to the tail of the list. If the head is a candidate, then there are two possibilities to be combined with Many.union: either the solutions found contain the head, or they do not. The solutions that do not contain the head are found with a recursive call on the tail, while the solutions that do contain it result from subtracting the head from the goal, and then attaching the head to the solutions that result from the recursive call.

(译者注：这是一个动态规划算法)对列表进行递归搜索。当输入列表为空且目标为 0 时，返回空列表表示成功；否则返回 Many.none 表示失败，因为空输入不可能得到非0加和。当列表非空时，有两种可能性：若输入列表的第一个元素大于goal，此时它的任何加和都大于 0 因此不可能是候选者；若第一个元素不大于goal，可以参与后续的搜索。如果列表的头部x 不是候选者，对列表的尾部xs递归搜索。如果头部是候选者，则有两种用 Many.union 合并起来的可能性：找到的解含有当前的x，或者不含有。不含x的解通过xs递归搜索找到；而含有x的解则通过从goal中减去x，然后将x附加到递归的解中得到。

Returning to the arithmetic evaluator that produces multisets of results, the both and neither operators can be written as follows:

让我们回到产生多重集合的算术求值器，both和 neither 运算符可以写成如下形式：

inductive NeedsSearch
  | div
  | choose

def applySearch : NeedsSearch → Int → Int → Many Int
  | NeedsSearch.choose, x, y =>
    Many.fromList [x, y]
  | NeedsSearch.div, x, y =>
    if y == 0 then
      Many.none
    else Many.one (x / y)

Using these operators, the earlier examples can be evaluated:

可以用这些运算符对前面的示例求值：

open Expr Prim NeedsSearch

#eval (evaluateM applySearch (prim plus (const 1) (prim (other choose) (const 2) (const 5)))).takeAll



[3, 6]



#eval (evaluateM applySearch (prim plus (const 1) (prim (other div) (const 2) (const 0)))).takeAll



[]



#eval (evaluateM applySearch (prim (other div) (const 90) (prim plus (prim (other choose) (const (-5)) (const 5)) (const 5)))).takeAll



[9]

Custom Environments

自定义环境

The evaluator can be made user-extensible by allowing strings to be used as operators, and then providing a mapping from strings to a function that implements them. For example, users could extend the evaluator with a remainder operator or with one that returns the maximum of its two arguments. The mapping from function names to function implementations is called an environment.

可以通过允许将字符串当作运算符，然后提供从字符串到它们的实现函数之间的映射，使求值器可由用户扩展。例如，用户可以用余数运算或最大值运算来扩展求值器。从函数名称到函数实现的映射称为环境。

The environments needs to be passed in each recursive call. Initially, it might seem that evaluateM needs an extra argument to hold the environment, and that this argument should be passed to each recursive invocation. However, passing an argument like this is another form of monad, so an appropriate Monad instance allows the evaluator to be used unchanged.

环境需要在每层递归调用之间传递。因此一开始 evaluateM 看起来需要一个额外的参数来保存环境，并且该参数需要在每次递归调用时传递。然而，像这样传递参数是单子的另一种形式，因此一个适当的 Monad 实例允许求值器本身保持不变。

Using functions as a monad is typically called a reader monad. When evaluating expressions in the reader monad, the following rules are used: * Constants $ n $ evaluate to constant functions $ λ e . n $, * Arithmetic operators evaluate to functions that pass their arguments on, so $ f + g $ evaluates to $ λ e . f(e) + g(e) $, and * Custom operators evaluate to the result of applying the custom operator to the arguments, so $ f \\ \\mathrm{OP}\\ g $ evaluates to \[ λ e . \\begin{cases} h(f(e), g(e)) & \\mathrm{if}\\ e\\ \\mathrm{contains}\\ (\\mathrm{OP}, h) \\\\ 0 & \\mathrm{otherwise} \\end{cases} \] with $ 0 $ serving as a fallback in case an unknown operator is applied.

将函数当作单子，这通常称为 reader 单子。在reader单子中对表达式求值使用以下规则：

常量 ( n ) 映射为常量函数 ( λ e . n )，
算术运算符映射为将参数各自传递然后计算的函数，因此 ( f + g ) 映射为 ( λ e . f(e) + g(e) )，并且
自定义运算符求值为将自定义运算符应用于参数的结果，因此 ( f \ \mathrm{OP}\ g ) 映射为 [ λ e . \begin{cases} h(f(e), g(e)) & \mathrm{if}\ e\ \mathrm{contains}\ (\mathrm{OP}, h) \\ 0 & \mathrm{otherwise} \end{cases} ] 其中 ( 0 ) 用于运算符未知的情况。

To define the reader monad in Lean, the first step is to define the Reader type and the effect that allows users to get ahold of the environment:

要在Lean中定义reader单子，第一步是定义 Reader 类型，和用户获取环境的作用：

1
2
3

def Reader (ρ : Type) (α : Type) : Type := ρ → α

def read : Reader ρ ρ := fun env => env

By convention, the Greek letter ρ, which is pronounced “rho”, is used for environments.

按照惯例，希腊字母ρ（发音为“rho”）用于表示环境。

The fact that constants in arithmetic expressions evaluate to constant functions suggests that the appropriate definition of pure for Reader is a a constant function:

算术表达式中的常量映射为常量函数这一事实表明，Reader的 pure 的适当定义是一个常量函数：

1	def Reader.pure (x : α) : Reader ρ α := fun _ => x

On the other hand, bind is a bit tricker. Its type is Reader ρ α → (α → Reader ρ β) → Reader ρ β. This type can be easier to understand by expanding the definitions of Reader, which yields (ρ → α) → (α → ρ → β) → ρ → β. It should take an environment-accepting function as its first argument, while the second argument should transform the result of the environment-accepting function into yet another environment-accepting function. The result of combining these is itself a function, waiting for an environment.

另一方面 bind 则有点棘手。它的类型是Reader ρ α → (α → Reader ρ β) → Reader ρ β。通过展开 Reader 的定义，可以更容易地理解此类型，从而产生(ρ → α) → (α → ρ → β) → ρ → β。它将读取环境的函数作为第一个参数，而第二个参数将第一个参数的结果转换为另一个读取环境的函数。组合这些结果本身就是一个读取环境的函数。

It’s possible to use Lean interactively to get help writing this function. The first step is to write down the arguments and return type, being very explicit in order to get as much help as possible, with an underscore for the definition’s body:

可以交互式地使用Lean，获得编写该函数的帮助。为了获得尽可能多的帮助，第一步是非常明确地写下参数的类型和返回的类型，用下划线表示定义的主体：

1
2
3

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  _

Lean provides a message that describes which variables are available in scope, and the type that’s expected for the result. The ⊢ symbol, called a turnstile due to its resemblance to subway entrances, separates the local variables from the desired type, which is ρ → β in this message:

Lean提供的消息描述了哪些变量在作用域内可用，以及结果的预期类型。 ⊢符号，由于它类似于地铁入口而被称为 turnstile ，将局部变量与所需类型分开，在此消息中为ρ → β：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β

⊢ ρ → β

Because the return type is a function, a good first step is to wrap a fun around the underscore:

因为返回类型是一个函数，所以第一步最好在下划线外套一层fun：

1
2
3

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => _

The resulting message now shows the function’s argument as a local variable:

产生的消息说明现在函数的参数已经成为一个局部变量：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ

⊢ β

The only thing in the context that can produce a β is next, and it will require two arguments to do so. Each argument can itself be an underscore:

上下文中唯一可以产生 β 的是 next，并且它需要两个参数。每个参数都可以用下划线表示：

1
2
3

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next _ _

The two underscores have the following respective messages associated with them:

这两个下划线分别有如下的消息：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ

⊢ α



don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ
⊢ ρ

Attacking the first underscore, only one thing in the context can produce an α, namely result:

先处理第一条下划线，注意到上下文中只有一个东西可以产生α，即result：

1
2
3

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result _) _

Now, both underscores have the same error:

现在两条下划线都有一样的报错了：

don't know how to synthesize placeholder
context:
ρ α β : Type
result : ρ → α
next : α → ρ → β
env : ρ

⊢ ρ

Happily, both underscores can be replaced by env, yielding:

值得高兴的是，两条下划线都可以被 env 替换，得到：

1
2
3

def Reader.bind {ρ : Type} {α : Type} {β : Type}
  (result : ρ → α) (next : α → ρ → β) : ρ → β :=
  fun env => next (result env) env

The final version can be obtained by undoing the expansion of Reader and cleaning up the explicit details:

要得到最后的版本，只需要把我们前面对 Reader 的展开撤销，并且去掉过于明确的细节：

1 2	def Reader.bind (result : Reader ρ α) (next : α → Reader ρ β) : Reader ρ β := fun env => next (result env) env

It’s not always possible to write correct functions by simply “following the types”, and it carries the risk of not understanding the resulting program. However, it can also be easier to understand a program that has been written than one that has not, and the process of filling in the underscores can bring insights. In this case, Reader.bind works just like bind for Id, except it accepts an additional argument that it then passes down to its arguments, and this intuition can help in understanding how it works.

仅仅跟着类型信息走并不总是能写出正确的函数，并且有未能完全理解产生的程序的风险。然而理解一个已经写出的程序比理解还没写出的要简单，而且逐步填充下划线的内容也可以提供思路。这张情况下，Reader.bind和 Id 的 bind 很像，唯一区别在于它接受一个额外的参数并传递到其他参数中。这个直觉可以帮助理解它的原理。

Reader.pure, which generates constant functions, and Reader.bind obey the monad contract. To check that Reader.bind (Reader.pure v) f is the same as f v, it’s enough to replace definitions until the last step:

Reader.pure和 Reader.bind 遵循单子约定。要检查 Reader.bind (Reader.pure v) f 与 f v 等价, 只需要不断地展开定义即可：

Reader.bind (Reader.pure v) f
===>
fun env => f ((Reader.pure v) env) env
===>
fun env => f ((fun _ => v) env) env
===>
fun env => f v env
===>
f v

For every function f, fun x => f x is the same as f, so the first part of the contract is satisfied. To check that Reader.bind r Reader.pure is the same as r, a similar technique works:

对任意函数 f 来说，fun x => f x和 f 是等价的，所以约定的第一部分已经满足。要检查 Reader.bind r Reader.pure 与 r 等价，只需要相似的技巧：

Reader.bind r Reader.pure
===>
fun env => Reader.pure (r env) env
===>
fun env => (fun _ => (r env)) env
===>
fun env => r env

Because reader actions r are themselves functions, this is the same as r. To check associativity, the same thing can be done for both Reader.bind (Reader.bind r f) g and Reader.bind r (fun x => Reader.bind (f x) g):

因为 r 本身是函数，所以这和 r 也是等价的。要检查结合律，只需要对 Reader.bind (Reader.bind r f) g 和 Reader.bind r (fun x => Reader.bind (f x) g) 重复同样的步骤：

Reader.bind (Reader.bind r f) g
===>
fun env => g ((Reader.bind r f) env) env
===>
fun env => g ((fun env' => f (r env') env') env) env
===>
fun env => g (f (r env) env) env



Reader.bind r (fun x => Reader.bind (f x) g)
===>
Reader.bind r (fun x => fun env => g (f x env) env)
===>
fun env => (fun x => fun env' => g (f x env') env') (r env) env
===>
fun env => (fun env' => g (f (r env) env') env') env
===>
fun env => g (f (r env) env) env

Thus, a Monad (Reader ρ) instance is justified:

至此，Monad (Reader ρ)实例已经得到了充分验证：

1
2
3

instance : Monad (Reader ρ) where
  pure x := fun _ => x
  bind x f := fun env => f (x env) env

The custom environments that will be passed to the expression evaluator can be represented as lists of pairs:

要被传递给表达式求值器的环境可以用键值对的列表来表示：

1	abbrev Env : Type := List (String × (Int → Int → Int))

For instance, exampleEnv contains maximum and modulus functions:

例如，exampleEnv包含最大值和模函数：

1	def exampleEnv : Env := [("max", max), ("mod", (· % ·))]

Lean already has a function List.lookup that finds the value associated with a key in a list of pairs, so applyPrimReader needs only check whether the custom function is present in the environment. It returns 0 if the function is unknown:

Lean已提供函数 List.lookup 用来在键值对的列表中根据键寻找对应的值，所以 applyPrimReader 只需要确认自定义函数是否存在于环境中即可。如果不存在则返回0：

def applyPrimReader (op : String) (x : Int) (y : Int) : Reader Env Int :=
  read >>= fun env =>
  match env.lookup op with
  | none => pure 0
  | some f => pure (f x y)

Using evaluateM with applyPrimReader and an expression results in a function that expects an environment. Luckily, exampleEnv is available:

将evaluateM、applyPrimReader、和一条表达式一起使用，即得到一个接受环境的函数。而我们前面已经准备好了exampleEnv：

open Expr Prim in
#eval evaluateM applyPrimReader (prim (other "max") (prim plus (const 5) (const 4)) (prim times (const 3) (const 2))) exampleEnv



9

Like Many, Reader is an example of an effect that is difficult to encode in most languages, but type classes and monads make it just as convenient as any other effect. The dynamic or special variables found in Common Lisp, Clojure, and Emacs Lisp can be used like Reader. Similarly, Scheme and Racket’s parameter objects are an effect that exactly correspond to Reader. The Kotlin idiom of context objects can solve a similar problem, but they are fundamentally a means of passing function arguments automatically, so this idiom is more like the encoding as a reader monad than it is an effect in the language.

与 Many 一样，Reader是难以在大多数语言中编码的作用，但类型类和单子使其与任何其他作用一样方便。 Common Lisp、Clojure和Emacs Lisp中的动态或特殊变量可以用作Reader。类似地，Scheme和Racket的参数对象是一个与 Reader 完全对应的作用。 Kotlin的上下文对象可以解决类似的问题，但根本上是一种自动传递函数参数的方式，因此更像是作为reader单子的编码，而不是语言中实现的作用。

Exercises

练习

Checking Contracts

检查约定

Check the monad contract for State σ and Except ε.

检查 State σ 和 Except ε 满足单子约定。

Readers with Failure

允许Reader失败

Adapt the reader monad example so that it can also indicate failure when the custom operator is not defined, rather than just returning zero. In other words, given these definitions:

调整例子中的reader单子，使得它可以在自定义的运算符不存在时提供错误信息而不是直接返回0。换句话说，给定这些定义：

1
2
3

def ReaderOption (ρ : Type) (α : Type) : Type := ρ → Option α

def ReaderExcept (ε : Type) (ρ : Type) (α : Type) : Type := ρ → Except ε α

do the following: 1. Write suitable pure and bind functions 2. Check that these functions satisfy the Monad contract 3. Write Monad instances for ReaderOption and ReaderExcept 4. Define suitable applyPrim operators and test them with evaluateM on some example expressions

要做的是：

实现恰当的 pure 和 bind 函数
验证这些函数满足 Monad 约定
为 ReaderOption 和 ReaderExcept 实现 Monad 实例
为它们定义恰当的 applyPrim 运算符，并且将它们和 evaluateM 一起测试一些例子

A Tracing Evaluator

带有跟踪信息的求值器

The WithLog type can be used with the evaluator to add optional tracing of some operations. In particular, the type ToTrace can serve as a signal to trace a given operator:

WithLog类型可以和求值器一起使用，来实现对某些运算的跟踪。特别地，可以使用 ToTrace 类型来追踪某个给定的运算符：

1 2	inductive ToTrace (α : Type) : Type where \| trace : α → ToTrace α

For the tracing evaluator, expressions should have type Expr (Prim (ToTrace (Prim Empty))). This says that the operators in the expression consist of addition, subtraction, and multiplication, augmented with traced versions of each. The innermost argument is Empty to signal that there are no further special operators inside of trace, only the three basic ones.

对于带有跟踪信息的求值器，表达式应该具有类型Expr (Prim (ToTrace (Prim Empty))). 这说明表达式中的运算符由附加参数的加、减、乘运算组成。最内层的参数是 Empty，说明在trace 内部没有特殊运算符，只有三种基本运算。

Do the following: 1. Implement a Monad (WithLog logged) instance 2. Write an applyTraced function to apply traced operators to their arguments, logging both the operator and the arguments, with type ToTrace (Prim Empty) → Int → Int → WithLog (Prim Empty × Int × Int) Int

要做的是：

实现 Monad (WithLog logged) 实例
写一个 applyTraced 来将被追踪的运算符应用到参数，将运算符和参数记录到日志，类型为：ToTrace (Prim Empty) → Int → Int → WithLog (Prim Empty × Int × Int) Int

If the exercise has been completed correctly, then

如果练习已经正确实现，那么

1 2	open Expr Prim ToTrace in #eval evaluateM applyTraced (prim (other (trace times)) (prim (other (trace plus)) (const 1) (const 2)) (prim (other (trace minus)) (const 3) (const 4)))

should result in

将有如下结果

1	{ log := [(Prim.plus, 1, 2), (Prim.minus, 3, 4), (Prim.times, 3, -1)], val := -3 }

Hint: values of type Prim Empty will appear in the resulting log. In order to display them as a result of #eval, the following instances are required:

提示：Prim Empty会出现在日志中。为了让它们能被 #eval 输出，需要下面几个实例：

1
2
3

 deriving instance Repr for WithLog
deriving instance Repr for Empty
deriving instance Repr for Prim

`do`-Notation for Monads

单子的 `do`-记法

While APIs based on monads are very powerful, the explicit use of >>= with anonymous functions is still somewhat noisy. Just as infix operators are used instead of explicit calls to HAdd.hAdd, Lean provides a syntax for monads called do-notation that can make programs that use monads easier to read and write. This is the very same do-notation that is used to write programs in IO, and IO is also a monad.

基于单子的 API 非常强大，但显式使用 >>= 和匿名函数仍然有些繁琐。正如使用中缀运算符代替显式调用 HAdd.hAdd 一样，Lean 提供了一种称为 do-记法 的单子语法，它可以使使用单子的程序更易于阅读和编写。这与用于编写 IO 程序的 do-记法完全相同，而 IO 也是一个单子。

In Hello, World!, the do syntax is used to combine IO actions, but the meaning of these programs is explained directly. Understanding how to program with monads means that do can now be explained in terms of how it translates into uses of the underlying monad operators.

在 Hello, World! 中，do 语法用于组合 IO 活动，但这些程序的含义是直接解释的。理解如何运用单子进行编程意味着现在可以用 do 来解释它如何转换为对底层单子运算符的使用。

The first translation of do is used when the only statement in the do is a single expression E. In this case, the do is removed, so

当 do 中的唯一语句是单个表达式 E 时，会使用 do 的第一种翻译。在这种情况下，do 被删除，因此

do E

会被翻译为

The second translation is used when the first statement of the do is a let with an arrow, binding a local variable. This translates to a use of >>= together with a function that binds that very same variable, so

当 do 的第一个语句是带有箭头的 let 绑定一个局部变量时，则使用第二种翻译。它会翻译为使用 >>= 以及绑定同一变量的函数，因此

do let x ← E1
   Stmt
   ...
   En

translates to

会被翻译为

E1 >>= fun x =>
do Stmt
   ...
   En

When the first statement of the do block is an expression, then it is considered to be a monadic action that returns Unit, so the function matches the Unit constructor and

当 do 块的第一个语句是一个表达式时，它会被认为是一个返回 Unit 的单子操作，因此该函数匹配 Unit 构造子，而

do E1
   Stmt
   ...
   En

translates to

会被翻译为

E1 >>= fun () =>
do Stmt
   ...
   En

Finally, when the first statement of the do block is a let that uses :=, the translated form is an ordinary let expression, so

最后，当 do 块的第一个语句是使用 := 的 let 时，翻译后的形式是一个普通的 let 表达式，因此

do let x := E1
   Stmt
   ...
   En

translates to

会被翻译为

let x := E1
do Stmt
   ...
   En

The definition of firstThirdFifthSeventh that uses the Monad class looks like this:

使用 Monad 类的 firstThirdFifthSeventh 的定义如下：

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) :=
  lookup xs 0 >>= fun first =>
  lookup xs 2 >>= fun third =>
  lookup xs 4 >>= fun fifth =>
  lookup xs 6 >>= fun seventh =>
  pure (first, third, fifth, seventh)

Using do-notation, it becomes significantly more readable:

使用 do-记法，它会变得更加易读：

def firstThirdFifthSeventh [Monad m] (lookup : List α → Nat → m α) (xs : List α) : m (α × α × α × α) := do
  let first ← lookup xs 0
  let third ← lookup xs 2
  let fifth ← lookup xs 4
  let seventh ← lookup xs 6
  pure (first, third, fifth, seventh)

Without the Monad type class, the function number that numbers the nodes of a tree was written:

若没有 Monad 类型，则对树的节点进行编号的函数 number 写作如下形式：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => ok BinTree.leaf
    | BinTree.branch left x right =>
      helper left ~~> fun numberedLeft =>
      get ~~> fun n =>
      set (n + 1) ~~> fun () =>
      helper right ~~> fun numberedRight =>
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

有了 Monad 和 do，其定义就简洁多了：

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => pure BinTree.leaf
    | BinTree.branch left x right => do
      let numberedLeft ← helper left
      let n ← get
      set (n + 1)
      let numberedRight ← helper right
      ok (BinTree.branch numberedLeft (n, x) numberedRight)
  (helper t 0).snd

使用 do 与 IO 的所有便利性在使用其他单子时也可用。例如，嵌套操作也适用于任何单子。mapM 的原始定义为：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM f xs >>= fun tl =>
    pure (hd :: tl)

With do-notation, it can be written:

使用 do-记法，可以写成：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs => do
    let hd ← f x
    let tl ← mapM f xs
    pure (hd :: tl)

Using nested actions makes it almost as short as the original non-monadic map:

使用嵌套活动会让它与原始非单子 map 一样简洁：

def mapM [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs => do
    pure ((← f x) :: (← mapM f xs))

Using nested actions, number can be made much more concise:

使用嵌套活动，number 可以变得更加简洁：

def increment : State Nat Nat := do
  let n ← get
  set (n + 1)
  pure n

def number (t : BinTree α) : BinTree (Nat × α) :=
  let rec helper : BinTree α → State Nat (BinTree (Nat × α))
    | BinTree.leaf => pure BinTree.leaf
    | BinTree.branch left x right => do
      pure (BinTree.branch (← helper left) ((← increment), x) (← helper right))
  (helper t 0).snd

Exercises

练习

Rewrite evaluateM, its helpers, and the different specific use cases using do-notation instead of explicit calls to >>=. * Rewrite firstThirdFifthSeventh using nested actions.
- 使用 do-记法而非显式调用 >>= 重写 evaluateM、辅助函数以及不同的特定用例。
- 使用嵌套操作重写 firstThirdFifthSeventh。

The IO Monad

IO 单子

IO as a monad can be understood from two perspectives, which were described in the section on running programs. Each can help to understand the meanings of pure and bind for IO.

IO 作为单子可以从两个角度理解，这在运行程序一节中进行了描述。每个角度都可以帮助理解 IO 的 pure 和 bind 的含义。

From the first perspective, an IO action is an instruction to Lean’s run-time system. For example, the instruction might be “read a string from this file descriptor, then re-invoke the pure Lean code with the string”. This perspective is an exterior one, viewing the program from the perspective of the operating system. In this case, pure is an IO action that does not request any effects from the RTS, and bind instructs the RTS to first carry out one potentially-effectful operation and then invoke the rest of the program with the resulting value.

从第一个视角看，IO 活动是 Lean 运行时系统的指令。例如，指令可能是「从该文件描述符读取字符串，然后使用该字符串重新调用纯 Lean 代码」。这是一种外部的视角，即从操作系统的视角看待程序。在这种情况下，pure 是一个不请求 RTS 产生任何作用的 IO 活动，而 bind 指示 RTS 首先执行一个产生潜在作用的操作，然后使用结果值调用程序的其余部分。

From the second perspective, an IO action transforms the whole world. IO actions are actually pure, because they receive a unique world as an argument and then return the changed world. This perspective is an interior one that matches how IO is represented inside of Lean. The world is represented in Lean as a token, and the IO monad is structured to make sure that each token is used exactly once.

从第二个视角看，IO 活动会变换整个世界。IO 活动实际上是纯（Pure）的，因为它接受一个唯一的世界作为参数，然后返回改变后的世界。这是一种内部的视角，它对应了 IO 在 Lean 中的表示方式。世界在 Lean 中表示为一个标记，而 IO 单子的结构化可以确保标记刚好使用一次。

To see how this works, it can be helpful to peel back one definition at a time. The #print command reveals the internals of Lean datatypes and definitions. For example,

为了了解其工作原理，逐层解析它的定义会很有帮助。 #print 命令揭示了 Lean 数据类型和定义的内部结构。例如，

1	#print Nat

results in

的结果为

inductive Nat : Type
number of parameters: 0
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

and

而

1	#print Char.isAlpha

results in

的结果为

1 2	def Char.isAlpha : Char → Bool := fun c => Char.isUpper c \|\| Char.isLower c

Sometimes, the output of #print includes Lean features that have not yet been presented in this book. For example,

有时，#print 的输出包含了本书中尚未展示的 Lean 特性。例如，

1	#print List.isEmpty

produces

会产生

def List.isEmpty.{u} : {α : Type u} → List α → Bool :=
fun {α} x =>
  match x with
  | [] => true
  | head :: tail => false

which includes a .{u} after the definition’s name, and annotates types as Type u rather than just Type. This can be safely ignored for now.

它在定义名的后面包含了一个 .{u} ，并将类型标注为 Type u 而非只是 Type。目前可以安全地忽略它。

Printing the definition of IO shows that it’s defined in terms of simpler structures:

打印 IO 的定义表明它是根据更简单的结构定义的：

#print IO



@[reducible] def IO : Type → Type :=
EIO IO.Error

IO.Error represents all the errors that could be thrown by an IO action:

IO.Error 表示 IO 活动可能抛出的所有错误：

#print IO.Error



inductive IO.Error : Type
number of parameters: 0
constructors:
IO.Error.alreadyExists : Option String → UInt32 → String → IO.Error
IO.Error.otherError : UInt32 → String → IO.Error
IO.Error.resourceBusy : UInt32 → String → IO.Error
IO.Error.resourceVanished : UInt32 → String → IO.Error
IO.Error.unsupportedOperation : UInt32 → String → IO.Error
IO.Error.hardwareFault : UInt32 → String → IO.Error
IO.Error.unsatisfiedConstraints : UInt32 → String → IO.Error
IO.Error.illegalOperation : UInt32 → String → IO.Error
IO.Error.protocolError : UInt32 → String → IO.Error
IO.Error.timeExpired : UInt32 → String → IO.Error
IO.Error.interrupted : String → UInt32 → String → IO.Error
IO.Error.noFileOrDirectory : String → UInt32 → String → IO.Error
IO.Error.invalidArgument : Option String → UInt32 → String → IO.Error
IO.Error.permissionDenied : Option String → UInt32 → String → IO.Error
IO.Error.resourceExhausted : Option String → UInt32 → String → IO.Error
IO.Error.inappropriateType : Option String → UInt32 → String → IO.Error
IO.Error.noSuchThing : Option String → UInt32 → String → IO.Error
IO.Error.unexpectedEof : IO.Error
IO.Error.userError : String → IO.Error

EIO ε α represents IO actions that will either terminate with an error of type ε or succeed with a value of type α. This means that, like the Except ε monad, the IO monad includes the ability to define error handling and exceptions.

EIO ε α 表示一个 IO 活动，它将以类型为 ε 的错误表示终止，或者以类型为 α 的值表示成功。这意味着，与 Except ε 单子一样，IO 单子也包括定义错误处理和异常的能力。

Peeling back another layer, EIO is itself defined in terms of a simpler structure: Peeling back another layer, EIO is itself defined in terms of a simpler structure:

剥离另一层，EIO 本身又是根据更简单的结构定义的：

#print EIO



def EIO : Type → Type → Type :=
fun ε => EStateM ε IO.RealWorld

The EStateM monad includes both errors and state—it’s a combination of Except and State. It is defined using another type, EStateM.Result:

EStateM 单子同时包括错误和状态——它是 Except 和 State 的组合。它使用另一个类型 EStateM.Result 定义：

#print EStateM



def EStateM.{u} : Type u → Type u → Type u → Type u :=
fun ε σ α => σ → EStateM.Result ε σ α

In other words, a program with type EStateM ε σ α is a function that accepts an initial state of type σ and returns an EStateM.Result ε σ α.

换句话说，类型为 EStateM ε σ α 的程序是一个函数，它接受类型为 σ 的初始状态并返回一个 EStateM.Result ε σ α。

EStateM.Result is very much like the definition of Except, with one constructor that indicates a successful termination and one constructor that indicates an error:

EStateM.Result 与 Except 的定义非常相似，一个构造子表示成功终止，令一个构造子表示错误：

#print EStateM.Result



inductive EStateM.Result.{u} : Type u → Type u → Type u → Type u
number of parameters: 3
constructors:
EStateM.Result.ok : {ε σ α : Type u} → α → σ → EStateM.Result ε σ α

1	EStateM.Result.error : {ε σ α : Type u} → ε → σ → EStateM.Result ε σ α

Just like Except ε α, the ok constructor includes a result of type α, and the error constructor includes an exception of type ε. Unlike Except, both constructors have an additional state field that includes the final state of the computation.

就像 Except ε α 一样，ok 构造子包含类型为 α 的结果， error 构造子包含类型为 ε 的异常。与 Except 不同，这两个构造子都有一个附加的状态字段，其中包含计算的最终状态。

The Monad instance for EStateM ε σ requires pure and bind. Just as with State, the implementation of pure for EStateM accepts an initial state and returns it unchanged, and just as with Except, it returns its argument in the ok constructor:

EStateM ε σ 的 Monad 实例需要 pure 和 bind。与 State 一样，EStateM 的 pure 实现接受一个初始状态并将其返回而不改变，并且与 Except 一样，它在 ok 构造子中返回其参数：

#print EStateM.pure



protected def EStateM.pure.{u} : {ε σ α : Type u} → α → EStateM ε σ α :=
fun {ε σ α} a s => EStateM.Result.ok a s

protected means that the full name EStateM.pure is needed even if the EStateM namespace has been opened.

protected 意味着即使打开了 EStateM 命名空间，也需要完整的名称 EStateM.pure。

Similarly, bind for EStateM takes an initial state as an argument. It passes this initial state to its first action. Like bind for Except, it then checks whether the result is an error. If so, the error is returned unchanged and the second argument to bind remains unused. If the result was a success, then the second argument is applied to both the returned value and to the resulting state.

类似地，EStateM 的 bind 将初始状态作为参数。它将此初始状态传递给其第一个操作。与 Except 的 bind 一样，它然后检查结果是否为错误。如果是，则错误将保持不变，并且 bind 的第二个参数保持未使用。如果结果成功，则将第二个参数应用于返回值和结果状态。

#print EStateM.bind



protected def EStateM.bind.{u} : {ε σ α β : Type u} → EStateM ε σ α → (α → EStateM ε σ β) → EStateM ε σ β :=
fun {ε σ α β} x f s =>
  match x s with
  | EStateM.Result.ok a s => f a s

1	\| EStateM.Result.error e s => EStateM.Result.error e s

Putting all of this together, IO is a monad that tracks state and errors at the same time. The collection of available errors is that given by the datatype IO.Error, which has constructors that describe many things that can go wrong in a program. The state is a type that represents the real world, called IO.RealWorld. Each basic IO action receives this real world and returns another one, paired either with an error or a result. In IO, pure returns the world unchanged, while bind passes the modified world from one action into the next action.

综上所述，IO 是同时跟踪状态和错误的单子。可用错误的集合由数据类型 IO.Error 给出，该数据类型具有描述程序中可能出错的许多情况的构造子。状态是一种表示现实世界的类型，称为 IO.RealWorld。每个基本的 IO 活动都会接收这个现实世界并返回另一个，与错误或结果配对。在 IO 中，pure 返回未更改的世界，而 bind 将修改后的世界从一个活动传递到下一个活动。

Because the entire universe doesn’t fit in a computer’s memory, the world being passed around is just a representation. So long as world tokens are not re-used, the representation is safe. This means that world tokens do not need to contain any data at all: Because the entire universe doesn’t fit in a computer’s memory, the world being passed around is just a representation. So long as world tokens are not re-used, the representation is safe. This means that world tokens do not need to contain any data at all:

由于计算机内存无法容纳整个宇宙，因此传递的世界仅仅是一种表示。只要不重复使用世界标记，该表示就是安全的。这意味着世界标记根本不需要包含任何数据：

#print IO.RealWorld



def IO.RealWorld : Type :=
Unit

Additional Conveniences

其他便利功能

Shared Argument Types

共享参数类型

When defining a function that takes multiple arguments that have the same type, both can be written before the same colon. For example,

定义具有相同类型的多个参数时，可以把它们写在同一个冒号之前。例如：

def equal? [BEq α] (x : α) (y : α) : Option α :=
  if x == y then
    some x
  else
    none

can be written

可以写成

def equal? [BEq α] (x y : α) : Option α :=
  if x == y then
    some x
  else
    none

This is especially useful when the type signature is large.

这在类型签名很长的时候特别有用。

Leading Dot Notation

开头的点号

The constructors of an inductive type are in a namespace. This allows multiple related inductive types to use the same constructor names, but it can lead to programs becoming verbose. In contexts where the inductive type in question is known, the namespace can be omitted by preceding the constructor’s name with a dot, and Lean uses the expected type to resolve the constructor names. For example, a function that mirrors a binary tree can be written:

一个归纳类型的所有构造子都存在于一个命名空间中。因此允许不同的归纳类型有同名构造子，但是这也会导致程序变得啰嗦。当问题中的归纳类型已知时，可以命名空间可以省略，只需要在构造子前保留点号，Lean可以根据该处期望的类型来决定如何选择构造子。例如将二叉树镜像的函数：

1
2
3

def BinTree.mirror : BinTree α → BinTree α
  | BinTree.leaf => BinTree.leaf
  | BinTree.branch l x r => BinTree.branch (mirror r) x (mirror l)

Omitting the namespaces makes it significantly shorter, at the cost of making the program harder to read in contexts like code review tools that don’t include the Lean compiler:

省略命名空间使代码显著变短，但代价是在没有Lean编译器，例如code review时，代码会变得难以阅读：

1
2
3

def BinTree.mirror : BinTree α → BinTree α
  | .leaf => .leaf
  | .branch l x r => .branch (mirror r) x (mirror l)

Using the expected type of an expression to disambiguate a namespace is also applicable to names other than constructors. If BinTree.empty is defined as an alternative way of creating BinTrees, then it can also be used with dot notation:

通过期望的类型来消除命名空间的歧义，同样可以应用于构造子之外的名称。例如BinTree.empty定义为一种创建BinTree的方式，那么它也可以和点号一起使用：

def BinTree.empty : BinTree α := .leaf

#check (.empty : BinTree Nat)



BinTree.empty : BinTree Nat

Or-Patterns

或-模式

In contexts that allow multiple patterns, such as match-expressions, multiple patterns may share their result expressions. The datatype Weekday that represents days of the week:

当有多个模式匹配的分支时，例如match表达式，那么不同的模式可以共享同一个结果表达式。表示一周的每一天的类型Weekday：

inductive Weekday where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday
  deriving Repr

Pattern matching can be used to check whether a day is a weekend:

可以用模式匹配检查某一天是否是周末：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | Weekday.saturday => true
  | Weekday.sunday => true
  | _ => false

This can already be simplified by using constructor dot notation:

首先可以用点号来简化：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday => true
  | .sunday => true
  | _ => false

Because both weekend patterns have the same result expression (true), they can be condensed into one:

因为周末的两天都有相同的结果true，所以可以精简成：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday | .sunday => true
  | _ => false

This can be further simplified into a version in which the argument is not named:

进一步可以简化成没有参数名称的函数：

1
2
3

def Weekday.isWeekend : Weekday → Bool
  | .saturday | .sunday => true
  | _ => false

Behind the scenes, the result expression is simply duplicated across each pattern. This means that patterns can bind variables, as in this example that removes the inl and inr constructors from a sum type in which both contain the same type of value:

实际上结果表达式只是简单地被复制。所以模式也可以绑定变量，这个例子在和类型(Sum Type)两边具有相同类型时，将inl和inr构造子去除：

1 2	def condense : α ⊕ α → α \| .inl x \| .inr x => x

Because the result expression is duplicated, the variables bound by the patterns are not required to have the same types. Overloaded functions that work for multiple types may be used to write a single result expression that works for patterns that bind variables of different types:

但是因为结果表达式只是被复制，所以模式绑定的变量也可以具有不同类型。重载的函数可以让同一个结果表达式用于多个绑定不同类型的变量的模式：

1 2	def stringy : Nat ⊕ Weekday → String \| .inl x \| .inr x => s!"It is {repr x}"

In practice, only variables shared in all patterns can be referred to in the result expression, because the result must make sense for each pattern. In getTheNat, only n can be accessed, and attempts to use either x or y lead to errors.

实践中，只有在所有模式都存在的变量才可以在结果表达式中引用，因为这条表达式必须对所有分支都有意义。 getTheNat中只有n可以被访问，使用x或y将会导致错误。

1 2	def getTheNat : (Nat × α) ⊕ (Nat × β) → Nat \| .inl (n, x) \| .inr (n, y) => n

Attempting to access x in a similar definition causes an error because there is no x available in the second pattern:

这种类似的情况中访问x同样会导致错误，因为x在第二个模式中不存在：

def getTheAlpha : (Nat × α) ⊕ (Nat × α) → α
  | .inl (n, x) | .inr (n, y) => x



unknown identifier 'x'

The fact that the result expression is essentially copy-pasted to each branch of the pattern match can lead to some surprising behavior. For example, the following definitions are acceptable because the inr version of the result expression refers to the global definition of str:

简单地对结果表达式进行复制，会导致某些令人惊讶的行为。例如，下列定义是合法的，因为inr分支实际上引用的是全局定义str：

def str := "Some string"

def getTheString : (Nat × String) ⊕ (Nat × β) → String
  | .inl (n, str) | .inr (n, y) => str

Calling this function on both constructors reveals the confusing behavior. In the first case, a type annotation is needed to tell Lean which type β should be:

在不同分支上调用该函数会让人困惑。第一种情况中，需要提供类型标记告诉Lean类型β是什么：

#eval getTheString (.inl (20, "twenty") : (Nat × String) ⊕ (Nat × String))



"twenty"

In the second case, the global definition is used:

第二种情况被使用的是全局定义：

#eval getTheString (.inr (20, "twenty"))



"Some string"

Using or-patterns can vastly simplify some definitions and increase their clarity, as in Weekday.isWeekend. Because there is a potential for confusing behavior, it’s a good idea to be careful when using them, especially when variables of multiple types or disjoint sets of variables are involved.

使用或-模式可以极大简化某些定义，让它们更加清晰，例如Weekday.isWeekend. 但因为存在可能导致困惑的行为，需要十分小心地使用，特别是涉及不同类型的变量，或不相交的变量集合时。

Summary

总结

Encoding Side Effects

编码副作用

Lean is a pure functional language. This means that it does not include side effects such as mutable variables, logging, or exceptions. However, most side effects can be encoded using a combination of functions and inductive types or structures. For example, mutable state can be encoded as a function from an initial state to a pair of a final state and a result, and exceptions can be encoded as an inductive type with constructors for successful termination and errors.

是一种纯函数式语言。这意味着它不包含副作用，例如可变变量、日志记录或异常。但是，大多数副作用都可以使用函数和归纳类型或结构体的组合进行编码。例如，可变状态可以编码为从初始状态到一对最终状态和结果的函数，异常可以编码为具有成功终止构造子和错误构造子的归纳类型。

Each set of encoded effects is a type. As a result, if a program uses these encoded effects, then this is apparent in its type. Functional programming does not mean that programs can’t use effects, it simply requires that they be honest about which effects they use. A Lean type signature describes not only the types of arguments that a function expects and the type of result that it returns, but also which effects it may use.

每组编码的作用都是一种类型。因此，如果程序使用这些编码作用，那么这在它的类型中是显而易见的。函数式编程并不意味着程序不能使用作用，它只是要求它们 诚实地 说明它们使用的作用。 Lean 类型签名不仅描述了函数期望的参数类型和它返回的结果类型，还描述了它可能使用的作用。

The Monad Type Class

单子类型类

It’s possible to write purely functional programs in languages that allow effects anywhere. For example, 2 + 3 is a valid Python program that has no effects at all. Similarly, combining programs that have effects requires a way to state the order in which the effects must occur. It matters whether an exception is thrown before or after modifying a variable, after all.

在允许在任何地方使用作用的语言中编写纯函数式程序是可能的。例如，2 + 3 是一个有效的 Python 程序，它没有任何作用。类似地，组合具有作用的程序需要一种方法来说明作用必须发生的顺序。毕竟，异常是在修改变量之前还是之后抛出是有区别的。

The type class Monad captures these two important properties. It has two methods: pure represents programs that have no effects, and bind sequences effectful programs. The contract for Monad instances ensures that bind and pure actually capture pure computation and sequencing.

类型类 Monad 刻画了这两个重要属性。它有两个方法：pure 表示没有副作用的程序， bind 顺序执行有副作用的程序。Monad 实例的约束确保了 bind 和 pure 实际上刻画了纯计算和顺序执行。

`do`-Notation for Monads

单子的 `do`-记法

Rather than being limited to IO, do-notation works for any monad. It allows programs that use monads to be written in a style that is reminiscent of statement-oriented languages, with statements sequenced after one another. Additionally, do-notation enables a number of additional convenient shorthands, such as nested actions. A program written with do is translated to applications of >>= behind the scenes.

do 符号不仅限于 IO，它也适用于任何单子。它允许使用单子的程序以类似于面向语句的语言的风格编写，语句一个接一个地顺序执行。此外，do-记法还支持许多其他方便的简写，例如嵌套动作。使用 do 编写的程序在幕后会被翻译为 >>= 的应用。

Custom Monads

定制单子

Different languages provide different sets of side effects. While most languages feature mutable variables and file I/O, not all have features like exceptions. Other languages offer effects that are rare or unique, like Icon’s search-based program execution, Scheme and Ruby’s continuations, and Common Lisp’s resumable exceptions. An advantage to encoding effects with monads is that programs are not limited to the set of effects that are provided by the language. Because Lean is designed to make programming with any monad convenient, programmers are free to choose exactly the set of side effects that make sense for any given application.

不同的语言提供不同的副作用集。虽然大多数语言都具有可变变量和文件 I/O，但并非所有语言都具有异常等特性。其他语言提供罕见或独特的副作用，例如 Icon 基于搜索的程序执行、Scheme 和 Ruby 的续体以及 Common Lisp 的可恢复异常。用单子对副作用进行编码的一个优点是，程序不受语言提供的副作用集的限制。由于 Lean 被设计为能方便地使用任何单子进行编程，因此程序员可以自由选择最适合任何给定应用的副作用集。

The `IO` Monad

`IO` 单子

Programs that can affect the real world are written as IO actions in Lean. IO is one monad among many. The IO monad encodes state and exceptions, with the state being used to keep track of the state of the world and the exceptions modeling failure and recovery.

可以在现实世界中产生影响的程序在 Lean 中被写作 IO 活动。 IO 是众多单子中的一个。IO 单子对状态和异常进行编码，其中状态用于跟踪世界的状态，异常则对失败和恢复进行建模。

Lean 函数式编程(二) | 重载与类型类

发表于 2025-10-10 更新于 2025-10-19 阅读次数：字数： 21k 时间 ≈ 1:17

重载与类型类

在许多语言中，内置数据类型有特殊的优待。例如，在 C 和 Java 中，+ 可以被用于 float 和 int，但不能用于其他第三方库的数字。类似地，数字字符可以被直接用于内置类型，但是不能用于用户定义的数字类型。其他语言为运算符提供 重载（overloading） 机制，使得同一个运算符可以在新的类型有意义。在这些语言中，比如 C++ 和 C#，多种内置运算符都可以被重载，编译器使用类型检查来选择一个特定的实现。

除了数字和运算符，许多语言还可以重载函数或方法。在 C++，Java，C# 和 Kotlin 中，对于不同的数字和类型参数，一个方法可以有多种实现。编译器使用参数的数字和它们的类型来决定使用哪个重载。

函数和运算符的重载有一个关键的受限之处：多态函数无法限定它们的类型参数为重载存在的那些类型。例如，一个重载方法可能在字符串，字节数组和文件指针上有定义，但是没有任何方法能写第二个方法能在任意这些类型上适用。如果想这样做的话，这第二个方法必须本身也为每一个类型都有一个原始方法的重载，最终产生许多繁琐的定义而不是一个简单的多态定义。这种限制的另一个后果是一些运算符（例如 Java 中的等号）对 每一个 参数组合都要有定义，即使这样做是完全没必要的。如果程序员没有很谨慎的话，这可能会导致程序在运行时崩溃，或者静静地计算出错误的结果。

Lean 用 类型类（type classes） 机制（源于 Haskell）来实现重载。这使得运算符，函数和字面量重载与多态有一个很好的配合。一个类型类描述了一族可重载的运算符。要将这些运算符重载到新的类型上，你需要创建一个包含对新类型的每一个运算的实现方式的 实例（instance） 。例如，Add 类型类描述了可加的类型，一个对 Nat 类型的 Add 实例提供了 Nat 上加法的实现。

类和实例这两个词可能会使面向对象程序员感到混淆，因为 Lean 中的它们与面向对象语言中的类和实例关系不大。然而，它们有相同的基本性质：在日常语言中，“类”这个词指的是具有某些共同属性的组。虽然面向对象编程中的类确实描述了具有共同属性的对象组，但该术语还指代描述此类对象组的特定编程语言机制。类型类也是描述共享共同属性的类型（即某些操作的实现）的一种方式，但它们与面向对象编程中的类并没有其他共同点。

Lean 的类型类更像是 Java 或 C# 中的 接口（interface） 。类型类和接口都描述了在概念上有联系的运算的集合，这些运算为一个类型或一个类型集合实现。类似地，类型类的实例也很像 Java 或 C# 中描述实现了的接口的类，而不是 Java 或 C# 中类的实例。不像 Java 或 C# 的接口，对于一个类型，该类型的作者并不能访问的类型类也可以给这个类型实例。从这种意义上讲，这和 Rust 的 traits 很像。

正整数

自定义类型

在某些应用场景中，只有正数才有意义。例如，编译器和解释器通常使用从1开始的行号和列号来表示源代码位置，而表示非空列表的数据类型永远不会报告长度为零的情况。与其依赖自然数并在代码中散布断言来确保数字不为零，不如设计一个只表示正数的数据类型。

表示正数的一种方法与 Nat 非常相似，只是用 one 作为基础情况而不是 zero：

1
2
3

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

这个数据类型准确地表示了我们想要的值集合，但使用起来并不方便。例如，数字字面量会被拒绝：

1	def seven : Pos := 7

1 2	failed to synthesize instance OfNat Pos 7

相反，必须直接使用构造子：

1 2	def seven : Pos := Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))

同样，加法和乘法也不容易使用：

def fourteen : Pos := seven + seven

failed to synthesize instance
  HAdd Pos Pos ?m.291

def fortyNine : Pos := seven * seven

failed to synthesize instance
  HMul Pos Pos ?m.291

这些错误消息都以 failed to synthesize instance 开头。这表明错误是由于尚未实现的重载操作引起的，并描述了必须实现的类型类。

类与实例

类型类由名称、一些参数和一组 方法（method） 组成。参数描述了要为其定义可重载操作的类型，方法是可重载操作的名称和类型签名。这里再次出现了与面向对象语言的术语冲突。在面向对象编程中，方法本质上是连接到内存中特定对象的函数，具有访问对象私有状态的特殊权限。对象通过其方法进行交互。在 Lean 中，"方法"一词指的是已声明为可重载的操作，与对象、值或私有字段没有特殊关联。

重载加法的一种方法是定义一个名为 Plus 的类型类，其中包含一个名为 plus 的加法方法。一旦为 Nat 定义了 Plus 的实例，就可以使用 Plus.plus 来相加两个 Nat：

1
2
3

#eval Plus.plus 5 3

8

添加更多实例可以让 Plus.plus 接受更多类型的参数。

在下面的类型类声明中，Plus 是类的名称，α : Type 是唯一的参数，plus : α → α → α 是唯一的方法：

1 2	class Plus (α : Type) where plus : α → α → α

这个声明表示存在一个类型类 Plus，它针对类型 α 重载操作。具体来说，有一个名为 plus 的重载操作，它接受两个 α 并返回一个 α。

类型类是一等公民，就像类型是一等公民一样。特别地，类型类是另一种类型。Plus 的类型是 Type → Type，因为它接受一个类型作为参数（α），并产生一个新类型，该类型描述了 Plus 操作对 α 的重载。

要为特定类型重载 plus，需要编写一个实例：

1 2	instance : Plus Nat where plus := Nat.add

instance 后的冒号表明 Plus Nat 确实是一个类型。类 Plus 的每个方法都应该使用 := 赋值。在这种情况下，只有一个方法：plus。

默认情况下，类型类方法在与类型类同名的命名空间中定义。打开命名空间会很方便，这样用户就不需要先输入类的名称。open 命令中的括号表示只有指定的名称才能从命名空间中访问：

open Plus (plus)

#eval plus 5 3

8

为 Pos 定义加法函数和 Plus Pos 的实例，可以使用 plus 来相加 Pos 或 Nat 值：

def Pos.plus : Pos → Pos → Pos
  | Pos.one, k => Pos.succ k
  | Pos.succ n, k => Pos.succ (n.plus k)

instance : Plus Pos where
  plus := Pos.plus

def fourteen : Pos := plus seven seven

因为还没有 Plus Float 的实例，尝试使用 plus 相加两个浮点数会失败，并显示熟悉的错误消息：

#eval plus 5.2 917.25861

failed to synthesize instance
  Plus Float

这些错误意味着 Lean 无法为给定的类型类找到实例。

重载加法

Lean 的内置加法运算符是名为 HAdd 的类型类的语法糖，它灵活地允许加法的参数具有不同的类型。HAdd 是 异构加法（heterogeneous addition） 的缩写。例如，可以编写一个 HAdd 实例来允许将 Nat 与 Float 相加，结果是一个新的 Float。当程序员写 x + y 时，它被解释为 HAdd.hAdd x y。

虽然对 HAdd 完全通用性的理解依赖于本章另一节中讨论的特性，但有一个更简单的类型类叫做 Add，它不允许混合参数类型。当两个参数具有相同类型时，Lean 库的设置会使得在找到 HAdd 实例时，会找到 Add 的实例。

定义 Add Pos 的实例将允许 Pos 值使用普通的加法语法：

instance : Add Pos where
  add := Pos.plus

-- instance : HAdd Pos Pos Pos where
--   hAdd : Pos → Pos → Pos := Pos.plus

def fourteen : Pos := seven + seven

转换为字符串

另一个有用的内置类叫做 ToString。ToString 的实例提供了将给定类型的值转换为字符串的标准方法。例如，当值出现在插值字符串中时会使用 ToString 实例，它决定了在 IO 描述开始处 使用的 IO.println 函数如何显示值。

例如，将 Pos 转换为 String 的一种方法是显示其内部结构。函数 posToString 接受一个 Bool 参数，该参数决定是否为 Pos.succ 的使用加括号，在函数的初始调用中应该为 true，在所有递归调用中应该为 false。

def posToString (atTop : Bool) (p : Pos) : String :=
  let paren s := if atTop then s else "(" ++ s ++ ")"
  match p with
  | Pos.one => "Pos.one"
  | Pos.succ n => paren s!"Pos.succ {posToString false n}"

将此函数用于 ToString 实例：

1 2	instance : ToString Pos where toString := posToString true

会产生信息丰富但令人眼花缭乱的输出：

1
2
3

#eval s!"There are {seven}"

"There are Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ (Pos.succ Pos.one)))))"

另一方面，每个正数都有对应的 Nat。将其转换为 Nat，然后使用 ToString Nat 实例（即 Nat 的 toString 重载）是生成更简短输出的快速方法：

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

instance : ToString Pos where
  toString x := toString (x.toNat)

#eval s!"There are {seven}"

"There are 7"

当定义了多个实例时，最新的实例优先。此外，如果类型有 ToString 实例，那么即使该类型没有使用 deriving Repr 定义，也可以用它来显示 #eval 的结果，所以 #eval seven 输出 7。

重载乘法

对于乘法，有一个名为 HMul 的类型类允许混合参数类型，就像 HAdd 一样。正如 x + y 被解释为 HAdd.hAdd x y，x * y 被解释为 HMul.hMul x y。对于两个相同类型参数相乘的常见情况，Mul 实例就足够了。

Mul 的实例允许在 Pos 中使用普通的乘法语法：

def Pos.mul : Pos → Pos → Pos
  | Pos.one, k => k
  | Pos.succ n, k => n.mul k + k

instance : Mul Pos where
  mul := Pos.mul

有了这个实例，乘法按预期工作：

#eval [seven * Pos.one,
       seven * seven,
       Pos.succ Pos.one * seven]

[7, 49, 14]

数字字面量

为正数写出一系列构造子是相当不方便的。解决这个问题的一种方法是提供一个将 Nat 转换为 Pos 的函数。然而，这种方法有缺点。首先，因为 Pos 不能表示 0，结果函数要么将 Nat 转换为更大的数字，要么返回 Option Pos。这两种方式对用户都不是特别方便。其次，需要显式调用函数会使使用正数的程序比使用 Nat 的程序编写起来不那么方便。在精确类型和方便的 API 之间进行权衡意味着精确类型变得不那么有用。

在 Lean 中，自然数字面量使用名为 OfNat 的类型类来解释：

1 2	class OfNat (α : Type) (_ : Nat) where ofNat : α

这个类型类接受两个参数：α 是要为其重载自然数的类型，未命名的 Nat 参数是程序中遇到的实际字面量数字。然后使用方法 ofNat 作为数字字面量的值。因为类包含 Nat 参数，所以可以只为那些数字有意义的值定义实例。

OfNat 展示了类型类的参数不需要是类型。因为在 Lean 中，类型是语言中的一等公民，可以作为参数传递给函数，并且可以使用 def 和 abbrev 给出定义。Lean 并不阻止非类型参数出现在类型类的参数位置上，但一些不够灵活的语言则不允许这种操作。这种灵活性能为特定的值以及特定的类型提供运算符重载。

例如，表示小于四的自然数的和类型可以定义如下：

inductive LT4 where
  | zero
  | one
  | two
  | three
deriving Repr

虽然允许任何字面量数字用于此类型没有意义，但小于四的数字显然是有意义的：

instance : OfNat LT4 0 where
  ofNat := LT4.zero

instance : OfNat LT4 1 where
  ofNat := LT4.one

instance : OfNat LT4 2 where
  ofNat := LT4.two

instance : OfNat LT4 3 where
  ofNat := LT4.three

有了这些实例，以下示例可以工作：

#eval (3 : LT4)
LT4.three

#eval (0 : LT4)
LT4.zero

另一方面，越界的字面量仍然不被允许：

#eval (4 : LT4)

failed to synthesize instance
OfNat LT4 4

对于 Pos，OfNat 实例应该适用于除 Nat.zero 之外的任何 Nat。另一种表达方式是说，对于所有自然数 n，实例应该适用于 n + 1。正如像 α 这样的名称自动成为 Lean 自己填充的函数的隐式参数一样，实例可以接受自动隐式参数。在这个实例中，参数 n 代表任何 Nat，实例为大一的 Nat 定义：

instance : OfNat Pos (n + 1) where
  ofNat :=
    -- 定义局部辅助函数 natPlusOne
    let rec natPlusOne : Nat → Pos
      | 0 => Pos.one
      | k + 1 => Pos.succ (natPlusOne k)
    natPlusOne n

因为 n 代表比用户写的数字小一的 Nat，辅助函数 natPlusOne 返回比其参数大一的 Pos。这使得可以为正数使用自然数字面量，但不能为零：

1
2
3

def eight : Pos := 8

def zero : Pos := 0

1 2	failed to synthesize instance OfNat Pos 0

练习

表示正数的另一种方法是作为某个 Nat 的后继。用一个构造子名为 succ 且包含 Nat 的结构体替换 Pos 的定义：

1
2
3

structure Pos where
  succ ::
  pred : Nat

定义 Add、Mul、ToString 和 OfNat 的实例，使这个版本的 Pos 能够方便地使用。

解答：

instance : Add Pos where
  add x y := Pos.succ (x.pred + y.pred + 1)

instance : Mul Pos where
  mul x y := Pos.succ (x.pred * y.pred + x.pred + y.pred)

instance : ToString Pos where
  toString x := toString (x.pred + 1)

instance : OfNat Pos (n + 1) where
  ofNat := Pos.succ n

定义一个只表示偶数的数据类型。定义 Add、Mul 和 ToString 的实例，使其能够方便地使用。OfNat 需要下一节中介绍的特性。

-- 定义偶数数据类型
inductive Even : Type where
  | zero : Even                    -- 0 是偶数
  | addTwo : Even → Even          -- 如果 n 是偶数，那么 n+2 也是偶数

-- 将偶数转换为自然数的辅助函数
def Even.toNat : Even → Nat
  | Even.zero => 0
  | Even.addTwo e => e.toNat + 2

def Even.add : Even → Even → Even
  | x, Even.zero => x
  | x, Even.addTwo y => Even.addTwo (Even.add x y)

-- Add 实例：两个偶数相加仍是偶数
instance : Add Even where
  add := Even.add

def Even.mul : Even → Even → Even
  | Even.zero, _ => Even.zero
  -- (2 + x) * y
  | Even.addTwo x, y => (y + y + Even.mul x y)

-- Mul 实例：两个偶数相乘仍是偶数
instance : Mul Even where
  mul := Even.mul

-- ToString 实例：显示为自然数形式
instance : ToString Even where
  toString e := toString e.toNat

HTTP 请求以 HTTP 方法的标识开始，如 GET 或 POST，以及 URI 和 HTTP 版本。定义一个归纳类型来表示 HTTP 方法的有趣子集，以及一个表示 HTTP 响应的结构体。响应应该有一个 ToString 实例，使其可以进行调试。使用类型类将不同的 IO 操作与每个 HTTP 方法关联，并编写一个测试工具作为 IO 操作，调用每个方法并打印结果。

类型类与多态

编写适用于给定函数的任意重载可能会很有用。例如，IO.println 适用于任何具有 ToString 实例的类型。通过在所需实例周围使用方括号来表示：IO.println 的类型是 {α : Type} → [ToString α] → α → IO Unit。这个类型表示 IO.println 接受一个类型为 α 的参数，并且 Lean 应该自动确定这个类型，而且必须有一个可用于 α 的 ToString 实例，最后返回一个 IO 操作。

注：这一节我们讨论如何编写作用于所有注册类型的函数。

对多态函数的类型检查

对接受隐式参数，或使用了类型类的函数进行类型检查时，我们需要用到一些额外的语法。简单地写

1	#check (IO.println)

会产生一个包含元变量的类型。

1	IO.println : ?m.3620 → IO Unit

这里显示出了元变量是因为即使 Lean 尽全力去寻找隐式参数，但还是没有找到足够的类型信息来做到这一点。要理解函数的签名，可以在函数名之前加上一个 at 符号（@）来抑制此特性。

1
2
3

#check @IO.println

@IO.println : {α : Type u_1} → [inst : ToString α] → α → IO Unit

在这个输出信息中，实例本身被给予了 inst 这个名字。此外，Type 后面有一个 u_1 ，这里使用了目前尚未介绍的 Lean 的特性。我们可以暂时忽略这些 Type 的参数。

定义含隐式实例的多态函数

前边介绍了常规的重载方式，比如为 Nat 定义 Add 实例，为 Pos 定义 ToString 实例。

-- 为具体类型直接定义实例
instance : Add Nat where
  add := Nat.add

instance : ToString Pos where
  toString x := toString (x.toNat)

特点是直接为具体类型提供实现。

我们这小节考虑更复杂的情形。先看一个例子，一个对列表中所有条目求和的函数需要两个实例：Add 允许对条目进行加法运算，而 OfNat 实例为 0 提供了一个合理的值，以便对空列表进行返回。

1
2
3

def List.sum [Add α] [OfNat α 0] : List α → α
  | [] => 0
  | x :: xs => x + xs.sum

这个函数可以被用于 Nat 列表：

def fourNats : List Nat := [1, 2, 3, 4]

#eval fourNats.sum

10

由于 Pos 在 0 处没有定义， [OfNat α 0] 匹配失败，无法用于 Pos 列表：

def fourPos : List Pos := [1, 2, 3, 4]

#eval fourPos.sum

failed to synthesize instance
  OfNat Pos 0

上边例子中，在方括号中的所需实例规范被称为 隐式实例（instance implicits） 。
在幕后，类型类都定义了一个结构，该结构具有重载操作的字段。实例则是该结构类型的值，每个字段包含一个实现。在调用时，Lean 负责为每个隐式实例参数找到一个实例值传递。

普通的隐式参数和隐式实例最重要的不同就是 Lean 寻找参数值的策略。对于普通的隐式参数，Lean 使用一种被称为 归一化（unification） 的技术来找到一个唯一的能使程序通过类型检查的参数值。这个过程只依赖于函数定义中的具体类型和调用时的类型。

就像对 Pos 的 OfNat 实例用一个自然数 n 作为自动隐式参数，实例本身也可能接受隐式实例参数。在 多态那一节 中展示了一个多态点类型：

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

点之间的加法需要将从属的 x 和 y 字段相加。因此，PPoint 的 Add 实例需要这些字段所具有的类型的 Add 实例。换句话说，PPoint 的 Add 实例还需要类型 α 的 Add 实例。我们用条件实例来表达：

1
2
3

-- α 为 Add 实例时，PPoint α 也有 Add 实例
instance [Add α] : Add (PPoint α) where
  add p1 p2 := { x := p1.x + p2.x, y := p1.y + p2.y }

当 Lean 遇到两点之间的加法，它会寻找并找到这个实例。然后会更进一步寻找 Add α 实例。

用这种方式构造的实例值是类型类的结构体值。一个成功的递归实例搜索会产生一个结构体值，该结构体值引用了另一个结构体值。比如一个 Add (PPoint Nat) 实例包含对找到的 Add Nat 实例的引用。

举个例子：

-- 假设我们有：
def point1 : PPoint Nat := { x := 1, y := 2 }
def point2 : PPoint Nat := { x := 3, y := 4 }
def result := point1 + point2  -- 这里发生了什么？

当 Lean 执行 point1 + point2 时：

寻找实例：需要 Add (PPoint Nat) 实例
找到条件实例：instance [Add α] : Add (PPoint α)
递归搜索：需要 Add Nat 实例
构造实例值：创建一个包含引用的结构体

这种递归搜索意味着类型类显著地比普通重载函数更加强大。一个多态实例库是一个由代码砖块组成的集合，编译器会根据所需的类型自行搭建。接受实例参数的多态函数是对类型类机制的潜在请求，以在幕后组装辅助函数。API 的客户端无需手工组合所有必要的部分，从而使用户从这类烦人的工作中解放出来。

方法与隐式参数

class OfNat (α : Type u) (_ : Nat) where
  ofNat : α

#check OfNat.ofNat
-- {α : Type} → (n : Nat) → [OfNat α n] → α

class Add (α : Type u) where
  add : α → α → α

#check Add.add
-- {α : Type u} [self : Add α] : α → α → α

@OfNat.ofNat 的类型可能会令人好奇。它是 {α : Type} → (n : Nat) → [OfNat α n] → α，其中 Nat 参数 n 作为显式函数参数出现。然而，在方法的声明中，ofNat 只是类型 α。这种看似的不一致是因为声明一个类型类实际上会产生以下结果：

声明一个包含了每个重载操作的实现的结构体类型
声明一个与类同名的命名空间
对于每个方法，会在类的命名空间中声明一个函数，该函数从实例中获取具体的实现。

这类似于声明新结构也声明访问器函数的方式。主要区别在于结构体的访问器函数（比如 PPoint.mk ）将结构值作为显式参数，而类型类方法将实例值作为隐式实例（比如 [Add α] ），由 Lean 自动查找。

为了让 Lean 找到一个实例，它的参数必须是可用的。这意味着类型类的每个参数必须是出现在实例之前的方法的参数。当这些参数是隐式的时候最方便，因为 Lean 会发现它们的值。例如，@Add.add 的类型是 {α : Type} → [Add α] → α → α → α。在这种情况下，类型参数 α 可以是隐式的，因为对 Add.add 的参数提供了关于用户意图的类型信息。然后，可以使用这种类型来搜索 Add 实例。

而在 ofNat 的例子中，要被解码的特定 Nat 字面量并没有作为其他参数的一部分出现。这意味着 Lean 在尝试确定隐式参数 n 时将没有足够的信息可以用。如果 Lean 选择使用隐式参数，那么结果将是一个非常不方便的 API。因此，在这些情况下，Lean 选择为类方法提供一个显式参数。

题外话：在表达类型时，中间参数允许用非类型的 (n : Nat)，但不能放在最后

def f : Nat -> (n : Nat) -> Nat := fun a _ => a
#eval f 2 0
2

def g : Nat -> (n : Nat) := sorry
type expected, got
  (n : Nat)

练习

偶数数字字面量为 上一节的练习题 中的偶数数据类型写一个使用递归实例搜索的 OfNat 实例。

-- 基本的 OfNat 实例：0 是偶数
instance : OfNat Even 0 where
  ofNat := Even.zero

-- 递归实例：如果 n 是偶数，那么 n+2 也是偶数
-- 这里利用了递归实例搜索：Lean 会自动寻找 OfNat Even n 实例
instance [OfNat Even n] : OfNat Even (n + 2) where
  ofNat := Even.addTwo (OfNat.ofNat n : Even)

#eval (2 : Even)

递归实例搜索深度：Lean 编译器尝试进行递归实例搜素的次数是有限的。这限制了前面的练习中定义的偶数字面量的尺寸。实验性地确定这个上限是多少。

实测为 256：

1	#check (256 : Even)

Lean 在寻找 OfNat Even 256 实例时，会递归地寻找 OfNat Even 254 实例，以此类推，直到找到 OfNat Even 0 实例。

控制实例搜索

要方便地相加两个 Pos 类型，并产生另一个 Pos，一个 Add 类的的实例就足够了。但是，在许多情况下，参数可能有不同的类型，重载一个灵活的 异质(heterogeneous) 运算符是更为有用的。例如，让 Nat 和 Pos，或 Pos 和 Nat 相加总会是一个 Pos：

def addNatPos : Nat → Pos → Pos
  | 0, p => p
  | n + 1, p => Pos.succ (addNatPos n p)

def addPosNat : Pos → Nat → Pos
  | p, 0 => p
  | p, n + 1 => Pos.succ (addPosNat p n)

这些函数允许自然数与正数相加，但他们不能在 Add 类型类中，因为它希望 add 的两个参数都有同样的类型。

异质重载

就像在重载加法一节提到的，Lean 提供了名为 HAdd 的类型类来重载异质加法。 HAdd 类接受三个类型参数：两个参数的类型和一个返回类型。HAdd Nat Pos Pos 和 HAdd Pos Nat Pos 的实例可以让常规加法符号可以接受不同类型。

instance : HAdd Nat Pos Pos where
  hAdd := addNatPos

instance : HAdd Pos Nat Pos where
  hAdd := addPosNat

有了上面两个实例，就有了下面的例子：

#eval (3 : Pos) + (5 : Nat)
8

#eval (3 : Nat) + (5 : Pos)
8

HAdd 的定义和下面 HPlus 的定义很像。下面是 HPlus 和它对应的实例：

class HPlus (α : Type) (β : Type) (γ : Type) where
  hPlus : α → β → γ

instance : HPlus Nat Pos Pos where
  hPlus := addNatPos

instance : HPlus Pos Nat Pos where
  hPlus := addPosNat

然而，HPlus 的实例明显没有 HAdd 的实例有用。当尝试用 #eval 使用这些实例时，一个错误就出现了：

#eval HPlus.hPlus (3 : Pos) (5 : Nat)

typeclass instance problem is stuck, it is often due to metavariables
  HPlus Pos Nat ?m.7527

发生错误是因为类型中有元变量，Lean 没办法解决它。

就像我们在 多态一开始的描述 里说的那样，元变量代表了程序无法被推断的未知部分。当一个表达式被写在 #eval 后时，Lean 会尝试去自动确定它的类型。在这种情况下，它无法做到自动确定类型。因为 HPlus 的第三个类型参数依然是未知的，Lean 没办法进行类型类实例搜索，但是实例搜索是 Lean 唯一可能确定表达式的类型的方式。也就是说，HPlus Pos Nat Pos 实例只能在表达式的类型为 Pos 时应用，但除了实例本身之外，程序中没有其他东西表明它应该具有这种类型。

一种解决方法是保证全部三个类型都是已知的，通过给整个表达式添加一个类型标记来实现这一点：

1 2	#eval (HPlus.hPlus (3 : Pos) (5 : Nat) : Pos) 8

然而，这种解决方式对使用我们的正数库的用户来说并不是很方便。

输出参数

刚才的问题也可以通过声明 γ 是一个 输出参数（output parameter） 来解决。多数类型类参数是作为搜索算法的输入：它们被用于选取一个实例。例如，在 OfNat 实例中，类型和自然数都被用于选取一个数字字面量的特定解释。然而，在一些情况下，在尽管有些类型参数仍然处于未知状态时就开始进行搜索是更方便的。这样就能使用在搜索中发现的实例来决定元变量的值。在开始搜索实例时不需要用到的参数就是这个过程的结果，该参数使用 outParam 修饰符来声明。

1 2	class HPlus (α : Type) (β : Type) (γ : outParam Type) where hPlus : α → β → γ

有了这个输出参数，类型类实例搜索就能够在不需要知道 γ 的情况下选取一个实例了。例如：

1 2	#eval HPlus.hPlus (3 : Pos) (5 : Nat) 8

在思考时，将输出参数视为定义某种函数可能会有帮助。任意给定的类型类的实例都有一个或更多输出参数提供给 Lean。这能指导 Lean 通过输入（的类型参数）来确定输出（的类型）。一个可能是递归的实例搜索过程，最终会比简单的重载更为强大。输出参数能够决定程序中的其他类型，实例搜索能够将一族附属实例组合成具有这种类型的程序。

默认实例

确定一个参数是否是输入或输出参数控制了 Lean 会在何时启动类型类搜索。具体而言，直到所有输入都变为已知，类型类搜索才会开始。然而，在一些情况下，输出参数是不足的。此时，即使一些输入参数仍然处于未知状态，实例搜索也应该开始。这有点像是 Python 或 Kotlin 中可选函数参数的默认值，但在这里是默认类型。

默认实例 是 当并不是全部输入均为已知时 可用的实例。当一个默认实例能被使用时，他就将会被使用。这能帮助程序成功通过类型检查，而不是因为关于未知类型和元变量的错误而失败。但另一方面，默认类型会让实例选取变得不那么可预测。具体来说，如果一个不合适的实例被选取了，那么表达式将可能具有和预期不同的类型。这会导致令人困惑的类型错误发生在程序中。更聪明做法是根据情况选择要使用默认实例的地方！

默认实例可以发挥作用的一个例子是可以从 Add 实例派生出的 HPlus 实例。换句话说，常规的加法是异质加法在三个参数类型都相同时的特殊情况。这可以用下面的实例来实现：

1 2	instance [Add α] : HPlus α α α where hPlus := Add.add

有了这个实例，hPlus 就可以被用于任何可加的类型，就像 Nat：

1
2
3

#eval HPlus.hPlus (3 : Nat) (5 : Nat)

8

然而，这个实例只会用在两个参数类型都已知的情况下。例如：

1	#check HPlus.hPlus (5 : Nat) (3 : Nat)

产生类型

1	HPlus.hPlus 5 3 : Nat

就像我们预想的那样，但是

1	#check HPlus.hPlus (5 : Nat)

产生了一个包含剩余参数和返回值类型的两个元变量的类型：

1	HPlus.hPlus 5 : ?m.7706 → ?m.7708

在绝大多数情况下，当提供一个加法参数时，另一个参数也会是同一个类型。通过 default_instance 属性来让这个实例成为默认实例：

1
2
3

@[default_instance]
instance [Add α] : HPlus α α α where
  hPlus := Add.add

有了默认实例，这个例子就有了更有用的类型：

1	#check HPlus.hPlus (5 : Nat)

结果为：

1	HPlus.hPlus 5 : Nat → Nat

通过这个语句，每个同时重载了异质和同质运算的运算符，都能在默认实例需要异质运算的语境中使用同质运算。中缀运算符会被替换为异质运算，并且在需要时尽可能选择同质的默认实例。

简单来说，简单地写 5 会给出一个 Nat 而不是一个需要更多信息来选取 OfNat 实例的一个包含元变量的类型。这是因为 OfNat 以 Nat 作为默认实例。

默认实例也可以被赋予 优先级 ，这会影响在可能的应用多于一种的情况下的选择。更多关于默认实例优先级的信息，请查阅 Lean 手册。

自然数 Nat 是 OfNat 的默认实例，源码可以看到：

1
2
3

@[default_instance 100] /- low prio -/
instance instOfNatNat (n : Nat) : OfNat Nat n where
  ofNat := n

练习

定义一个 HMul (PPoint α) α (PPoint α) 的实例，该实例将两个投影都乘以标量。它应适用于任何存在 Mul α 实例的类型 α。例如：

1	#eval {x := 2.5, y := 3.7 : PPoint Float} * 2.0

结果应为

1	{ x := 5.000000, y := 7.400000 }

数组与索引

我们在插曲中描述了如何使用索引符号来通过位置查找列表中的条目。此语法也由类型类管理，并且可以用于各种不同的类型。

回顾目前为止，我们学到的一些缩写记号包括：

{} 用于构造结构体：{a:= .., b:= .., c:= ...}，结合 with 来构造结构体 `{p with a := …}
⟨⟩ 用于按顺序构造结构体：⟨a, b, c⟩ 是一个结构体
[] 用于构造列表 List，用 x :: xs 表达列表的拼接

数组

Lean 中的数组在多数情况下就比链表更为高效。在 Lean 中，Array α 类型是一个动态大小的数组，可以用来装类型为 α 的值。这很像是 Java 中的 ArrayList，C++ 中的 std::vector，或者 Rust 中的 Vec。不像是 List 在每一次用到 cons 构造子的地方都会有一个指针指向每个节点，数组会占用内存中一段连续的空间。这会带来更好的处理器缓存效果。并且，在数组中查找值的时间复杂度为常数，但在链表中查找值所需要的时间则与遍历的节点数量成正比。

在像 Lean 这样的纯函数式语言中，在数据结构中改变某位置上的数据的值是不可能的。相反，Lean 会制作一个副本，该副本具有所需的修改。当使用一个数组时，Lean 编译器和运行时包含了一个优化：当该数组只被引用了一次时，会在幕后将制作副本优化为原地操作。

数组写起来很像列表，只是在开头多了一个 #：

1 2	def northernTrees : Array String := #["sloe", "birch", "elm", "oak"]

数组中值的数量可以通过 Array.size 找到。例如：northernTrees.size 结果是 4。对于小于数组大小的索引值，索引符号可以被用来找到对应的值，就像列表一样。就是说，northernTrees[2] 会被计算为 "elm"。类似地，编译器需要一个索引值未越界的证明。尝试去查找越界的值会导致编译时错误，就和列表一样。例如：northernTrees[8] 的结果为：

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 8 < Array.size northernTrees

非空列表

一个表示非空列表的数据类型可以被定义为一个结构，这个结构有一个列表头字段，和一个尾字段。尾字段是一个常规的，可能为空的列表。

1
2
3

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

例如：非空列表 idahoSpiders（包含了一些美国爱达荷州的本土蜘蛛品种）由 "Banded Garden Spider" 和四种其它蜘蛛构成，一共有五种蜘蛛：

def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}

通过递归函数在列表中查找特定索引的值需要考虑到三种情况：

索引是 0，此时应返回列表头。
索引是 n + 1 并且列表尾是空的，这意味着索引越界了。
索引是 n + 1 并且列表尾非空，此时应该在列表尾上递归调用函数并传入 n。

例如，一个返回 Option 的查找函数可以写成如下形式：

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  -- 如果 tail 空白，且越界
  | {head := _, tail := []}, _ + 1 => none
  -- 如果 tail 非空，递归
  | {head := _, tail := h :: t}, n + 1 => get? {head := h, tail := t} n

每种模式匹配的情况都对应于上面的一种可能性。get? 的递归调用不需要 NonEmptyList 命名空间标识符，因为定义内部隐式地在定义的命名空间中。另一种方式来编写这个函数是：当索引大于零时就将 get? 应用在列表上。

1
2
3

def NonEmptyList.get? : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | xs, n + 1 => xs.tail.get? n

如果列表包含一个条目，那么只有 0 是合法的索引。如果它包含两个条目，那么 0 和 1 是合法的索引。如果它包含三个条目，那么 0, 1, 和 2 都是合法的索引。换句话说，非空列表的合法索引是严格小于列表长度的自然数。同时它也是小于等于列表尾的长度的。

“索引值没有出界”意味着什么的这个定义，应该被写成一个 abbrev。因为这个用来证明索引值未越界的策略（tactics）要在不知道 NonEmptyList.inBounds 这个方法的情况下解决数字之间的不等关系。 (此处原文表意不明，按原文字面意思译出。原文大致意思应为 abbrev 比 def 对 tactic 的适应性更好)

1 2	abbrev NonEmptyList.inBounds (xs : NonEmptyList α) (i : Nat) : Prop := i ≤ xs.tail.length

这个函数返回一个可能为真也可能为假的命题。例如，2 对于 idahoSpiders 未越界，而 5 就越界了。

1
2
3

theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by simp

theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by simp

逻辑非运算符有很低的结合度，这意味着 ¬idahoSpiders.inBounds 5 等价于 ¬(idahoSpiders.inBounds 5)。

这个事实可被用于编写能证明索引值合法的查找函数，并且无需返回一个 Option。该证据会在编译时检查。下面给出代码：

def NonEmptyList.get (xs : NonEmptyList α) (i : Nat) (ok : xs.inBounds i) : α :=
  match i with
  | 0 => xs.head
  | n + 1 => xs.tail[n]

当然，将这个函数写成直接证明的形式也是可能的。但这需要会玩证明和命题的一些技术，这些内容会在本书后续内容中提到。

重载索引

对于列表类型的索引符号，可通过定义 GetElem 类型类的实例来重载。出于灵活性考虑，GetElem 有四个参数：

列表的类型
索引的类型
列表中元素的类型
一个函数，用于确定什么是索引在边界内的证据

元素类型和证明函数都是输出参数。GetElem 有一个方法 getElem，其接受一个列表，一个索引值，和一个索引未越界的证明，并且返回一个元素：

1 2	class GetElem (coll : Type) (idx : Type) (item : outParam Type) (inBounds : outParam (coll → idx → Prop)) where getElem : (c : coll) → (i : idx) → inBounds c i → item

在 NonEmptyList α 中，这些参数是：

列表是 NonEmptyList α
索引的类型是 Nat
元素的类型是 α
索引如果小于等于列表尾那么就没有越界

事实上，GetElem 实例可以直接使用 NonEmptyList.get：

1 2	instance : GetElem (NonEmptyList α) Nat α NonEmptyList.inBounds where getElem := NonEmptyList.get

有了这个实例，NonEmptyList 就和 List 一样方便了。计算 idahoSpiders[0] 结果为 "Banded Garden Spider"，而 idahoSpiders[9] 会导致编译时错误：

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ NonEmptyList.inBounds idahoSpiders 9

因为列表的类型和索引的类型都是 GetElem 类型类的参数，所以可以使用新类型来索引现有的列表。之前的 Pos 是一个完全合理的可以用来索引 List 的类型，但注意它不能指向第一个条目。下面 GetElem 的实例使 Pos 在查找列表条目方面和 Nat 一样方便。

1 2	instance : GetElem (List α) Pos α (fun list n => list.length > n.toNat) where getElem (xs : List α) (i : Pos) ok := xs[i.toNat]

使用非数字索引值来进行索引也可以是合理的。例如：Bool 可以被用于选择结构体的字段，比如我们可以让 false 对应于 x，true 对应于 y：

1
2
3

instance : GetElem (PPoint α) Bool α (fun _ _ => True) where
  getElem (p : PPoint α) (i : Bool) _ :=
    if not i then p.x else p.y

在这个例子中，布尔值都是合法的索引。因为每个可能的 Bool 值都是未越界的，证据我们只需简单地给出 True 命题。

标准类

本节中展示了各种可重载的运算符和函数。在 Lean 中，它们都通过类型类来重载。每个运算符或函数都对应于一个类型类中的方法。不像 C++，Lean 中的中缀操作符定义为命名函数的缩写；这意味着为新类型重载它们不是使用操作符本身，而是使用其底层名称（例如 HAdd.hAdd）。

算术符号

多数算术运算符都是可以进行异质运算的。这意味着参数可能有不同的类型，并且输出参数决定了结果表达式的类型。对于每个异质运算符，都有一个同质运算符与其对应。只要把字母 h 去掉就能找到那个同质运算符了，HAdd.hAdd 对应 Add.add。下面的算术运算符都可以被重载：

Expression	Desugaring	Class Name
`x + y`	`HAdd.hAdd x y`	`HAdd`
`x - y`	`HSub.hSub x y`	`HSub`
`x * y`	`HMul.hMul x y`	`HMul`
`x / y`	`HDiv.hDiv x y`	`HDiv`
`x % y`	`HMod.hMod x y`	`HMod`
`x ^ y`	`HPow.hPow x y`	`HPow`
`(- x)`	`Neg.neg x`	`Neg`

位运算符

Lean 包含了许多标准位运算符，他们也可以用类型类来重载。Lean 中有对于定长类型的实例，例如 UInt8，UInt16，UInt32，UInt64，和 USize。

Expression	Desugaring	Class Name
`x &&& y`	`HAnd.hAnd x y`	`HAnd`
`x
`x ^^^ y`	`HXor.hXor x y`	`HXor`
`~~~ x`	`Complement.complement x`	`Complement`
`x >>> y`	`HShiftRight.hShiftRight x y`	`HShiftRight`
`x <<< y`	`HShiftLeft.hShiftLeft x y`	`HShiftLeft`

由于 And 和 Or 已经是逻辑连接词了，所以 HAnd 和 HOr 的同质对应叫做 AndOp 和 OrOp 而不是 And 和 Or。

相等性与有序性

测试两个值之间的相等性通常会用 BEq 类，该类名是 Boolean equality（布尔等价）的缩写。由于 Lean 是一个定理证明器，所以在 Lean 中其实有两种类型的相等运算符：

布尔等价（Boolean equality） 和你能在其他编程语言中看到的等价是一样的。这是一个接受两个值并且返回一个 Bool 的函数。布尔等价使用两个等号表示，就像在 Python 和 C# 中那样。因为 Lean 是一个纯函数式语言，指针并不能被直接看到，所以引用和值等价并没有符号上的区别。
命题等价（Propositional equality） 是一个 数学陈述（mathematical statement） ，指两个东西是等价的。命题等价并不是一个函数，而是一个可以证明的数学陈述。可以用一个单等号表示。一个命题等价的陈述就像一个能检查等价性证据的类型。

这两种等价都很重要，它们有不同的用处。布尔等价在程序中很有用，有时我们需要考察两个值是否是相等的。例如："Octopus" == "Cuttlefish" 结果为 false，以及 "Octopodes" == "Octo".append "podes" 结果为 true。有一些值，比如函数，无法检查等价性。例如，(fun (x : Nat) => 1 + x) == (Nat.succ ·) 会报错：

1 2	failed to synthesize instance BEq (Nat → Nat)

就像这条信息说的，== 是使用了类型类重载的。表达式 x == y 事实上是 BEq.beq x y 的缩写。

命题等价是一个数学陈述，而不是程序调用。因为命题就像描述一些数学陈述的证据的类型，命题等价和像是 String 和 Nat → List Int 这样的类型有更多的相同之处，而不是布尔等价。这意味着它并不能被自动检查。然而，在 Lean 中，只要两个表达式具有相同的类型，就可以陈述它们的相等性。(fun (x : Nat) => 1 + x) = (Nat.succ ·) 是一个十分合理的陈述。从数学角度来讲，如果两个函数把相等的输入映射到相等的输出，那么这两个函数就是相等的。所以那个陈述是真的，尽管它需要一个两行的证明来让 Lean 相信这个事实。

通常来说，当把 Lean 作为一个编程语言来用时，用布尔值函数会比用命题要更简单。

在 Lean 中，if 语句适用于可判定命题。例如：2 < 4 是一个命题。

1
2
3

#check 2 < 4

2 < 4 : Prop

尽管如此，将其写作 if 语句中的条件是完全可以接受的。例如，if 2 < 4 then 1 else 2 的类型是 Nat，并且计算结果为 1。

并不是所有的命题都是可判定的。如果所有的命题都是可判定的，那么计算机通过运行判定程序就可以证明任何的真命题，数学家们就此失业了。更具体来说，可判定的命题都会有一个 Decidable 类型的实例，实例中的方法是判定程序。因为认为会返回一个 Bool 而尝试去用一个不可判定的命题，最终会报错，因为 Lean 无法找到 Decidable 实例。例如，if (fun (x : Nat) => 1 + x) = (Nat.succ ·) then "yes" else "no" 会导致：

1 2	failed to synthesize instance Decidable ((fun x => 1 + x) = fun x => Nat.succ x)

下面的命题，通常都是重载了可判定类型类的：

Expression	Desugaring	Class Name
`x < y`	`LT.lt x y`	`LT`
`x ≤ y`	`LE.le x y`	`LE`
`x > y`	`LT.lt y x`	`LT`
`x ≥ y`	`LE.le y x`	`LE`

因为还没有演示如何定义新命题，所以定义新的 LT 和 LE 实例可能会比较困难。

另外，使用 <, ==, 和 > 来比较值可能效率不高。首先检查一个值是否小于另一个值，然后再检查它们是否相等，这可能需要对大型数据结构进行两次遍历。为了解决这个问题，Java 和 C# 分别有标准的 compareTo 和 CompareTo 方法，可以通过类来重写以同时实现这三种操作。这些方法在接收者小于参数时返回负整数，等于时返回零，大于时返回正整数。Lean 与其重载整数，不如有一个内置的归纳类型来描述这三种可能性：

inductive Ordering where
| lt
| eq
| gt

Ord 类型类可以被重载，这样就可以用于比较。对于 Pos 一个实现可以是：

def Pos.comp : Pos → Pos → Ordering
  | Pos.one, Pos.one => Ordering.eq
  | Pos.one, Pos.succ _ => Ordering.lt
  | Pos.succ _, Pos.one => Ordering.gt
  | Pos.succ n, Pos.succ k => comp n k

instance : Ord Pos where
  compare := Pos.comp

#eval Ord.compare 1 2 == Ordering.lt -- true

对于 Java 中应该使用 compareTo 的情形，在 Lean 中用 Ord.compare 就对了。

哈希

Java 和 C# 有 hashCode 和 GetHashCode 方法，用于计算值的哈希值，以便在哈希表等数据结构中使用。Lean 中的等效类型类称为 Hashable：

1 2	class Hashable (α : Type) where hash : α → UInt64

对于两个值而言，如果它们根据各自类型的 BEq 实例是相等的，那么它们也应该有相同的哈希值。换句话说，如果 x == y，那么有 hash x == hash y。如果 x ≠ y，那么 hash x 不一定就和 hash y 不一样（毕竟 Nat 有无穷多个，而 UInt64 最多只能有有限种组合方式。），但是如果不一样的值有不一样的哈希值的话，那么建立在其上的数据结构会有更好的表现。这与 Java 和 C# 中对哈希的要求是一致的。

在标准库中包含了一个函数 mixHash，它的类型是 UInt64 → UInt64 → UInt64。它可以用来组合构造子不同字段的哈希值。一个合理的归纳数据类型的哈希函数可以通过给每个构造函数分配一个唯一的数字，然后将该数字与每个字段的哈希值混合来编写。例如，可以这样编写 Pos 的 Hashable 实例：

def hashPos : Pos → UInt64
  | Pos.one => 0
  | Pos.succ n => mixHash 1 (hashPos n)

instance : Hashable Pos where
  hash := hashPos

Hashable 实例对于多态可以使用递归类型搜索。哈希化一个 NonEmptyList α 需要 α 是可以被哈希化的。

1 2	instance [Hashable α] : Hashable (NonEmptyList α) where hash xs := mixHash (hash xs.head) (hash xs.tail)

在二叉树的 BEq 和 Hashable 的实现中，递归和递归实例搜索这二者都被用到了。

inductive BinTree (α : Type) where
  -- 叶子节点（空节点）
  | leaf : BinTree α
  -- 分支节点：左子树 → 节点值 → 右子树
  | branch : BinTree α → α → BinTree α → BinTree α

def eqBinTree [BEq α] : BinTree α → BinTree α → Bool
  -- 两个叶子节点相等
  | BinTree.leaf, BinTree.leaf =>
    true
  -- 分支节点相等需要：节点值相等 且 左右子树都相等
  | BinTree.branch l x r, BinTree.branch l2 x2 r2 =>
    x == x2 && eqBinTree l l2 && eqBinTree r r2
  -- 其他情况（一个是叶子一个是分支）不相等
  | _, _ =>
    false

instance [BEq α] : BEq (BinTree α) where
  beq := eqBinTree

def hashBinTree [Hashable α] : BinTree α → UInt64
  -- 叶子节点的哈希值为 0
  | BinTree.leaf =>
    0
  -- 分支节点的哈希值：混合常数1、左子树哈希、节点值哈希、右子树哈希
  | BinTree.branch left x right =>
    mixHash 1 (mixHash (hashBinTree left) (mixHash (hash x) (hashBinTree right)))

instance [Hashable α] : Hashable (BinTree α) where
  hash := hashBinTree

派生标准类

像 BEq 和 Hashable 这样的类的实例，手动实现起来通常相当繁琐。Lean 包含一个称为 实例派生（instance deriving） 的特性，它使得编译器可以自动构造许多类型类的良好实例。事实上，结构那一节 中 Point 定义中的 deriving Repr 短语就是实例派生的一个例子。

派生实例的方法有两种。第一种在定义一个结构体或归纳类型时使用。在这种情况下，添加 deriving 到类型声明的末尾，后面再跟实例应该派生自的类。对于已经定义好的类型，单独的 deriving 也是可用的。写 deriving instance C1, C2, ... for T 来为类型 T 派生 C1, C2, ... 实例。

Pos 和 NonEmptyList 上的 BEq 和 Hashable 实例可以用很少量的代码派生出来：

1 2	deriving instance BEq, Hashable for Pos deriving instance BEq, Hashable, Repr for NonEmptyList

至少以下几种类型类的实例都是可以派生的：

Inhabited
BEq
Repr
Hashable
Ord

然而，有些时候 Ord 的派生实例可能不是你想要的。当发生这种事情的时候，就手写一个 Ord 实例把。你如果对自己的 Lean 水平足够有自信的话，你也可以自己添加可以派生实例的类型类。

实例派生除了在开发效率和代码可读性上有很大的优势外，它也使得代码更易于维护，因为实例会随着类型定义的变化而更新。对数据类型的一系列更新更易于阅读，因为不需要一行又一行地对相等性测试和哈希计算进行公式化的修改。

连接符

许多数据类型都有某种形式的连接操作符。在 Lean 中，连接两个值的操作被重载为类型类 HAppend，这是一个异质操作，与用于算术运算的操作类似：

1 2	class HAppend (α : Type) (β : Type) (γ : outParam Type) where hAppend : α → β → γ

语法 xs ++ ys 会被脱糖为 HAppend.hAppend xs ys. 对于同质的情形，按照常规模式实现一个 Append 即可：

1
2
3

instance : Append (NonEmptyList α) where
  append xs ys :=
    { head := xs.head, tail := xs.tail ++ ys.head :: ys.tail }

在定义了上面的实例后，

1	#eval idahoSpiders ++ idahoSpiders

就有了下面的结果：

{ head := "Banded Garden Spider",
tail := ["Long-legged Sac Spider",
         "Wolf Spider",
         "Hobo Spider",
         "Cat-faced Spider",
         "Banded Garden Spider",
         "Long-legged Sac Spider",
         "Wolf Spider",
         "Hobo Spider",
         "Cat-faced Spider"] }

类似地：定义一个 HAppend 来使常规列表可以和一个非空列表连接。

1
2
3

instance : HAppend (NonEmptyList α) (List α) (NonEmptyList α) where
  hAppend xs ys :=
    { head := xs.head, tail := xs.tail ++ ys }

有了这个实例后，

1	#eval idahoSpiders ++ ["Trapdoor Spider"]

结果为

1 2	{ head := "Banded Garden Spider", tail := ["Long-legged Sac Spider", "Wolf Spider", "Hobo Spider", "Cat-faced Spider", "Trapdoor Spider"] }

函子

如果一个多态类型重载了一个函数 map，这个函数将位于上下文中的每个元素都用一个函数来映射，那么这个类型就是一个 函子（functor） 。虽然大多数语言都使用这个术语，但C#中等价于 map 的是 System.Linq.Enumerable.Select。例如，用一个函数对一个列表进行映射会产生一个新的列表，列表中的每个元素都是函数应用在原列表中元素的结果。用函数 f 对一个 Option 进行映射，如果 Option 的值为 none，那么结果仍为 none；如果为 some x，那么结果为 some (f x)。

下面是一些函子，这些函子是如何重载 map 的例子：

Functor.map (· + 5) [1, 2, 3] 结果为 [6, 7, 8]
Functor.map toString (some (List.cons 5 List.nil)) 结果为 some "[5]"，打开了 Option 类型，而非 List
Functor.map List.reverse [[1, 2, 3], [4, 5, 6]] 结果为 [[3, 2, 1], [6, 5, 4]]

因为 Functor.map 这个操作很常用，但它的名字又有些长了，所以 Lean 也提供了一个中缀运算符来映射函数，叫做 <$>。下面是一些简单的例子：

(· + 5) <$> [1, 2, 3] 结果为 [6, 7, 8]
toString <$> (some (List.cons 5 List.nil)) 结果为 some "[5]"
List.reverse <$> [[1, 2, 3], [4, 5, 6]] 结果为 [[3, 2, 1], [6, 5, 4]]

Functor 对于 NonEmptyList 的实例需要我们提供 map 函数。

1 2	instance : Functor NonEmptyList where map f xs := { head := f xs.head, tail := f <$> xs.tail }

在这里，map 使用 List 上的 Functor 实例来将函数映射到列表尾。这个实例是在 NonEmptyList 下定义的，而不是 NonEmptyList α。因为类型参数 α 在当前类型类中用不上。 无论条目的类型是什么 ，我们都可以用一个函数来映射 NonEmptyList。如果 α 是类型类的一个参数，那么我们就可以做出只工作在某个 α 类型上的 Functor，比如 NonEmptyList Nat。但成为一个函子类型的必要条件就是 map 对任意条目类型都是有效的。

这里有一个将 PPoint 实现为一个函子的实例：

1 2	instance : Functor PPoint where map f p := { x := f p.x, y := f p.y }

在这里，f 被应用到 x 和 y 上。

即使包含在一个函子类型中的类型本身也是一个函子，映射一个函数也只会向下一层。也就是说，当在 NonEmptyList (PPoint Nat) 上 map 时，被映射的函数会接受 PPoint Nat 作为参数，而不是 Nat。

Functor 类型类的定义中用到了一个还没介绍的语言特性：默认方法定义。正常来说，一个类型类会指定一些有意义的最小的可重载操作集合，然后使用具有隐式实例参数的多态函数，这些函数建立在重载操作的基础上，以提供更大的功能库。例如，函数 concat 可以连接任何非空列表的条目，只要条目是可连接的：

def concat [Append α] (xs : NonEmptyList α) : α :=
  let rec catList (start : α) : List α → α
    | [] => start
    | (z :: zs) => catList (start ++ z) zs
  catList xs.head xs.tail

然而，对于一些类型类，如果你对数据类型的内部又更深的理解的话，那么就会有一些更高效的运算实现。

在这些情况下，可以提供一个默认方法定义。默认方法定义提供了一个基于其他方法的默认实现。然而，实例实现者可以选择用更高效的方法来重写这个默认实现。默认方法定义在 class 定义中，包含 :=。

对于 Functor 而言，当被映射的函数并不需要参数时，许多类型有更高效的 map 实现方式。

class Functor (f : Type → Type) where
  map : {α β : Type} → (α → β) → f α → f β

  mapConst {α β : Type} (x : α) (coll : f β) : f α :=
    map (fun _ => x) coll

可以使用默认实现：

-- 使用默认的 mapConst
[1, 2, 3, 4].mapConst "hello"
===>
Functor.mapConst "hello" [1, 2, 3, 4]
===>
Functor.map (fun _ => "hello") [1, 2, 3, 4]
===>
["hello", "hello", "hello", "hello"]

就像不符合 BEq 的 Hashable 实例是有问题的一样，一个在映射函数时移动数据的 Functor 实例也是有问题的。例如，一个有问题的 List 的 Functor 实例可能会丢弃其参数并总是返回空列表，或者它可能会反转列表。一个有问题的 PPoint 实例可能会将 f x 放在 x 和 y 字段中。具体来说，Functor 实例应遵循两条规则：

映射恒等函数应返回原始参数。
映射两个复合函数应具有与它们的映射组合相同的效果。

更形式化的讲，第一个规则说 id <$> x 等于 x。第二个规则说 map (fun y => f (g y)) x 等于 map f (map g x)。fun y => f (g y) 也可以写成 f ∘ g。这些规则能防止 map 的实现移动数据或删除一些数据。

你也许会遇到的问题

Lean 不能为所有类派生实例。例如代码

1	deriving instance ToString for NonEmptyList

会导致如下错误：

1	default handlers have not been implemented yet, class: 'ToString' types: [NonEmptyList]

调用 deriving instance 会使 Lean 查找一个类型类实例的内部代码生成器的表。如果找到了代码生成器，那么就会调用它来创建实例。然而这个报错就意味着没有发现对 ToString 的代码生成器。

练习

写一个 HAppend (List α) (NonEmptyList α) (NonEmptyList α) 的实例并测试它
为二叉树实现一个 Functor 的实例。

强制转换

在数学中，用同一个符号来在不同的语境中代表数学对象的不同方面是很常见的。例如，如果在一个需要集合的语境中给出了一个环，那么理解为该环对应的集合也是很有道理的。在编程语言中，有一些规则自动地将一种类型转换为另一种类型也是很常见的。例如，Java 允许 byte 自动转换为一个 int，Kotlin 也允许非空类型在可为空的语境中使用。

在 Lean 中，这两个目的都是用一个叫做 强制转换（coercions） 的机制实现的。当 Lean 遇到了在某语境中某表达式的类型与期望类型不一致时，Lean 在报错前会尝试进行强制转换。不像 Java，C，和 Kotlin，强制转换是通过定义类型类实例实现的，并且是可扩展的。

正数

例如，每个正数都对应一个自然数。之前定义的函数 Pos.toNat 可以将一个 Pos 转换成对应的 Nat：

1
2
3

def Pos.toNat : Pos → Nat
  | Pos.one => 1
  | Pos.succ n => n.toNat + 1

函数 List.drop，的类型是 {α : Type} → Nat → List α → List α，它将列表的前缀移除。将 List.drop 应用到 Pos 会产生一个类型错误：

[1, 2, 3, 4].drop (2 : Pos)

application type mismatch
  List.drop 2
argument
  2
has type
  Pos : Type
but is expected to have type
  Nat : Type

因为 List.drop 在定义时，没有让它成为一个类型类的方法，所以它没有办法通过定义新实例的方式来重写。

Coe 类型类描述了类型间强制转换的重载方法。

1 2	class Coe (α : Type) (β : Type) where coe : α → β

一个 Coe Pos Nat 的实例就足够让前边报错的代码正常工作了。

instance : Coe Pos Nat where
  coe x := x.toNat

#eval [1, 2, 3, 4].drop (2 : Pos)

[3, 4]

用 #check 来看隐藏在幕后的实例搜索。

1
2
3

#check [1, 2, 3, 4].drop (2 : Pos)

List.drop (Pos.toNat 2) [1, 2, 3, 4] : List Nat

链式强制转换

在寻找强制转换时，Lean 会尝试通过一系列较小的强制转换来组成一个完整的强制转换。例如，已经存在一个从 Nat 到 Int 的强制转换实例。由于这个实例结合了 Coe Pos Nat 实例，我们就可以写出下面的代码：

1	def oneInt : Int := Pos.one

这个定义用到了两个强制转换：从 Pos 到 Nat，再从 Nat 到 Int。

Lean 编译器在存在循环强制转换的情况下不会陷入无限循环。例如，即使两个类型 A 和 B 可以互相强制转换，在转换中 Lean 也可以找到一个路径。

inductive A where
  | a

inductive B where
  | b

instance : Coe A B where
  coe _ := B.b

instance : Coe B A where
  coe _ := A.a

instance : Coe Unit A where
  coe _ := A.a

def coercedToB : B := ()

提示：双括号 () 是构造子 Unit.unit 的简写。从 Repr B 实例派生，

1	#eval coercedToB

结果为：

B.b

整个过程，() 先被强制转换为 Unit A，然后再被强制转换为 B。

(() : B)
===>
(() : Unit A)
===>
((() : Unit A) : B)

Option 类型类似于 C# 和 Kotlin 中可为空的类型：none 构造子就代表了一个不存在的值。Lean 标准库定义了一个从任意类型 α 到 Option α 的强制转换，效果是会将值包裹在 some 中。这使得 option 类型用起来更像是其他语言中可为空的类型，因为 some 是可以忽略的。例如，可以找到列表中最后一个元素的函数 List.getLast?，就可以直接返回值 x 而无需加上 some：

def List.last? : List α → Option α
  | [] => none
  | [x] => x
  | _ :: x :: xs => last? (x :: xs)

实例搜索找到强制转换，并插入对 coe 的调用，该调用会将参数包装在 some 中。这些强制转换可以是链式的，这样嵌套使用 Option 时就不需要嵌套的 some 构造子：

def perhapsPerhapsPerhaps : Option (Option String) :=
  "Please don't tell me"

#eval perhapsPerhapsPerhaps

-- some (some "Please don't tell me")

仅当 Lean 遇到推断出的类型和剩下的程序需要的类型不匹配时，才会自动使用强制转换。在遇到其它错误时，强制转换不会被使用。例如，如果遇到的错误是实例缺失，强制类型转换不会被使用：

1 2	def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) := 392

1 2	failed to synthesize instance OfNat (Option (Option (Option Nat))) 392

这可以通过手动指定 OfNat 所需的类型来解决：

1 2	def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) := (392 : Nat)

此外，强制转换用一个上箭头手动调用。

1 2	def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) := ↑(392 : Nat)

在一些情况下，这可以保证 Lean 找到了正确的实例。这也会让程序员的意图更加清晰。

非空列表与依值强制转换

当 β 类型中的值可以对应每一个 α 类型中的值时，Coe α β 实例才是合理的。将 Nat 强制转换为 Int 是合理的，因为 Int 类型中包含了全部的自然数。类似地，一个从非空列表到常规列表的强制转换也是合理的，因为 List 类型可以表示每一个非空列表：

1
2
3

instance : Coe (NonEmptyList α) (List α) where
  coe
    | { head := x, tail := xs } => x :: xs

这使得非空列表可以使用全部的 List API。

另一方面，我们不可能写出一个 Coe (List α) (NonEmptyList α) 的实例，因为没有任何一个非空列表可以表示一个空列表。这个限制可以通过其他方式的强制转换来解决，该强制转换被称为 依值强制转换（dependent coercions） 。当是否能将一种类型强制转换到另一种类型依赖于具体的值时，依值强制转换就派上用场了。就像 OfNat 类型类需要具体的 Nat 来作为参数，依值强制转换也接受要被强制转换的值作为参数：

1 2	class CoeDep (α : Type) (x : α) (β : Type) where coe : β

这可以使得只选取特定的值，通过加上进一步的类型类约束或者直接写出特定的构造子。例如，任意非空的 List 都可以被强制转换为一个 NonEmptyList：

1 2	instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where coe := { head := x, tail := xs }

强制转换为类型

在数学中，一个建立在集合上，但是比集合具有额外的结构的概念是很常见的。例如，一个幺半群就是一些集合 S ，一个 S 中的元素 s ，以及一个 S 上结合的二元运算，使得 s 在运算的左侧和右侧都是不变的(neutral)。 S 是这个幺半群的“载体集”。自然数集上的零和加法构成一个幺半群，因为加法是满足结合律的，并且为任何一个数字加零都是恒等的。类似地，自然数上的一和乘法也构成一个幺半群。幺半群在函数式编程中的应用也很广泛：列表，空列表，和连接运算符构成一个幺半群。字符串，空字符串，和连接运算符也构成一个幺半群：

structure Monoid where
  Carrier : Type
  neutral : Carrier
  op : Carrier → Carrier → Carrier

def natMulMonoid : Monoid :=
  { Carrier := Nat, neutral := 1, op := (· * ·) }

def natAddMonoid : Monoid :=
  { Carrier := Nat, neutral := 0, op := (· + ·) }

def stringMonoid : Monoid :=
  { Carrier := String, neutral := "", op := String.append }

def listMonoid (α : Type) : Monoid :=
  { Carrier := List α, neutral := [], op := List.append }

给定一个幺半群，我们就可以写出一个 foldMap 函数，该函数在一次遍历中将整个列表中的元素映射到载体集中，然后使用幺半群的运算符将它们组合起来。由于幺半群有单位元，所以当列表为空时我们就可以返回这个值。又因为运算符是满足结合律的，这个函数的用户不需要关心函数结合元素的顺序到底是从左到右的还是从右到左的。

-- M 是一个的幺半群，f 映射到 M 的群元素，xs 是一个 α 列表
-- 记 op 为乘法，结果为 1 * f(x1) * f(x2) * ... * f(xn)
def foldMap (M : Monoid) (f : α → M.Carrier) (xs : List α) : M.Carrier :=
  let rec go (soFar : M.Carrier) : List α → M.Carrier
    -- 递归终点
    | [] => soFar
    -- 通过 M.op 吞掉头部元素（左乘 soFar）
    | y :: ys => go (M.op soFar (f y)) ys
  -- 从单位元开始作用
  go M.neutral xs

尽管一个幺半群是由三部分信息组成的，但在提及它的载体集时使用幺半群的名字也是很常见的。说“令 A 为一个幺半群，并令 x 和 y 为 A 中的元素”是很常见的，而不是说“令 A 为一个幺半群，并令 x 和 y 为载体集中的元素”。这种方式可以通过定义一种新的强制转换在 Lean 中实现，该转换从幺半群到它的载体集。

在 Lean 中，Sort 是一个特殊概念，指的是用来分类其他类型的"元类型"：

Type：分类那些用来描述数据的类型
- 例如：Nat、String、List Nat 都是 Type
- 这些类型的值是具体的数据：42 : Nat、"hello" : String
Prop：分类那些用来描述命题的类型
- 例如：2 + 2 = 4、∀ n : Nat, n + 0 = n 都是 Prop
- 这些类型的值是证明：2 + 2 = 4 的证明

CoeSort 类型类和 Coe 大同小异，只是要求强制转换的目标一定要是一个 sort ，即 Type 或 Prop。

正如在类型不匹配时会检查 Coe 一样，当在预期为 sort 的上下文中提供了其他东西时，会使用 CoeSort。

比如，当 Lean 期望一个类型，但你提供了一个值时， CoeSort 会被触发

1 2	instance : CoeSort Monoid Type where coe m := m.Carrier

这意味着：

-- 定义一个具体的幺半群
def NatAddMonoid : Monoid := {
  Carrier := Nat,
  neutral := 0,
  op := (· + ·),
}

-- 现在可以直接使用 NatAddMonoid 作为类型！
def example_value : NatAddMonoid := (42 : Nat)
-- 如果用 Coe，此时需要显式地写出转化
-- def example_value : (NatAddMonoid : Type) := (42 : Nat)

-- 等价于
def example_value' : NatAddMonoid.Carrier := (42 : Nat)

有了这个强制转换，类型签名变得不那么繁琐了：

def foldMap (M : Monoid) (f : α → M) (xs : List α) : M :=
  let rec go (soFar : M) : List α → M
    | [] => soFar
    | y :: ys => go (M.op soFar (f y)) ys
  go M.neutral xs

另一个有用的 CoeSort 使用场景是它可以让 Bool 和 Prop 建立联系。就像在有序性和等价性那一节我们提到的，Lean 的 if 表达式需要条件为一个可判定的命题而不是一个 Bool。然而，程序通常需要能够根据布尔值进行分支。Lean 标准库并没有定义两种 if 表达式，而是定义了一种从 Bool 到命题的强制转换，即该 Bool 值等于 true：

1 2	instance : CoeSort Bool Prop where coe b := b = true

如此，这个 sort 将是一个 Prop 而不是 Bool。

因此，这个定义语句是合法的：

1	def a : true := by rfl

强制转换为函数

在编程中，许多常见的数据类型都由一个函数及其附加信息组成。例如，函数可能附带用于日志显示的名称或配置数据。此外，将类型放在结构体字段中（类似于 Monoid 示例）在某些场景下很有意义，特别是当存在多种操作实现方式，且需要比类型类更精细的手动控制时。例如，JSON 序列化器输出值的具体细节可能至关重要，因为其他应用程序可能期望特定的格式。有时，仅从配置数据就能推导出函数本身。

CoeFun 类型类能够将非函数类型的值转换为函数类型的值。CoeFun 接受两个参数：第一个是待转换为函数的值的类型，第二个是输出参数，用于确定应转换为哪种具体的函数类型。

1 2	class CoeFun (α : Type) (makeFunctionType : outParam (α → Type)) where coe : (x : α) → makeFunctionType x

第二个参数本身是一个能够计算类型的函数。在 Lean 中，类型是一等公民，可以像其他值一样作为函数参数传递或作为返回值。

例如，一个给参数加上常量的函数可以表示为对待加数值的包装，而无需定义实际的函数：

1 2	structure Adder where howMuch : Nat

一个给参数加 5 的函数，其 howMuch 字段为 5：

1	def add5 : Adder := ⟨5⟩

Adder 类型本身并非函数，直接将其应用于参数会产生错误：

#eval add5 3

function expected at
  add5
term has type
  Adder

定义一个 CoeFun 实例，让 Lean 将 adder 转换为 Nat → Nat 函数：

instance : CoeFun Adder (fun _ => Nat → Nat) where
  coe a := (· + a.howMuch)

#eval add5 3

8

由于所有 Adder 都应转换为 Nat → Nat 函数，CoeFun 的第二个参数被忽略了（使用 fun _ =>）。

当需要根据值来确定正确的函数类型时，CoeFun 的第二个参数就发挥作用了。例如，给定以下 JSON 值表示：

inductive JSON where
  | true : JSON
  | false : JSON
  | null : JSON
  | string : String → JSON
  | number : Float → JSON
  -- 字典
  | object : List (String × JSON) → JSON
  | array : List JSON → JSON
deriving Repr

JSON 序列化器是一个结构体，它需要包含如何序列化的类型，以及序列化的代码本身：

1
2
3

structure Serializer where
  Contents : Type
  serialize : Contents → JSON

字符串序列化器只需将给定字符串包装在 JSON.string 构造子中：

def Str : Serializer :=
  { Contents := String,
    serialize := JSON.string
  }

要将 JSON 序列化器视为序列化其参数的函数，需要提取可序列化数据的内部类型：

1
2
3

-- 把 Serializer 转化成函数，通过内部的 Contents 函数，来序列化对象
instance : CoeFun Serializer (fun s => s.Contents → JSON) where
  coe s := s.serialize

有了这个实例，序列化器就能直接应用于参数。

def buildResponse (title : String) (R : Serializer) (record : R.Contents) : JSON :=
  JSON.object [
    ("title", JSON.string title),
    ("status", JSON.number 200),
    ("record", R record)
  ]

序列化器可以直接传递给 buildResponse：

#eval buildResponse "Functional Programming in Lean" Str "Programming is fun!"

JSON.object
  [("title", JSON.string "Functional Programming in Lean"),
   ("status", JSON.number 200.000000),
   ("record", JSON.string "Programming is fun!")]

这里虽然 Str "hello" 的效果看起来和 JSON.string "hello" 等价，但前者用 Serializer 统一了这类函数接口，使得其他定义类型的转化器也可以用 buildResponse 函数。

附注：将 JSON 表示为字符串

当 JSON 被编码为 Lean 对象时可能有点难以理解。为了确保序列化的响应符合预期，编写一个简单的从 JSON 到 String 的转换器会很方便。第一步是简化数字的显示。JSON 不区分整数和浮点数，Float 类型可以表示两者。在 Lean 中，Float.toString 包含尾随零。

1
2
3

#eval (5 : Float).toString

"5.000000"

解决方案是编写一个小函数来清理所有尾随零和尾随小数点：

def dropDecimals (numString : String) : String :=
  if numString.contains '.' then
    let noTrailingZeros := numString.dropRightWhile (· == '0')
    noTrailingZeros.dropRightWhile (· == '.')
  else numString

有了这个定义，#eval dropDecimals (5 : Float).toString 结果为 "5"，#eval dropDecimals (5.2 : Float).toString 结果为 "5.2"。

下一步是定义一个辅助函数来连接字符串列表，在中间添加分隔符：

1
2
3

def String.separate (sep : String) : List String -> String
  | [] => ""
  | x :: xs => String.join (x :: xs.map (sep ++ ·))

这个函数用于处理 JSON 数组和对象中的逗号分隔元素。#eval ", ".separate ["1", "2"] 结果为 "1, 2"，#eval ", ".separate ["1"] 结果为 "1"，#eval ", ".separate [] 结果为 ""。

最后，需要一个字符串转义程序来处理 JSON 字符串，以便包含 “Hello!” 的 Lean 字符串可以输出为 ““Hello!””。幸运的是，Lean 编译器已经包含了一个用于转义 JSON 字符串的内部函数，叫做 Lean.Json.escape。要使用这个函数，可以在文件开头添加 import Lean。

将 JSON 值转换为字符串的函数被声明为 partial，因为 Lean 无法确定它是否终止。这是因为函数中 asString 的递归调用被应用于 List.map，这种递归模式过于复杂，Lean 无法确定递归过程中值的规模是否在减小。在只需要生成 JSON 字符串而不需要数学推理的应用中，函数为 partial 不太可能造成问题。

partial def JSON.asString (val : JSON) : String :=
  match val with
  | true => "true"
  | false => "false"
  | null => "null"
  | string s => "\"" ++ Lean.Json.escape s ++ "\""
  | number n => dropDecimals n.toString
  | object members =>
    let memberToString mem :=
      "\"" ++ Lean.Json.escape mem.fst ++ "\": " ++ asString mem.snd
    "{" ++ ", ".separate (members.map memberToString) ++ "}"
  | array elements =>
    "[" ++ ", ".separate (elements.map asString) ++ "]"

有了这个定义，序列化的输出更加易读：

1
2
3

#eval (buildResponse "Functional Programming in Lean" Str "Programming is fun!").asString

"{\\"title\\": \\"Functional Programming in Lean\\", \\"status\\": 200, \\"record\\": \\"Programming is fun!\\"}"

如果不加 partial，这里会报错：

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
a✝ : List JSON
val : JSON
⊢ sizeOf val < 1 + sizeOf a✝

可能会遇到的问题

自然数字面量通过 OfNat 类型类重载。由于强制转换是在类型不匹配时触发，而不是在缺少实例时，所以当某类型的 OfNat 实例缺失时，不会触发强制转换：

1 2	def perhapsPerhapsPerhapsNat : Option (Option (Option Nat)) := 392

1 2	failed to synthesize instance OfNat (Option (Option (Option Nat))) 392

设计原则

强制转换是一个强大的工具，应当负责任地使用。一方面，它可以使 API 更贴近领域使用习惯。这是繁琐的手动转换函数和清晰程序之间的差别。正如 Abelson 和 Sussman 在《计算机程序的构造和解释》（Structure and Interpretation of Computer Programs）（麻省理工学院出版社，1996年）前言中所写：

Programs must be written for people to read, and only incidentally for machines to execute.

写程序须以让人读明白为主，让计算机执行为辅。

明智地使用强制转换可以使代码更加易读——这是与领域专家交流的基础。然而，严重依赖强制转换的 API 有许多限制。在自己的代码中使用强制转换前，应认真考虑这些限制。

首先，强制转换只在类型信息充足、Lean 能够知道所有参与类型的上下文中应用，因为强制转换类型类中没有输出参数。这意味着在函数上添加返回类型注释可以决定是类型错误还是成功应用强制转换。例如，从非空列表到列表的强制转换使以下程序得以运行：

1
2
3

-- def idahoSpiders : NonEmptyList String
def lastSpider : Option String :=
  List.getLast? idahoSpiders

另一方面，如果省略类型注释，那么结果类型就是未知的，Lean 就无法找到对应的强制转换。

def lastSpider :=
  List.getLast? idahoSpiders

application type mismatch
  List.getLast? idahoSpiders
argument
  idahoSpiders
has type
  NonEmptyList String : Type
but is expected to have type
  List ?m.34258 : Type

通常，如果强制转换因某些原因失败，用户会收到原始的类型错误，这使得在强制转换链上定位错误变得困难。

最后，强制转换不会在字段访问符号的上下文中生效。这意味着需要强制转换的表达式与不需要强制转换的表达式之间仍然存在重要区别，这个区别对用户是可见的。

其他便利功能

实例的构造子语法

在幕后，类型类 class 都是一些结构体类型，实例都是那些类型的值。唯一的区别是 Lean 存储关于类型类的额外信息，例如哪些参数是输出参数，和记录要被搜索的实例。虽然结构体类型的值通常要么是用 ⟨...⟩ 定义的，要么是用大括号和字段定义的，而实例通常使用 where 定义，但这两种语法都适用于这两种定义方式。

例如，一个林业应用程序可能会这样表示树木：

structure Tree : Type where
  latinName : String
  commonNames : List String

def oak : Tree :=
  ⟨"Quercus robur", ["common oak", "European oak"]⟩

def birch : Tree :=
  { latinName := "Betula pendula",
    commonNames := ["silver birch", "warty birch"]
  }

def sloe : Tree where
  latinName := "Prunus spinosa"
  commonNames := ["sloe", "blackthorn"]

这些语法都是等价的

类似地，这三种语法也可以用于定义类型类的实例。

class Display (α : Type) where
  displayName : α → String

instance : Display Tree :=
  ⟨Tree.latinName⟩

instance : Display Tree :=
  { displayName := Tree.latinName }

instance : Display Tree where
  displayName t := t.latinName

一般来说，where 语法应该用于实例，单书名号应该用于结构体。当强调一个结构类型非常类似于一个字段被命名的元组，但名字此刻并不重要时，⟨...⟩ 语法会很有用。然而，有些情况用其他方式可能才是合理的。比如，一个库可能提供一个构建实例值的函数。在实例声明中的 := 之后调用这个函数是使用此类函数的最简单方法。

例子

在使用 Lean 代码进行实验时，定义往往比 #eval 或 #check 指令更加便利。首先，定义不会产生任何输出，这有助于让读者将注意力集中在最重要的输出上。其次，从类型签名开始编写 Lean 程序是最简单的方式，这样 Lean 能够提供更多帮助和更好的错误信息。相比之下，#eval 和 #check 在 Lean 能够从表达式推断出类型时使用起来最为简单。第三，#eval 无法用于那些类型没有 ToString 或 Repr 实例的表达式，比如函数。最后，多步骤的 do 语法块、let 表达式以及其他多行语法形式在 #eval 或 #check 中往往需要复杂的括号来区分优先级，在这种情况下插入类型标注会使代码变得难以阅读。

为了解决这些问题，Lean 支持在源码中显式指定示例。示例就像是一个没有名称的定义。例如，一个包含哥本哈根绿地中常见鸟类的非空列表可以这样写：

example : NonEmptyList String :=
  { head := "Sparrow",
    tail := ["Duck", "Swan", "Magpie", "Eurasian coot", "Crow"]
  }

示例也可以通过接受参数来定义函数：

1 2	example (n : Nat) (k : Nat) : Bool := n + k == k + n

虽然这会在幕后创建一个函数，但这个函数没有名称，无法被调用。不过，这对于演示如何在给定类型的任意值或未知值上使用库函数非常有用。在源码中，example 声明最好与解释相关概念的注释配合使用。

总结

类型类和重载

类型类是 Lean 中重载函数和运算符的机制。多态函数可以用于多种类型，但无论使用什么类型，其行为都是一致的。例如，一个连接两个列表的多态函数在使用时不关心列表中元素的类型，但它无法根据具体的元素类型表现出不同的行为。相比之下，使用类型类重载的运算符同样可以用于多种类型，但每个类型都需要提供自己的重载运算实现，这意味着可以根据不同的类型表现出不同的行为。

一个 类型类 包含名称、参数和类体，其中类体由若干个带有类型的名称组成。名称用于引用重载的运算，参数决定了定义的哪些方面可以被重载，类体提供了可重载运算的名称和类型签名。每一个可重载运算都被称为类型类的一个方法。类型类可以为某些方法提供基于其他方法的默认实现，从而使程序员无需手动实现每个重载（当可以自动完成时）。

类型类的实例为给定参数提供方法的具体实现。实例可以是多态的，在这种情况下它们能够适用于多种参数，同时也可以在某些类型存在更高效实现时提供更加特化的实现。

类型类参数分为 输入参数（默认情况）和 输出参数（通过 outParam 修饰）。Lean 只有在所有输入参数不再是元变量时才会开始实例搜索，而输出参数可以在实例搜索过程中被确定。类型类的参数不一定是类型，也可以是普通值。例如，OfNat 类型类用于重载自然数字面量，它将要被重载的 Nat 值本身作为参数，这使得实例可以限制允许的数字范围。

实例可以被标注为 @[default_instance] 属性。当一个实例是默认实例时，它会作为 Lean 因类型中存在元变量而无法找到实例时的回退选择。

常见语法的类型类

Lean 中的大多数中缀运算符都通过类型类进行重载。例如，加法运算符对应于 Add 类型类。大多数运算符都有对应的异构版本，其中两个参数不需要是相同类型。这些异构运算符使用以 H 开头的类型类进行重载，如 HAdd。

索引语法通过 GetElem 类型类进行重载，该类型类涉及证明。GetElem 有两个输出参数：要从集合中提取的元素类型，以及用于确定索引值是否在集合边界内的证据函数。这个证据通过命题来描述，Lean 在使用数组索引时会尝试证明这个命题。当 Lean 在编译时无法检查列表或数组访问操作是否越界时，可以通过在索引操作后添加 ? 将检查推迟到运行时。

函子

一个函子是一个支持映射运算的泛型。这个映射运算“在原地”映射所有的元素，不会改变其他结构。例如，列表是函子，所以列表上的映射不会删除，复制或混合列表中的元素。

虽然函子是通过拥有 map 方法来定义的，但 Lean 中的 Functor 类型类还包含一个额外的默认方法，该方法负责将常量函数映射到值上，将所有类型由多态类型变量给出的值替换为同一个新值。对于某些函子，这比遍历整个结构更加高效。

派生实例

许多类型类都有非常标准的实现。例如，布尔相等类型类 BEq 通常的实现方式是先检查两个参数是否使用相同的构造器，然后检查它们的所有参数是否相等。这些类型类的实例可以自动创建。

在定义归纳类型或结构体时，在声明末尾添加 deriving 子句会使实例自动创建。此外，deriving instance ... for ... 命令可以在数据类型定义之外使用来生成实例。由于每个可以派生实例的类都需要特殊处理，因此并非所有类都是可派生的。

强制转换

强制转换允许 Lean 通过插入一个将数据从一种类型转换为另一种类型的函数调用，从原本会出现的编译时错误中恢复。例如，从任意类型 α 到类型 Option α 的强制转换使得值可以直接写出，而不需要用 some 构造器包装，这使得 Option 的工作方式更像面向对象语言中的可空类型。

存在多种不同类型的强制转换，它们可以从不同类型的错误中恢复，并且都由各自的类型类来表示。Coe 类型类用于从类型错误中恢复。当 Lean 遇到类型为 α 的表达式，但上下文期望类型为 β 的表达式时，Lean 会首先尝试构建一个能将 α 强制转换为 β 的转换链，只有在无法做到这一点时才会显示错误。CoeDep 类将被强制转换的具体值作为额外参数，这允许对该值进行进一步的类型类搜索，或者在实例中使用构造器来限制转换的适用范围。CoeFun 类在编译函数应用时会拦截“不是函数”的错误，并允许将函数位置的值转换为实际函数（如果可能的话）。

Lean 函数式编程(一) | 了解 Lean

发表于 2025-10-09 更新于 2025-10-19 分类于 LEAN 阅读次数：字数： 19k 时间 ≈ 1:10

关于 Lean 的函数式编程第一章，编程基础，了解 Lean 的基本概念，包括数据结构，多态，以及语法特性。

阅读全文 »

Blueprint 技术指南｜构建数学协作新生态

发表于 2025-07-26 更新于 2025-07-30 阅读次数：字数： 2.8k 时间 ≈ 10 分钟

探索数学形式化的新工具，管理大型证明项目的得力助手

阅读全文 »

Lean4 项目实战指南

发表于 2025-02-14 更新于 2025-07-11 分类于形式化阅读次数：字数： 2.5k 时间 ≈ 9 分钟

前文对 Lean 开发三件套工具(elan、lake 和 lean)进行了介绍，这些工具的组合类似于 Rust 的 rustup + cargo + rustc 或 Node.js 的 nvm + npm + node 等语言生态中的工具链。在介绍了 Lean 项目的基本结构和文件组织方式后，本文将通过实战演练，展示 Lean 项目的完整开发流程，包括项目创建、依赖管理与配置、元编程代码编写，以及测试、自动化和收录等环节。

阅读全文 »

Lean4 REPL 使用教程

发表于 2024-12-29 分类于形式化阅读次数：字数： 6.6k 时间 ≈ 24 分钟

REPL (Read-Eval-Print Loop) 是一个交互式编程环境，它允许用户输入命令，执行并看到结果。Lean 4 REPL 基于 JSON 通信的交互式环境，它支持三种工作模式。

阅读全文 »

Lean 教程(二) ｜函数式编程

发表于 2024-12-15 更新于 2025-10-09 阅读次数：字数： 512 时间 ≈ 2 分钟

学习 Lean 的途径很多，具体取决于你的背景和偏好，这些教程有偏重数学的也有偏重编程的。

阅读全文 »

本书的目的

本书的结构

「元」是什么？

元编程示例

引入符号（定义新语法）

构建命令

构建 DSL 和语法

编写我们自己的策略

Monads

检查none：避免重复代码

中缀运算符

错误消息的传递

日志记录

对树节点编号

单子：一种函数式设计模式

Monad 类型类

通用的单子运算符

The Identity Monad

恒等单子

The Monad Contract

单子约定

Exercises

练习

Mapping on a Tree

映射一棵树

The Option Monad Contract

Option单子的约定

Example: Arithmetic in Monads

例子：利用单子实现算术表达式求值

Arithmetic Expressions

算术表达式

Evaluating Expressions

对表达式求值

Further Effects

额外的作用

No Effects

无作用

Nondeterministic Search

非确定性搜索

Custom Environments

自定义环境

Exercises

练习

Checking Contracts

检查约定

Readers with Failure

允许Reader失败

A Tracing Evaluator

带有跟踪信息的求值器

do-Notation for Monads

单子的 do-记法

Exercises

练习

The IO Monad

IO 单子

Additional Conveniences

其他便利功能

Shared Argument Types

共享参数类型

Leading Dot Notation

开头的点号

Or-Patterns

或-模式

Summary

总结

Encoding Side Effects

编码副作用

The Monad Type Class

单子类型类

do-Notation for Monads

单子的 do-记法

Custom Monads

定制单子

The IO Monad

IO 单子

重载与类型类

正整数

自定义类型

类与实例

重载加法

检查`none`：避免重复代码

`do`-Notation for Monads

单子的 `do`-记法

`do`-Notation for Monads

单子的 `do`-记法

The `IO` Monad

`IO` 单子