Division Examples

[mmport80]

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:

john-orford/div/-/blob/main/Main.hs?ref_type=heads

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.

[ReleaseCandidate]

maybeDiv (Just n) (Just 0) = Nothing
maybeDiv _ Nothing = Nothing

So 1 / 0 = Nothing and 1 / Nothing = Nothing => 1 / (1 / 0) = Nothing <=> 0 / 1 = Nothing <=> 0 = Nothing.
There is a reason NaN and (+/-) Inf exist.

[Vlix]

I’m having a hard time following what you’re trying to convey.
Could you reformulate with more words instead of arrows?

[ReleaseCandidate]

Oh, sorry, of course.

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 .

[Vlix]

Uhhhm, that’s not what maybeDiv would do, though

1 / (1 / 0) = Nothing is equivalent to 1 / 0 (or 1 / Nothing), not 0 / 1

[ReleaseCandidate]

@Vlix

Uhhhm, that’s not what maybeDiv would do, though

Yes, and that’s the problem, because this (1 / (1 / 0) /= 0 / 1) would be a maybeSomethingThatIsntDiv.

[Vlix]

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?

[Vlix]

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.

[ReleaseCandidate]

@Vlix

I don’t understand the point you’re trying to make, to be honest.

@Vlix

1 / 0 is impossible / undefined

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.

[ReleaseCandidate]

@Vlix

1 / 0 is impossible / undefined. So 1 / (1 / 0) is equivalent to 1 / 0.

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 = 0 must 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

[atravers]

@ReleaseCandidate

I’m sorry, as I’m a mathematician, this is about as evident as […]

…you are not alone - from another mathematician:

Monads schmonads

Haskell uses the seriously complex machinery of monads to do I/O, supposedly without side effects (I don’t accept this). And you end up writing stuff like

      main = do {   putStrLn "Hello, World!" ;   return ()   }

which to me looks like C. There must be a more functional approach.

[rhendric]

@ReleaseCandidate

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.

[ReleaseCandidate]

@rhendric

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.

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”.

[chrisdone]

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.

[treblacy]

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?

[treblacy]

And now for something more constructive:

You should not be afraid of creating your own types.

data DivSafe a = Good a | DivByZero a

Then you can make it an instance of Num, Fractional, etc., and they are also total. Then a / b / c is fine.

Which I guess is what chrisdone did.

[rhendric]

@treblacy

Then you can make it an instance of Num, Fractional, etc.

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.

[mmport80]

@chrisdone

I have been going thru your Inflex material. Impressive! A lot of energy put into this.

You make a good pt. Bailing out might be the best in many / most simple usecases… Nice idea about evaluating as much as possible for the user also.

[treblacy]

@rhendric

You can, but it won’t be lawful, assuming that Good 0 * recip (Good 0) is something other than Good 1.

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?

  0
= 0 * 1
= 0 * (0 * recip 0)
= (0 * 0) * recip 0
= 0 * recip 0
= 1

We also need not bring up Double. We can refer to Rational instead, which is more, um, rational.

I never meant to say that Inf and/or NaN are bad. I only meant: if they don’t fit your use case, you can create your own type to fit your use case.