Quantcast

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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

signature.asc (836 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: 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 <[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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Ben Gamari-2
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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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

Oleg Grenrus
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
Loading...