# Is it possible to prevent arithmetic errors with a dependent type system?

In a functional programming language I have functions like $$f\colon Int \times Int \times \cdots \times Int \to Int$$ which do some computation. However for certain arguments $(x_0, \dots, x_n)$ the function will cause arithmetic errors like Integer overflows, Integer underflow or even Division by zero. I do not want to handle those special cases within the function. Instead I would like to throw a type error at compile-time if someone calls the function with a undefined input.

So, my question is: Is possible to prevent arithmetic errors with a dependent type system?

And if so, does Adga, Idris or any other dependent type language support this?

• Unsolvability of Hilbert's 10th problem might be an issue here. – Yuval Filmus Jun 20 '16 at 16:39
• @YuvalFilmus It's only an issue for (unbounded) integer arithmetic, not for bounded arithmetic. And it's only an issue for type inference: if the programmer has to annotate the program with proofs of well-typedness, there's no theoretical limit. – Gilles Jun 20 '16 at 18:03

In theory, you can do anything of this sort with dependent types! Typically you would define your own (dependent) type, say

b_int = {z : Z | MIN_INT <= z <= MAX_INT}


Depending on the "flavor" of your dependent types, you might need a bunch of functions for going from b_int to Z and vice-versa (for well-defined values).

and then your function f would have to be of type:

 f : b_int * ... * b_int -> b_int


Now the tricky part. First you have to specify all the arithmetic operators, say b_add : b_int * b_int -> b_int in terms of the "ordinary" add function add. Ah except this isn't quite right. b_add MAX_INT 1 shouldn't be allowed! So you would have to give it a stricter specification, along the lines of

 b_add : { (n, m) : b_int * b_int | MIN_INT <= n + m <= MAX_INT } -> b_int


Then you want to prove something along the lines of:

b_add_correct : forall n m, n + m = b_add(n,m)


where the pair (n,m) needs to be in the domain of definition of b_add. Here, again, there may be a lot of pain if you need to translate to and from the Z type of unbounded integers, depending on how explicit the sub-types are.

Similarly for division:

b_div : { (n, m) | MIN_INT <= n / m <= MAX_INT, m =/= 0 }


So, if your program only uses the bounded operations, then there should be no way of writing a type correct program that has overflow or NaN operations.

However, I hope to convince you as well that there may be a significant amount of pain if there are no natural inclusions of types into sub-types, b_nat -> Z and if proofs of the inequalities have to be carried around explicitly.

One example is if the coercion box : Z -> b_nat explicitly carries the proof of inequality, i.e. box actually has the type:

 box : (x : Z) -> (p : x <= MAX_INT) -> b_nat


(I'm omitting the lower bound for simplicity). Then the correctness for b_add might be something more like:

 b_add_correct : forall n m : Z, (p : n <= MAX_INT) ->
(q : m <= MAX_INT) ->
(r : n + m <= MAX_INT) ->
n + m = unbox (b_add (box n p) (box m q) r)


Whew! It gets even worse if just applying a bop operation requires explicitly building a proof that some bound holds (for example if you know $n < m$, then you might want to use the fact that $m - n \neq 0$ to do division). That can make your program look quite messy, and be hard to write, since your proof obligations and program writing become inextricably linked.