[Haskell-cafe] A new case for the pointed functor class

[roconnor at theorem.ca]

>From <http://r6research.livejournal.com/28338.html>:


There has been some debate for some time as to whether there should be a 
superclass for Applicative with just the pure function should exist:

-- Natural law:
-- fmap f . pure = pure . f
class Functor f => Pointed f where
   pure :: a -> f a

The charge laid against this class is that there are no laws for this 
single function beyond the single law that is naturally implied. Compare 
this to a more reasonable class

-- Natural laws:
-- distRight . right . fmap f = fmap (right f) . distRight
-- distRight . left f = fmap (left f) . distRight
--
-- Other laws:
-- 1. either absurd (fmap Right) = distRight :: Either Void (f a) -> f (Either Void a)
-- 2. fmap assocL . distRight . right distRight . assocR = distRight :: Either (Either a b) (f c) -> f (Either (Either a b) c)
--  where
--   assocL :: Either a (Either b c) -> Either (Either a b) c
--   assocL (Left a) = Left (Left a)
--   assocL (Right (Left a)) = Left (Right a)
--   assocL (Right (Right a)) = Right a
--   assocR :: Either (Either a b) c -> Either a (Either b c)
--   assocR (Left (Left a)) = Left a
--   assocR (Left (Right a)) = Right (Left a)
--   assocR (Right a) = Right (Right a)
class Functor f => StrongSum f where
   distRight :: Either a (f b) -> f (Either a b)

   distLeft :: Either (f a) b -> f (Either a b)
   distLeft = fmap switch . distRight . switch
    where
     switch :: Either a b -> Either b a
     switch = Right ||| Left

StrongSum is a honest class with two additional real laws in addition to 
its natural laws. No one would object to creating and using such a class.

What if I told you that Pointed and StrongSum are in fact the same class?

class Functor f => Pointed f where
   pure :: a -> f a
   pure = fmap (id ||| absurd) . distRight . Left

   distRight : Either a (f b) -> f (Either a b)
   distRight = either (fmap Left . pure) (fmap Right)

Theorem 1. If we define pure, then the distRight automatically satisfies 
the 2 required laws.

Proof. Law 1:

either absurd (fmap Right)
= { extensionality of absurd }
either (fmap Left . pure) (fmap Right)
= { definition in terms of pure }
distRight :: Either Void (f a) -> f (Either Void a)

Law 2: fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR
  = either (fmap Left . pure) (fmap Right)

case 1: Right x

fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR $ Right x
=
fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) $ Right (Right x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (either (fmap Left . pure) (fmap Right) (Right x))
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (fmap Right x)
=
fmap assocL $ fmap Right (fmap Right x)
=
fmap (assocL . Right . Right) x
=
fmap Right x
=
either (fmap Left . pure) (fmap Right) $ Right x

case 2: Left (Right x)

fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR $ Left (Right x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) $ Right (Left x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (either (fmap Left . pure) (fmap Right) (Left x))
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Right (fmap Left (pure x))
=
fmap assocL $ fmap Right (fmap Left (pure x))
=
fmap (assocL . Right . Left) (pure x)
=
fmap (Left . Right) (pure x)
=
fmap Left . fmap Right . pure $ x
=
fmap Left . pure . Right $ x
=
fmap Left . pure $ Right x
=
either (fmap Left . pure) (fmap Right) $ Left (Right x)

case 3: Left (Left x)

fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) . assocR $ Left (Left x)
=
fmap assocL . either (fmap Left . pure) (fmap Right) . right (either (fmap Left . pure) (fmap Right)) $ Left x
=
fmap assocL . either (fmap Left . pure) (fmap Right) $ Left x
=
fmap assocL . fmap Left . pure $ x
=
fmap (assocL . Left) . pure $ x
=
fmap (Left . Left) . pure $ x
=
fmap Left . fmap Left . pure $ x
=
fmap Left . pure . Left $ x
=
fmap Left . pure $ Left x
=
either (fmap Left . pure) (fmap Right) $ Left (Left x)

Theorem 2. If we define pure, then
pure = fmap (id ||| absurd) . distRight . Left where distRight = either (fmap Left . pure) (fmap Right)

Proof.

fmap (id ||| absurd) . distRight . Left
=
fmap (id ||| absurd) . either (fmap Left . pure) (fmap Right) . Left
=
fmap (id ||| absurd) . fmap Left . pure
=
fmap ((id ||| absurd) . Left) . pure
=
fmap id . pure
=
pure

Theorem 3. If we define distRight such that distRight satisfies its two 
laws then distRight = either (fmap Left . pure) (fmap Right) where pure = 
fmap (id ||| absurd) . distRight . Left.

Proof. either (fmap Left . fmap (id ||| absurd) . distRight . Left) (fmap Right)
  = distRight

case 1: Left x

either (fmap Left . fmap (id ||| absurd) . distRight . Left) (fmap Right) $ Left x
=
fmap Left . fmap (id ||| absurd) . distRight $ Left x
=
fmap (Left . (id ||| absurd)) $ distRight (Left x)
=
fmap (Left ||| (Left . absurd)) $ distRight (Left x)
=
fmap (Left ||| absurd) $ distRight (Left x)
= { extensionality of absurd }
fmap (Left ||| Right) $ distRight (Left x)
=
fmap id $ distRight (Left x)
=
distRight (Left x)

case 2: Right x

either (fmap Left . fmap (id ||| absurd) . distRight . Left) (fmap Right) $ Right x
=
fmap Right x
=
fmap (left absurd . Right) x
=
fmap (left absurd) $ fmap Right x
=
fmap (left absurd) . either absurd (fmap Right) $ Right x
= { Law 1 for distRight }
fmap (left absurd) . distRight $ Right x
= { Natural law for distRight }
distRight . left absurd $ Right x
=
distRight $ Right x

Interestingly we only ever used the first law for distRight. By composing 
these proofs together we should be able to show that the second law for 
distRight holds whenever the first law does.

In conclusion we have seen that the StrongSum class and the Pointed class 
are equivalent classes. The pure function contains the heart of what a law 
abiding distRight function is, such that whenever we have a law abiding 
distRight function it can be written in terms of pure and every instance 
of pure yields a law abiding distRight function. Given that I think people 
would welcome a StrongSum class, it only makes sense to equally welcome 
the Pointed class.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''