Applicative Laws for []
Type
Haskell’s list type []
is an Applicative functor. Similar to the previous post, this post will verify that the applicative laws hold for the []
type.
This is Part2 of my series on verifying Applicative laws for various Haskell types. Part1 is Applicative Laws for Maybe Type.
For reference, []
is made an instance of the Applicative
class as:
instance Applicative [] where
pure x = [x]
(<*>) fs xs = [f x  f < fs, x < xs]
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)
Now, letâ€™s test the Applicative laws for the []
type one by one:
Identity
We need to prove that the following holds for the []
type:
pure id <*> v = v
Consider the left side of the equation:
pure id <*> v
 applying definition of pure for []
[id] <*> v
 applying definition of <*>
[id x  x < v]
 applying id
[x  x < v]
 list comprehension reduces to v
v  Same as the right side
Homomorphism
The law’s statement is:
pure f <*> pure x = pure (f x)
Starting from the left side:
pure f <*> pure x
 applying definition of pure
[f] <*> [x]
 Note that both the lists have one element each. So
 applying the definition of <*>, this reduces to:
[f x]
 unapplying pure
pure (f x)  Same as the right side
Interchange
The law’s statement is:
u <*> pure y = pure ($y) <*> u
Starting from the left side,
u <*> pure y
 applying definition of pure
u <*> [y]  A list of functions applied to
 a single element list
 via definition of <*>
[f y  f < u]
 replacing f y by the function application operator
[f $ y  f < u]
 Using the section representation of the $ infix operator
[($y) f  f < u]
 Unapplying the definition of <*>
[($y)] <*> u
 Unapplying pure
pure ($y) <*> u  Same as the right side
Composition
The law’s statement is:
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
Starting from the left:
pure (.) <*> u <*> v <*> w
 applying definition of pure
[(.)] <*> u <*> v <*> w
 as u, v, w are all lists, for clarity rewriting
 u as fs, v as gs, w as xs
[(.)] <*> fs <*> gs <*> xs
 applying definition of <*>
[(.) f  f < fs] <*> gs <*> xs
 applying definition of <*>
[z g  z < [(.) f  f < fs], g < gs] <*> xs
 replace the value of z, and reduce
[(.) f g  f < fs, g < gs] <*> xs
 applying function composition
[f.g  f < fs, g < gs] <*> xs
 applying the definition of <*>
[ z x  z < [f.g  f < fs, g < gs],
x < xs]
[ f.g x  f < fs, g < gs, x < xs]
 applying definition of function composition
[ f (g x)  f < fs, g < gs, x < xs]  (A)
In the same manner, let’s consider the right side of the equation:
u <*> (v <*> w)
 as u, v, w are all lists, for clarity rewriting
 u as fs, v as gs, w as xs
fs <*> (gs <*> xs)
 applying definition of <*>
fs <*> ( [g x  g < gs, x < xs] )
 applying definition of <*>
[f z  f < fs, z < [g x  g < gs, x < xs] ]
 replacing z
[f (g x)  f < fs, g < gs, x < xs]  (B)
(A) & (B) prove that both the left and right side of the composition law reduce to the same statement, and thus composition law is proved for the []
type