On Wed, Jun 25, 2014 at 12:33 PM, Mateusz Kowalczyk

wrote:

On 06/25/2014 05:54 AM, Rafael Almeida wrote:

...

Hello,

You guys have been great taking my questions. Thank you. Now I have another one :)

What can go wrong if I make an Monad instance but don't follow Monad rules (identity and associativity)? Sure it would be misleading for someone using the non-conforming class. They may make code that assume those laws, although they don't hold. However, could it make the compiler generate bad code

The compiler makes no assumption (at least that I know of) that laws are followed. It should never generate ‘bad’ code (whatever that might mean) anyway.

The compiler makes assumptions about associativity when de-sugaring do-notation. If the monad laws aren't followed, it's possible for these two blocks to show different behavior (given that a,b,c are all values of the misbehaved Monad instance):

do { a; b; c }

a >> b >> c

I think everyone can agree that this is surprising, at the very least. Although it's not the compiler that's generating bad code here. John L.

If the monad in question upholds the associativity law, then the chunks evaluate to the same result, but they're still distinct.

Distinct with respect to what equivalence relation? Also, an object isn't a monad if it isn't associative. On Wed, Jun 25, 2014 at 11:14 AM, Richard Eisenberg wrote:

On Jun 25, 2014, at 12:52 AM, John Lato wrote:

The compiler makes assumptions about associativity when de-sugaring do-notation. If the monad laws aren't followed, it's possible for these two blocks to show different behavior (given that a,b,c are all values of the misbehaved Monad instance):

...

do { a; b; c }

...

a >> b >> c

I think everyone can agree that this is surprising, at the very least. Although it's not the compiler that's generating bad code here.

As far as I know, GHC makes no assumptions about associativity, or any class-based laws. The effect John observes above is accurate, but it is a direct consequence of the design of Haskell in the Haskell 2010 Report, not any assumptions in the compiler.

Specifically, Section 3.14 ( https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-470003.1...) says that `do { e; stmts }` desugars to `e >> do {stmts}`. In the case of `do { a; b; c }`, that means we get `a >> (b >> c)`. However, in Table 4.1 in Section 4.4.2 (under https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-800004....), we see that (>>) is *left*-associative, meaning that `a >> b >> c` means `(a >> b) >> c`.

Are the different meanings here an "assumption" of associativity? I suppose one could construe it that way, but I just see `do { a; b; c}` and `a >> b >> c` as different chunks of code with different meanings. If the monad in question upholds the associativity law, then the chunks evaluate to the same result, but they're still distinct.

Richard

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Jun 25, 2014 at 3:14 PM, Richard Eisenberg wrote:

On Jun 25, 2014, at 12:52 AM, John Lato wrote:

The compiler makes assumptions about associativity when de-sugaring do-notation. If the monad laws aren't followed, it's possible for these two blocks to show different behavior (given that a,b,c are all values of the misbehaved Monad instance):

...

do { a; b; c }

...

a >> b >> c

I think everyone can agree that this is surprising, at the very least. Although it's not the compiler that's generating bad code here.

As far as I know, GHC makes no assumptions about associativity, or any class-based laws. The effect John observes above is accurate, but it is a direct consequence of the design of Haskell in the Haskell 2010 Report, not any assumptions in the compiler.

Specifically, Section 3.14 ( https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-470003.1...) says that `do { e; stmts }` desugars to `e >> do {stmts}`. In the case of `do { a; b; c }`, that means we get `a >> (b >> c)`. However, in Table 4.1 in Section 4.4.2 (under https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-800004....), we see that (>>) is *left*-associative, meaning that `a >> b >> c` means `(a >> b) >> c`.

Are the different meanings here an "assumption" of associativity? I suppose one could construe it that way, but I just see `do { a; b; c}` and `a >> b >> c` as different chunks of code with different meanings. If the monad in question upholds the associativity law, then the chunks evaluate to the same result, but they're still distinct.

Great explanation! Would you say that the main reason for implementing monads so >> is associative is to make sure the do notation does the "right thing"? Monad is a notion from math which was imported into Haskell. As far as I know, the reason behind it was to give Haskell the possibility of doing IO while keeping itself pure. If there was a data type just like Moand, with

...

=, >>, return and all. It behaved exactly the same, but no one cared about identity or associativity, then it wouldn't be a monad, but it would solve the computation with side-effects thing just the same. Why was associativity and identity brought to the language as well? What is there to be gained by such a law which can't be enforced by the compiler?

On Sun, Jun 29, 2014 at 12:11 AM, Brandon Allbery wrote:

On Sat, Jun 28, 2014 at 10:59 PM, Rafael Almeida wrote:

...

What is there to be gained by such a law which can't be enforced by the compiler?

There are lots of things that can't be enforced by the compiler; for example, it can't force you to write an Ord instance that implements a correct total ordering. Does this make Ord less useful to you? Or pointless?

No. I'm not trying to say Monad laws are useless or pointless. Rather, I am looking to understand the usefulness of those laws. People are indeed going to expect that the < operator is transitive. Even though the compiler can do nothing about it. I'm not sure how to explain why we need < to be transitive. If you do so, please explain that to me as well. I always took it for granted that such law must be obeyed.

On Sat, Jun 28, 2014 at 10:52 PM, Brandon Allbery wrote:

