PROPOSAL: Add 'Natural' type to base:Data.Word

[Herbert Valerio Riedel]

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?