Question, re: Typeclassopedia Ex. 4.2.1
Hi all, In trying to solve exercise 4.2.1 in Typeclassopedia, I’ve come up with the following: To prove: pure f <*> x = pure (flip ($)) <*> x <*> pure f Proof: pure (flip ($)) <*> x <*> pure f = (interchange) pure (flip ($)) <*> pure ($ f) <*> x = (homomorphism) pure (flip ($) ($ f)) <*> x = (definition of flip) pure ($ ($ f)) <*> x = (interchange) x <*> pure ($ f) = (interchange) (Is this step valid?) pure f <*> x Is the last step in my proof valid? Thanks, -db
On Tue, Sep 29, 2015 at 07:48:05AM -0700, David Banas wrote:
pure (flip ($)) <*> x <*> pure f = (interchange) pure (flip ($)) <*> pure ($ f) <*> x = (homomorphism)
For one thing, this step doesn't look right. <*> does not associate that way. It's probably worth at least putting each expression into ghci to check they have the same time Prelude> import Control.Applicative Prelude Control.Applicative> let l = \x f -> pure (flip ($)) <*> x <*> pure f Prelude Control.Applicative> :t l l :: Applicative f => f a -> (a -> b) -> f b Prelude Control.Applicative> let l2 = \x f -> pure (flip ($)) <*> pure ($ f) <*> x Prelude Control.Applicative> :t l2 l2 :: Applicative f => f (((a -> b1) -> b1) -> b) -> a -> f b I imagine you're probably going to want to go via ($ x) rather than ($ f), and possibly use that 'pure f <*> x = fmap f x = ($ x) <*> pure f'. Tom
participants (2)
-
David Banas -
Tom Ellis