# A new case for the pointed functor class

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.

• #### Simplicity is the Initial Distributive Category

Simplicity is a combinator-based typed language with the unit type, sum types and product types. Types: 𝟙; A + B; A × B Every Simplicity…

• #### From Van Laarhoven Isomorphisms in one shot.

The type ∀ f, g : Functor. (g a → f b) → g s → f t is isomorphic to the type (s → a)×(b → t). The Van…

• #### Grate: A new kind of Optic

James Deikun (known as xplat on freenode) and I discovered a new kind of Optic today. If not discovered, then at least characterized it. We know…

• Post a new comment

#### Error

default userpic
When you submit the form an invisible reCAPTCHA check will be performed.