Applicative Laws for Maybe
Type
Applicative functors come with a set of laws that apply for all Applicative instances. These laws are as follows:

Identity:
pure id <*> v = v

Homomorphism:
pure f <*> pure x = pure (f x)

Interchange:
u <*> pure y = pure ($y) <*> u

Composition:
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
For more information about these laws, check out this Haskell wiki post.
Maybe
is an Applicative functor, and this post will verify that the applicative laws hold for the Maybe
instance.
Before we begin, let’s review the definition for Applicative
typeclass:
class Functor f => Applicative f where
pure :: a > f a
(<*>) :: f (a>b) > f a > f b
Maybe
is made an instance of the Applicative
class as:
instance Applicative Maybe where
pure x = Just x
(<*>) Nothing _ = Nothing
(<*>) (Just f) someMaybe = fmap f someMaybe
Note that the last line above can be rewritten as:
(<*>) (Just f) Nothing = Nothing
(<*>) (Just f) (Just x) = Just (f x)
Now, let’s test the Applicative laws for the Maybe
type one by one:
Identity
We need to prove that the following holds for the Maybe
type:
pure id <*> v = v
Let’s start from the left side of the equation:
pure id <*> v
 applying definition of pure for Maybe
(Just id) <*> v
 v could be either Nothing, or (Just x)
case v of
Nothing > Nothing
(Just x) > Just (id x)
 applying id to x is simply x
case v of
Nothing > Nothing
(Just x) > Just x
v  the right side of equation
Homomorphism
The law’s statement is:
pure f <*> pure x = pure (f x)
To prove this for Maybe
type, let’s begin from the left side of the equation:
pure f <*> pure x
 applying definition of pure
(Just f) <*> (Just x)
 applying defintion of <*>
Just (f x)
 unapplying the definition of pure
pure (f x)  the right side
Interchange
The law’s statement is:
u <*> pure y = pure ($y) <*> u
Starting from the left side:
u <*> pure y
 applying definition of pure
u <*> (Just y)
 u can be either Nothing, or (Just f). Let's evaluate both
case u of
Nothing > Nothing
(Just f) > Just (f y)
 rewriting (f y) using function application operator
case u of
Nothing > Nothing
(Just f) > Just (f $ y)
 Using the section representation of the $ infix operator
case u of
Nothing > Nothing
(Just f) > Just (($y) f)
 Unapplying the definition of <*>
case u of
Nothing > Nothing
(Just f) > Just ($y) <*> (Just f)
 Replacing the Nothing clause with an equivalent (via
 the defintion) of <*> for Maybe
case u of
Nothing > Just ($y) <*> Nothing
(Just f) > Just ($y) <*> (Just f)
 Unapplying the definition of pure and u
pure ($y) <*> u  Equal to the right side
Composition
The law’s statement is:
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
Starting from the left side:
pure (.) <*> u <*> v <*> w
 applying definition of pure
(Just (.)) <*> u <*> v <*> w
 u, v & w can all be either Nothing or (Just something).
 From the definition of <*>, we know that if either
 argument to <*> is Nothing, the entire expression reduces
 to Nothing.
 Therefore, I am only going to focus on the Just cases
(Just (.)) <*> (Just f) <*> (Just g) <*> (Just x)
 Appying <*> to the first two terms
(Just (.) f) <*> (Just g) <*> (Just x)
 Appying <*> to the first two terms again
(Just (.) f g) <*> (Just x)
 Applying the function composition
(Just (f.g) ) <*> (Just x)
 Applying <*> one more time
(Just (f.g) x)
 via the definition of the function composition
 operator
(Just f (g x))
 Applying Homomorphism law
(Just f) <*> Just (g x)
 Applying Homomorphism law to the 2nd term
(Just f) <*> ( (Just g) <*> (Just x) )
 Unapplying the definitions of u, v, w
u <*> (v <*> w)  Equal to the right side