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

Oleg Grenrus oleg.grenrus at
Mon Jan 23 00:10:15 UTC 2017

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-


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

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


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: <>

More information about the Libraries mailing list