3 ms·
So what type is `integer - integer`? It might be zero, but the type system doesn't statically know whether it is or not. If the result of every arithmetic exp
by recursive 8y ago
So what type is `integer - integer`? It might be zero, but the type system doesn't statically know whether it is or not. If the result of every arithmetic expression is possibly zero, then you're back to run-time checks for every value. I don't see how this is practically useful.
- c3534l 8y agoI would think that the result of a nonzero int minus a nonzero int would be an integer. So f(nonzero x, y) = y / x is fine, but f(nonzero x, nonzero y, z) = z / (x - y) is not.
- Zalastax 8y agoIn Agda you have the choice of either making it truncate at 0 or constrain the domain to (a - b, a >= b) in which case you don't hve to define the function when a < b. This of course is only suitable for theorem proving at the moment, but research is being done on how to have proofs like a >= b without sacrificing performance.