Follow

no type system will save you from dividing by zero

· · Web · 8 · 2 · 14

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

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

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

@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)

@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.
Sign in to participate in the conversation
Merveilles

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.