应用函子的契约

就像 FunctorMonad 以及实现了 BEqHashable 的类型一样,Applicative 也有一套所有实例都应遵守的规则。

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

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

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

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

第二条规则指出 some (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)。如果 uvw 中有任何一个是 none,则两边均为 none,因此该属性成立。假设 usome fvsome gwsome 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)

在第四种情况下,假设 usome f,因为如果它是 none,则等式的两边都是 nonesome 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 的契约时,这才能用来实现 FunctorFunctor 的第一条规则是 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。这是应用函子遵守函数复合规则的一个实例。

这证明了定义一个扩展自 FunctorApplicative 是合理的,其中 map 的默认定义可以用 pureseq 来表示:

class Applicative (f : TypeType) 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 的默认定义。

本节的其余部分包含一个论点,即基于bindseq 的这种实现实际上满足了 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 xf 是相同的,所以这与 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 >>= }=
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)

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

class Monad (m : TypeType) 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 实例都会自动生成 ApplicativeFunctor 实例。

附加规定

除了遵守每个类型类相关的单独契约之外,FunctorApplicativeMonad 的组合实现应与这些默认实现等效。换句话说,一个同时提供 ApplicativeMonad 实例的类型,其 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 := [] }

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

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 := [] }