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

**URL:** <https://forum.crystal-lang.org/t/thoughts-on-preventing-divide-by-zero-errors-with-the-crystal-type-system-refinement-types-type-safe-division/1470>\
**Category:** Crystal Contrib\
**Created:** [December 10, 2019, 9:37am UTC](https://forum.crystal-lang.org/t/thoughts-on-preventing-divide-by-zero-errors-with-the-crystal-type-system-refinement-types-type-safe-division/1470 "2019-12-10T09:37:56Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![ndbroadbent](https://yyz2.discourse-cdn.com/flex036/user_avatar/forum.crystal-lang.org/ndbroadbent/32/637_2.png) [@ndbroadbent](https://forum.crystal-lang.org/u/ndbroadbent)\
**Post date:** [December 10, 2019, 9:37am UTC](https://forum.crystal-lang.org/t/thoughts-on-preventing-divide-by-zero-errors-with-the-crystal-type-system-refinement-types-type-safe-division/1470/1 "2019-12-10T09:37:56Z")

</div>

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:

```crystal
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:

```auto
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:

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

```

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

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

```

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

```auto
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:

```auto
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:

```auto
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](https://github.com/microsoft/TypeScript/issues/28682). (But fortunately we don’t need to worry about `NaN` in Crystal, so this is not as important!)

See also:

- [Typescript issue: refinement types](https://github.com/Microsoft/TypeScript/issues/7599)
- [Type-safe division in Idris (gist)](https://gist.github.com/edwinb/0047a2aff46a0f49c881#file-divide-idr-L12)

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!

---

<div class="post-metadata">

**Author:** ![bcardiff](https://yyz2.discourse-cdn.com/flex036/user_avatar/forum.crystal-lang.org/bcardiff/32/3_2.png) [@bcardiff](https://forum.crystal-lang.org/u/bcardiff)\
**Post date:** [December 10, 2019, 1:12pm UTC](https://forum.crystal-lang.org/t/thoughts-on-preventing-divide-by-zero-errors-with-the-crystal-type-system-refinement-types-type-safe-division/1470/2 "2019-12-10T13:12:36Z")

</div>

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](https://crystal-lang.org/reference/syntax_and_semantics/structs.html)

> A struct cannot inherit from a non-abstract struct.

---

<div class="post-metadata">

**Author:** ![rogerdpack](https://yyz2.discourse-cdn.com/flex036/user_avatar/forum.crystal-lang.org/rogerdpack/32/117_2.png) [@rogerdpack](https://forum.crystal-lang.org/u/rogerdpack)\
**Post date:** [December 10, 2019, 2:19pm UTC](https://forum.crystal-lang.org/t/thoughts-on-preventing-divide-by-zero-errors-with-the-crystal-type-system-refinement-types-type-safe-division/1470/3 "2019-12-10T14:19:16Z")

</div>

Another option FWIW:

```auto
def divide(a, b)
  a // b
end

```