[Agda] Defining subtraction for naturals

[Dan Doel]

On Thursday 17 March 2011 6:41:33 PM wren ng thornton wrote:
> How about "pragmatically efficacious"?

Well...

> (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.

As far as this goes, one has to ask where we'd get this proof. It's unlikely 
that we'd just have one already, so the most likely answer is that we'd have 
to compute the proof.

But, the way to compute the proof of whether we're allowed to do subtraction 
is to *do subtraction*. So, if we don't want saturating subtraction, arguably 
we don't want subtraction at all, but a prior *comparison* of our two numbers, 
which will tell us:

  compare m n
    m = n + k + 1
    m = n
    m + k + 1 = n

in which case we already have the information we want. I think this article is 
relevant:

  http://existentialtype.wordpress.com/2011/03/15/boolean-blindness/

Inasmuch as we shouldn't be throwing away all propositional information by 
crushing to a boolean, we also shouldn't be throwing away information that we 
will later have to recompute by deciding the wrong proposition.

-- Dan