4 Mar
2013
4 Mar
'13
2:49 a.m.
On Sun, Mar 3, 2013 at 11:43 PM, Shachaf Ben-Kiki
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.
Note: It turns out this isn't actually true, since Is can derive Typeable: λ> data Is :: * -> * -> * where Refl :: Is a a deriving Typeable λ> let cast' :: forall a b. (Typeable a, Typeable b) => Maybe (Is a b); cast' = cast (Refl :: Is a a) It probably still makes sense to provide an equality witness in a less roundabout way, though. Shachaf