Now, let’s test the Applicative laws for the Maybe type one by one:

Identity

We need to prove that the following holds for the Maybe type:

1

pureid<*>v=v

Let’s start from the left side of the equation:

1234567891011121314

pureid<*>v-- applying definition of pure for Maybe(Justid)<*>v-- v could be either Nothing, or (Just x)casevofNothing->Nothing(Justx)->Just(idx)-- applying id to x is simply xcasevofNothing->Nothing(Justx)->Justxv-- the right side of equation

Homomorphism

The law’s statement is:

1

puref<*>purex=pure(fx)

To prove this for Maybe type, let’s begin from the left side of the equation:

12345678

puref<*>purex-- applying definition of pure(Justf)<*>(Justx)-- applying defintion of <*>Just(fx)-- un-applying the definition of purepure(fx)-- the right side

u<*>purey-- applying definition of pure u<*>(Justy)-- u can be either Nothing, or (Just f). Let's evaluate bothcaseuofNothing->Nothing(Justf)->Just(fy)-- re-writing (f y) using function application operatorcaseuofNothing->Nothing(Justf)->Just(f$y)-- Using the section representation of the $ infix operator caseuofNothing->Nothing(Justf)->Just(($y)f)-- Un-applying the definition of <*>caseuofNothing->Nothing(Justf)->Just($y)<*>(Justf)-- Replacing the Nothing clause with an equivalent (via -- the defintion) of <*> for MaybecaseuofNothing->Just($y)<*>Nothing(Justf)->Just($y)<*>(Justf)-- Un-applying the definition of pure and upure($y)<*>u-- Equal to the right side

pure(.)<*>u<*>v<*>w-- applying definition of pure(Just(.))<*>u<*>v<*>w-- u, v & w can all be either Nothing or (Just something). -- From the definition of <*>, we know that if either -- argument to <*> is Nothing, the entire expression reduces-- to Nothing. -- Therefore, I am only going to focus on the Just cases(Just(.))<*>(Justf)<*>(Justg)<*>(Justx)-- Appying <*> to the first two terms(Just(.)f)<*>(Justg)<*>(Justx)-- Appying <*> to the first two terms again(Just(.)fg)<*>(Justx)-- Applying the function composition(Just(f.g))<*>(Justx)-- Applying <*> one more time(Just(f.g)x)-- via the definition of the function composition -- operator(Justf(gx))-- Applying Homomorphism law(Justf)<*>Just(gx)-- Applying Homomorphism law to the 2nd term(Justf)<*>((Justg)<*>(Justx))-- Un-applying the definitions of u, v, wu<*>(v<*>w)-- Equal to the right side