On Mon, Mar 4, 2013 at 8:43 AM, Shachaf Ben-Kiki
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.
gcast does, though
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
-- Your ship was destroyed in a monadic eruption.