Proposal: Introduce GHC.TypeNats module with natVal :: forall n proxy. KnownNat n => proxy n -> Natural
oleg.grenrus at iki.fi
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-184.108.40.206.
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
- 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))
• 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the Libraries