This is Part-2 of my series on verifying Applicative laws for various Haskell types. Part-1 is Applicative Laws for Maybe 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. For reference, [] is made an instance of the Applicative class as:

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:

1

pureid<*>v=v

Consider the left side of the equation:

12345678910111213

pureid<*>v-- applying definition of pure for [][id]<*>v-- applying definition of <*>[idx|x<-v]-- applying id[x|x<-v]-- list comprehension reduces to vv-- Same as the right side

Homomorphism

The law’s statement is:

1

puref<*>purex=pure(fx)

Starting from the left side:

1234567891011

puref<*>purex-- applying definition of pure[f]<*>[x]-- Note that both the lists have one element each. So-- applying the definition of <*>, this reduces to:[fx]-- un-applying purepure(fx)-- Same as the right side

Interchange

The law’s statement is:

1

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

Starting from the left side,

1234567891011121314151617181920

u<*>purey-- applying definition of pure u<*>[y]-- A list of functions applied to -- a single element list-- via definition of <*>[fy|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 purepure($y)<*>u-- Same as the right side

Composition

The law’s statement is:

1

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

Starting from the left:

1234567891011121314151617181920212223242526272829

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 <*>[zg|z<-[(.)f|f<-fs],g<-gs]<*>xs-- replace the value of z, and reduce[(.)fg|f<-fs,g<-gs]<*>xs-- applying function composition[f.g|f<-fs,g<-gs]<*>xs-- applying the definition of <*>[zx|z<-[f.g|f<-fs,g<-gs],x<-xs][f.gx|f<-fs,g<-gs,x<-xs]-- applying definition of function composition[f(gx)|f<-fs,g<-gs,x<-xs]-- (A)

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

1234567891011121314

u<*>(v<*>w)-- as u, v, w are all lists, for clarity re-writing-- u as fs, v as gs, w as xsfs<*>(gs<*>xs)-- applying definition of <*>fs<*>([gx|g<-gs,x<-xs])-- applying definition of <*>[fz|f<-fs,z<-[gx|g<-gs,x<-xs]]-- replacing z[f(gx)|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