<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto"><div>Not sure. You can go back and forth between normal Leibnizian equality and :~: in Haskell.</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">The notion of an Equality in lens can be seen as a Leibnizian equality, just with an extra set of parameters and encoding it that way lets us compose them with (.) from the Prelude. I suppose if you stripped off your newtype you could do the same here. Other than that? If we didn't have ~ or ~~ already it'd bring something to the table as it provides you some ability to talk about type equality without them in your language. But we do have them.<br><br>Sent from my iPhone</div><div><br>On Jul 10, 2017, at 2:18 PM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br><br></div><blockquote type="cite"><div><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>
</div></blockquote></body></html>