Re: new-typeable, new cast?

Hi, On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg wrote:

Unless I'm missing something, this all looks very straightforward. The implementation is there, already, in the guise of (gcast Refl). We would just shuffle the definitions around a bit. Am I indeed missing something?

I think that is the case indeed. Though I agree that it would be a nice addition to Data.Typeable. Cheers, Pedro

As for the name, I agree that :~: is awkward to type. But, I think == should be saved for type-level Boolean equality, as a closer analogue to its term-level meaning. I don't have a better suggestion than :~:. Or, if we just allow Constraint/* polymorphism, than we can simply use ~, as that *already* is a GADT wrapping around an even more primitive denotation of equality. (Just kidding about the Constraint/* polymorphism…)

Richard

On 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 | >