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.