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 a
On Thu, Mar 17, 2011 at 6:41 PM, wren ng thornton wrote:
> On 3/17/11 5:12 PM, Conor McBride wrote:
>
>> On 17 Mar 2011, at 18:35, wren ng thornton wrote:
>>
>>> Another question on particulars. When dealing with natural numbers, we
>>> run into the problem of defining subtraction. There are a fe
On 3/17/11 5:12 PM, Conor McBride wrote:
On 17 Mar 2011, at 18:35, wren ng thornton wrote:
Another question on particulars. When dealing with natural numbers, we
run into the problem of defining subtraction. There are a few
reasonable definitions:
No there aren't.
How about "pragmatically ef
On 3/17/11 4:22 PM, Martin Escardo wrote:
On 17/03/11 18:35, wren ng thornton wrote:
(2) Use saturating subtraction, i.e. if the result would drop below zero
then return zero;
This is what people working with quantales do.
Subtraction y-z, when it exists, is the solution in s to the equation
On 17 Mar 2011, at 18:35, wren ng thornton wrote:
Another question on particulars. When dealing with natural numbers,
we run into the problem of defining subtraction. There are a few
reasonable definitions:
No there aren't.
Conor
___
Haskell-C
On 2011-03-17 19:35, wren ng thornton wrote:
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.
There is a fourth option
On 3/17/11 2:50 PM, Luke Palmer wrote:
If you are implementing lazy naturals, I wonder if defining 0 - 1 to
be infinity makes mathematical sense. It's like arithmetic mod
infinity
Actually, I'm specifically implementing strict naturals :)
There are a number of libraries for lazy naturals
If you are implementing lazy naturals, I wonder if defining 0 - 1 to
be infinity makes mathematical sense. It's like arithmetic mod
infinity
Luke
On Thu, Mar 17, 2011 at 12:35 PM, wren ng thornton wrote:
> Another question on particulars. When dealing with natural numbers, we run
> into the
