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

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

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

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

算术表达式

一条算术表达式要么是一个字面量(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

表达式 2 + 3 表示为：

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

而 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)))

对表达式求值

由于表达式包含除法，而除以零是未定义的，因此求值可能会失败。 表示失败的一种方法是使用 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)

此定义使用 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

运行 #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

唯一区别是：类型签名提到的是 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

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

#eval evaluateM applyPrimOption fourteenDivided

none

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

#eval evaluateM applyPrimExcept fourteenDivided

Except.error "Tried to divide 14 by zero"

代码仍有改进空间。 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

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

额外的作用

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

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

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

inductive CanFail where
  | div

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

第二步是将 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

无作用

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

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

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

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

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

-9

非确定性搜索

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

求值结果现在变成一个多重集合(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 \} \)。

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

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

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

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

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

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

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

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

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

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

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

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

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和 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

空集是 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}。

最后，要检查 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}，则：

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

与此类似，

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

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

由此得到的单子实例为：

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

利用此单子，下例可找到列表中所有加起来等于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))

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

让我们回到产生多重集合的算术求值器，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)

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

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]

自定义环境

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

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

将函数当作单子，这通常称为 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 \) 用于运算符未知的情况。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

对任意函数 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

因为 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

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

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

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

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

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

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

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)

将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

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

练习

检查约定

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

允许Reader失败

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

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

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

要做的是：

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

带有跟踪信息的求值器

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

inductive ToTrace (α : Type) : Type where
  | trace : α → ToTrace α

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

要做的是：

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

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

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)))

将有如下结果

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

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

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