<div dir="ltr"><div dir="auto"><div>Wow, that email really got garbled. I was in the process of drafting it when I sent it accidentally and then went off into the mountains and forgot about it. Sorry about that! I had a few more things to say.</div><div dir="auto"><br></div><div dir="auto">First, it might be possible to get away from the non-linear pattern using a version of generics. In particular, if we derive Rep and From type families for each type, we can define (==) by comparing generic representations. Or we could derive (==) directly. Moreover, the non-linear pattern approach won't help us define type-level Ord; for that we need either direct or generic-mediated derivation. Related: it's a bit annoying that when the case  ((f :: j -> k) (a :: j)) is rejected, we *know* that the type being matched must be a constructor, but we can't really do anything directly with that information.<br></div><div dir="auto"><br></div><div dir="auto">Second, you write</div><div dir="auto"><br></div><div dir="auto"><span style="font-family:sans-serif">> If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected?</span><br></div><div dir="auto"><font face="sans-serif">> [...]</font></div><div dir="auto"><span style="font-family:sans-serif">> </span><span style="font-family:sans-serif">Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. </span></div><div dir="auto"><span style="font-family:sans-serif"><br></span></div><div dir="auto"><font face="sans-serif">How is this really different from the situation on the term level? User code must always take care to respect the quotient. You say (==) is only "useful" if</font><font face="sans-serif"> we can produce<br><br>reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.<br><br></font></div><div><font face="sans-serif">I'm not convinced that this is the only measure of utility, although it's an important one. That said, I suspect that the version of (==) in Data.Type.Equality should be the simple polykinded one; others would probably fit better elsewhere. Feel free to accept D3835 if you think we should just do that.<br></font></div><div dir="auto"><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On Aug 11, 2017 6:28 PM, "David Feuer" <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail-m_4265456177604390981quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto"><div class="gmail_extra" dir="auto"><div class="gmail_quote">On Aug 11, 2017 9:39 AM, "Richard Eisenberg" <<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>> wrote:<br type="attribution"><blockquote class="gmail-m_4265456177604390981m_-6499704812767348275quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;"><div><br></div><div>But I wonder if we're better off dxaa aembracing the distinction between a reflexive (==) and a structurally recursive (==) and provide both, with different names.</div></div></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I don't think it would be bad to offer a canonical reflexive equality test. There are probably situations where having such a thing would be marginally useful. In particular,</div><div dir="auto"><br></div><div dir="auto">MyEqual a b ~ 'False</div><div dir="auto"><br></div><div dir="auto">isn't quite the same ass Alaska</div><div dir="auto"><br></div><div dir="auto">YourEqual a b ~ 'False</div><div dir="auto"><br></div><div dir="auto">even if the two type families are defined the same.</div><div dir="auto"><br></div><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="gmail-m_4265456177604390981m_-6499704812767348275quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;"><div>Or, we could just decide to go with the structurally recursive one, which seems to be more useful, especially as I have become much more skeptical of non-linear patterns (necessary Aziz a a add as ad ahs asf as s for the reflexive (==)).</div></div></blockquote></div></div><div dir="auto"><br></div><div dir="auto">I'm a bit fuzzy on this. Don't *both* of my versions rely essentially on nonlinear patterns to compare constructors? I suppose it might c always xd Hz</div><div class="gmail-m_4265456177604390981elided-text"><div dir="auto"><br></div><div dir="auto"><br></div><div class="gmail_extra" dir="auto"><div class="gmail_quote"><blockquote class="gmail-m_4265456177604390981m_-6499704812767348275quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;"><div>In particular, I don't have a good story for how they would work in Dependent Haskell. Section 5.13.2 of my thesis (<a href="http://cs.brynmawr.edu/%7Erae/papers/2016/thesis/eisenberg-thesis.pdf" target="_blank">http://cs.brynmawr.edu/~rae/p<wbr>apers/2016/thesis/eisenberg-th<wbr>esis.pdf</a>) contains some technical discussion of the challenges, but that section may not be digestible on its own. </div><div><br></div><div>The point of difference between David's two proposed changes is extensibility: that is, could someone decide to have a custom equality operator on a user-defined type? This is indeed a reasonable thing to want -- for example, you could imagine a record system that stores names of fields and their types in a type-level list, but that list should really be regarded as a set. However, worms lurk under this stone. If we have a more flexible notion of equality, how can we be sure that this more inclusive equality is always respected? Specifically, you would want this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context, everything still works. Sadly, there is no way to guarantee such a property. If (==) is to be useful in a type system, we would need such a guarantee. (By "useful", I mean that this is implementable: reifyEq :: ((a == b) ~ True, Typeable a, Typeable b) => a :~: b.) This brings us to the doorstep of higher inductive types -- a door that might be fun to enter, but is a long long way off.</div><div><br></div><div>In sum, I argue for David's first, inextensible version.</div><div><br></div><div>By the way, nothing about this requires TypeInType. If I had thought of David's version (that splits apart type applications) in 2013, I probably would have implemented (==) that way.</div><font color="#888888"><div><br></div><div>Richard</div></font><div class="gmail-m_4265456177604390981m_-6499704812767348275elided-text"><br><div><blockquote type="cite"><div>On Aug 10, 2017, at 9:00 PM, David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:</div><br class="gmail-m_4265456177604390981m_-6499704812767348275m_-5759152986954744988Apple-interchange-newline"><div><div dir="auto">I tend to agree with you, although I don't think () is a compelling argument. Rather,  it reuses the name == that Haskellers are accustomed to defining flexibly. But for that same reason, as well as the convenience, I do think we should consider using a kind class. That way things at the type level look pretty much like they do at the term level.</div><div class="gmail_extra"><br><div class="gmail_quote">On Aug 10, 2017 10:59 AM, "Ryan Scott" <<a href="mailto:ryan.gl.scott@gmail.com" target="_blank">ryan.gl.scott@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Personally, I'd be more inclined towards latter approach (in<br>
<a href="https://phabricator.haskell.org/D3837" rel="noreferrer" target="_blank">https://phabricator.haskell.or<wbr>g/D3837</a>). After all, one of the key<br>
properties of (==) (for which the Haddocks even make a special note)<br>
is that it does not attempt to provide an instance that works for<br>
every possible kind. Indeed, as you've discovered, there are cases<br>
when it doesn't make sense to use DefaultEq, such as for ().<br>
<br>
I'll tentatively give my support for D3837, although I'd be curious to<br>
hear what Richard has to say about this (since I'm reasonably<br>
confident he gave (==) its current implementation).<br>
<br>
Ryan S.<br>
______________________________<wbr>_________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">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-bi<wbr>n/mailman/listinfo/libraries</a><br>
</blockquote></div></div>
______________________________<wbr>_________________<br>Libraries mailing list<br><a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/libraries</a><br></div></blockquote></div><br></div></div></blockquote></div><br></div></div></div>
</blockquote></div><br></div></div></div>
</div>