[Haskell-beginners] Type depending on value

[Dmitriy Matrosov]

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