LawfulApplicative

LawfulApplicative 型クラスは、Applicative 型クラスのインスタンスが満たすべき法則を明文化したものです。LawfulApplicative クラスのインスタンスになっていることで、「Applicative 型クラスは、関数適用の一般化であり、計算効果をエンコードしている」という意味論が適切であることが保証されます。

定義

LawfulApplicative は、おおむね次のように定義されています。

variable {α β γ : Type}

/-- アプリカティブ則 -/
class LawfulApplicative (f : Type → Type) [Applicative f] : Prop extends LawfulFunctor f where
  /-- `pure` が `seq` の直前にくる場合、その部分はただの `Functor.map` と同じになる -/
  pure_seq (g : α → β) (x : f α) : pure g <*> x = g <$> x

  /-- `pure` の結果に関数を `map` することは、その関数を `pure` の内部で適用することと同じ。 -/
  map_pure (g : α → β) (x : α) : g <$> (pure x : f α) = pure (g x)

  /-- `seq` の後に `pure` を使うことは、`Functor.map` と同じになる。 -/
  seq_pure (g : f (α → β)) (x : α) : g <*> pure x = (fun h => h x) <$> g

  /--
  `seq` は結合的である。

  計算の順序を保ったまま `seq` 呼び出しの入れ子構造を変えても、同値な計算になる。
  これは、`seq` が単に順序付け以上のことはしていないことを意味する。
  -/
  seq_assoc (x : f α) (g : f (α → β)) (h : f (β → γ)) : h <*> (g <*> x) = ((@Function.comp α β γ) <$> h) <*> g <*> x

Applicative 則の帰結

variable {F : Type → Type} [Applicative F] [LawfulApplicative F]
variable {A B C D : Type}

/-- `pure`を介して関数適用と`<*>`が整合している -/
example {x : A} {f : A → B} : pure f <*> (pure x : F A) = pure (f x) := calc
  _ = f <$> pure x := by rw [pure_seq]
  _ = pure (f x) := by rw [map_pure]