Henning Thielemann wrote:
However the applicative functor laws from http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/Control-A... 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