[Haskell-beginners] Type depending on value

Dmitriy Matrosov sgf.dma at gmail.com
Fri May 6 10:42:18 UTC 2016


> {-# 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
<marcin.jan.mrotek at gmail.com> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


More information about the Beginners mailing list