Thoughts on preventing divide-by-zero errors with the Crystal type system? (Refinement types / Type-safe division)

Crystal Contrib
1

I built a Sudoku game for iOS and Android with React Native, and I used Flow for type checking. Unfortunately Flow couldn’t catch all of the NaN bugs I ran into, so I still occasionally get crashes where I’m dividing something by zero, or array index out of bounds errors, etc. (And I still haven’t figured out where some of these errors are coming from!) So I’m really interested in type systems that can try to prevent some of these errors.

It’s really nice that the following Crystal program compiles and just prints “Infinity” without crashing:

def divide(a, b)
  a / b
end

puts divide(100, 0)

However, if you only want to return an Int32, then calling to_i on the result does crash with an overflow error:

def divide(a, b) : Int32
  (a / b).to_i
end

puts divide(100, 0)

Unhandled exception: Arithmetic overflow (OverflowError)
  from src/main.cr:0:11 in 'divide'
  from src/main.cr:8:1 in '__crystal_main'
  from /usr/local/Cellar/crystal/0.31.1/src/crystal/main.cr:97:5 in 'main_user_code'
  from /usr/local/Cellar/crystal/0.31.1/src/crystal/main.cr:86:7 in 'main'
  from /usr/local/Cellar/crystal/0.31.1/src/crystal/main.cr:106:3 in 'main'

I was just wondering if it might be possible to extend the Crystal type system with some “NonZero” types that could be used to catch divide-by-zero errors at compile time?

struct Int8 currently has:

Number.expand_div [Int8, UInt8, ...], Float64

But I thought it could be interesting if this was defined as:

Number.expand_div [NZInt8, NZUInt8, ...], Float64

Then this would show a type error (something like this):

def foo(a : Int32)
  100 / a
end

In src/main.cr:*:*

 2 | a / b
         ^------
Error: divisor must be a non-zero number (NZInt32), but it is Int32

So you would need to refine the type:

def foo(a: Int32)
  return if a == 0   # or a.zero?
  # The compiler refines the type to NZInt32
  100 / a
end

It’s also pretty easy to infer when some return types will be non-zero if you already know that the arguments are non-zero:

struct NZBigDecimal < BigDecimal
  def *(other : BigDecimal) : BigDecimal
    # ...
  end

  def *(other : NZBigDecimal) : NZBigDecimal
    # ...
  end
end

(e.g. a non-zero number multiplied by another non-zero number can never be zero.)

This might be similar to an issue that I opened for TypeScript: Add a --strictNaNChecks option, and a NaN / integer / float type to avoid runtime NaN errors. (But fortunately we don’t need to worry about NaN in Crystal, so this is not as important!)

See also:

Anyway, I don’t know if that’s a good idea! Maybe it would make things too complicated and slow down the compiler. But I thought it might be interesting to discuss!

1 Like
2

To achieve something like that I would go in a direction of an implementation based on type-state. A more ambitious but more powerful mechanism that could help validate other constructs in the language that are not expressed in more traditional type systems. It’s an idea I found attractive to try, but way after 1.0.

Having these properties be in the type itself (and not a type-state or tag) will generate many unions and type explosion I think.

Also, Structs - Crystal

A struct cannot inherit from a non-abstract struct.

3 Likes
3

Another option FWIW:

def divide(a, b)
  a // b
end
1 Like