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

[Iavor Diatchki]

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

>
> 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
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20141112/e95cfc7f/attachment.html>