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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries signature.asc (836 bytes) Download Attachment |
+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 <[hidden email]> 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 > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
In reply to this post by Oleg Grenrus
Oleg Grenrus <[hidden email]> writes:
> 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. > This sounds quite reasonable to me and given how many much larger 8.2 changes are still not in the tree, I think it is in-scope for the release. I agree with David that it would make sense if the evidence itself were a Natural. I'm not terribly concerned about compatibility in the face of unsafeCoerce. We should be certain to clearly document the change though. Cheers, - Ben _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries signature.asc (497 bytes) Download Attachment |
I made a trac ticket for tracking the progress
https://ghc.haskell.org/trac/ghc/ticket/13181 - Oleg On 24.01.2017 16:05, Ben Gamari wrote: > Oleg Grenrus <[hidden email]> writes: > >> 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. >> > This sounds quite reasonable to me and given how many much larger > 8.2 changes are still not in the tree, I think it is in-scope for the > release. I agree with David that it would make sense if the evidence > itself were a Natural. > > I'm not terribly concerned about compatibility in the face of > unsafeCoerce. We should be certain to clearly document the change > though. > > Cheers, > > - Ben _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries signature.asc (836 bytes) Download Attachment |
Free forum by Nabble | Edit this page |