# Applicative Laws for `((->) r)` Type

Haskell’s function type `((->) r)` is an Applicative functor. Similar to the previous two posts in this series, in this post I will verify that the applicative laws hold for the `((->) r)` type.

This is Part-3 of my series on verifying Applicative laws for various Haskell types. Here are Part-1 Applicative Laws for Maybe Type and Part-2 Applicative Laws for [] Type

For reference, `((->) r)` is made an instance of the `Applicative` class as:

``````instance Applicative ((->) r) where
pure x = (\_ -> x)
-- pure can also be written as:
-- pure x = const x

-- (<*>) :: f (a->b) -> f a -> f b
-- (<*>) :: ((->) r (a->b)) -> ((->) r a) -> ((->) r b)
-- (<*>) :: (r -> (a->b)) -> (r -> a) -> (r -> b)
-- the entire lambda has type r -> b, which implies x :: r
(<*>) f g = (\x -> f x (g x))
``````

For review, here are the applicative laws:

• 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)`

## Identity

We need to prove that the following holds for the `((->) r)` type:

``````pure id <*> v = v
``````

Beginning from LHS:

``````pure (id) <*> v
-- using definition of pure
const id <*> v

-- applying definition of <*>
(\x -> const id x (v x))

-- applying const
(\x -> id (v x))

-- applying id
(\x -> v x)

v -- RHS
``````

## Homomorphism

The law’s statement is:

``````pure f <*> pure x = pure (f x)
``````

Here’s the proof:

``````pure f <*> pure x

-- applying definition of pure
const f <*> const x

-- applying definition of <*>
(\y -> const f y (const x y))

-- applying const
(\y -> f (x))

-- As y is unused, replace with _
(\_ -> f x)

-- un-applying definition of pure
pure (f x) -- RHS
``````

## Interchange

The law’s statement is:

``````u <*> pure y = pure (\$y) <*> u
``````

Starting from the LHS:

``````u <*> pure y

-- applying definition of pure
u <*> const y

-- applying definition of <*>
\x -> u x (const y x)

-- applying const
\x -> u x (y)

\x -> u x y
``````

Now, starting from the RHS:

``````pure (\$y) <*> u

-- applying definition of pure
const (\$y) <*> u

-- applying definition of <*>
\x -> const (\$y) x (u x)

-- applying const
\x -> (\$y) (u x)

-- applying definition of function application operator (\$)
\x -> (u x) \$ y

\x -> u x y
``````

As both the left and right sides reduce to the same statement, the interchange law is proved for the `((->) r)` type

## Composition

The law’s statement is:

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

Starting from the right side of the equation:

``````u <*> (v <*> w)

-- applying definition of <*>
u <*> ( \y -> v y (w y) )

-- applying definition of <*>
\x -> u x ( (\y -> v y (w y)) x )

-- Apply the lambda ( (\y -> v y (w y)) to its
-- argument x, which results in:
\x -> u x ( v x (w x)) -- (A)

``````

In the same manner, let’s consider the left side of the equation:

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

-- applying definition of pure
const (.) <*> u <*> v <*> w

-- applying definition of <*> to the 1st two terms
(\f -> const (.) f (u f)) <*> v <*> w

-- applying const
(\f -> (.) (u f)) <*> v <*> w

-- applying definition of <*> to the 1st two terms
(\g -> (\f -> (.) (u f)) g (v g)) <*> w

-- applying definition of <*>
\x -> (\g -> (\f -> (.) (u f)) g (v g)) x (w x)

-- Expanding the lambda (\g -> ...) by applying to x
\x -> ((\f -> (.) (u f)) x (v x)) (w x)

-- Expanding the inner lambda (\f -> ...) by applying to x
\x -> (( (.) (u x)) (v x))  (w x)

-- Using definition of function composition (.)
\x -> ((u x) . (v x)) (w x)

-- Using definition of (.), i.e. f.g x = f (g x)
\x -> u x ( v x (w x) ) -- (B)

``````

(A) & (B) prove that both the left and right side of the composition law for `((->) r)` type reduce to the same statement, and thus the law is proved for the function type.

## Acknowledgements

Thanks to Daniel Wagner who nudged me in the right direction by answering my questions (1 and 2) on Stack Overflow.