new-typeable, new cast?

[Gábor Lehel]

On Mon, Mar 4, 2013 at 8:43 AM, Shachaf Ben-Kiki <shachaf at gmail.com> wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries



-- 
Your ship was destroyed in a monadic eruption.