newtypeable, new cast?
Simon PeytonJones
simonpj at microsoft.com
Mon Mar 4 16:30:17 CET 2013
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 BenKiki
 Cc: Simon PeytonJones; libraries at haskell.org; Richard Eisenberg
 (eir at cis.upenn.edu); Dimitrios Vytiniotis; Iavor Diatchki; Conor
 McBride; Pedro Magalhães
 Subject: Re: newtypeable, new cast?

 Nice! I agree that having a (polykinded!) 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 higherorder
 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 specialpurpose
 thougheqT 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 kindindexed, so that we can have Sing True, Sing
 0, and (eventually) Sing Int.

 Stephanie


 On Mar 4, 2013, at 8:46 AM, Shachaf BenKiki wrote:

 > On Mon, Mar 4, 2013 at 4:24 AM, Simon PeytonJones
 > <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 ferociouslyunintuitive 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
 >
More information about the Libraries
mailing list