[Haskell-cafe] natVal straight to Word#

[Li-yao Xia]

Hi Timotej,

A KnownNat constraint gets desugared into an Integer parameter by GHC, 
so it seems difficult to get rid of the conversion altogether.

If you mimic the KnownNat type class, for Word instead of Integer:


     newtype Tagged n a = Tagged a

     class KnownWord n where
       word :: Tagged n Word


then you can push out the Integer -> Word conversions to the boundaries 
of your application. I mean that internally, you need only to pass Words 
around, and your internal functions would look like:


     internalFunction :: (KnownWord n, KnownWord m) => ...


But on the outside, you may still have to do a conversion.


     instance (KnownNat n, n <= MaxWord) => KnownWord n where
       word = Tagged (integerToWord (natVal (Proxy :: Proxy n)))

     externalFunction :: (KnownNat n, KnownNat m, n <= MaxWord, m <= 
MaxWord) => ...
     externalFunction = internalFunction


There are also a few GHC-specific tricks to help work with such a type 
class without GHC plugins; the constraints[1] package gives some 
examples (in particular, see the Data.Constraint.Nat module); this 
involves unsafeCoerce. You can avoid Integer -> Word conversions by 
instead getting the Word from a runtime value. In particular, it is 
possible to write the following:


     someWord :: Word -> SomeWord

     -- or some variants, depending on the extensions available, 
specifically AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables.
     data SomeWord where SomeWord :: KnownWord n => SomeWord


You can also reflect type-level operations with operations on Word (as 
opposed to having to do everything with Integers first), and even 
provide tools for reasoning about these operations, all of that without 
getting out of the compiler, as opposed to plugins.


     plusWord :: (KnownWord n, KnownWord m) :- KnownWord (n + m) -- 
maybe with (n + m <= MaxWord) on the left hand side too


As I mentioned earlier, this requires internal use of unsafeCoerce, but 
it is possible to keep it contained and expose a safe interface.

Regards,
Li-yao

[1] http://hackage.haskell.org/package/constraints