Instantly share code, notes, and snippets.

Last active Jun 26, 2018
draft

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)