From <http://r6research.livejournal.com/28338.html>:
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. -- Russell O'Connor <http://r6.ca/> ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.'' _______________________________________________ Haskell-Cafe mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe |
On November 29, 2015 at 11:23:24 PM, [hidden email] ([hidden email]) 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. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |