# [Haskell-cafe] [Agda] Defining subtraction for naturals

Dan Doel dan.doel at gmail.com
Sat Mar 19 22:11:25 CET 2011

```On Thursday 17 March 2011 6:41:33 PM wren ng thornton wrote:

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

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

```