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

[David Feuer]

+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 <oleg.grenrus at iki.fi> wrote:
> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>