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