[Haskell-cafe] natVal straight to Word#

[Oleg Grenrus]

FWIW. In GHC-8.2 the `natVal` from GHC.TypeNats (not TypeLits!) will
return `Natural`.

- Oleg


On 13.05.2017 13:53, Timotej Tomandl wrote:
> Hi,
> I am using type-level naturals constrained to be at max the size of
> Word#, as such I have found myself casting the type-level naturals
> first to Integer and then to Word# like this
>
> type MaxConstraint a=a<=MaxNat
> toNatural :: forall n. (MaxConstraint n,KnownNat n)=>Natural n
> toNatural = Natural (integerToWord (natVal (Proxy :: Proxy n)))
>
> where MaxNat is the hard-coded value of maxBound :: Word for now,
>
> type MaxNat=18446744073709551615
>  
> My data type and the constrained constructor for Natural are
>
> data Natural (x::Nat) where
>      Natural :: (MaxConstraint x)=>{-# UNPACK #-} !Word# -> Natural x
>
> I have tried to eliminate the integerToWord cast from toNatural, yet I
> have failed at doing so.
> As such I would like to ask, if anyone has some insight, whether it is
> possible to eliminate this one step of indirection. The only option I
> came up with is writing GHC plugin to do this.
>
> Timo
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.


-------------- 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/haskell-cafe/attachments/20170513/41dc6901/attachment.sig>