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 <eir@cis.upenn.edu> wrote:

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