What are the applicative functor laws in terms of pure and liftA2?

Question

I'm playing around with formulating Applicative in terms of pure and liftA2 (so that (<*>) = liftA2 id becomes a derived combinator).

I can think of a bunch of candidate laws, but I'm not sure what the minimal set would be.

1. f <$> pure x = pure (f x)
2. f <$> liftA2 g x y = liftA2 ((f .) . g) x y
3. liftA2 f (pure x) y = f x <$> y
4. liftA2 f x (pure y) = liftA2 (flip f) (pure y) x
5. liftA2 f (g <$> x) (h <$> y) = liftA2 (\x y -> f (g x) (h y)) x y
6. ...

Hodges

liftA2 is defined in terms of <$> and <*>, I don't know why you would want to instead define <*> in terms of liftA2. – Gripe

Yeah, but I'd like to do something similar to what EZ Yang does in his post comparing Applicative and Monoidal: blog.ezyang.com/2012/08/applicative-functors – Sailing

Applicative with pure and liftA2 is the same as this Monoidal class which has a list of laws. To get from Monoidal to Applicative with pure and liftA2 you replace explicit types and constructors in the interface with things that the type or constructor can be passed into to recover the original interface. – Worldshaking

@Cirdec, neat. Is is easy to read off the corresponding laws for pure and liftA2? – Sailing

Answer 1

Based on McBride and Paterson's laws for Monoidal(section 7) I'd suggest the following laws for liftA2 and pure.

left and right identity

liftA2 (\_ y -> y) (pure x) fy       = fy
liftA2 (\x _ -> x) fx       (pure y) = fx

associativity

liftA2 id           (liftA2 (\x y z -> f x y z) fx fy) fz =
liftA2 (flip id) fx (liftA2 (\y z x -> f x y z)    fy  fz)

naturality

liftA2 (\x y -> o (f x) (g y)) fx fy = liftA2 o (fmap f fx) (fmap g fy)

It isn't immediately apparent that these are sufficient to cover the relationship between fmap and Applicative's pure and liftA2. Let's see if we can prove from the above laws that

fmap f fx = liftA2 id (pure f) fx

We'll start by working on fmap f fx. All of the following are equivalent.

fmap f fx
liftA2 (\x _ -> x) (fmap f fx) (         pure y )     -- by right identity
liftA2 (\x _ -> x) (fmap f fx) (     id (pure y))     -- id x = x by definition
liftA2 (\x _ -> x) (fmap f fx) (fmap id (pure y))     -- fmap id = id (Functor law)
liftA2 (\x y -> (\x _ -> x) (f x) (id y)) fx (pure y) -- by naturality
liftA2 (\x _ -> f x                     ) fx (pure y) -- apply constant function

At this point we've written fmap in terms of liftA2, pure and any y; fmap is entirely determined by the above laws. The remainder of the as-yet-unproven proof is left by the irresolute author as an exercise for the determined reader.

Worldshaking

Interesting, that the identity law can be rewritten like so: liftA2 const fx (pure y) == const fx (pure y) and flip (liftA2 (flip const)) fx (pure y) == const fx (pure y) (or liftA2 (flip const) (pure x) fy == flip const (pure x) fy), which perhaps adds an interesting angle. – Inguinal

Answer 2

If you define (<.>) = liftA2 (.) then the laws become very nice:

pure id <.> f = f
f <.> pure id = f
f <.> (g <.> h) = (f <.> g) <.> h

Apparently pure f <.> pure g = pure (f . g) follows for free. I believe this formulation originates with Daniel Mlot.

Ashleeashleigh

Answer 3

Per the online book, Learn You A Haskell:Functors, Applicative Functors and Monoids, the Appplicative Functor laws are bellow but reorganized for formatting reasons; however, I am making this post community editable since it would be useful if someone could embed derivations:

    identity]               v = pure id <*> v
homomorphism]      pure (f x) = pure f <*> pure x
 interchange]    u <*> pure y = pure ($ y) <*> u
 composition] u <*> (v <*> w) = pure (.) <*> u <*> v <*> w

Note:

function composition]  (.) = (b->c) -> (a->b) -> (a->c)
application operator]    $ = (a->b) -> a -> b

Found a treatment on Reddit

Tablecloth

Should (.) not be (a->b) -> (b->c) -> (a->c) ? – Epithelioma

No, it should be (b->c) -> (a->b) -> (a->c). – Tomboy

Indeed: (f . g) a = f (g(a)) – Tablecloth

"... in terms of pure and liftA2", asks the question. – Spire