[Haskell-beginners] Type depending on value
Dmitriy Matrosov
sgf.dma at gmail.com
Thu May 5 10:14:26 UTC 2016
> {-# 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
<marcin.jan.mrotek at gmail.com> 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.html#g:1
> ) 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
More information about the Beginners
mailing list