While we&#39;re talking about poly-kinding and the role of gcast as applied to (:~:) nee (==), it is worth noting that Control.Category should get a PolyKinded flag, so that (==) can have an instance for the transitivity of type equality.<div>
<div><br></div><div>-Edward<br><br><div class="gmail_quote">On Mon, Mar 4, 2013 at 10:30 AM, Simon Peyton-Jones <span dir="ltr">&lt;<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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?<br>

<br>
Simon<br>
<div class="im"><br>
| -----Original Message-----<br>
| From: Stephanie Weirich [mailto:<a href="mailto:sweirich@cis.upenn.edu">sweirich@cis.upenn.edu</a>]<br>
| Sent: 04 March 2013 14:24<br>
| To: Shachaf Ben-Kiki<br>
| Cc: Simon Peyton-Jones; <a href="mailto:libraries@haskell.org">libraries@haskell.org</a>; Richard Eisenberg<br>
| (<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>); Dimitrios Vytiniotis; Iavor Diatchki; Conor<br>
| McBride; Pedro Magalhães<br>
| Subject: Re: new-typeable, new cast?<br>
|<br>
</div>| Nice! I agree that having a (poly-kinded!) function of type<br>
|<br>
| &gt;&gt; eqT :: forall (a :: k) (b :: k). (Typeable a, Typeable b) =&gt; Maybe (a<br>
| &gt;&gt; :~: b)<br>
|<br>
| around is The Right Way to Go. I&#39;d call this function &quot;eqT&quot; or<br>
| &quot;eqTypeable&quot;, after the similar operation in Data.Type.Equality. Thanks<br>
| for pointing out that we can get such a function so easily from gcast.<br>
| (Note that gcast itself can be polykinded now, I&#39;m writing down the<br>
| kinds to make them obvious.)<br>
|<br>
| gcast :: forall (a :: k) (b::k) (c::k -&gt;*). (Typeable a, Typeable b) -&gt;<br>
| c a -&gt; Maybe (c b)<br>
|<br>
| WRT to gcast1 and gcast2, these functions can be subsumed by eqT, but<br>
| not by polykinded gcast due to the restrictions on higher-order<br>
| polymorphism.<br>
|<br>
| gcast1 can convert [b Int] to [Maybe Int], but gcast cannot. eqT can do<br>
| so with a pattern match. This behavior does seem rather special-purpose<br>
| though---eqT is much more flexible.<br>
|<br>
| With singletons, we could imagine two different polykinded operations,<br>
| that differ only in whether their arguments are explicit/implicit.<br>
|<br>
| eqTypeable :: (Typeable a, Typeable b) =&gt; Maybe (a :~: b)<br>
|<br>
| eqSing :: Sing a -&gt; Sing b -&gt; Maybe (a :~: b)<br>
|<br>
| Again, Sing should be kind-indexed, so that we can have Sing True, Sing<br>
| 0, and (eventually) Sing Int.<br>
|<br>
| --Stephanie<br>
<div class="HOEnZb"><div class="h5">|<br>
|<br>
| On Mar 4, 2013, at 8:46 AM, Shachaf Ben-Kiki wrote:<br>
|<br>
| &gt; On Mon, Mar 4, 2013 at 4:24 AM, Simon Peyton-Jones<br>
| &gt; &lt;<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>&gt; wrote:<br>
| &gt;&gt; |     λ&gt; data a :~: b where Refl :: a :~: a<br>
| &gt;&gt; |     λ&gt; :t gcast Refl<br>
| &gt;&gt; |     gcast Refl :: forall a b. (Typeable a, Typeable b) =&gt; Maybe<br>
| &gt;&gt; | ((:~:) * a b)<br>
| &gt;&gt;<br>
| &gt;&gt; That is a ferociously-unintuitive use of &#39;gcast&#39;!  It too me dome<br>
| while to convince myself that it was right.   Though it does indeed<br>
| work.  I&#39;d see (gcast Refl) as the primitive, with &#39;gcast&#39; itself as a<br>
| simple derived function.<br>
| &gt;&gt;<br>
| &gt;&gt; I&#39;m not sure what name to give the new cast function<br>
| &gt;&gt;        ?? :: Typeable a, Typeable b) =&gt; Maybe (a :~: b)<br>
| &gt;&gt;<br>
| &gt;&gt;<br>
| &gt;&gt; Do we need gcast1 and gcast2 any more, in our new polykinded world?<br>
| Can they be depreceated?<br>
| &gt;&gt;<br>
| &gt;&gt; Simon<br>
| &gt;&gt;<br>
| &gt;<br>
| &gt; A couple of people have suggested &quot;same&quot;. (I wonder if this would also<br>
| &gt; subsume eqSingNat/eqSingSym?).<br>
| &gt;<br>
| &gt; By the way -- since (:~:) seems to be in HEAD now, but not yet<br>
| &gt; released, is there a chance of renaming it? &quot;:~:&quot; is pretty awkward to<br>
| &gt; type, given all the new TypeOperators options these days; how about<br>
| &gt; &quot;==&quot;?<br>
| &gt;<br>
| &gt;    Shachaf<br>
| &gt;<br>
<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
</div></div></blockquote></div><br></div></div>