A monad is also a applicative functor, that seems pretty obvious, right?
Let's formalize this idea a bit:
This is record that houses the laws of applicative functors.
record IsApplicative {ℓ} (F : Set ℓ → Set ℓ)
(pure : {A : Set ℓ} → A → F A)
(_⊛_ : {A B : Set ℓ} → (F (A → B)) → F A → F B)
: Set (suc ℓ) where
field
identity : {A : Set ℓ} (x : F A) → pure id ⊛ x ≡ x
compose : {A B C : Set ℓ} (f : F (B → C)) (g : F (A → B))
→ (x : F A)
→ ((pure _∘′_ ⊛ f) ⊛ g) ⊛ x ≡ f ⊛ (g ⊛ x)
homo : ∀ {A B} (f : A → B) (x : A)
→ pure f ⊛ pure x ≡ pure (f x)
interchange : ∀ {A B} (f : F (A → B)) (x : A)
→ f ⊛ pure x ≡ pure (λ f → f x) ⊛ f
Given the definition of the carrier F : Set ℓ → Set ℓ
and both operations pure : {A : Set ℓ} → A → F A
and _⊛_ : {A B : Set ℓ} → (F (A → B)) → F A → F B
,
the 4 properties listed above should hold.
To prove that a monad is also a applicative functor, we need to provide the definition of pure
and _⊛_
in terms of return
and _>>=_
pure = return
_⊛_ = λ fs xs → fs >>= λ f → xs >>= λ x → return (f x)
Now, let's do some equation reasoning, and see if we can prove that interchange : ∀ {A B} (f : F (A → B)) (x : A) → f ⊛ pure x ≡ pure (λ f → f x) ⊛ f
holds.
Rewrite pure
and _⊛_
with return
and _>>=_
, we get:
interchange = λ fs x →
begin
(fs >>= λ f → return x >>= λ x' → return (f x'))
≡⟨ ? ⟩
(return (λ g → g x) >>= (λ g' → fs >>= (λ f → return (g' f))))
∎
With the left-identity law of monad: return x >>= g ≡ g x
, we can do something about the RHS of the equation and make both sides closer:
interchange = λ fs x →
begin
(fs >>= λ f → return x >>= λ x' → return (f x'))
≡⟨ ? ⟩
(fs >>= λ f → return (f x))
≡⟨ sym (Mon.left-identity (λ f → f x) (λ f' → fs >>= (λ f → return (f' f)))) ⟩
(return (λ g → g x) >>= (λ g' → fs >>= (λ f → return (g' f))))
∎
Rephrase both sides of the equation using do-notation, we get:
f ← fs
x' ← return x
return (f x')
and
f ← fs
return (f x)
It's tempting to remove the line x' ← return x
and replace x'
with x
,
and the left-identity law return x >>= g ≡ g x
seems to fit the job, right?
Nope.
(WIP)