new-typeable, new cast?

[Simon Peyton-Jones]

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 at haskell.org [mailto:libraries-
| bounces at haskell.org] On Behalf Of Shachaf Ben-Kiki
| Sent: 04 March 2013 07:44
| To: libraries at 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/libraries