new-typeable, new cast?
shachaf at gmail.com
Mon Mar 4 11:17:30 CET 2013
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?
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
>> 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.
As Gábor pointed out, Data.Typeable already has gcast, which gives you
λ> 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