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