new-typeable, new cast?

[Shachaf Ben-Kiki]

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