Re: [Haskell-cafe] A question about monad laws
C K Kashyap schrieb: Hi, I am trying to get a better understanding of the monad laws - right now, it seems too obvious and pointless. I had similar feelings about identity function when I first saw it but understood its use when I saw it in action. Could someone please help me get a better understanding of the necessity of monads complying with these laws? I think, examples of somethings stop working if the monad does not obey these laws will help me understand it better. http://www.haskell.org/haskellwiki/Monad_laws ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Hi Kashyap, Could someone please help me get a better understanding of the necessity of monads complying with these laws? Maybe it helps to write them in do-notation. Once written like this, it becomes clear(er?) that do-notation would be much less intuitive if the laws would not hold: Left Unit: return x = \y - f y = f x do y - return x f y = do f x Right Unit: a = \x - return x = a do x - a return x = do a Associativity: (a = \x - f x) = \y - g y = a = \x - (f x = \y - g y) do y - do x - a f x g y = do x - a y - f x g y So, at least, the monad laws ensure that do-notation behaves as one would expect. Sebastian ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Thank you very much Sebastian, The example did make it clearer. I can see now that monads obeying the laws is what lets the 'do' notation work on all monads in a consistent manner. Regards, Kashyap ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Perhaps this might help: I wrote a kind of logger monad that inserted messages with a context. Behind was an algebraic data type, let's say LoggerState. The API provided methods to add a message like this: addError :: String - Logger () addError Fatal error occurred addWarning Some warning etc. There were methods to enter and exit the context: enterContext :: String - Logger () exitContext :: Logger () enterContext System x enterContext SubSystem x.y enterContext Module x.y.z exitContext exitContext exitContext Well, the context was stored in an attribute of LoggerState, let's call it ctx. The add function would pick the current ctx and add it to the message. A message was defined as: ([Context], (State, String)) where State was Ok, Warning, Error. This, however, violates the associativity. In consequence, the context of messages would depend on parentheses, e.g.: someFunction :: Logger () someFunction = do enterContext A addError Some Error callSomeOtherFunction exitContext enterContext B ... produces a different result than: someFunction = enterContext A addError Some Error callSomeOtherFunction exitContext enterContext B ... Imagine: someFunction = enterContext A (addError Some Error callSomeOtherFunction exitContext) enterContext B ... Here, addError and callSomeOtherFunction would operate on a LoggerState without any Context, whereas in the previous example, there is context A. Without the associativity law, it would be very hard to determine the current state of the monad. Since the compiler, on desugaring do-blocks, will insert brackets, there is no guarantee that the results are the same as for the brace-less and sugar-free version of the code. Hope this helps! Tobias On 01/17/2011 04:21 AM, C K Kashyap wrote: Hi, I am trying to get a better understanding of the monad laws - right now, it seems too obvious and pointless. I had similar feelings about identity function when I first saw it but understood its use when I saw it in action. Could someone please help me get a better understanding of the necessity of monads complying with these laws? I think, examples of somethings stop working if the monad does not obey these laws will help me understand it better. Regards, Kashyap ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Thanks Tobias, Without the associativity law, it would be very hard to determine the current state of the monad. Since the compiler, on desugaring do-blocks, will insert brackets, there is no guarantee that the results are the same as for the brace-less and sugar-free version of the code. Indeed this example helps me. Regards, Kashyap ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A question about monad laws
Hi, I am trying to get a better understanding of the monad laws - right now, it seems too obvious and pointless. I had similar feelings about identity function when I first saw it but understood its use when I saw it in action. Could someone please help me get a better understanding of the necessity of monads complying with these laws? I think, examples of somethings stop working if the monad does not obey these laws will help me understand it better. Regards, Kashyap ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
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.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
G'day all. Quoting askyle [EMAIL PROTECTED]: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
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.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Wolfgang Jeltsch-2 wrote: No, I think, it’s the Prelude’s fault to define (==) as “floating point equality”. My bad, I meant IEEE (==) when I said it was our fault. I concur that the Prelude is at fault for using the (==) symbol for FP equality. Even if you don't demand from (==) to be an equivalence, you're giving a pure functional type to an impure operation (e.g because of SNaNs) My point was that since Haskell has a known and established mechanism for delimiting impurity, it seems as a shame not to use it to add some rigour to the myth-ridden, poorly understood floating point world. We need good FP for FP =) - Ariel J. Birnbaum -- View this message in context: http://www.nabble.com/A-question-about-%22monad-laws%22-tp15411587p16044986.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
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.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
G'day all. Quoting askyle [EMAIL PROTECTED]: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Am Donnerstag, 13. März 2008 21:10 schrieben Sie: Not to be picky, but where did you hear that (==) established an equivalence relation? I think that’s the way it should be according to most Haskeller’s opinion. It might be true that the Haskell 98 report doesn’t say so but I think that many library types and functions (Data.Set stuff, for example) rely on this. A future standard should state laws an instance has to obey for every class it introduces. […] Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Am Mittwoch, 12. März 2008 00:53 schrieb askyle: […] So if floating point (==) doesn't correspond with numeric equality, it's not FP's fault, but ours for expecting it to do! No, I think, it’s the Prelude’s fault to define (==) as “floating point equality”. We should us a different identifier like floatingPointEq. (==) is expected to be an equivalence relation. (I think I already said this.) […] Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Not to be picky, but where did you hear that (==) established an equivalence relation? Not I expect from the Haskell98 Report! The only law I can find there is that x /= y iff not (x == y) So, the definition x == y = False x /= y = True would be perfectly legitimate, making x /= x = True, which kind of ruins the equivalence relation thing, no? Dan Wolfgang Jeltsch wrote: Am Mittwoch, 12. März 2008 00:53 schrieb askyle: […] So if floating point (==) doesn't correspond with numeric equality, it's not FP's fault, but ours for expecting it to do! No, I think, it’s the Prelude’s fault to define (==) as “floating point equality”. We should us a different identifier like floatingPointEq. (==) is expected to be an equivalence relation. (I think I already said this.) […] Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re: [Haskell-cafe] A question about monad laws
I'm not sure whether this is the right branch of the thread for this post. Maybe it belongs to a different thread altogether. But here goes: Maybe most of our gripes with floating point arithmetic (besides broken implementations) is that we expect it to behave like Real arithmetic, and when it doesn't, we whine that it's unreliable, ill-defined, etc etc etc. If we consider FP as a mathematical entity of its own (e.g as defined in IEEE 754), we see that it has a well-defined, reliable behaviour which happens to emulate the behaviour of the real numbers within some margins. The accuracy of this emulation can be analyzed in a rigorous manner, see http://www.validlab.com/goldberg/paper.pdf So if floating point (==) doesn't correspond with numeric equality, it's not FP's fault, but ours for expecting it to do! By the way, IEEE754 does define another comparison operator which corresponds to our notion of 'equality'. FP (==) is just a partial equivalence relation which makes more sense than mathematical equality in an FP context. Of course, if an implementation doesn't guarantee that 'x == x' yields true whenever x is not a NaN, then the implementation is broken. An earlier post said that Haskell is not math (or something like it). I beg to differ -- one of its selling points, after all, is supposed to be the ability to perform equational reasoning. We work hard to give well-defined semantics to our expressions. We rely on types to tell us which properties to expect of which values, and which manipulations are valid. But then Haskell goes and fools us (just like most other languages do) into thinking FP arithmetic is something that it's not: the behaviour of operations depends on an unseen environment (e.g. rounding mode), the order of evaluation matters, evaluation can fail... not at all what we'd call purely functional! So if FP arithmetic is not purely functional, what do we do? If we could do Haskell all over again, I'd propose a different approach to FP arithmetic (and for stuff like Int, for that matter), which I'm actually surprised not to see discussed more often since it's after all the usual Haskell approach to things which are not purely functional. The original topic of this thread should already have hinted at it. ;) - Ariel J. Birnbaum -- View this message in context: http://www.nabble.com/A-question-about-%22monad-laws%22-tp15411587p15976463.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
G'day all. Quoting askyle [EMAIL PROTECTED]: 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
2008/2/12 Uwe Hollerbach [EMAIL PROTECTED]: Well... I dunno. Looking at the source to GHC.Real, I see infinity, notANumber :: Rational infinity = 1 :% 0 notANumber = 0 :% 0 This is actually the reason I imported GHC.Real, because just plain % normalizes the rational number it creates, and that barfs very quickly when the denominator is 0. But the values themselves look perfectly reasonable... no? Ummm... I'm going to have to go with no. In particular we can't have signed infinity represented like this and maintain reasonable numeric laws: 1/0 = 1/(-0) = (-1)/0 Rationals are defined not to have a zero denomiator, so I'll bet in more than one place in Data.Ratio that assumption is made. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On Feb 12, 2008 6:12 AM, Jan-Willem Maessen [EMAIL PROTECTED] wrote: On Feb 12, 2008, at 1:50 AM, David Benbennick wrote: On Feb 11, 2008 10:18 PM, Uwe Hollerbach [EMAIL PROTECTED] wrote: If I fire up ghci, import Data.Ratio and GHC.Real, and then ask about the type of infinity, it tells me Rational, which as far as I can tell is Ratio Integer...? Yes, Rational is Ratio Integer. It might not be a good idea to import GHC.Real, since it doesn't seem to be documented at http://www.haskell.org/ghc/docs/latest/html/libraries/. If you just import Data.Ratio, and define pinf :: Integer pinf = 1 % 0 ninf :: Integer ninf = (-1) % 0 Then things fail the way you expect (basically, Data.Ratio isn't written to support infinity). But it's really odd the way the infinity from GHC.Real works. Anyone have an explanation? An educated guess here: the value in GHC.Real is designed to permit fromRational to yield the appropriate high-precision floating value for infinity (exploiting IEEE arithmetic in a simple, easily- understood way). If I'm right, it probably wasn't intended to be used as a Rational at all, nor to be exploited by user code. -Jan-Willem Maessen Well... I dunno. Looking at the source to GHC.Real, I see infinity, notANumber :: Rationalinfinity = 1 :% 0notANumber = 0 :% 0 This is actually the reason I imported GHC.Real, because just plain % normalizes the rational number it creates, and that barfs very quickly when the denominator is 0. But the values themselves look perfectly reasonable... no? Uwe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On Feb 12, 2008, at 1:50 AM, David Benbennick wrote: On Feb 11, 2008 10:18 PM, Uwe Hollerbach [EMAIL PROTECTED] wrote: If I fire up ghci, import Data.Ratio and GHC.Real, and then ask about the type of infinity, it tells me Rational, which as far as I can tell is Ratio Integer...? Yes, Rational is Ratio Integer. It might not be a good idea to import GHC.Real, since it doesn't seem to be documented at http://www.haskell.org/ghc/docs/latest/html/libraries/. If you just import Data.Ratio, and define pinf :: Integer pinf = 1 % 0 ninf :: Integer ninf = (-1) % 0 Then things fail the way you expect (basically, Data.Ratio isn't written to support infinity). But it's really odd the way the infinity from GHC.Real works. Anyone have an explanation? An educated guess here: the value in GHC.Real is designed to permit fromRational to yield the appropriate high-precision floating value for infinity (exploiting IEEE arithmetic in a simple, easily- understood way). If I'm right, it probably wasn't intended to be used as a Rational at all, nor to be exploited by user code. -Jan-Willem Maessen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
David Benbennick wrote: Some months ago I pointed out that Ratio Int (which is an Ord instance) doesn't satisfy this property. I provided a patch to fix the problem, but my bug report was closed as wontfix: http://hackage.haskell.org/trac/ghc/ticket/1517. Richard A. O'Keefe wrote: I'm not happy about that response... I am extremely grateful for this report, because now I know NEVER USE Ratio Int, it's too broken. Ian wrote, in the Trac ticket: Thanks for the patch, but I see a couple of problems: ...If you still think that this change should be made then I think that it should go through the library submissions process: http://www.haskell.org/haskellwiki/Library_submissions The wontfix resolution does not mean that the patch was rejected. It just means that there are reasons for and against it, so GHC HQ is not unilaterally implementing it without giving the community a chance to discuss the issues. I think that is an admirable attitude. If you feel that this issue is important, why not go ahead and start the process to get it adopted? Regards, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On Feb 11, 2008 11:24 AM, Wolfgang Jeltsch [EMAIL PROTECTED] wrote: a b b c = a c If an Ord instances doesn't obey these laws than it's likely to make Set and Map behave strangely. Some months ago I pointed out that Ratio Int (which is an Ord instance) doesn't satisfy this property. I provided a patch to fix the problem, but my bug report was closed as wontfix: http://hackage.haskell.org/trac/ghc/ticket/1517. -- I'm doing Science and I'm still alive. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On Mon, Feb 11, 2008 at 01:59:09PM +, Neil Mitchell wrote: Hi (x = f) = g == x = (\v - f v = g) Or stated another way: (x = f) = g == x = (f = g) Which is totally wrong, woops. See this page for lots of details about the Monad Laws and quite a nice explanation of where you use them: http://www.haskell.org/haskellwiki/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 Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Am Montag, 11. Februar 2008 14:57 schrieb Michael Reid: Now it should be easier to see that this is simply associativity. It's easy enough to violate, if you want to - but I don't have any nice simple examples to hand. I have recently been reading a tutorial or paper where a Monad that violated this law was presented. The authors shrugged it off as not important, that the notation gained by implementing the operation as a Monad was worth it, but what is not clear is what the consequences of violating such associativity are. Does violating this law introduce the potential that your program will not do what you think it should? /mike. Other libraries might (and probably will) expect Monad instances to satisfy the monad laws and will not work as intended or even make sense if the monad laws aren’t satisfied. Sometimes it looks as if people think that monads are special in that they have to satisfy certain laws. But this isn’t the case. Practically every Haskell type class has some laws (informally) attached to it which instances should satisfy. For example, the following should hold for instances of the Ord class: a b = compare a b = LT a == b = compare a b = EQ a b = compare a b = GT a = b = a b || a == b a = b = a b || a == b a b = b a a b b c = a c If an Ord instances doesn’t obey these laws than it’s likely to make Set and Map behave strangely. Best wishes, Wolfgang ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
IOn Feb 11, 2008 9:46 AM, Miguel Mitrofanov [EMAIL PROTECTED] wrote: It's well known that ListT m monad violates this law in general (though it satisfies it for some particular monads m). For example, I went through this example in quite a bit of detail a while ago and wrote it up here: http://sigfpe.blogspot.com/2006/11/why-isnt-listt-monad.html . I tried to show not just why the monad laws fails to hold for ListT [], but also show how it almost holds. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On 11 Feb 2008, at 5:33 AM, Deokjae Lee wrote: Tutorials about monad mention the monad axioms or monad laws. The tutorial All About Monads says that It is up to the programmer to ensure that any Monad instance he creates satisfies the monad laws. The following is one of the laws. (x = f) = g == x = (\v - f v = g) However, this seems to me a kind of mathematical identity. What do you mean by identity? It's easy enough to violate: newtype Gen a = Gen (StdGen - a) runGen :: Gen a - StdGen - a runGen (Gen f) = f instance Monad Gen where return x = Gen (const x) a = f = Gen (\ r - let (r1, r2) = split r in runGen (f (runGen a r1)) r2) [1] split returns two generators independent of each other and of its argument; thus, this `monad' violates all *three* of the monad laws, in the sense of equality. So, for example, the program do x - a return x denotes a random variable independent of (and hence distinct from) a. In general, you want some kind of backstop `equality' (e.g., that the monad laws hold in the sense of identical distribution) when you violate them; otherwise, you will violate the expectations your users have from the syntax of the do notation. jcc [1] Test.QuickCheck ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Deokjae Lee cites: The tutorial All About Monads says that It is up to the programmer to ensure that any Monad instance he creates satisfies the monad laws. The following is one of the laws. (x = f) = g == x = (\v - f v = g) However, this seems to me a kind of mathematical identity. If it is mathematical identity, a programmer need not care about this law to implement a monad. Can anyone give me an example implementation of monad that violate this law ? After three or five reactions to this posting, I think it it is time to generalize. Haskell is not math. Or rather, there is no way to be sure that the *implementation* of some mathematical domains and operations thereupon are fool-proof. Sometimes you break en passant some sacred laws. For example the transitivity of ordering. 52, right? and 85 as well. But, imagine a - little esoteric example of cyclic arithmetic modulo 10, where the shortest distance gives you the order, so 28. A mathematician will shrug, saying that calling +that+ an order relation is nonsense, and he/she will be absolutely right. But people do that... There is a small obscure religious sect of people who want to implement several mathematical entities as functional operators, where multiplication is f. composition. You do it too generically, too optimistically, and then some octonions come and break your teeth. So, people *should care*. Jerzy Karczmarczuk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Now it should be easier to see that this is simply associativity. It's easy enough to violate, if you want to - but I don't have any nice simple examples to hand. I have recently been reading a tutorial or paper where a Monad that violated this law was presented. The authors shrugged it off as not important, that the notation gained by implementing the operation as a Monad was worth it, but what is not clear is what the consequences of violating such associativity are. Does violating this law introduce the potential that your program will not do what you think it should? /mike. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A question about monad laws
Tutorials about monad mention the monad axioms or monad laws. The tutorial All About Monads says that It is up to the programmer to ensure that any Monad instance he creates satisfies the monad laws. The following is one of the laws. (x = f) = g == x = (\v - f v = g) However, this seems to me a kind of mathematical identity. If it is mathematical identity, a programmer need not care about this law to implement a monad. Can anyone give me an example implementation of monad that violate this law ? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
Ratio Integer may possibly have the same trouble, or maybe something related. I was messing around with various operators on Rationals and found that positive and negative infinity don't compare right. Here's a small program which shows this; if I'm doing something wrong, I'd most appreciate it being pointed out to me. If I fire up ghci, import Data.Ratio and GHC.Real, and then ask about the type of infinity, it tells me Rational, which as far as I can tell is Ratio Integer...? So far I have only found these wrong results when I compare the two infinities. Uwe module Main where import Prelude import Data.Ratio import GHC.Real pinf = infinity ninf = -infinity zero = 0 main = do putStrLn (pinf = ++ (show pinf)) putStrLn (ninf = ++ (show ninf)) putStrLn (zero = ++ (show zero)) putStrLn (min pinf zero =\t ++ (show (min pinf zero))) putStrLn (min ninf zero =\t ++ (show (min ninf zero))) putStrLn (min ninf pinf =\t ++ (show (min ninf pinf))) putStrLn (min pinf ninf =\t ++ (show (min pinf ninf)) ++ \twrong) putStrLn (max pinf zero =\t ++ (show (max pinf zero))) putStrLn (max ninf zero =\t ++ (show (max ninf zero))) putStrLn (max ninf pinf =\t ++ (show (max ninf pinf))) putStrLn (max pinf ninf =\t ++ (show (max pinf ninf)) ++ \twrong) putStrLn (() pinf zero =\t ++ (show (() pinf zero))) putStrLn (() ninf zero =\t ++ (show (() ninf zero))) putStrLn (() ninf pinf =\t ++ (show (() ninf pinf)) ++ \twrong) putStrLn (() pinf ninf =\t ++ (show (() pinf ninf))) putStrLn (() pinf zero =\t ++ (show (() pinf zero))) putStrLn (() ninf zero =\t ++ (show (() ninf zero))) putStrLn (() ninf pinf =\t ++ (show (() ninf pinf))) putStrLn (() pinf ninf =\t ++ (show (() pinf ninf)) ++ \twrong) putStrLn ((=) pinf zero =\t ++ (show ((=) pinf zero))) putStrLn ((=) ninf zero =\t ++ (show ((=) ninf zero))) putStrLn ((=) ninf pinf =\t ++ (show ((=) ninf pinf))) putStrLn ((=) pinf ninf =\t ++ (show ((=) pinf ninf)) ++ \twrong) putStrLn ((=) pinf zero =\t ++ (show ((=) pinf zero))) putStrLn ((=) ninf zero =\t ++ (show ((=) ninf zero))) putStrLn ((=) ninf pinf =\t ++ (show ((=) ninf pinf))) putStrLn ((=) pinf ninf =\t ++ (show ((=) pinf ninf)) ++ \twrong) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On Feb 11, 2008 10:18 PM, Uwe Hollerbach [EMAIL PROTECTED] wrote: If I fire up ghci, import Data.Ratio and GHC.Real, and then ask about the type of infinity, it tells me Rational, which as far as I can tell is Ratio Integer...? Yes, Rational is Ratio Integer. It might not be a good idea to import GHC.Real, since it doesn't seem to be documented at http://www.haskell.org/ghc/docs/latest/html/libraries/. If you just import Data.Ratio, and define pinf :: Integer pinf = 1 % 0 ninf :: Integer ninf = (-1) % 0 Then things fail the way you expect (basically, Data.Ratio isn't written to support infinity). But it's really odd the way the infinity from GHC.Real works. Anyone have an explanation? -- I'm doing Science and I'm still alive. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
(x = f) = g == x = (\v - f v = g) However, this seems to me a kind of mathematical identity. If it is mathematical identity, a programmer need not care about this law to implement a monad. Can anyone give me an example implementation of monad that violate this law ? It's well known that ListT m monad violates this law in general (though it satisfies it for some particular monads m). For example, Prelude Control.Monad.List runListT ((ListT [[(),()]] ListT [[()], [()]]) ListT [[1],[2]]) [[1,1],[1,2],[2,1],[2,2],[1,1],[1,2],[2,1],[2,2],[1,1],[1,2],[2,1], [2,2],[1,1],[1,2],[2,1],[2,2]] Prelude Control.Monad.List runListT (ListT [[(),()]] (ListT [[()], [()]] ListT [[1],[2]])) [[1,1],[1,2],[1,1],[1,2],[2,1],[2,2],[2,1],[2,2],[1,1],[1,2],[1,1], [1,2],[2,1],[2,2],[2,1],[2,2]] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On 12 Feb 2008, at 10:35 am, David Benbennick wrote: Some months ago I pointed out that Ratio Int (which is an Ord instance) doesn't satisfy this property. I provided a patch to fix the problem, but my bug report was closed as wontfix: http://hackage.haskell.org/trac/ghc/ticket/1517. I'm not happy about that response. Basically, if the inputs to a mathematical operation are representable, and the mathematically correct result is representable, I expect a system to deliver it or die trying. What the intermediate calculations get up to is the implementor's problem, not the user's. On the other hand, if I knew in advance whether a particular + or * was going to overflow, I probably wouldn't need the computer to actually do it. But if I give the computer some numbers that are clearly representable and just ask it to *sort* them, it had better d--- well get that RIGHT. I am extremely grateful for this report, because now I know NEVER USE Ratio Int, it's too broken. Sad aside: back in the 70s I had my own Ratio Int written in Burroughs Algol. I was not smart enough to use double precision numbers for anything, but because of one hardware feature, it didn't matter a lot. That hardware feature was that integer overflows were TRAPPED and REPORTED. I have since used precisely one C compiler on precisely one Unix system that took advantage of the fact that the C standard (both C89 and C99) was very carefully written to ALLOW TRAPPING of signed integer overflows. (Contrary to mythology, C only requires wrapping for unsigned integers.) I found that a surprisingly valuable debugging aid. This all supports the general point, of course: data types whose operations are so implemented as to break sensible laws can and WILL land you in great piles of fresh steaming hot fertiliser. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A question about monad laws
On Mon, 2008-02-11 at 13:34 -0800, Stefan O'Rear wrote: On Mon, Feb 11, 2008 at 01:59:09PM +, Neil Mitchell wrote: Hi (x = f) = g == x = (\v - f v = g) Or stated another way: (x = f) = g == x = (f = g) Which is totally wrong, woops. See this page for lots of details about the Monad Laws and quite a nice explanation of where you use them: http://www.haskell.org/haskellwiki/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 Indeed. The monad laws are just that the Kleisli category is actually a category. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
