On November 29, 2015 at 11:23:24 PM, roconnor@theorem.ca (roconnor@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-... 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.