Hi all,

I'm trying to check that the Applicative laws hold for the function type ((->) r), and here's what I have so far:

-- Identiy

pure (id) <*> v = v

pure (id) <*> v

const id <*> v

(\x -> const id x (g x))

(\x -> id (g x))

(\x -> g x)

g x

-- Homomorphism

pure f <*> pure x = pure (f x)

pure f <*> pure x

const f <*> const x

(\y -> const f y (const x y))

(\y -> f (x))

(\_ -> f x)

pure (f x)

Did I perform the steps for the first two laws correctly?

I'm struggling with the interchange & composition laws. For interchange, so far I have the following:

-- Interchange

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

u <*> pure y

u <*> const y

(\x -> g x (const y x))

(\x -> g x y)

-- I'm not sure how to proceed beyond this point.

I would appreciate any help for the steps to verify the Interchange & Composition applicative laws for the ((->) r) type.

Thank you,

~Umair