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