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

[Gershom B]

On November 29, 2015 at 11:23:24 PM, roconnor at theorem.ca (roconnor at theorem.ca) wrote:
>
> class Functor f => StrongSum f where 
>     distRight :: Either a (f b) -> f (Either a b) 
>
> -- 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)

This is very interesting, but I’m not exactly convinced. This is what I’ve worked out thus far:

Here is a pretty minimal instance of StrongSum that fails the laws:

data WithInt a = WithInt Int a deriving Show

instance Functor WithInt where
   fmap f (WithInt no x) = WithInt no (f x)

instance StrongSum WithInt where
    distRight (Left x) = WithInt 42 (Left x)
    distRight (Right (WithInt no x)) = WithInt (no + 1) (Right x)

From this it becomes clear why StrongSum requires laws and fmap does not. Consider the induced Pointed instance from:

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

This completely ignores the Right case, which is where all the potential for an “unlawful” StrongSum resides.

(
i.e., in this case:

distVoidRight1 = either absurd (fmap Right)
distVoidRight2 = distRight

distVoidRight1 (Right (WithInt 12 “hi”)) = WithInt 12 (Right “hi”)
distVoidRight2 (Right (WithInt 12 “hi”)) = WithInt 13 (Right “hi”)
)

In the induced StrongSum from Pointed case, the Right instance is given definitively by “fmap Right”. The laws, as far as I can tell, just require that “distRight . Right == fmap Right” which is what is freely generated by inducing StrongSum from Pointed.

So this at core leaves us with a class with additional structure, which has Pointed as a subclass, which is a familiar story. Except here there is a twist — we’ve added some extra laws to that class such that it corresponds precisely to the instance we can freely generate from Functor and Pointed.

So posit we had a class Apply as in https://hackage.haskell.org/package/semigroupoids-5.0.0.4/docs/Data-Functor-Apply.html#t:Apply  but did not yet have Pointed.

Now we can play the same game (well, almost — there are a few more subtleties here). A lawful Applicative could be generated by Apply and Pointed*, and every Applicative gives rise to Pointed. But if that doesn’t motivate Pointed, why should this? :-)

Cheers,
Gershom

*The subtlety being in particular that not every Apply/Pointed combination directly gives rise to a proper Applicative.