How to divide by zero?

What’s the benefit of dependent types, anyway? Pyry pointed this out to me: they allow you to make your functions total by moving the preconditions to the caller side.

You often end up with partial functions because of some preconditions. For example, you might write an integer division function, but division by zero isn’t defined. How do you handle this? In Haskell, you get a runtime exception.

λ> 1 `div` 0
*** Exception: divide by zero
λ> 1 `rem` 0
*** Exception: divide by zero

Elm tries to avoid runtime exceptions and it makes division total by extending the usual definition of division:

> 1 // 0
0 : Int
> 1 `rem` 0
NaN : Int

The unorthodox result for 1 `rem` 0 is likely a bug. This solution quietly breaks the invariant x == (x // y) * y + x `rem` y, but it’s not a big deal. Coq does the same thing. Another solution would be to make the division function return Maybe. In Haskell:

safeDiv :: Integral a => a -> a -> Maybe a
safeDiv a 0 = Nothing
safeDiv a b = Just (a `div` b)

This means that you have to lift all your division-using computations into Maybe. A language like Coq offers you yet another possibility: you can demand that the caller proves that the divisor is non-zero:

Require Import Arith.
Require Import Nat.

Definition safeDiv x (y : { n : nat | 0 < n }) : nat :=
  match y with
    | exist _ O pf => match lt_irrefl _ pf with end
    | exist _ (S y') _ => div x (S y')
  end.

This is a total function. If you want to call it, you have to do it along with a proof that y is non-zero. For example, divide 3 by 2:

Example div_3_2 : nat := safeDiv 3 (exist _ 2 Nat.lt_0_2).
Eval compute in div_3_2. (* = 1 : nat *)

We could try dividing 3 by 0. Let’s do it in type-driven style with the refine tactic. It allows us to leave holes (_) in a term and fill them using Coq’s goal mechanism:

Example div_3_0 : nat.
  refine (safeDiv 3 (exist _ 0 _)).

Here’s the goal we get:

1 subgoal, subgoal 1 (ID 9)
  
  ============================
   0 < 0

Good luck with that.