[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