no type system will save you from dividing by zero

· · Web · · ·

@nasser i just invented the types nonZeroFloat and nonZeroInt, checkmate

@nasser dammit i keep getting the "addition not supported" error on my nonZeroInts

@ranjit the checkmater has become the checkmated 👀

@nasser I was NaN years old when

@ranjit @nasser see, if you'd defined it as Zero, PositiveInts, and NegativeInts, you'd at least be able to support addition

@phooky @ranjit @nasser Maybe ImInHell Double

@ranjit @nasser Just make a "tryAdd"

@technomancy @nasser *laughs in Rust's NonZero* types*

@nasser If people would listen to me that we should import ideas from abstract algebra and allow types such as "group" "magma" and "field", it *could*!

@nasser (I'm not sure how serious I am about that, but I would very much like a language where the type system can guarantee that a particular variable contains an integer-valued float. This could be enforced by simply losing the "known integer" type status every time division is performed.)

@mcc @nasser A similar sort of static typing is already done to implement dimensional analysis in languages like F#, which is wonderfully helpful for avoiding bugs in scientific/physics code.

I'm also fond of the work of famous comp sci crank John Gustafson who designed a system called "posits and valids" which can represent the imprecision of any computer math operation including divide by zero.

@mcc @nasser there’s a thing called typestate that sort of does this! also linear logic based type systems

@nasser
#define 0 0.01

(Early FORTRAN compilers made it possible to accidentally redefine constants, so 0 could be any locally convenient value)

@scruss @nasser i have stared into the abyss

@nasser make zero a type which, based on however the division op gets parsed, is invalid as the divisor position in the function.

it solves the DivideByZero error most languages have (in exchange for a TypeError).

also completely useless, and less user-friendly. :P

@nasser

Don't know how serious this was intended, and whether you want info, so feel free to ignore...

Type systems absolutely can save you from dividing by zero. There are a number of ways to approach this. Simplest is to have 'NonZero' types that wrap the denominator and can only be constructed from a nonzero value. Something like this:

mkNonZeroInt : Integer -> Maybe NonZeroInteger
div : Integer -> NonZeroInteger -> Rational

This still likely involves a runtime check at some point (when constructing the 'NonZero' value), but it will push it into a more appropriate place in most cases.

Type systems that support dependent types or refinement types let you take this even further by providing a proof that the value is non-zero at compile time, without having to handle the branch where 'mkNonZeroInt' returns Nothing at runtime.

You've also always got the option that technomancy mentioned and work in a number system where division by zero is well-defined. IEEE 754 floats have well-defined semantics for division by zero, but they're kinda unfortunate mathematically. https://en.wikipedia.org/wiki/Real_projective_line has nicer properties. Whether or not this is actually useful depends on context.

@nasser `-Wdiv-by-zero`

@nasser Except NonZero* types in Rust.

Revel in the marvels of the universe. We are a collective of forward-thinking individuals who strive to better ourselves and our surroundings through constant creation. We express ourselves through music, art, games, and writing. We also put great value in play. A warm welcome to any like-minded people who feel these ideals resonate with them.