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

Hello, 1. I like the idea of having a `Natual` type similar to `Integer`, so +1 from me. 2. I am a bit worried about the partiality of some of the operations, but I don't see an appealing alternative... I guess we should just throw some informative exceptions. 3. I don't mind where it lives, although `Data.Word` does seem a little odd. 4. On the question about the link with type-level Nats: As Richard points out, with the current implementation the two would be unrelated: type-level nats belong to the kind `Nat`, which is just a lifted empty type called `Nat`. I think it would be possible to modify the implementation, to link the two: when promoting, GHC would promote `Natural` to an empty kind, and we'd modify the type-literals to have kind `Natural` instead of `Nat`. I imagine that should not be too hard to do. From a design point of view, I don't know if this is a good idea, but I have not thought about it. As a data point, we don't do this for kind `Symbol` (i.e., it is not linked in any way `String` or `Text`). -Iavor On Wed, Nov 12, 2014 at 7:46 AM, Richard Eisenberg wrote:

On Nov 11, 2014, at 2:06 PM, David Feuer 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 _______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries