Proving Composition Law for Maybe Applicative

Question

So, I wanted to manually prove the Composition law for Maybe applicative which is:

u <*> (v <*> w) = pure (.) <*> u <*> v <*> w

I used these steps to prove it:

u <*> (v <*> w)          [Left hand side of the law]
  = (Just f) <*> (v <*> w)  [Assume u ~ Just f]
  = fmap f (v <*> w)
  = fmap f (Just g <*> w)   [Assume v ~ Just g]
  = fmap f (fmap g w)
  = fmap (f . g) w

pure (.) <*> u <*> v <*> w  [Right hand side of the law]
  = Just (.) <*> u <*> v <*> w
  = fmap (.) u <*> v <*> w
  = fmap (.) (Just f) <*> v <*> w  [Replacing u with Just f]
  = Just (f .) <*> v <*> w
  = Just (f .) <*> Just g <*> w    [Replacing v with Just g]
  = fmap (f .) (Just g) <*> w
  = Just (f . g) <*> w
  = fmap (f . g) w

Is proving like this correct? What really concerns me is that I assume u and v for some functions embedded in Just data constructor to proceed with my proof. Is that acceptable? Is there any better way to prove this?

Answer 1

Applicative functor expressions are just function applications in the context of some functor. Hence:

pure f <*> pure a <*> pure b <*> pure c

-- is the same as:

pure (f a b c)

We want to prove that:

pure (.) <*> u <*> v <*> w == u <*> (v <*> w)

Consider:

u = pure f
v = pure g
w = pure x

Therefore, the left hand side is:

pure (.) <*> u <*> v <*> w

pure (.) <*> pure f <*> pure g <*> pure x

pure ((.) f g x)

pure ((f . g) x)

pure (f (g x))

pure f <*> pure (g x)

pure f <*> (pure g <*> pure x)

u <*> (v <*> w)

For Maybe we know that pure = Just. Hence if u, v and w are Just values then we know that the composition law holds.

However, what if any one of them is Nothing? We know that:

Nothing <*> _ = Nothing
_ <*> Nothing = Nothing

Hence if any one of them is Nothing then the entire expression becomes Nothing (except in the second case if the first argument is undefined) and since Nothing == Nothing the law still holds.

Finally, what about undefined (a.k.a. bottom) values? We know that:

(Just f) <*> (Just x) = Just (f x)

Hence the following expressions will make the program halt:

(Just f) <*> undefined
undefined <*> (Just x)
undefined <*> Nothing

However the following expression will result in Nothing:

Nothing <*> undefined

In either case the composition law still holds.

Answer 2

You translated the use of (<*>) through fmap. The other answers also do some pattern matching.

Usually you need to open the definition of the functions to reason about them, not just assume what they do. (You assume (pure f) <*> x is the same as fmap f x)

For example, (<*>) is defined as ap for Maybe in Control.Applicative (or can be proven to be equivalent to it for any Monad, even if you redefine it), and ap is borrowed from Monad, which is defined as liftM2 id, and liftM2 is defined like so:

liftM2 f m1 m2 = do
    x <- m1
    y <- m2
    return $ f x y

So, reduce both left- and right-hand sides to see they are equivalent:

u <*> (v <*> w) = liftM2 id u (liftM2 id v w)
 = do
     u1 <- u
     v1 <- do
             v1 <- v
             w1 <- w
             return $ id v1 w1
     return $ id u1 v1
 = do
     u1 <- u
     v1 <- do
             v1 <- v
             w1 <- w
             return $ v1 w1
     return $ u1 v1
 -- associativity law: (see [1])
 = do
     u1 <- u
     v1 <- v
     w1 <- w
     x <- return $ v1 w1
     return $ u1 x
 -- right identity: x' <- return x; f x'  == f x
 = do
     u1 <- u
     v1 <- v
     w1 <- w
     return $ u1 $ v1 w1

Now, the right-hand side:

pure (.) <*> u <*> v <*> w
 = liftM2 id (liftM2 id (liftM2 id (pure (.)) u) v) w
 = do
     g <- do
            f <- do
                   p <- pure (.)
                   u1 <- u
                   return $ id p u1
            v1 <- v
            return $ id f v1
     w1 <- w
     return $ id g w1
 = do
     g <- do
            f <- do
                   p <- return (.)
                   u1 <- u
                   return $ p u1
            v1 <- v
            return $ f v1
     w1 <- w
     return $ g w1
 -- associativity law:
 = do
    p <- return (.)
    u1 <- u
    f <- return $ p u1
    v1 <- v
    g <- return $ f v1
    w1 <- w
    return $ g w1
 -- right identity: x' <- return x; f x'  ==  f x
 = do
    u1 <- u
    v1 <- v
    w1 <- w
    return $ ((.) u1 v1) w1
 -- (f . g) x  == f (g x)
 = do
    u1 <- u
    v1 <- v
    w1 <- w
    return $ u1 $ v1 w1

That's it.

[1] http://www.haskell.org/haskellwiki/Monad_laws

Answer 3

The rules that are generated by the definition of Maybe are

x :: a
---------------
Just x :: Maybe a

and

a type
-----------------
Nothing :: Maybe a

Along with

a type
------------------
bottom :: a

If these are the only rules which result in Maybe A then we can always invert them (run from bottom to top) in proofs so long as we're exhaustive. This is argument by case examination of a value of type Maybe A.

You did two cases analyses, but weren't exhaustive. It might be that u or v are actually Nothing or bottom.

Answer 4

A useful tool to learn when proving stuff about Haskell code is Agda: Here is a short proof stating what you want to prove:

data Maybe (A : Set) : Set where
  Just : (a : A) -> Maybe A
  Nothing : Maybe A

_<*>_ : {A B : Set} -> Maybe (A -> B) -> Maybe A -> Maybe B
Just f <*> Just a = Just (f a)
Just f <*> Nothing = Nothing
Nothing <*> a = Nothing

pure : {A : Set} -> (a : A) -> Maybe A
pure a = Just a

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

_∘_ : {A B C : Set} ->
      (B -> C) -> (A -> B) -> A -> C
_∘_ f g = λ z → f (g z)

maybeAppComp : {A B C : Set} -> (u : Maybe (B -> A)) -> (v : Maybe (C -> B)) -> (w : Maybe C)
            -> (u <*> (v <*> w)) ≡ (((pure _∘_ <*> u) <*> v) <*> w)
maybeAppComp (Just f) (Just g) (Just w) = refl
maybeAppComp (Just f) (Just g) Nothing = refl
maybeAppComp (Just f) Nothing (Just w) = refl
maybeAppComp (Just f) Nothing Nothing = refl
maybeAppComp Nothing (Just g) (Just w) = refl
maybeAppComp Nothing (Just a) Nothing = refl
maybeAppComp Nothing Nothing (Just w) = refl
maybeAppComp Nothing Nothing Nothing = refl

This illustrates a couple of points others have pointed out:

• Which definitions you use are important for the proof, and should be made explicit. In my case I did not want to use Agda's libraries.
• Case analysis is key to making these kinds of proofs.
• In fact, the proof becomes trivial once case analysis is done. The Agda compire/proof system is able to unify the proof for you.