<div>I wonder what are the reasons for 'natVal' not having polymorphic type like 'natVal :: (KnownNat n, Num a) => proxy n -> a</div><div>?</div><div><br><div class="gmail_quote"><div>сб, 13 мая 2017 г. в 17:46, Li-yao Xia <<a href="mailto:lysxia@gmail.com">lysxia@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Timotej,<br>
<br>
A KnownNat constraint gets desugared into an Integer parameter by GHC,<br>
so it seems difficult to get rid of the conversion altogether.<br>
<br>
If you mimic the KnownNat type class, for Word instead of Integer:<br>
<br>
<br>
     newtype Tagged n a = Tagged a<br>
<br>
     class KnownWord n where<br>
       word :: Tagged n Word<br>
<br>
<br>
then you can push out the Integer -> Word conversions to the boundaries<br>
of your application. I mean that internally, you need only to pass Words<br>
around, and your internal functions would look like:<br>
<br>
<br>
     internalFunction :: (KnownWord n, KnownWord m) => ...<br>
<br>
<br>
But on the outside, you may still have to do a conversion.<br>
<br>
<br>
     instance (KnownNat n, n <= MaxWord) => KnownWord n where<br>
       word = Tagged (integerToWord (natVal (Proxy :: Proxy n)))<br>
<br>
     externalFunction :: (KnownNat n, KnownNat m, n <= MaxWord, m <=<br>
MaxWord) => ...<br>
     externalFunction = internalFunction<br>
<br>
<br>
There are also a few GHC-specific tricks to help work with such a type<br>
class without GHC plugins; the constraints[1] package gives some<br>
examples (in particular, see the Data.Constraint.Nat module); this<br>
involves unsafeCoerce. You can avoid Integer -> Word conversions by<br>
instead getting the Word from a runtime value. In particular, it is<br>
possible to write the following:<br>
<br>
<br>
     someWord :: Word -> SomeWord<br>
<br>
     -- or some variants, depending on the extensions available,<br>
specifically AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables.<br>
     data SomeWord where SomeWord :: KnownWord n => SomeWord<br>
<br>
<br>
You can also reflect type-level operations with operations on Word (as<br>
opposed to having to do everything with Integers first), and even<br>
provide tools for reasoning about these operations, all of that without<br>
getting out of the compiler, as opposed to plugins.<br>
<br>
<br>
     plusWord :: (KnownWord n, KnownWord m) :- KnownWord (n + m) --<br>
maybe with (n + m <= MaxWord) on the left hand side too<br>
<br>
<br>
As I mentioned earlier, this requires internal use of unsafeCoerce, but<br>
it is possible to keep it contained and expose a safe interface.<br>
<br>
Regards,<br>
Li-yao<br>
<br>
[1] <a href="http://hackage.haskell.org/package/constraints" rel="noreferrer" target="_blank">http://hackage.haskell.org/package/constraints</a><br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div>