6
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ Unsolvability of Hilbert's 10th problem might be an issue here. $\endgroup$ – Yuval Filmus Jun 20 '16 at 16:39
  • 3
    $\begingroup$ @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. $\endgroup$ – Gilles Jun 20 '16 at 18:03
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.