On Sun, May 3, 2015 at 6:50 PM, Carter Schonwald <carter.schonwald@gmail.com> wrote:

.... how would you have an implementation of finite precision floating point that has the "expected" exact algebraic laws for * and +?

That's model #1 that we can't have. So you don't.

I would argue that Float and Double do satisfy a form of the standard algebric laws where equality is approximate.

eg (a+(b+c)) - ((a+b)+c) <= \epsilon, where epsilon is some constant multiple of max(ulp(a),ulp(b),ulp(c)).
(a similar idea applies to pretty much any other algebraic law you can state, such as distributivity etc)

So how do you fix the fact that any comparison with a NaN and a non-NaN is false? Among other IEEE oddities.

I do think that it'd be useful if the RealFloat class provided an ulp function (unit of least precision), which is available as part of any IEEE compliant c float library.

there are MANY computable number represntations where the *exact* algebraic laws dont hold, but this *approximate* form which provides some notion of bounded forwards/backwards relative/absolute error bound guarantee in a particularly strong way.

True. That's the root of the problem the proposal is trying to solve.

i think we should figure out articulating laws that play nice for both the *exact* and *approximate* universes.

We also need laws that play nice for the IEEE universe, because people doing serious numerical work want that one. I believe you will wind up with two different sets of laws, which is why I proposed taking the parts that don't agree out of the Prelude, and letting users import the ones they want to use.