[Haskell-cafe] natVal straight to Word#

[Alexey Vagarenko]

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 <lysxia at gmail.com>:

> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170513/eeea807b/attachment.html>