[Haskell-cafe] A new case for the pointed functor class
Gershom B
gershomb at gmail.com
Wed Dec 2 04:34:41 UTC 2015
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.
More information about the Haskell-Cafe
mailing list