newtypeable, new cast?
Simon PeytonJones
simonpj at microsoft.com
Mon Mar 4 13:24:03 CET 2013
 λ> data a :~: b where Refl :: a :~: a
 λ> :t gcast Refl
 gcast Refl :: forall a b. (Typeable a, Typeable b) => Maybe ((:~:) *
 a b)
That is a ferociouslyunintuitive use of 'gcast'! It too me dome while to convince myself that it was right. Though it does indeed work. I'd see (gcast Refl) as the primitive, with 'gcast' itself as a simple derived function.
I'm not sure what name to give the new cast function
?? :: Typeable a, Typeable b) => Maybe (a :~: b)
Do we need gcast1 and gcast2 any more, in our new polykinded world? Can they be depreceated?
Simon
 Original Message
 From: Shachaf BenKiki [mailto:shachaf at gmail.com]
 Sent: 04 March 2013 10:18
 To: Simon PeytonJones
 Cc: libraries at haskell.org; Stephanie Weirich; Richard Eisenberg
 (eir at cis.upenn.edu); Dimitrios Vytiniotis; Iavor Diatchki; Conor
 McBride; Pedro Magalhães
 Subject: Re: newtypeable, new cast?

 On Mon, Mar 4, 2013 at 1:07 AM, Simon PeytonJones
 <simonpj at microsoft.com> wrote:
 > Shachaf's idea (below) makes sense to me, though I'd present it
 slightly differently.
 >
 > * Currently, cast :: (Typeable a, Typeable b) => a > Maybe b
 > provides a function to convert a value of type 'a' to 'b'.
 > But it does not provide a way to convert a [a] to [b], or
 > a>Int to b>Int.
 >
 > * Of course these things can be done with 'map', but that's a pain,
 > and the type involved might not be an instance of Functor
 >
 > * So the Right Thing is provide a witness for a~b, wrapped as usual
 > in a GADT. Then it will "lift" automatically to any type, such as
 > those above.
 >
 > * The type GHC.TypeLits.(:~:) is the current library version of a
 > GADTwrapped equality
 > So we need
 > newCast :: (Typeable a, Typeable b) => Maybe (a :~: b)
 >
 > As usual this relies absolutely on the veracity of Typeable, but now
 we only derive it mechanically that should be assured.
 >
 > Iavor/Pedro, what do you think?
 >
 > Simon
 >

 I sent this message to the wrong address before:

 On Mon, Mar 4, 2013 at 12:44 AM, Shachaf BenKiki <shachaf at gmail.com>
 wrote:
 > On Mon, Mar 4, 2013 at 12:28 AM, Gábor Lehel <illissius at gmail.com>
 wrote:
 >>> Any of these lets you write any of the other ones, of course. But
 >>> "cast" doesn't let you write any of them, because it only goes in
 >>> one direction.
 >>
 >> gcast does, though
 >>
 >
 > You're complete right. Somehow I'd managed not to notice gcast. So the
 > primitive I want already exists  there isn't much point to the rest
 > of the message.
 >
 > Thanks!
 > Shachaf

 As Gábor pointed out, Data.Typeable already has gcast, which gives you
 Leibnizstyle equality:

 λ> data a :~: b where Refl :: a :~: a
 λ> :t gcast Refl
 gcast Refl :: forall a b. (Typeable a, Typeable b) => Maybe ((:~:) *
 a b)

 So this isn't needed as a primitive.

 I didn't realize HEAD had a standard version of Refl  given that, it
 might makes sense to add this as a convenience definition in
 Data.Typeable. But it's not as important as I'd thought.

 Shachaf
More information about the Libraries
mailing list