For Want of Difference Types

So I ran into a discussion on Lambda the Ultimate wherein was raised the topic of what the "real" mathematical type for (integral) division should be since :: Int -> Int -> Int doesn't cut it. Someone proposed :: Int -> Int -> Int+1, which is the normal way it's implemented— that is, the result is an integer or a singleton value representing (the single divide-by-zero) error it can generate. In a total functional world this has the problem of how to percolate exceptions up, since the caller isn't allowed to fail either.

That type is flagrantly wrong.

Invoking the abstract of the paper presented there (the site seems offline, so I can't read the paper), the reason it's flagrantly wrong is because it's not mathematical. Mathematics doesn't define an "undefined" value which would be permissible to return, it simply fails to define any value whatsoever. So if extending the result type is both mathematically incorrect and also a programming infrastructure nightmare, then what is the right answer?

The right answer is to restrict the inputs to the function. The usual way of doing this involves using dependent types to carry extra information about values in the types. Dependent types have many benefits (and many many issues), but we don't need even need them for this. All we need is difference types :: Int -> (Int \\ 0) -> Int.

( Read more... )