2

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 
-- Starting with the LHS
pure (id) <*> v
const id <*> v
(\x -> const id x (g x))
(\x -> id (g x))
(\x -> g x)
g x
v


-- Homomorphism
pure f <*> pure x = pure (f x)
-- Starting with the LHS
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
-- Starting with the LHS
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. For reference, the Composition applicative law is as follows:

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

1 Answer 1

5

I think in your "Identity" proof, you should replace g with v everywhere (otherwise what is g and where did it come from?). Similarly, in your "Interchange" proof, things look okay so far, but the g that magically appears should just be u. To continue that proof, you could start reducing the RHS and verify that it also produces \x -> u x y.

Composition is more of the same: plug in the definitions of pure and (<*>) on both sides, then start calculating on both sides. You'll soon come to some bare lambdas that will be easy to prove equivalent.

2
  • Thank you for the tips. When I used g in place of u & v, it made sense to my head, but now I cannot think why I chose to do so. Your suggestion of reducing LHS and RHS independently certainly helped, and I was able to solve the Interchange equation. As a Haskell beginner, I will need to spend some time with the Composition lambdas before I'm done.
    – Umair
    Nov 21, 2015 at 1:51
  • I couldn't post my attempt for the Composition law here, as I couldn't format the code correctly. Instead, I have posted a new follow-up question: stackoverflow.com/questions/34538754/…
    – Umair
    Dec 30, 2015 at 23:22

Your Answer

Reminder: Answers generated by Artificial Intelligence tools are not allowed on Stack Overflow. Learn more

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.