wren ng thornton wren at freegeek.org
Tue Jul 27 12:25:55 EDT 2010

Henning Thielemann wrote:
> However the applicative functor laws from
> are quite unintuitive and the proofs are certainly not very
> illustrative.

I always found it more illustrative to break it down and talk about
pointed functors, where 'return' is trivial in 'fmap' (forgive the Coq
syntax):

fmap_pointed
: forall {A B : Type} (f : A -> B) (a : A)
, f <\$> return a = return \$ f a

And then you only need three laws, the obvious ones:

app_return_left
: forall {A B : Type} (f : A -> B) (xa : F A)
, return f <*> xa = f <\$> xa

app_return_right
: forall {A B : Type} (xf : F (A -> B)) (a : A)
, xf <*> return a = (\$a) <\$> xf

app_compose
: forall {A B C : Type}
, forall (xf : F (B -> C)) (xg : F (A -> B)) (xa : F A)
, compose <\$> xf <*> xg <*> xa = xf <*> (xg <*> xa)

That is, we have that 'return' is (in the appropriate sense) the left
and right identity for (<*>), which allows us to apply fmap_pointed to
reduce (<*>) into (<\$>). Since only one of the arguments has a
non-trivial structure, that's the structure we use for (<\$>).

And then we have (again in the appropriate sense) associativity of
composition. Which is really just to say that composition from the pure
world is preserved as composition in the applicative world.

The other two laws (app_identity : ..., return id <\$> xa = xa) and
(app_homomorphism : ..., return f <*> return a = return (f a)) follow
directly from fmap_pointed. Or conversely, given these five laws we can
always prove fmap_pointed.

--
Live well,
~wren