应用函子的契约

就像 Functor、Monad 以及实现了 BEq 和 Hashable 的类型一样，Applicative 也有一套所有实例都应遵守的规则。

应用函子应该遵循四条规则：

应遵循同一律，即 pure id <*> v = v
应遵循函数复合律，即 pure (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)
对纯操作进行排序应等同于无操作，即 pure f <*> pure x = pure (f x)
纯操作的顺序不应影响结果，即 u <*> pure x = pure (fun f => f x) <*> u

要检验对于 Applicative Option 实例的这些规则，首先将 pure 展开为 some。

第一条规则表明 some id <*> v = v。 Option 的 seq 定义指明，这与 id <$> v = v 相同，这是已被检查过的 Functor 规则之一。

第二条规则指出 some (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)。如果 u、v 或 w 中有任何一个是 none，则两边均为 none，因此该属性成立。假设 u 是 some f，v 是 some g，w 是 some x，那么这等价于声明 some (· ∘ ·) <*> some f <*> some g <*> some x = some f <*> (some g <*> some x)。对两边求值得到相同的结果：

some (· ∘ ·) <*> some f <*> some g <*> some x
===>
some (f ∘ ·) <*> some g <*> some x
===>
some (f ∘ g) <*> some x
===>
some ((f ∘ g) x)
===>
some (f (g x))

some f <*> (some g <*> some x)
===>
some f <*> (some (g x))
===>
some (f (g x))

第三条规则直接源于 seq 的定义：

some f <*> some x
===>
f <$> some x
===>
some (f x)

在第四种情况下，假设 u 是 some f，因为如果它是 none，则等式的两边都是 none。 some f <*> some x 的求值结果直接为 some (f x)，正如 some (fun g => g x) <*> some f 也是如此。

所有的应用函子都是函子

Applicative 的两个运算符足以定义 map：

def map [Applicative f] (g : α → β) (x : f α) : f β :=
  pure g <*> x

但是，只有当 Applicative 的契约保证了 Functor 的契约时，这才能用来实现 Functor。 Functor 的第一条规则是 id <$> x = x，这直接源于 Applicative 的第一条规则。 Functor 的第二条规则是 map (f ∘ g) x = map f (map g x)。在这里展开 map 的定义会得到 pure (f ∘ g) <*> x = pure f <*> (pure g <*> x)。使用将纯操作进行排序视为无操作的规则，其左侧可以重写为 pure (· ∘ ·) <*> pure f <*> pure g <*> x。这是应用函子遵守函数复合规则的一个实例。

这证明了定义一个扩展自 Functor 的 Applicative 是合理的，其中 map 的默认定义可以用 pure 和 seq 来表示：

class Applicative (f : Type → Type) extends Functor f where
  pure : α → f α
  seq : f (α → β) → (Unit → f α) → f β
  map g x := seq (pure g) (fun () => x)

所有单子都是应用函子

Monad 的一个实例已经需要实现 pure。结合 bind，这足以定义 seq：

def seq [Monad m] (f : m (α → β)) (x : Unit → m α) : m β := do
  let g ← f
  let y ← x ()
  pure (g y)

再一次，检验 Monad 的契约暗含 Applicative 的契约，如果 Monad 扩展自 Applicative，这将允许将其用作 seq 的默认定义。

本节的其余部分包含一个论点，即基于 bind 的 seq 的这种实现实际上满足了 Applicative 契约。函数式编程的一个美妙之处在于，这种论点可以用铅笔在纸上完成，使用表达式求值初步小节中的求值规则。在阅读这些论点时，思考操作的含义有时有助于理解。

将 do 表示法替换为 >>= 的显式使用可以更容易地应用 Monad 规则：

def seq [Monad m] (f : m (α → β)) (x : Unit → m α) : m β := do
  f >>= fun g =>
  x () >>= fun y =>
  pure (g y)

为了检查这个定义遵循恒等性，请检验 seq (pure id) (fun () => v) = v。左侧等价于 pure id >>= fun g => (fun () => v) () >>= fun y => pure (g y)。中间的单位函数可以立即消除，得到 pure id >>= fun g => v >>= fun y => pure (g y)。利用 pure 是 >>= 的左恒等性这一事实，其等同于 v >>= fun y => pure (id y)，也就是 v >>= fun y => pure y。因为 fun x => f x 与 f 是相同的，所以这与 v >>= pure 相同，并且 pure 是 >>= 的右恒等性可以被用来获取 v。

这种非正式的推理可以通过稍微的重新编排来使其更易阅读。在下表中，读取 "EXPR1 ={ REASON }= EXPR2" 时，请将其理解为 "EXPR1 因为 REASON 与 EXPR2 相同":

pure id >>= fun g => v >>= fun y => pure (g y)

={ pure is a left identity of >>= }=

v >>= fun y => pure (id y)

={ Reduce the call to id }=

v >>= fun y => pure y

={ fun x => f x is the same as f }=

v >>= pure

={ pure is a right identity of >>= }=

要检查它遵守函数复合的规则，请验证 pure (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)。第一步是用 seq 的这个定义替换 <*>。之后，使用 Monad 契约中的恒等律和结合律规则的一系列（有点长的）步骤，以从一个得到另一个：

seq (seq (seq (pure (· ∘ ·)) (fun _ => u))
      (fun _ => v))
  (fun _ => w)

={ Definition of seq }=

