newtypeable, new cast?
Simon PeytonJones
simonpj at microsoft.com
Mon Mar 4 10:07:09 CET 2013
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
GADTwrapped 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: librariesbounces at haskell.org [mailto:libraries
 bounces at haskell.org] On Behalf Of Shachaf BenKiki
 Sent: 04 March 2013 07:44
 To: libraries at haskell.org
 Subject: newtypeable, 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)  GADTstyle
 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 builtin 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 newtypeable). 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 performancewise, 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
 newtypeable to provide something stronger than cast.

 Shachaf

 _______________________________________________
 Libraries mailing list
 Libraries at haskell.org
 http://www.haskell.org/mailman/listinfo/libraries
More information about the Libraries
mailing list