new-typeable, new cast?

[Edward Kmett]

While we're talking about poly-kinding and the role of gcast as applied to
(:~:) nee (==), it is worth noting that Control.Category should get a
PolyKinded flag, so that (==) can have an instance for the transitivity of
type equality.

-Edward

On Mon, Mar 4, 2013 at 10:30 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

> ok good. Since this is in the intersection of singletons and Typeable, I
> wonder if Pedro and Richard might together lead on driving this to a
> conclusion and implementing it?
>
> Simon
>
> | -----Original Message-----
> | From: Stephanie Weirich [mailto:sweirich at cis.upenn.edu]
> | Sent: 04 March 2013 14:24
> | To: Shachaf Ben-Kiki
> | Cc: Simon Peyton-Jones; libraries at haskell.org; Richard Eisenberg
> | (eir at cis.upenn.edu); Dimitrios Vytiniotis; Iavor Diatchki; Conor
> | McBride; Pedro Magalhães
> | Subject: Re: new-typeable, new cast?
> |
> | Nice! I agree that having a (poly-kinded!) function of type
> |
> | >> eqT :: forall (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a
> | >> :~: b)
> |
> | around is The Right Way to Go. I'd call this function "eqT" or
> | "eqTypeable", after the similar operation in Data.Type.Equality. Thanks
> | for pointing out that we can get such a function so easily from gcast.
> | (Note that gcast itself can be polykinded now, I'm writing down the
> | kinds to make them obvious.)
> |
> | gcast :: forall (a :: k) (b::k) (c::k ->*). (Typeable a, Typeable b) ->
> | c a -> Maybe (c b)
> |
> | WRT to gcast1 and gcast2, these functions can be subsumed by eqT, but
> | not by polykinded gcast due to the restrictions on higher-order
> | polymorphism.
> |
> | gcast1 can convert [b Int] to [Maybe Int], but gcast cannot. eqT can do
> | so with a pattern match. This behavior does seem rather special-purpose
> | though---eqT is much more flexible.
> |
> | With singletons, we could imagine two different polykinded operations,
> | that differ only in whether their arguments are explicit/implicit.
> |
> | eqTypeable :: (Typeable a, Typeable b) => Maybe (a :~: b)
> |
> | eqSing :: Sing a -> Sing b -> Maybe (a :~: b)
> |
> | Again, Sing should be kind-indexed, so that we can have Sing True, Sing
> | 0, and (eventually) Sing Int.
> |
> | --Stephanie
> |
> |
> | On Mar 4, 2013, at 8:46 AM, Shachaf Ben-Kiki wrote:
> |
> | > On Mon, Mar 4, 2013 at 4:24 AM, Simon Peyton-Jones
> | > <simonpj at microsoft.com> wrote:
> | >> |     λ> data a :~: b where Refl :: a :~: a
> | >> |     λ> :t gcast Refl
> | >> |     gcast Refl :: forall a b. (Typeable a, Typeable b) => Maybe
> | >> | ((:~:) * a b)
> | >>
> | >> That is a ferociously-unintuitive use of 'gcast'!  It too me dome
> | while to convince myself that it was right.   Though it does indeed
> | work.  I'd see (gcast Refl) as the primitive, with 'gcast' itself as a
> | simple derived function.
> | >>
> | >> I'm not sure what name to give the new cast function
> | >>        ?? :: Typeable a, Typeable b) => Maybe (a :~: b)
> | >>
> | >>
> | >> Do we need gcast1 and gcast2 any more, in our new polykinded world?
> | Can they be depreceated?
> | >>
> | >> Simon
> | >>
> | >
> | > A couple of people have suggested "same". (I wonder if this would also
> | > subsume eqSingNat/eqSingSym?).
> | >
> | > By the way -- since (:~:) seems to be in HEAD now, but not yet
> | > released, is there a chance of renaming it? ":~:" is pretty awkward to
> | > type, given all the new TypeOperators options these days; how about
> | > "=="?
> | >
> | >    Shachaf
> | >
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130304/0de4ca8e/attachment-0001.htm>