Re: new-typeable, new cast?

On Mon, Mar 4, 2013 at 1:07 AM, Simon Peyton-Jones 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 GADT-wrapped 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 Ben-Kiki wrote:

On Mon, Mar 4, 2013 at 12:28 AM, Gábor Lehel 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 Leibniz-style 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