{-# LANGUAGE DataKinds, GADTs, StandaloneDeriving, Rank2Types, PolyKinds, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables #-}

Hi. Thanks for your answer! There was quite some time passed by, but.. well, i was trying to figure out how reflection works. I've read [1] (not till the end). It's a bit too complex for me, but i thought i understand the idea how `reify` works. But still i can't understand how `reifyNat` works. Here is my code:

import Unsafe.Coerce

data Nat = Z | S Nat deriving (Show)

data SNat :: Nat -> * where SZ :: SNat 'Z SN :: SNat n -> SNat ('S n) deriving instance Show (SNat n)

SNat is a singleton type for Nat. Then i (re-)define `reifyNat`

data Proxy s = Proxy

class Reifies s a | s -> a where reflect :: p s -> a

class SNatClass (a :: Nat) where singN :: SNat a

instance SNatClass 'Z where singN = SZ instance SNatClass n => SNatClass ('S n) where singN = SN singN

fromSNat :: SNat n -> Nat fromSNat SZ = Z fromSNat (SN n) = S (fromSNat n) {-# NOINLINE fromSNat #-}

instance SNatClass n => Reifies n Nat where reflect _ = fromSNat (singN :: SNat n)

newtype MagicNat r = MagicNat (forall (n :: Nat). SNatClass n => Proxy n -> r)

reifyNat :: forall r. Nat -> (forall (n :: Nat). SNatClass n => Proxy n -> r) -> r reifyNat x k = unsafeCoerce (MagicNat k :: MagicNat r) x Proxy {-# NOINLINE reifyNat #-}

testNat :: forall (n :: Nat). SNatClass n => Proxy n -> IO () testNat p = case (reflect p) of Z -> print "a" S Z -> print "b" S (S Z) -> print "c" _ -> print "d"

testSNat :: forall (n :: Nat). SNatClass n => Proxy n -> IO () testSNat p = case (singN :: SNat n) of SZ -> print "A" SN SZ -> print "B" SN (SN SZ) -> print "C" _ -> print "D"

main = do print (reifyNat (S (S Z)) reflect) reifyNat (S (S Z)) testNat reifyNat (S (S Z)) testSNat

and now if i dump core: ghc-core --no-syntax --no-asm --no-cast -- -dsuppress-var-kinds -dsuppress-type-applications -dsuppress-uniques from-snat.hs i may see, that k takes two arguments: SNatClass dictionary and Proxy reifyNat = \ (@ r) (x :: Nat) (k :: forall (n :: Nat). SNatClass n => Proxy Nat n -> r) -> (k `cast` ...) x (Proxy) main7 = S Z main6 = S main7 main5 = \ (@ (n :: Nat)) ($dSNatClass :: SNatClass n) _ -> fromSNat ($dSNatClass `cast` ...) main4 = reifyNat main6 main5 but because SNatClass class has only one method, its dictionary is just a function `singN` with type `singN :: SNat a`. But if so, why we supply `x :: Nat` as dictionary in `reifyNat`? Shouldn't we supply value of type `SNat n`? No need to say, that code above works, and both `testNat` and `testSNat` find correct instance *Main> main S (S Z) "c" "C" but why? [1]: https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection On Mon, Apr 11, 2016 at 4:59 PM, Marcin Mrotek wrote:

Hello,

In your function, the type `n`, and thus also the value of the argument, would have to be known at compile time. I'm not sure if you could make it to work. However, you can use the reflection package (https://hackage.haskell.org/package/reflection) where you can find a `reifyNat` function ( https://hackage.haskell.org/package/reflection-2.1.2/docs/Data-Reflection.ht... ) that lets you create a "temporary" type that never escapes the callback you give to it, and so it doesn't have to be known at compile time:

reifyNat :: forall r. Integer -> (forall n. KnownNat n => Proxy n -> r) -> r

The only requirement is that type `r` doesn't depend in any way on `n` (but the computation itself can use it, it just has to return the same type every time).

Best regards, Marcin Mrotek _______________________________________________ Beginners mailing list Beginners@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners

{-# 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 wrote:

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

{-# LANGUAGE DataKinds, GADTs, StandaloneDeriving, Rank2Types, PolyKinds, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables #-}

data Nat = Z | S Nat deriving (Show)

On Fri, May 6, 2016 at 2:24 PM, Marcin Mrotek wrote:

You could define SNat as something

newtype SNat (n :: Nat) = SNat Nat deriving (Show)

to be on the safer side, and then define SNatClass and natVal as something like:

class SNatClass (n :: Nat) where singN :: SNat n

instance SNatClass Z where singN = SNat Z

instance SNatClass n => SNatClass (S n) where singN = SNat (S n) where SNat n = (singN :: SNat n)

natVal :: forall n proxy. SNatClass n => proxy n -> Nat natVal _ = case (singN :: SNat n) of SNat n -> n

Hi. Hm.. but such singleton definition differs from mine and i can't get it working. Your singleton defines function `type -> singleton`: *Main> singN :: SNat ('S 'Z) SNat (S Z) and function `type -> Nat`: *Main> natVal (undefined :: SNat ('S 'Z)) S Z Mine singleton:

data SNat2 :: Nat -> * where SZ :: SNat2 'Z SN :: SNat2 n -> SNat2 ('S n) deriving instance Show (SNat2 n)

class SNatClass2 (a :: Nat) where singN2 :: SNat2 a

instance SNatClass2 'Z where singN2 = SZ instance SNatClass2 n => SNatClass2 ('S n) where singN2 = SN singN2

natVal2 :: forall p n. SNatClass2 n => p n -> Nat natVal2 _ = case singN2 :: SNat2 n of SZ -> Z SN SZ -> S Z

does this too: *Main> singN2 :: SNat2 ('S 'Z) SN SZ *Main> natVal2 (undefined :: SNat2 ('S 'Z)) S Z But mine singleton also defines function `singleton -> type`: *Main> :t SN SZ SN SZ :: SNat2 ('S 'Z) which yours does not: *Main> :t SNat (S Z) SNat (S Z) :: SNat n or in other words: *Main> :t SN SZ :: SNat2 'Z <interactive>:1:1: Couldn't match type ‘'S 'Z’ with ‘'Z’ Expected type: SNat2 'Z Actual type: SNat2 ('S 'Z) In the expression: SN SZ :: SNat2 Z but *Main> :t SNat (S Z) :: SNat 'Z SNat (S Z) :: SNat 'Z :: SNat 'Z Then when i try to define recursive function on singletons, i need that relation:

data Vec :: * -> Nat -> * where Nil :: Vec a 'Z Cons :: a -> Vec a n -> Vec a ('S n) deriving instance Show a => Show (Vec a n)

natVec2 :: SNat2 n -> Vec Int n natVec2 SZ = Nil natVec2 (SN n) = Cons 1 (natVec2 n)

as i understand, here (in `natVec2`) pattern matching on value level introduces type equalities (n ~ 'Z) or (n ~ 'S n) at type level correspondingly. But with your singleton it can't be done that way. I've tried to use witness (well, i've probably used it wrong, but still..), but can't figure out how to specify "if (n ~ 'S m), then" at type level:

data SingInst (n :: Nat) where SingInst :: SNatClass n => SingInst n

singInst :: forall p n. SNatClass n => p ('S n) -> SingInst n singInst _ = case (singN :: SNat ('S n)) of SNat _ -> SingInst

natVec :: forall p n. SNatClass2 n => p n -> Vec Int n natVec _ = case (singN :: SNat n) of SNat Z -> Nil SNat (S n) -> natVec (singInst (singN :: SNat n))

Is there a way to define `natVec` with your singleton?