A few years ago I had an idea of writing functions as simple as Excel, but with extra safety.
I came unstuck for several reasons, but division seemed a nice nugget which never sat well with me.
There are several ways to do division here:
The idea is to search for something safe which an Excel user could use.
E.g. this might be idiomatic:
safeDiv :: (Eq a, Fractional a) => a -> a -> Maybe a
safeDiv _ 0 = Nothing
safeDiv x y = Just (x / y)
doEx :: (Eq b, Fractional b) => b -> b -> b -> Maybe b
doEx a b c = do
a' <- a `safeDiv` b
a' `safeDiv` c
but, I found this more appealing:
maybeDiv :: (Eq a, Fractional a) => Maybe a -> Maybe a -> Maybe a
maybeDiv (Just n) (Just 0) = Nothing
maybeDiv (Just n) (Just d) = Just (n / d)
maybeDiv Nothing _ = Nothing
maybeDiv _ Nothing = Nothing
maybeDivEx :: (Eq a, Fractional a) => a -> a -> a -> Maybe a
maybeDivEx a b c = Just a `maybeDiv` Just b `maybeDiv` Just c
I.e. the operations can be chained together with minimum fuss (like any nice algebraā¦). I imagine the maybeDiv function could be hidden away in a library out of sight.
But of course, itās domain specific (e.g. simple calculator) and doesnāt have the general type definition that Haskellers love.
Any other ideas?
I am thinking about a Liquid Haskell exampleā¦ Unsure whether it would really help much thoughā¦ Curious.
From 1 / 0 = Nothing and 1 / Nothing = Nothing follows that 1 / (1 / 0) = Nothing which is equivalent to 0 / 1 = Nothing and this is the same as 0 = Nothing .
I donāt understand the point youāre trying to make, to be honest.
1 / 0 is impossible / undefined. So 1 / (1 / 0) is equivalent to 1 / 0.
Whereas 0 / 1 is just 0. maybeDiv defines both of these as youād expect.
Yes, and thatās the problem, because this (1 / (1 / 0) /= 0 / 1 ) would be a maybeSomethingThatIsntDiv .
The Nothing functions as a sort of NaN in this case, I guess? Or as the replacement of the DivideByZero exception. How is maybeDiv not the same as div, except instead of throwing an error, it propogates a Nothing?
To come back to the OPās question: Liquid Haskell would make it simple to not allow the second argument to be 0 when using it in directly in code, IIRC, but if it is a value thatās passed in from getLine for example, even Liquid Haskell canāt prevent that from being a 0.
Knowing that if thereās even one x / 0 in an equation, the entire equation is non-sensical. So just allowing it and catching the DivideByZero exception in the IO that would evaluate the equation would be the easiest / most straight-forward way, IMO.
I donāt really have any other ideas, you covered pretty much all options in your Main.hs, I feel.
Yes. But what the OP did wasnāt to use Nothing just as undefined, but to define rules for how to ācalculateā with this symbolical value of 1/0. And now there are exactly two possibilities for this value, if the multiplication and addition should behave as āusualā. Not that there is any problem with defining other relations ā+ā and ā*ā that donāt form a field, but it should be kept in mind.
So, about these two possibilities: if 1/0 is foo, what is 0 * foo = 0/0 and what is 0/foo? If this is foo, this is what the OP defined, this foo should be 0, or you are getting problems with addition.
You cannot define 0/0 as foo /= 0, because this leads to problems, you need some bar, which isnāt foo, something like āok, the other value foo is somehow defined, but this - 0/0 - is now really undefinedā. So we end up with Inf and NaN, where
1/0 = Inf
-1/0 = -Inf
1/Inf = 0
Inf = Inf
0/0 = NaN
0*Inf = NaN
Inf - Inf = NaN
NaN /= NaN
All rules for NaN are just equivalent ways to write 0/0 = 0*(1/0) = (1 - 1) / 0 = 1/0 - 1/0.
Btw. defining for all n, n / 0 = 0 is what total languages like Rocq, Lean, Idris,ā¦ do.
I guess Iāve found the problem now
Iām sorry, as Iām a mathematician, this is about as evident as a monad being a monoid in the ā¦
I bit slower: for all n /=0, 1/n * n = 1 (and n * 1/n = 1), 1/n is the multiplicative inverse to n. And the multiplicative inverse of 1/n must be n, 1/(1/n) = n.
The āproblemā is 0, as there is no multiplicative inverse 1/0 defined, but what we do know is, that if there is such a multiplicative inverse, the inverse of it is (per definition) 0: 1/(1/0) = 0.
But if we define a multiplicative inverse of 0, some foo with 1/0 = foo, 1/foo = 0must hold too, or we didnāt define the multiplicative inverse for 0.
With all that, the two possible definitions of maybeDiv are:
maybeDiv :: (Eq a, Fractional a) => Maybe a -> Maybe a -> Maybe a
maybeDiv (Just 0) (Just 0) = ???
maybeDiv (Just n) (Just 0) = Nothing
maybeDiv (Just n) (Just d) = Just (n / d)
maybeDiv Nothing (Just n) = Nothing
-- Here we have to be careful!
maybeDiv (Just 0) Nothing = 0
maybeDiv (Just n) Nothing = 0
maybeDiv Nothing Nothing = ???
maybeDiv' :: (Eq a, Fractional a) => a -> a -> a
maybeDiv' _ 0 = 0
maybeDiv' n d = n / d
Of course, as a mathematician, you know that adopting this definitionāor any definition that makes division by zero yield a finite numberāalso means violating the field axioms. Namely distributivity: a ā (b + c) = a ā b + a ā c. If a is the multiplicative inverse of 0, and b and c are 0, then on the left we have
0ā»Ā¹ ā (0 + 0) = 0ā»Ā¹ ā 0
= 1 (by the definition of multiplicative inverse)
and on the right we have
0ā»Ā¹ ā 0 + 0ā»Ā¹ ā 0 = 1 + 1 (ditto)
= 2
Thereās no way out of this bind: if you include the result of division by zero in your number system, whether you call it 0, infinity, or NaN, some principle you expect to hold for all numbers will fail you.
Yes, Iāve mentioned that above, but badly phrased. The two sentences could be read as if such definitions still form a field.
The starting point of the whole idea should be that division by zero is not undefined because some mathematicians like to make division hard for people, but because there is no (finite) rational number that can be used as the multiplicative inverse of 0 and still having a field of rational numbers. Non-finite ānumbersā (a symbol like Inf) doesnāt help much either, as we do need some other symbol for 0/0, which has the meaning of āthis division is now really undefinedā.
When I was working on Haskell as a spreadsheet (Inflex), after a couple weeks of research and deliberation, I decided that division by zero would stop evaluation, but evaluation around it would continue normalising as much as it could. So eg (2+6)/0 would produce 8/0 as a final expression. Rather than just unwinding the stack and bailing out, or doing a Maybe monad (thereās nothing interesting to be done with the Nothing value), or applying Liquid Haskell (too hard for my target audience; spreadsheet users). E.g if you have a list of 200 rows and one of them is a divide by zero, you donāt abandon the whole thing, you show the user all the other 199 values which might be enough for them to answer their question.
Still quite happy with this choice for the given use case. YMMV.
Very tangential and just whining against the Monads Schmonads viewpoint:
The following are mathematical and unlike C; the second one is straight up alpha-equivalent to category theory textbook notation:
doExV2 a b c = a `safeDiv` b >>= \a' -> a' `safeDiv` c
doExV3 a b c = join (fmap (\a' -> a' `safeDiv` c) (a `safeDiv` b))
BTW Monad Schmonads chose a stupid example. The following is mathematical and functional by all standards:
main = putStrLn "Hello, World!"
If one dislikes ālooks like Cā, how is ālooks like Pythonā better? And how is ālooks like Python plus dynamic scoping for a specially named variableā even better? Or has the real, hidden objective been always ālooks like Fortranā all along?
You can, but it wonāt be lawful, assuming that Good 0 * recip (Good 0) is something other than Good 1.
Of course, Fractional Double isnāt lawful either. So donāt let that get in the way of a good time. Itās just not correct to claim that this is somehow more legit than NaN from a mathematical perspective.
It is time to talk about how the cited Prelude doc goofed up the multiplcative inverse law.
By way of contradiction, suppose we truly meant to require unconditionally x * recip x = 1 even when x = 0 (as opposed to merely forgetting to add āif x ā 0ā), then what do I do wrong in the following?
