new-typeable, new cast?

Shachaf Ben-Kiki shachaf at
Mon Mar 4 11:17:30 CET 2013

On Mon, Mar 4, 2013 at 1:07 AM, Simon Peyton-Jones
<simonpj at> 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> wrote:
> On Mon, Mar 4, 2013 at 12:28 AM, Gábor Lehel <illissius at> 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.


More information about the Libraries mailing list