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

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.