+1. The current situation is pretty weird. We also really should make
the SNat carried in the KnownNat dictionary hold a Natural rather than
an Integer, but we'll need to watch out for backwards compatibility
with anyone using unsafeCoerce on those dictionaries.
On Sun, Jan 22, 2017 at 7:10 PM, 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
_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries