{-# LANGUAGE DataKinds, GADTs, StandaloneDeriving, Rank2Types, PolyKinds, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables #-}
import Unsafe.Coerce
Have you tried using a SNatClass that works more like KnownNat, that is, having a method that returns a Nat?
I don't sure what you mean, but i've checked now the differences between my code and reflection package, and there are some substantial ones. I define Nat as data Nat = Z | S Nat but they define only kind
data Nat
Hm, well.. then we have similar definition of SNat class: class SNatClass (a :: Nat) where singN :: SNat a
class KnownNat (n :: Nat) where natSing :: SNat n
but very different definition of SNat itself: data SNat :: Nat -> * where SZ :: SNat 'Z SN :: SNat n -> SNat ('S n) against
newtype SNat (n :: Nat) = SNat Integer deriving instance Show (SNat n)
and from this follows another main difference: i've defined instances of SNatClass: instance SNatClass 'Z where singN = SZ instance SNatClass n => SNatClass ('S n) where singN = SN singN but they're not (and, if i'm correct, they can't, because there is no types with kind Nat (remember, they've defined only kind)). And then the identical code:
data Proxy s = Proxy
class Reifies s a | s -> a where reflect :: p s -> a
natVal :: forall n proxy. KnownNat n => proxy n -> Integer natVal _ = case natSing :: SNat n of SNat x -> x
instance KnownNat n => Reifies n Integer where reflect = natVal
newtype MagicNat r = MagicNat (forall (n :: Nat). KnownNat n => Proxy n -> r)
reifyNat :: forall r. Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r reifyNat x k = unsafeCoerce (MagicNat k :: MagicNat r) x Proxy {-# NOINLINE reifyNat #-}
main = do print $ reifyNat 4 reflect print $ reifyNat 4 natVal reifyNat 4 (print . asNatProxyTypeOf natSing) --reifyNat 4 (print . asWrongNatProxyTypeOf natSing)
-- Note the type: type argument in `SNat n` is the same as for Proxy. Thus, i -- will found exactly KnownNat instance, which i have defined in -- `reifyNat`. asNatProxyTypeOf :: KnownNat n => SNat n -> Proxy n -> SNat n asNatProxyTypeOf = const
-- On the other hand, if type will be `KnownNat n => SNat r -> Proxy n -> -- SNat r`, then i won't be able to find correct instance of `KnownNat r` and -- thus can't e.g. print `SNat r` value. asWrongNatProxyTypeOf :: KnownNat n => SNat r -> Proxy n -> SNat r asWrongNatProxyTypeOf = const
So, you're right: `reifyNat` defines dictionary for `KnownNat n` (and
this is the only instance we have) as Integer. But though dictionary is a
function `natSing :: SNat n`, now SNat is newtype and its runtime
representation should indeed be equivalent to Integer and all is fine.
Well, ok, i think i understand how correct `reifyNat` works. Thanks!
But i still don't understand why mine works too, though is probably wrong.
On Thu, May 5, 2016 at 2:56 PM, Marcin Mrotek
Hello,
My guess is that the Nat parameter in SNat gets erased, and both types end up with the same runtime representation. I'm not sure how reliable this is. Have you tried using a SNatClass that works more like KnownNat, that is, having a method that returns a Nat?
Best regards, Marcin Mrotek _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners