Send Beginners mailing list submissions to
beginners@haskell.org
To subscribe or unsubscribe via the World Wide Web, visit
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
beginners-requ...@haskell.org
You can reach the person managing the list at
beginners-ow...@haskell.org
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Type depending on value (Marcin Mrotek)
----------------------------------------------------------------------
Message: 1
Date: Fri, 6 May 2016 13:24:55 +0200
From: Marcin Mrotek <marcin.jan.mro...@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Type depending on value
Message-ID:
<CAJcfPz=crgvp_6uyfoyzmv5mijqqvhmngfle4h_pye8okrw...@mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
> 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
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 95, Issue 11
*****************************************
