#8695: Arithmetic overflow from (minBound :: Int) `quot` (-1) ------------------------------------------------+-------------------------- Reporter: rleslie | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: libraries/haskell2010 | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result at runtime | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Comment (by ekmett): One could argue that it is the status quo making the special case out of {{{y = -1}}}. But, without prejudging the answer, let's look at what the class is attempting to model. It has taken me a few times to get this to come out to the correct answer here, so I'm going to be very very pedantic. =) The current class laws are insufficient to properly model the notion of a Euclidean domain. To be a proper Euclidean domain {{{(x `quot` y)*y + (x `rem` y) == x}}} isn't the only law. The standard statement of the Euclidean domain axiom is that there exists a Euclidean gauge function `f :: r -> Nat` such that if `a` and `b` are in the domain and `b /= 0`, then there are `q` and `r` such that `a = bq + r` and either `r = 0` or `f(r) < f(b)`. Both the (`div`,`mod`) pair and the (`quot`, `rem`) pair (more or less) satisfy these conditions with `f = abs`, so whenever I say `f` in the sequel, you can just think `abs`, but I'm using it to keep my head straight. It'll only matter that I'm making this distinction at the very end. The assumption that `b` is non-zero rules out Herbert's case directly, but if you remove the side-condition that `b /= 0`, it is ruled out by the conditions on `r`. e.g. If `(q,r) = quotRem x 0` then {{{x = q*0 + r}}} by the simplified definition, but then `x = r`, so `f(x) < f(r)` fails to hold and the `r == 0` case only saves you when you divide 0 by 0. These rules kind of rule out the tongue-in-cheek extension of `quotRem` to cover `0` in one sense. In another, however, the definition doesn't say what happens when `b == 0`. For simplicity I'd like to carry on with the convention that either `r = 0` or `f(r) < f(y)` holds regardless and continue to treat `b == 0` as an error it makes sense both by convention and by the underlying mathematics. With that as a warmup, let's get back to {{{(x `quot` -1)}}} in {{{Z mod 2^n}}}. {{{ (minBound `quot` -1)* (-1) + (minBound `rem` y) minBound + (minBound `rem` y) = minBound }}} says that `q = minBound` and `r = 0` would be the required answers. The only issue here is that stating `f = abs` doesn't work as we have the wart forced on us by the asymmetry of 2s complement arithmetic {{{
abs (minBound :: Int) -9223372036854775808 }}}
on the other hand, we've been using `abs` as an approximation of an injection into the natural numbers `f`, which does not have this limitation! Basically this requires `f = abs . toInteger`, then the side condition on `f` holds. So all of this indicates to me that the extension to support {{{minBound `quot` -1 = minBound}}} is correct and _is_ consistent with the definition of a Euclidean domain independent of 2s complement concerns. This frankly seems like a slam dunk to me and I'm in favor of the change. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8695#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler