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

YueCompl compl.yue at icloud.com
Mon Aug 9 11:51:36 UTC 2021


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 <olf at aatal-apotheke.de> 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 <haskell-cafe at haskell.org> 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 <haskell-cafe at haskell.org <mailto:haskell-cafe at 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 <olf at aatal-apotheke.de <mailto:olf at 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.
> 
> <haskell_for_analysists.lhs><surreal.hs>



More information about the Haskell-Cafe mailing list