5.3. 应用函子约定🔗

就像 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 xsome (f ∘ ·) <*> some g <*> some xsome (f ∘ g) <*> some xsome ((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 xf <$> some xsome (f x)

在第四种情形中，假设 u 是 some f，因为如果它是 none，则等式两边都是 none。 some f <*> some x 直接求值为 some (f x)，some (fun g => g x) <*> some f 亦然。

5.3.1. 所有应用函子都是函子🔗

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。这是应用函子尊重函数复合这一规则的一个实例。

这证明了如下 Applicative 定义的合理性：它扩展 Functor，并给出用 pure 和 seq 表示的 map 的默认定义：

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

5.3.2. 所有单子都是应用函子🔗

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 (id y) 就是 v >>= fun y => pure y。因为 fun x => f x 与 f 相同，所以这与 v >>= pure 相同；再利用 pure 是 >>= 的右单位元这一事实，可以得到 v。

这种非形式化推理可以通过稍作重新排版而变得更易读。在下表中，将“EXPR1 ={ REASON }= EXPR2”读作“EXPR1 与 EXPR2 相同，因为 REASON”：

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

v

要检查它是否尊重函数复合，需检查 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)

这说明可以合理地定义一个扩展 Applicative 的 Monad，并为 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 实例。

5.3.3. 附加约定🔗

除了遵守与每个类型类相关联的各自约定之外，组合实现 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 <*> notArgmatch 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 := [] }