I wonder what are the reasons for 'natVal' not having polymorphic type like
'natVal :: (KnownNat n, Num a) => proxy n -> a
?
сб, 13 мая 2017 г. в 17:46, 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
_______________________________________________ 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.