Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment