Re: A bug with Sum (as in Monoid)

As pointed out, most "usual" algebraic equations simply do not hold for IEEE754 floating-point numbers. Another example is `1+x == 1 /\ x /= 0` is a satisfiable statement. Just wanted to point out you can use modern SMT solvers to analyze such equalities, and Haskell SBV package (shameless plug) provides a convenient interface. Here's the counter-example showing the non-associativity of addition: http://hackage.haskell.org/package/sbv-8.5/docs/Documentation-SBV-Examples-M... There are other examples in there as well that might be of interest. Cheers, -Levent. On Wed, Nov 6, 2019 at 2:31 PM Lana Black wrote:

On 06/11/2019 22:19, Dannyu NDos wrote:

...

Omg, addition is not even associative? The zeros truly ruined everything.

2019년 11월 7일 (목) 06:58, Brent Yorgey 님이 작성:

...

How is that worse than the fact that addition is already not associative for floating point types? At least +0 is really the identity up to (==).

On Wed, Nov 6, 2019, 3:49 PM Dannyu NDos wrote:

...

Sum has bug with floating points. Current definition states +0 as the identity element, while the actual identity is -0 since +0 + -0 = +0. _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

This has little to do with zeroes per se. IEEE 754 addition isn't associative for any numbers, and examples not involving zeroes aren't hard to find. Here's one:

Prelude> let a = 1e30 :: Double Prelude> let b = -1e30 :: Double Prelude> let c = 1 :: Double Prelude> a + b + c 1.0 Prelude> a + (b + c) 0.0

There is a good document describing how IEEE754 works, including this kind of peculiarities: https://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries