new-typeable, new cast?

[José Pedro Magalhães]

Hi,

On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg <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]
> > | 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
> > | >
> >
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130304/7b6305ad/attachment.htm>