Follow

no type system will save you from dividing by zero

@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

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

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

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

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.

ranjit@ranjit@friend.camp@nasser i just invented the types nonZeroFloat and nonZeroInt, checkmate