[Agda] Re: [Haskell-cafe] Defining subtraction for naturals

[David Menendez]

On Thu, Mar 17, 2011 at 2:35 PM, wren ng thornton <wren at freegeek.org> wrote:
> 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 "What About the Natural Numbers", Colin Runciman argues for
definition 2, but he doesn't provide much analysis beyond noting that
it gives you

    length (drop n xs) = length xs - n

He also argues for setting x / 0 = x for strict naturals or x / 0 =
infinity for lazy naturals.

There are some use cases for both in the paper.

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>