<div dir="auto">That's the idea I was after. Is it good for anything?</div><div class="gmail_extra"><br><div class="gmail_quote">On Jul 10, 2017 2:06 PM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
<br>
Sent from my iPad<br>
<br>
> On Jul 10, 2017, at 1:11 PM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br>
><br>
> Well, I came up with another notion of heterogeneous equality (much,<br>
> much more limited in practice):<br>
><br>
> newtype HEqual (a :: j) (b :: k) = HEqual (forall (f :: forall l. l -><br>
> Type). f a -> f b)<br>
<br>
This is "heterogeneous Leibnizian equality".<br>
<br>
> Implementing<br>
><br>
> fromHEqual :: forall j k (a :: j) (b :: k). HEqual a b -> a :~~: b<br>
> seems to require something like OtherEquality.<br>
><br>
> I'm not sure what you mean about not being able to reorder type<br>
> indices. OtherEquality can also be defined as a newtype around (:~~:):<br>
><br>
> newtype OtherEquality :: forall j. j -> forall k. k -> Type where<br>
>  OtherEquality :: a :~~: q -> OtherEquality a q<br>
><br>
> But perhaps you mean it's more convenient than :~~:?<br>
><br>
>> On Mon, Jul 10, 2017 at 1:03 PM, Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br>
>> This OtherEquality is actually a tad bit more general, given that GHC can't (currently) reorder type indices. But would anyone take advantage of the generality? I tend to doubt it...<br>
>><br>
>> Richard<br>
>><br>
>>> On Jul 10, 2017, at 12:20 PM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br>
>>><br>
>>> There's another version of heterogeneous equality that takes its<br>
>>> arguments in the other order. I'm not sure if this is generally useful<br>
>>> enough to want to include.<br>
>>><br>
>>> -- (:~~:) :: forall j k. j -> k -> *<br>
>>><br>
>>> data OtherEquality :: forall j. j -> forall k. k -> Type where<br>
>>> OtherRefl :: OtherEquality a a<br>
>>><br>
>>>> On Mon, Jul 10, 2017 at 11:24 AM, Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com">ryan.gl.scott@gmail.com</a>> wrote:<br>
>>>> I also agree that we should keep HRefl a distinct name, and moreover, we<br>
>>>> should keep :~: and :~~: as distinct datatypes.<br>
>>>><br>
>>>> I'm also on-board with the idea that we should introduce a separate<br>
>>>> Data.Type.Equality.Hetero module that reexports :~~: and defines<br>
>>>> heterogeneous counterparts for sym, trans, etc. from Data.Type.Equality. I<br>
>>>> don't have a strong opinion on how they should be named (e.g., sym vs.<br>
>>>> hsym).<br>
>>>><br>
>>>> Ryan S.<br>
>>>><br>
>>>> ______________________________<wbr>_________________<br>
>>>> Libraries mailing list<br>
>>>> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
>>>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
>>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Libraries mailing list<br>
>>> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
>>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
>><br>
> ______________________________<wbr>_________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div>