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:

12345678910

instanceApplicative((->)r)wherepurex=(\_->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(<*>)fg=(\x->fx(gx))

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:

1

pureid<*>v=v

Beginning from LHS:

1234567891011121314

pure(id)<*>v-- using definition of pureconstid<*>v-- applying definition of <*>(\x->constidx(vx))-- applying const(\x->id(vx))-- applying id(\x->vx)v-- RHS

Homomorphism

The law’s statement is:

1

puref<*>purex=pure(fx)

Here’s the proof:

12345678910111213141516

puref<*>purex-- applying definition of pureconstf<*>constx-- applying definition of <*>(\y->constfy(constxy))-- applying const(\y->f(x))-- As y is unused, replace with _(\_->fx)-- un-applying definition of purepure(fx)-- RHS

Interchange

The law’s statement is:

1

u<*>purey=pure($y)<*>u

Starting from the LHS:

123456789101112

u<*>purey-- applying definition of pureu<*>consty-- applying definition of <*>\x->ux(constyx)-- applying const\x->ux(y)\x->uxy

Now, starting from the RHS:

123456789101112131415

pure($y)<*>u-- applying definition of pureconst($y)<*>u-- applying definition of <*>\x->const($y)x(ux)-- applying const\x->($y)(ux)-- applying definition of function application operator ($)\x->(ux)$y\x->uxy

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:

1

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

Starting from the right side of the equation:

1234567891011

u<*>(v<*>w)-- applying definition of <*>u<*>(\y->vy(wy))-- applying definition of <*>\x->ux((\y->vy(wy))x)-- Apply the lambda ( (\y -> v y (w y)) to its -- argument x, which results in:\x->ux(vx(wx))-- (A)

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

12345678910111213141516171819202122232425262728

pure(.)<*>u<*>v<*>w-- applying definition of pureconst(.)<*>u<*>v<*>w-- applying definition of <*> to the 1st two terms(\f->const(.)f(uf))<*>v<*>w-- applying const(\f->(.)(uf))<*>v<*>w-- applying definition of <*> to the 1st two terms(\g->(\f->(.)(uf))g(vg))<*>w-- applying definition of <*>\x->(\g->(\f->(.)(uf))g(vg))x(wx)-- Expanding the lambda (\g -> ...) by applying to x\x->((\f->(.)(uf))x(vx))(wx)-- Expanding the inner lambda (\f -> ...) by applying to x\x->(((.)(ux))(vx))(wx)-- Using definition of function composition (.)\x->((ux).(vx))(wx)-- Using definition of (.), i.e. f.g x = f (g x)\x->ux(vx(wx))-- (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.