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?

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  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  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  
                                 (q : m  
                                 (r : n + m 
    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.

StackExchange Computer Science Q#59829, answer score: 5