<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Great! I'm intrigued by the idea that GHCi can make such math sentences runnable! I've never thought it this way before.<div class=""><br class=""></div><div class="">But I need some help to get it going:</div><div class=""><br class=""></div><div class=""><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">:set -XTypeSynonymInstances</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">:set -XFlexibleInstances</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(90, 35, 249); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">λ> </span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">import Data.Ratio</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">type Q = Rational -- this is probably wrong ...</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(90, 35, 249); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">λ> </span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">type NonNegativeNumber = ([Q],[Q])</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(90, 35, 249); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures; color: #74e5ca" class="">:{</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ| </span><span style="font-variant-ligatures: no-common-ligatures" class="">  instance Num NonNegativeNumber where</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ| </span><span style="font-variant-ligatures: no-common-ligatures" class="">    (l,r) * (l',r') = ([x*x'|x <- l, x' <- l'],[y*y'|y <- r, y' <- r'])</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(90, 35, 249); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">λ| </span><span style="font-variant-ligatures: no-common-ligatures; color: #74e5ca" class="">:}</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24); min-height: 13px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(251, 34, 255); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #98f4f5" class=""><b class=""><interactive>:9:12: </b></span><span style="font-variant-ligatures: no-common-ligatures" class=""><b class="">warning:</b></span><span style="font-variant-ligatures: no-common-ligatures; color: #98f4f5" class=""><b class=""> [</b></span><span style="font-variant-ligatures: no-common-ligatures" class=""><b class="">-Wmissing-methods</b></span><span style="font-variant-ligatures: no-common-ligatures; color: #98f4f5" class=""><b class="">]</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(152, 244, 245); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><b class="">    • No explicit implementation for</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(152, 244, 245); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><b class="">        ‘+’, ‘abs’, ‘signum’, ‘fromInteger’, and (either ‘negate’ or ‘-’)</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(152, 244, 245); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><b class="">    • In the instance declaration for ‘Num NonNegativeNumber’</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(90, 35, 249); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">λ> </span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">zero  = ([],Q)</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24); min-height: 13px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(152, 244, 245); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""><interactive>:13:13: </b></span><span style="font-variant-ligatures: no-common-ligatures; color: #fc3522" class=""><b class="">error:</b></span><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""> Data constructor not in scope: Q</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">infty = (Q,[])</span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24); min-height: 13px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(152, 244, 245); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""><interactive>:14:10: </b></span><span style="font-variant-ligatures: no-common-ligatures; color: #fc3522" class=""><b class="">error:</b></span><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""> Data constructor not in scope: Q</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(90, 35, 249); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">λ> </span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #5a23f9" class="">λ> </span><span style="font-variant-ligatures: no-common-ligatures" class="">zero * infty -- expect: = ([],[]) </span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24); min-height: 13px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(152, 244, 245); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""><interactive>:16:1: </b></span><span style="font-variant-ligatures: no-common-ligatures; color: #fc3522" class=""><b class="">error:</b></span><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""> Variable not in scope: zero</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(116, 229, 202); background-color: rgb(22, 27, 24); min-height: 13px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(152, 244, 245); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""><interactive>:16:8: </b></span><span style="font-variant-ligatures: no-common-ligatures; color: #fc3522" class=""><b class="">error:</b></span><span style="font-variant-ligatures: no-common-ligatures" class=""><b class=""> Variable not in scope: infty</b></span></div><div style="margin: 0px; font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo; color: rgb(90, 35, 249); background-color: rgb(22, 27, 24);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">λ> </span></div></div><div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class=""></span></div><div class="">I'd like to do more exercises, but I'm stuck here ...</div><div class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On 2021-08-07, at 06:16, Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" class="">olf@aatal-apotheke.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">On Fri, 2021-08-06 at 22:21 +0800, YueCompl wrote:<br class=""><blockquote type="cite" class="">Thanks Olaf,<br class=""><br class="">Metaphors to other constructs are quite inspiring to me, though I don't have sufficient theoretical background to fully understand them atm.<br class=""><br class=""></blockquote>Pen-and-paper or GHCi experiments suffice here, no fancy theoretical<br class="">background needed. Say Q is the type of rationals 0 < q and we express<br class="">type NonNegativeNumber = ([Q],[Q])<br class="">where the first (infinite) list is the lower approximants and the<br class="">second the upper approximants. Multiplication is then defined as<br class="">(l,r) * (l',r') = ([x*x'|x <- l, x' <- l'],[y*y'|y <- r, y' <- r'])<br class="">The extremes of this type are <br class="">0     = ([],Q)<br class="">infty = (Q,[])<br class="">It is easily seen that <br class="">0 * infty = ([],[]) <br class="">a number with no lower and no upper approximants, in other words, NaN. <br class="">Excercise: Define division for this type and find out what 1/0 and 0/0<br class="">is.<br class=""><br class=""><blockquote type="cite" class="">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?<br class=""><br class=""></blockquote>Yes. I think it is vital that we provide a migration path for<br class="">programmers coming from other languages. Under the Dedekind<br class="">cut/interval interpretation, NaN would behave differently, as I pointed<br class="">out. So I'd leave Float as it is, but be more verbose about its<br class="">violation of type class laws. To this end, one could have (and now I<br class="">might be closer to your initial question) numerical type classes like<br class="">HonestEq, HonestOrd, HonestMonoid and HonestRing whose members are only<br class="">those types that obey the laws in all elements. Naturally, Float would<br class="">not be a member. Who would use these new classes? Probably no one,<br class="">because we all like to take the quick and dirty route. But at least it<br class="">says clearly: Careful, you can not rely on these laws when using Float.<br class=""><br class="">Olaf<br class=""><br class=""></div></div></blockquote></div><br class=""></div></body></html>