-Edward

On Mon, Mar 4, 2013 at 10:30 AM, Simon Peyton-Jones <simonpj@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@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
| > <simonpj@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@haskell.org
http://www.haskell.org/mailman/listinfo/libraries