new-typeable, new cast?

[Simon Peyton-Jones]

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?

Correct. It’s just a question of agreeing API, naming, data types, and which module they are all declared in.  And deciding whether to deprectate gcast1 gcast2 etc.

It may be more sensible to declare (:~:) in Data.Typeable for example.  I don’t really have much of an opinion: you guys are closer to it than me.

Simon


From: josepedromagalhaes at gmail.com [mailto:josepedromagalhaes at gmail.com] On Behalf Of José Pedro Magalhães
Sent: 04 March 2013 19:12
To: Richard Eisenberg
Cc: Simon Peyton-Jones; Stephanie Weirich; Shachaf Ben-Kiki; libraries at haskell.org; Dimitrios Vytiniotis; Iavor Diatchki; Conor McBride
Subject: Re: new-typeable, new cast?

Hi,
On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>> 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 at cis.upenn.edu<mailto:sweirich at cis.upenn.edu>]
> | Sent: 04 March 2013 14:24
> | To: Shachaf Ben-Kiki
> | Cc: Simon Peyton-Jones; libraries at haskell.org<mailto:libraries at haskell.org>; Richard Eisenberg
> | (eir at cis.upenn.edu<mailto: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<mailto: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
> | >
>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130304/2d12b75b/attachment-0001.htm>