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 Part3 of my series on verifying Applicative laws for various Haskell types. Here are Part1 Applicative Laws for Maybe Type and Part2 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)
 unapplying 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.