Proposal: Introduce GHC.TypeNats module with natVal :: forall n proxy. KnownNat n => proxy n -> Natural

[Oleg Grenrus]

Currently we have in the GHC.TypeLits module

natVal :: forall n proxy. KnowNat n => proxy n -> Integer

However, the result integer is never negative. Numeric.Natural module is
in base since base-4.8.0.0.

---

I propose that we introduce new module GHC.TypeNats with natVal and natVal'

natVal :: forall n proxy. KnownNat n => proxy n -> Natural

and

natVal' :: forall n. KnownNat n => Proxy# n -> Natural

and other KnownNat related terms and type families.

---

This change would propagate to give more precise type to someNatVal:

someNatVal :: Natural -> SomeNat

which is currently someNatVal :: Integer -> Maybe SomeNat

---

The alternative would be to change the types in GHC.TypeLits, but

- it would be breaking change
- hard to shim (where new module is implementable for older base, in
e.g. base-compat)
- we lose opportunity to separate Nat and Symbol data kinds

---

Additionally we'd deprecate the GHC.TypeLits natVal, natVal' and someNatVal

---

As related "nice to know", `Nat` and `Natural` "agree" on negation:

> (1 - 2) :: Natural
*** Exception: arithmetic underflow

> natVal (Proxy :: Proxy (1 - 2))

<interactive>:9:1: error:
    • No instance for (KnownNat (1 - 2)) arising from a use of ‘natVal’
    • In the expression: natVal (Proxy :: Proxy (1 - 2))
      In an equation for ‘it’: it = natVal (Proxy :: Proxy (1 - 2))

---

The change is quite straightforward to do, and I'm willing to implement
it even for GHC 8.2


Oleg Grenrus



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170123/caf46644/attachment.sig>