[Agda] Defining subtraction for naturals

[wren ng thornton]

Another question on particulars. When dealing with natural numbers, we 
run into the problem of defining subtraction. There are a few reasonable 
definitions:

(1) If the result would drop below zero then throw an overflow error;

(2) Use saturating subtraction, i.e. if the result would drop below zero 
then return zero;

(3) Use type hackery to disallow performing subtraction when the result 
would drop below zero, e.g. by requiring a proof that the left argument 
is not less than the right.

Dependently typed languages tend to use the second definition because it 
gives a pure total function (unlike the first) and because it's less 
obnoxious to use than the third. In Haskell the third would be even more 
obnoxious.

So my question is, mathematically speaking, is there any reason to 
prefer the second option over the first or third? Purity aside, I mean; 
do the natural numbers with saturating subtraction form any interesting 
mathematical object, or is it just what we're stuck with?


In a similar vein. Given a finite set (e.g., the natural numbers with 
some finite upper bound) and assuming we've already decided not to use 
modular arithmetic, is there any mathematical reason to prefer 
saturating addition and/or multiplication instead of throwing an 
overflow error?

-- 
Live well,
~wren