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.