アプリカティブ関手の約定

Functor や Monad 、BEq と Hashable を実装した型と同じように、Applicative にはすべてのインスタンスで順守すべきルールがあります。

アプリカティブ関手は以下の4つのルールに従わなければなりません：

恒等性に配慮すべき、つまり pure id <*> v = v
合成に配慮すべき、つまり pure (· ∘ ·) <*> u <*> v <*> w = u <*> (v <*> w)
pure演算を連ねても何も起こらないこと、つまり pure f <*> pure x = pure (f x)
pure演算は実行順序によらないこと、つまり u <*> pure x = pure (fun f => f x) <*> u

これらを Applicative Option のインスタンスでチェックするには、まず pure を some に展開します。

最初のルールは some id <*> v = v です。Option の seq の定義によると、これは id <$> v = v と同じであり、この式はすでにチェック済みの Functor についてのルールのひとつです。

2つ目のルールは 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))

3つ目のルールは、seq の定義から直接導かれます：

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

4つ目のケースでは u を some f と仮定します。というのも、もし none であれば、等式の両辺は none になるからです。some f <*> some x は some (f x) へ直接評価され、some (fun g => g x) <*> some f も同じ式へ評価されます。

すべてのアプリカティブ関手は関手

map を定義するには、Applicative の2つの演算子で事足ります：

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

ただし、これは Applicative の約定が Functor の約定を保証している場合にのみ Functor の実装に使うことができます。Functor の最初のルールは id <$> x = x で、これは Applicative の最初のルールから直接導かれます。Functor の2番目のルールは map (f ∘ g) x = map f (map g x) です。ここで map の定義を展開すると pure (f ∘ g) <*> x = pure f <*> (pure g <*> x) となります。pure演算の連続は何も起こらないというルールを使えば、左辺は 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)

すべてのモナドはアプリカティブ関手

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 の約定を満たすという議論からなります。関数型プログラミングの素晴らしい点の1つは、このような論証が式の評価に関する最初の節　にある評価ルールなどを使って、鉛筆で紙の上に書くことができることです。こうした議論を読みながら操作の意味を考えることは理解の助けになり得ます。

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

pure演算の列が何もしないことのチェックは次のようになります：

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)

そして最後に、pure演算の順序が重要でないことを確認します：

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 インスタンスの両方を提供する型は、Monad インスタンスがデフォルトの実装として生成するバージョンと異なる動作をする seq の実装を持つべきではありません。これは多相関数をリファクタリングして >>= を等価な <*> に置き換えたり、<*> を等価な >>= に置き換えたりする場合があるため重要です。このリファクタリングによって、このコードを使用するプログラムの意味が変わることはあってはなりません。

このルールは、前節においてなぜ Validate.andThen を Monad インスタンスの bind の実装に使ってはいけないのかを説明します。この関数自体はモナドの約定に従います。しかし、seq を実装するために使用した場合、その動作は seq 自体と同等になりません。両者の違いを見るために、エラーを返す2つの計算を例にとってみましょう。2つのエラーを返すべきケースの例から始めると、1つは関数をバリデーションした結果（これは関数に先に渡された引数によるものでも同様に発生します）、もう1つは引数のバリデーションによるものです：

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

Functional Programming in Lean 日本語訳

アプリカティブ関手の約定

すべてのアプリカティブ関手は関手

すべてのモナドはアプリカティブ関手

追加の条項