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 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@cis.upenn.edu] | Sent: 04 March 2013 14:24 | To: Shachaf Ben-Kiki | Cc: Simon Peyton-Jones; libraries@haskell.org; Richard Eisenberg | (eir@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 | > 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@haskell.org http://www.haskell.org/mailman/listinfo/libraries