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

Okay, I got it working to some extent: (and I find it a good showcase for my https://marketplace.visualstudio.com/items?itemName=ComplYue.vscode-ghci https://marketplace.visualstudio.com/items?itemName=ComplYue.vscode-ghci extension, improved it a bit to support this very scenario, with the src file at https://github.com/complyue/typing.hs/blob/main/src/PoC/Floating.hs https://github.com/complyue/typing.hs/blob/main/src/PoC/Floating.hs ) Obviously my naive implementation `(l, r) / (l', r') = ([x / x' | x <- l, x' <- l'], [y / y' | y <- r, y' <- r'])` is wrong, I think I need to figure out how to represent 1 (the unit number) of this type, even before I can come to a correct definition of the division (/) operation, but so far no clue ...

On 2021-08-07, at 16:16, YueCompl via Haskell-Cafe wrote:

Another failed attempt:

λ> :set -XTypeSynonymInstances λ> :set -XFlexibleInstances λ> λ> data Q = Q λ> λ> 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>:12:25: error: • No instance for (Num Q) arising from a use of ‘*’ • In the expression: x * x' In the expression: [x * x' | x <- l, x' <- l'] In the expression: ([x * x' | x <- l, x' <- l'], [y * y' | y <- r, y' <- r']) λ> λ> zero = ([],Q) λ> infty = (Q,[]) λ> zero * infty

<interactive>:17:8: error: • Couldn't match type ‘Q’ with ‘[a]’ Expected type: ([a], Q) Actual type: (Q, [a0]) • In the second argument of ‘(*)’, namely ‘infty’ In the expression: zero * infty In an equation for ‘it’: it = zero * infty • Relevant bindings include it :: ([a], Q) (bound at <interactive>:17:1) λ>

...

On 2021-08-07, at 15:35, YueCompl via Haskell-Cafe mailto:haskell-cafe@haskell.org> wrote:

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 mailto:olf@aatal-apotheke.de> 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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Thanks Olaf, The surreal implementation should help a lot for me to understand the ideas deep enough. I developed the habit to understand things by tweaking code one little bit a time, and see the differences I made, to get intuitions about how it works, that's due to my career as a software engineer / hacker I guess. I already felt the difference with Haskell in software engineering practices, than with other programming communities, and I'm quite happy that I can enjoy the beauty of math here, though I'm some slow in understanding things mathematically. I think I just need more time :-) Best regards, Compl

On 2021-08-08, at 04:54, Olaf Klinke wrote:

Dear Compl,

Apologies, my code was meant as math formula in Haskell syntax. For starters, something like [x*y | x <- xs, y <- ys] will not go past the first element of xs if the other list ys is infinite. Hence you need another way to enumerate an infinite 2-D grid. I also used the symbol Q as shorthand for "a list that is cofinal in the set Q" which in case of lower approximants can be [1..] and in the case of upper approximants can be (fmap recip [1..]). If you can maintain the invariant that both lists of approximants are ascending or descending, respecively, then you can replace the above list comprehension by zipWith (*) xs ys which will also be much faster and does the right thing if one list is empty and the other is infinite.

Further I wouldn't go directly for a full Num instance but define the arithmetic functions one by one under a different name. That way the "No explicit implementation for ..." doesn't bite you. Once you have defined all, the Num instance is just aliasing the Num functions with your type-specific ones.

For division, you need to think this way: I have a quotient a/b. When I wobble a or b in either direction, does the quotient get smaller (lower approximant) or larger (upper approximant)? Clearly, when replacing a by one of its lower approximants x, then x/b < a/b. (This is only true because we're excluding negative numbers!) Likewise for upper approximants to a. Next, if b is replaced by one of its upper approximants y', then x/y' < x/b < a/b. We conclude that the lower approximants of a/b are of the form x/y' where x is a lower approximant of a and y' is an upper approximant of b.

When you're done, you will have implemented exact real arithmetic, which does not suffer from the rounding errors but is usually also much slower than floating point arithmetic. And as a by-product you will have a proof that NaN is the price we must pay for totality of (/) and (*).

I also attach a chapter from my monograph "Haskell for mathematicians" which is a literate program containing three different implementations of exact reals in Haskell, Conway's surreal numbers being one of them, as well as a more comprehensive surreal numbers implementation.

Olaf

On Sat, 2021-08-07 at 18:21 +0800, YueCompl wrote:

...

Okay, I got it working to some extent: (and I find it a good showcase for my https://marketplace.visualstudio.com/items?itemName=ComplYue.vscode-ghci https://marketplace.visualstudio.com/items?itemName=ComplYue.vscode-ghci extension, improved it a bit to support this very scenario, with the src file at https://github.com/complyue/typing.hs/blob/main/src/PoC/Floating.hs https://github.com/complyue/typing.hs/blob/main/src/PoC/Floating.hs )

Obviously my naive implementation `(l, r) / (l', r') = ([x / x' | x <- l, x' <- l'], [y / y' | y <- r, y' <- r'])` is wrong, I think I need to figure out how to represent 1 (the unit number) of this type, even before I can come to a correct definition of the division (/) operation, but so far no clue ...

...

On 2021-08-07, at 16:16, YueCompl via Haskell-Cafe wrote:

Another failed attempt:

λ> :set -XTypeSynonymInstances λ> :set -XFlexibleInstances λ> λ> data Q = Q λ> λ> 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>:12:25: error: • No instance for (Num Q) arising from a use of ‘*’ • In the expression: x * x' In the expression: [x * x' | x <- l, x' <- l'] In the expression: ([x * x' | x <- l, x' <- l'], [y * y' | y <- r, y' <- r']) λ> λ> zero = ([],Q) λ> infty = (Q,[]) λ> zero * infty

<interactive>:17:8: error: • Couldn't match type ‘Q’ with ‘[a]’ Expected type: ([a], Q) Actual type: (Q, [a0]) • In the second argument of ‘(*)’, namely ‘infty’ In the expression: zero * infty In an equation for ‘it’: it = zero * infty • Relevant bindings include it :: ([a], Q) (bound at <interactive>:17:1) λ>

...

On 2021-08-07, at 15:35, YueCompl via Haskell-Cafe mailto:haskell-cafe@haskell.org> wrote:

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 mailto:olf@aatal-apotheke.de> 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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.