new-typeable, new cast?

[Simon Peyton-Jones]

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