Re: [Haskell-cafe] A question about "monad laws"
My favorite presentation of the monad laws is associativity of Kliesli composition: (a1 >=> a2) x = a1 x >>= a2 -- predefined in 6.8 control.monad -- The laws return >=> a = a a >=> return = a a >=> (b >=> c) = (a >=> b) >=> c
If you use this presentation you also need the following law: (a . b) >=> c = (a >=> c) . b that is, compatibility with ordinary function composition. I like to call this "naturality", since it's instrumental in proving return and bind to be natural transformations. The law looks less alien if we use a flipped version of (>=>): (<=<) = flip (>=>) {- Monad Laws in terms of (<=<) -} return <=< f = f <=< return = f -- Identity f <=< (g <=< h) = (f <=< g) <=< h -- Associativity f <=< (g . h) = (f <=< g) . h -- Naturality (which happens to be my favorite presentation of the laws, followed by the derivations that lead to the 'do' notation, which lead to various 'ah' moments from unsuspecting FP-challenged friends) ----- Ariel J. Birnbaum -- View this message in context: http://www.nabble.com/A-question-about-%22monad-laws%22-tp15411587p15975734.... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
G'day all.
Quoting askyle
If you use this presentation you also need the following law: (a . b) >=> c = (a >=> c) . b
that is, compatibility with ordinary function composition. I like to call this "naturality", since it's instrumental in proving return and bind to be natural transformations.
Define: f >=> g = \x -> f x >>= g fmap f xs = xs >>= return . f Then: fmap f . return = (expand fmap) \x -> (return x >>= return . f) = (defn. of >=>) \x -> (return >=> return . f) x = (left identity) \x -> (return . f) x = return . f Therefore return is natural. Bind (or, equivalently, join) is left as an exercise. Cheers, Andrew Bromage
ajb-2 wrote:
Define: f >=> g = \x -> f x >>= g
So you're either not taking (>=>) as primitive or you're stating the additional property that there exists (>>=) such that f >=> g === (>>= g) . f (from which you can easily show that (f . g) >=> h === (f >=> h) . g ). A presentation of the monad laws based on (>=>) (I prefer (<=<) since it meshes better with (.) ) should (IMHO) regard (>=>) as primitive and state its needed properties whence one can derive all other formulations (Note that he Identity law then requires the existence of return as another primitive). That done, you define (>>=), fmap and the rest in terms of (<=<) : (>>=) = flip (<=< id) -- I like to put it as (>>= g) = (g <=< id) fmap f = (return . f) <=< id ----- Ariel J. Birnbaum -- View this message in context: http://www.nabble.com/A-question-about-%22monad-laws%22-tp15411587p16045123.... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
G'day all.
Quoting askyle
So you're either not taking (>=>) as primitive or you're stating the additional property that there exists (>>=) such that f >=> g === (>>= g) . f (from which you can easily show that (f . g) >=> h === (f >=> h) . g ).
If you wanted to prove that bind is natural, you would need to define bind, no? Cheers, Andrew Bromage
ajb-2 wrote:
If you wanted to prove that bind is natural, you would need to define bind, no?
Yup: bind f = f <=< id -- whence you can say (>>=) = flip bind My point is that (as far as I can see) you cannot prove the properties of bind by only assuming identity and associativity for (<=<). You need some way to relate (<=<) to normal composition. To be more explicit: Given: 1. m :: * -> * 2. return :: a -> m a 3. (<=<) :: (b -> m c) -> (a -> m b) -> (a -> m c) such that: 1. return <=< f === f <=< return === f 2. (f <=< g) <=< h === f <=< (g <=< h) Define: bind f = f <=< id (>>=) = flip bind fmap f = bind (return . f) join = bind id Show the monad laws hold, either for (return,bind), (return,(>>=)) or (fmap,return,join) (in the latter case, there's also showing that fmap is a functor and return and join are natural transformations). If someone can show it can be done without also assuming: 3. (f <=< g) . h === f <=< (g . h) I'll stand corrected. ----- Ariel J. Birnbaum -- View this message in context: http://www.nabble.com/A-question-about-%22monad-laws%22-tp15411587p16065960.... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
G'day all.
Quoting askyle
Yup: bind f = f <=< id -- whence you can say (>>=) = flip bind
Ah, yes.
My point is that (as far as I can see) you cannot prove the properties of bind by only assuming identity and associativity for (<=<).
One thing that may help is that if you can prove that fmap is sane: fmap (f . g) = fmap f . fmap g then the naturality of return is precisely its free theorem, and ditto for bind. So perhaps this law: (f <=< g) . h === f <=< (g . h) is actually the fmap law in disguise? Cheers, Andrew Bromage
ajb-2 wrote:
One thing that may help is that if you can prove that fmap is sane: fmap (f . g) = fmap f . fmap g
I get stuck after expanding the rhs into: ((return . f) <=< id) . ((return . g) <=< id) ajb-2 wrote:
then the naturality of return is precisely its free theorem, and ditto for bind.
Care to develop? IIRC the free theorems have a certain parametericity requirement (which probably holds in all interesting cases, but still sounds like an additional assumption). I'm not too familiar with these, so a link would be appreciated =) ajb-2 wrote:
So perhaps this law: (f <=< g) . h === f <=< (g . h) is actually the fmap law in disguise?
Could be. Maybe the fmap law is this one in disguise ;) ----- Ariel J. Birnbaum -- View this message in context: http://www.nabble.com/A-question-about-%22monad-laws%22-tp15411587p16069396.... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
participants (2)
-
ajb＠spamcop.net -
askyle