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

Oleg Grenrus oleg.grenrus at iki.fi
Tue Jan 24 15:42:03 UTC 2017


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 <oleg.grenrus at iki.fi> 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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170124/58857b27/attachment.sig>


More information about the Libraries mailing list