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.