Applicative and Functor

3 Mar 2006

      Shouldn't Applicative be a subclass of Functor? "<$>" can then be dropped.

The Functor laws are this:

fmap id = id
fmap (a . b) = (fmap a) . (fmap b)

These are already implied by the Applicative laws:

(<$>) id = id
Proof:

   LHS = (<$>) id = \v -> id <$> v
     = \v -> (pure id) <*> v   -- "pure application"
     = \v -> v                 -- "identity"
     = id = RHS QED.

(<$>) (a . b) = ((<$>) a) . ((<$>) b)
Proof:

   LHS = (<$>) (a . b) = \v -> (a . b) <$> v
     = \v -> pure (a . b) <*> v                 -- "pure application"
     = \v -> (pure ((.) a) <*> (pure b)) <*> v  -- "homomorphism"
     = \v -> ((pure (.) <*> (pure a)) <*> (pure b)) <*> v
          -- "homomorphism"
     = \v -> (pure a) <*> ((pure b) <*> v)      -- "composition"
     = \v -> (a <$> (b <$> v))                  -- "pure application"
     = ((<$>) a) . ((<$>) b) = RHS QED.

-- 
Ashley Yakeley