I imagine that, like Ord, a decision was made to implement the proper mathematical abstraction and not merely a convenient one. This seems to be the "Haskell way". (I'm not sure how it explains Double, though the numeric hierarchy has a lot of compromises in the name of convenience or expected behavior. Possibly Monad was in some sense a reaction to this, even: "we got that one wrong, let's do this one correctly".)

Double, like Int, is a computer construct, not a mathematical one. They both map to hardware types that act like mathematical ones until you look closely, but have better performance than the software constructs that have better behavior.

On the subject of Double and laws, I imagine it would have been possible to do the kind of thing the SML Basis Library does for equality. SML spells equality '=' and it's not defined on the floating point types, which have a *different* operator, '=='. In the same way, the Prelude could have been structured so that integers and ratios belonged to Ord but floats did not. Floats could have had operators like #< #= instead. It would have been surprising, but so is x == x being False surprising.

Is x == x being false really any more surprising than x + 1 == x being true?

Yes, a lot more. Equality is a symmetric relation. So "x equals x" is true for every x. A logic/language in which that is not true is unsound. x + 1 == x is just an equation. Coming up with a theory where it holds is straightforward. For example, addition followed by the "fractional part" operation, on the set [0,1].

On Sun, Jun 29, 2014 at 4:29 PM, Mike Meyer wrote:

On Sun, Jun 29, 2014 at 6:05 PM, Alexander Solla wrote:

...

...

Is x == x being false really any more surprising than x + 1 == x being true?

Yes, a lot more. Equality is a symmetric relation. So "x equals x" is true for every x. A logic/language in which that is not true is unsound.

x + 1 == x is just an equation. Coming up with a theory where it holds is straightforward. For example, addition followed by the "fractional part" operation, on the set [0,1].

Your theory is wrong. This is the same problem you run into with "x == x" being False: you create theories from assumptions about how these things behave based on your experience with abstract mathematical objects, and there are values for which those assumptions do not hold. Surprise results when you run into those cases.

You can call it "wrong", but it doesn't make it so. (==) is supposed to model (witness) equality. The laws for Eq are the theory.

IEEE 754 floats under + and * are *not* ℝ. Or even ℚ. They just play them in the computer. There are simple large subsets of possible operands for which addition (and hence the other three operators) doesn't work like the mathematical realities they model.

I didn't say they are. I had not committed myself to any position about floating point numbers. They are certainly degenerate objects, similar to bottom, and do not "model" numbers. Specifically because they (floats) I think the problem here is that you're confusing the theory with the model. You are definitely misusing the terminology, and unfortunately, projecting at us for not understanding it they way you want us to.

On 29/06/2014, at 9:53 PM, Mike Meyer wrote:

On Sun, Jun 29, 2014 at 4:28 AM, wrote: On the subject of Double and laws, I imagine it would have been possible to do the kind of thing the SML Basis Library does for equality. SML spells equality '=' and it's not defined on the floating point types, which have a *different* operator, '=='.

If you do that, where do you stop?

Well, SML stopped right there.

Not all Int's have additive inverses, and most floats have multiple things they can be added to that don't change their value. Can we call both of those +? Or do we need a name for them or two?

For what it's worth, O'CAML *does* have separate operators for integer addition and floating-point addition.

Actually, I don't know if SML got it right or not, because I don't know what the "==" operator does.

It's really very easy to find on the web. val == real * real -> bool val != real * real -> bool val ?= real * real -> bool [x == y] returns true if and only if neither x nor y is a NaN and x and y are equal, ignoring signs on zeros. This function is equivalent to the IEEE = operator. The second function != is equivalent to (not o op ==) and the IEEE ?<> operator. [?=] returns true if and only if either argument is a NaN or the arguments are bitwise equal, ignoring signs on zeros. It is equivalent to the IEEE ?= operator.

But you should *never* compare floats for equality.

You are mistaken.

While there are exceptions, they are so rare that you're likely never to run into one, so just be safe, and don't do it.

I have in fact *often* run into the so-called exceptions. Indeed, anyone using Javascript and wanting to compare two "integers" will in fact be comparing floating point numbers and they will be fully justified in doing so.

So if SML's "==" operator is an equality comparison, they at best got it half right.

It depends on what you want to call 'an equality comparison'. It is one of the comparison operators specified in the IEEE standard. There is no fuzziness or ambiguity about its semantics. They COULDN'T leave it out and claim IEEE conformance.

If it's some kind of programmer-controlled "fuzzy equality", well, maybe. But I think just leaving it out would be a better solution.

I have seldom seen any kind of programmer-controlled "fuzzy equality" that wasn't either dangerously wrong or dangerously misapplied, and I speak as an old APLer who knows what ⌷CT stands for, where to find it in the standard, and why it is risky. If you leave out ==, some irritated programmer will just define fun ==(x, y) = x >= y andalso x <= y and you're back where you started. To prevent anyone doing that, you have to leave out *ALL* the floating-point comparison operators. That is not sensible.

Is x == x being false really any more surprising than x + 1 == x being true?

Yes. The idea of there being a "number" x such that x + 1 == x is familiar to anyone who has ever met the extended real line. Or who knows that ℵ₀ + 1 = ℵ₀.