Written by Umair Saeed
on 

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 Part-2 of my series on verifying Applicative laws for various Haskell types. Part-1 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:

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]

-- un-applying 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]

-- Un-applying the definition of <*>
[($y)] <*> u

-- Un-applying 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 re-writing
-- 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 re-writing
-- 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