Re: [Haskell-cafe] Why not some subclass of Floating to model NaNs as some handleable bottom?

Great! I'm intrigued by the idea that GHCi can make such math sentences runnable! I've never thought it this way before. But I need some help to get it going: λ> :set -XTypeSynonymInstances λ> :set -XFlexibleInstances λ> λ> import Data.Ratio λ> type Q = Rational -- this is probably wrong ... λ> λ> type NonNegativeNumber = ([Q],[Q]) λ> :{ λ| instance Num NonNegativeNumber where λ| (l,r) * (l',r') = ([x*x'|x <- l, x' <- l'],[y*y'|y <- r, y' <- r']) λ| :} <interactive>:9:12: warning: [-Wmissing-methods] • No explicit implementation for ‘+’, ‘abs’, ‘signum’, ‘fromInteger’, and (either ‘negate’ or ‘-’) • In the instance declaration for ‘Num NonNegativeNumber’ λ> λ> zero = ([],Q) <interactive>:13:13: error: Data constructor not in scope: Q λ> infty = (Q,[]) <interactive>:14:10: error: Data constructor not in scope: Q λ> λ> zero * infty -- expect: = ([],[]) <interactive>:16:1: error: Variable not in scope: zero <interactive>:16:8: error: Variable not in scope: infty λ> I'd like to do more exercises, but I'm stuck here ...

On 2021-08-07, at 06:16, Olaf Klinke wrote:

On Fri, 2021-08-06 at 22:21 +0800, YueCompl wrote:

...

Thanks Olaf,

Metaphors to other constructs are quite inspiring to me, though I don't have sufficient theoretical background to fully understand them atm.

Pen-and-paper or GHCi experiments suffice here, no fancy theoretical background needed. Say Q is the type of rationals 0 < q and we express type NonNegativeNumber = ([Q],[Q]) where the first (infinite) list is the lower approximants and the second the upper approximants. Multiplication is then defined as (l,r) * (l',r') = ([x*x'|x <- l, x' <- l'],[y*y'|y <- r, y' <- r']) The extremes of this type are 0 = ([],Q) infty = (Q,[]) It is easily seen that 0 * infty = ([],[]) a number with no lower and no upper approximants, in other words, NaN. Excercise: Define division for this type and find out what 1/0 and 0/0 is.

...

Am I understanding it right, that you mean `0/0` is hopeful to get ratified as "a special Float value corresponding to one non-proper Dedekind-cuts", but `NaN` as with IEEE semantics is so broken that it can only live outlaw, even Haskell the language shall decide to bless it?

Yes. I think it is vital that we provide a migration path for programmers coming from other languages. Under the Dedekind cut/interval interpretation, NaN would behave differently, as I pointed out. So I'd leave Float as it is, but be more verbose about its violation of type class laws. To this end, one could have (and now I might be closer to your initial question) numerical type classes like HonestEq, HonestOrd, HonestMonoid and HonestRing whose members are only those types that obey the laws in all elements. Naturally, Float would not be a member. Who would use these new classes? Probably no one, because we all like to take the quick and dirty route. But at least it says clearly: Careful, you can not rely on these laws when using Float.

Olaf