# Applicative Laws for ((->) 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

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.

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

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:

Beginning from LHS:

### Homomorphism

The law’s statement is:

Here’s the proof:

### Interchange

The law’s statement is:

Starting from the LHS:

Now, starting from the RHS:

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:

Starting from the right side of the equation:

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

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