Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for 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 w...@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 a similar vein. Given a finite set (e.g., the natural numbers with some finite upper bound) and assuming we've already decided not to use modular arithmetic, is there any mathematical reason to prefer saturating addition and/or multiplication instead of throwing an overflow error? -- Live well, ~wren ___ Agda mailing list a...@lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
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 out there already, but for my current project I need the efficiency of Int/Integer--- without the errors or defensive programming that comes from using them when we mean Nat/Natural. So far I haven't actually needed arithmetic operations (Enum, Eq, and Ord have been enough) but I figure I should square that away before splitting the code off for a public release. Since the whole thing is done as newtypes I can always make the Num instances the right ones, since people who obsess over performance can manually unwrap them to perform raw operations they know/hope will succeed and then revalidate the invariants when they're done with the arithmetic section. I just want to make sure the instance I give has the nice mathematical properties it could/should. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
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: a comparison view. See The view from the left by Conor McBride and James McKinna (Section 6). (This option is similar to what Henning Thielemann suggested.) -- /NAD ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
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-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
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 s+z =y. Truncated subtraction y - z is the supremum of the set of solutions s to the inequality s+z = y, when this supremum exists. (In your example, when zy, the set of solutions is empty, and the empty set has supremum zero.) This amounts to saying that the truncated subtraction function (-) - z is the right adjoint to the addition function (-) + z. So (2) is very natural. Thanks! That's exactly the kind of thing I was looking for. I'd been needlessly thinking of it as a hack :) -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
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 efficacious? -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Agda] Defining subtraction for naturals
On Thu, Mar 17, 2011 at 6:41 PM, wren ng thornton w...@freegeek.org 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 few reasonable definitions: No there aren't. How about pragmatically efficacious? If you must, you could always fall back on an encoding similar to the one that Brent used when introducing virtual species: http://byorgey.wordpress.com/2010/11/24/species-subtraction-made-simple/ along with some setoid that normalized for comparison on them, or you could just switch to type level Integers. -Edward -- Live well, ~wren ___ Agda mailing list a...@lists.chalmers.se https://lists.chalmers.se/mailman/listinfo/agda ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
