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

[Richard Eisenberg]

On Nov 11, 2014, at 2:06 PM, David Feuer <david.feuer at gmail.com> wrote:

> How (if at all) would you like these term-level natural numbers to relate to the type-level ones?

Not at all.

It's my belief that there is exists some moderately remote future (2-3 years) in which all datatypes -- including ones with unboxed fields -- will be promotable. At that point, this new `Natural` will promote, too. That future may also contain overloaded numeric literals in types, in which case things would just work. The only problem would be that this `Natural` doesn't have the right inductive structure to reason about in types, but it's no worse than today's `Nat`s.

My work for the next few years is to make that future a reality. :)

Richard