[Haskell-beginners] Type depending on value

[Marcin Mrotek]

> 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.

Sorry, I thought that natVal is a part of KnownNat, and I didn't
bother to check.

> 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)).

Nat is somewhat magic, as it's built into GHC. Type literals like
0,1,2,3... are all legal types of this kind. It is possible to write
type class instances for them, but they're uninhabited, and thus can
only be used as parameters for other types. I guess KnownNat is just
magic too, but I think in principle it could be defined by induction,
though the last time I've checked GHC had problems with realizing that
'0' and 'n + 1' are not overlapping.

> 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.

I think that, while "newtype SNat (n :: Nat) = SNat Integer" is
reliably coercible to Integer, your SNat happens to be coercible to
your Nat too, but again, I have no idea if this is the expected
behavior. It's playing with unsafeCoerce and GHC internals after all,
so weird things can happen. You could define SNat as something
"newtype SNat (n :: Nat) = SNat Nat" to be on the safer side, and then
define SNatClass and natVal as something like:

class SNatClass (n :: Nat) where
  singN :: SNat n

instance SNatClass Z where
  singN = SNat Z

instance SNatClass n => SNatClass (S n) where
  singN = SNat (S n)
    where SNat n = (singN :: SNat n)

natVal :: forall n proxy. SNatClass n => proxy n -> Nat
natVal _ = case (singN :: SNat n) of SNat n -> n

Best regards,
Marcin Mrotek