On Sun, Mar 3, 2013 at 11:43 PM, Shachaf Ben-Kiki 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.

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

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 | -----Original Message----- | From: libraries-bounces@haskell.org [mailto:libraries- | bounces@haskell.org] On Behalf Of Shachaf Ben-Kiki | Sent: 04 March 2013 07:44 | To: libraries@haskell.org | Subject: new-typeable, new cast? | | This came up in #haskell -- rather than just provide coerce, cast (or a | primitive that cast can be built on, as well as other things) can give a | type equality witness of some kind. Some possible signatures | are: | | cast :: (Typeable a, Typeable b) => Maybe (p a -> p b) -- Leibniz- | style equality | cast :: (Typeable a, Typeable b) => p a -> Maybe (p b) -- another | form | cast :: (Typeable a, Typeable b) => Maybe (Is a b) -- GADT-style | equality | cast :: (Typeable a, Typeable b) => MightBe a b -- another form | -- With | data Is a b where { Refl :: Is a a } -- standard equality GADT | data MightBe a b where -- version with built-in Maybe, for more | convenient types | Is :: MightBe a a | Isn't :: MightBe a b | | 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. | | The GADT form can let you write code like | | foo :: forall a. Typeable a => a -> ... | foo x | | Is <- cast :: MightBe a Int = ...x... | | Is <- cast :: MightBe a Char = ...x... | | otherwise = ... | | Without coming up with a new name for x. It's possible to provide other | functions on top of this primitive, like | | cast :: (Typeable a, Typeable b) => proxy a -> qroxy b -> ... -- to | save some type annotations | cast :: (Typeable a, Typeable b) => (a ~ b => r) -> Maybe r -- to | use an expression directly | cast :: (Typeable a, Typeable b) => a -> Maybe b -- the original | | Of the primitives I mentioned, the first two are H2010. The last two are | nice to use directly, but use extensions (this probably doesn't matter | so much for new-typeable). The Maybe form lets you say things like `fmap | (\Is -> ...) (cast :: ...)` -- unfortunately, there's no "proper" Is | type in base right now. The fourth version might save some typing, and | might be slightly better performance-wise, since it saves a ⊥ (it's just | represented like Bool at runtime)? Probably it all gets inlined so that | doesn't matter anyway. | | Regardless of which particular primitive is used, it would be great for | new-typeable to provide something stronger than cast. | | Shachaf | | _______________________________________________ | Libraries mailing list | Libraries@haskell.org | http://www.haskell.org/mailman/listinfo/libraries