#
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`

type-class:

```
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 re-written 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)
-- un-applying 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)
-- re-writing (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)
-- Un-applying 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)
-- Un-applying 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) )
-- Un-applying the definitions of u, v, w
u <*> (v <*> w) -- Equal to the right side
```