draft

monad-interchange.md

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)