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

[Gershom B]

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.

As a general principle, I think our goal should be to make base more
total, not less.

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.

-g

> Herbert Valerio Riedel wrote:
>>> I hereby suggest to add a type for encoding term-level naturals...
>>> to `base:Data.Word` module
>
> +1
>
> because Edward, who is the current leading purveyor of term-level
> nats, is in favor.
>
> Roman Cheplyaka wrote:
>> Yeah, having Natural in Data.Word feels unnatural to me.
>
> Agreed. I'm not sure what the solution is though. I'd be in
> favor if someone comes up with something decent.
> *However*
> I'd be strongly opposed to letting any kind of bikeshedding
> getting in the way of Herbert's proposal.
>
> Thanks,
> Yitz