[Haskell-cafe] natVal straight to Word#
lysxia at gmail.com
Sat May 13 12:44:12 UTC 2017
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 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.
More information about the Haskell-Cafe