On 2014-11-12 at 19:17:21 +0100, Gershom B wrote:
Let me throw in one key bikeshed to be painted.
I don't like the fact that subtraction on naturals is a partial operation as proposed. I would much prefer saturated subtraction where for y > x, x - y = 0. This prior discussion on -cafe tends towards such a definition as being 'universally better'
https://www.haskell.org/pipermail/haskell-cafe/2011-March/090265.html
Here is my motivation for saturated subtraction: On all non-bottom calculations, it agrees. On calculations that are bottom under partial subtraction, it nonetheless gives a mathematically meaningful and useful result in a coherent way.
I'd point out that while for single operations saturated arithmetic seems fine, it leads to less obvious results for compound expression where an intermediate result gets saturated, like in 100 + 20 - 40 => 80 100 + (20 - 40) => 100 (or ⊥ for partial (-)) or (1 - 2) * (10 - 20) => 0 (or ⊥ for partial (-)) . I have to admit I feel a bit uneasy here, and I'd rather get a final ⊥ than a result obtained by continuing the computations with 0s. FWIW, we do already have a precedent of allowing partial functions, like e.g. for quot/Rem/div/mod with a 0-divisor resulting in ⊥
As a general principle, I think our goal should be to make base more total, not less.
Btw, are we talking only about '(-)' and 'negate'? (e.g. is it ok for 'fromInteger' to diverge for negative input values, or shall it rather map everything negative into '0::Natural'?)
The arguments cited in the thread from Runciman's "What About the Natural Numbers" (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.3442) are also fairly compelling in this regard.
Btw, that paper also argues for "x / 0 = x" instead of throwing a div/0 exception. Should we consider that as well?