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