((pure (· ∘ ·) >>= fun f =>
   u >>= fun x =>
   pure (f x)) >>= fun g =>
  v >>= fun y =>
  pure (g y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

={ pure is a left identity of >>= }=

((u >>= fun x =>
   pure (x ∘ ·)) >>= fun g =>
   v >>= fun y =>
  pure (g y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

={ Insertion of parentheses for clarity }=

((u >>= fun x =>
   pure (x ∘ ·)) >>= (fun g =>
   v >>= fun y =>
  pure (g y))) >>= fun h =>
 w >>= fun z =>
 pure (h z)

={ Associativity of >>= }=

(u >>= fun x =>
  pure (x ∘ ·) >>= fun g =>
 v  >>= fun y => pure (g y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

={ pure is a left identity of >>= }=

(u >>= fun x =>
  v >>= fun y =>
  pure (x ∘ y)) >>= fun h =>
 w >>= fun z =>
 pure (h z)

={ Associativity of >>= }=

u >>= fun x =>
v >>= fun y =>
pure (x ∘ y) >>= fun h =>
w >>= fun z =>
pure (h z)

={ pure is a left identity of >>= }=

u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure ((x ∘ y) z)

={ Definition of function composition }=

u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure (x (y z))

={ Time to start moving backwards!pure is a left identity of >>= }=

u >>= fun x =>
v >>= fun y =>
w >>= fun z =>
pure (y z) >>= fun q =>
pure (x q)

={ Associativity of >>= }=

u >>= fun x =>
v >>= fun y =>
 (w >>= fun p =>
  pure (y p)) >>= fun q =>
 pure (x q)

={ Associativity of >>= }=

u >>= fun x =>
 (v >>= fun y =>
  w >>= fun q =>
  pure (y q)) >>= fun z =>
 pure (x z)

={ This includes the definition of seq }=

u >>= fun x =>
seq v (fun () => w) >>= fun q =>
pure (x q)

={ This also includes the definition of seq }=

seq u (fun () => seq v (fun () => w))

以检验对纯操作进行排序为无操作：

seq (pure f) (fun () => pure x)

={ Replacing seq with its definition }=

pure f >>= fun g =>
pure x >>= fun y =>
pure (g y)

={ pure is a left identity of >>= }=

pure f >>= fun g =>
pure (g x)

={ pure is a left identity of >>= }=

pure (f x)

最后，以检验纯操作的顺序是无关紧要的：

seq u (fun () => pure x)

={ Definition of seq }=

u >>= fun f =>
pure x >>= fun y =>
pure (f y)

={ pure is a left identity of >>= }=

u >>= fun f =>
pure (f x)

={ Clever replacement of one expression by an equivalent one that makes the rule match }=

u >>= fun f =>
pure ((fun g => g x) f)

={ pure is a left identity of >>= }=

pure (fun g => g x) >>= fun h =>
u >>= fun f =>
pure (h f)

={ Definition of seq }=

seq (pure (fun f => f x)) (fun () => u)

这证明了 Monad 的定义扩展自 Applicative，并提供一个 seq 的默认定义：

class Monad (m : Type → Type) extends Applicative m where
  bind : m α → (α → m β) → m β
  seq f x :=
    bind f fun g =>
    bind (x ()) fun y =>
    pure (g y)

Applicative 自身对 map 的默认定义意味着每个 Monad 实例都会自动生成 Applicative 和 Functor 实例。

附加规定

除了遵守每个类型类相关的单独契约之外，Functor、Applicative 和 Monad 的组合实现应与这些默认实现等效。换句话说，一个同时提供 Applicative 和 Monad 实例的类型，其 seq 的实现不应与 Monad 实例生成的默认实现不同。这很重要，因为多态函数可以被重构，以使用 <*> 的等效使用去替换 >>=，或者用 >>= 的等效使用去替换 <*>。这种重构不应改变使用该代码的程序的含义。

这条规则解释了为什么在 Monad 实例中不应使用 Validate.andThen 来实现 bind。就其本身而言，它遵守单子契约。然而，当它用于实现 seq 时，其行为并不等同于 seq 本身。要了解它们的区别，举一个两个计算都返回错误的例子。首先来看一个应该返回两个错误的情况，一个来自函数验证（这也可能是由函数先前的一个参数导致的），另一个来自参数验证：

def notFun : Validate String (Nat → String) :=
  .errors { head := "First error", tail := [] }

def notArg : Validate String Nat :=
  .errors { head := "Second error", tail := [] }

将它们与 Validate 的 Applicative 实例中的 <*> 版本结合起来，会导致两个错误都被报告给用户：

notFun <*> notArg
===>
match notFun with
| .ok g => g <$> notArg
| .errors errs =>
  match notArg with
  | .ok _ => .errors errs
  | .errors errs' => .errors (errs ++ errs')
===>
match notArg with
| .ok _ => .errors { head := "First error", tail := [] }
| .errors errs' => .errors ({ head := "First error", tail := [] } ++ errs')
===>
.errors ({ head := "First error", tail := [] } ++ { head := "Second error", tail := []})
===>
.errors { head := "First error", tail := ["Second error"]}

使用由 >>= 实现的 seq 版本（这里重写为 andThen）会导致只出现第一个错误：

seq notFun (fun () => notArg)
===>
notFun.andThen fun g =>
notArg.andThen fun y =>
pure (g y)
===>
match notFun with
| .errors errs => .errors errs
| .ok val =>
  (fun g =>
    notArg.andThen fun y =>
    pure (g y)) val
===>
.errors { head := "First error", tail := [] }

Lean 函数式编程

应用函子的契约

所有的应用函子都是函子

所有单子都是应用函子

附加规定