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