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.