<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">tl;dr: I like David's first version, D3835.</div><div class=""><br class=""></div><div class="">There is a fundamental tension in the definition of (==): Should it be reflexive or not? By "reflexive" here, I mean that (a == a) reduces to True, even if you know nothing further about a. The current definition of (==) is reflexive in this way for types of kind Type, but not for any of the other concrete instances (except the one for ()).</div><div class=""><br class=""></div><div class="">We can't currently have our cake and it eat, too: as David points out in this thread, (==) is either reflexive or structurally recursive. It can't do both. Possibly a solution to #4259 (<a href="https://ghc.haskell.org/trac/ghc/ticket/4259" class="">https://ghc.haskell.org/trac/ghc/ticket/4259</a>) would allow us to have (==) that is both reflexive and structurally recursive, but I have no idea how to do it.</div><div class=""><br class=""></div><div class="">I agree that the current choice of implementation for (==) is inconsistent in this regard and is perhaps foolish. I have no principled argument for why it is the way it is. But I wonder if we're better off embracing the distinction between a reflexive (==) and a structurally recursive (==) and provide both, with different names. 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 for the reflexive (==)). 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/~rae/papers/2016/thesis/eisenberg-thesis.pdf" class="">http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf</a>) contains some technical discussion of the challenges, but that section may not be digestible on its own. </div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">In sum, I argue for David's first, inextensible version.</div><div class=""><br class=""></div><div class="">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><div class=""><br class=""></div><div class="">Richard</div><br class=""><div><blockquote type="cite" class=""><div class="">On Aug 10, 2017, at 9:00 PM, David Feuer <<a href="mailto:david.feuer@gmail.com" class="">david.feuer@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="auto" class="">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 class=""><div class="gmail_quote">On Aug 10, 2017 10:59 AM, "Ryan Scott" <<a href="mailto:ryan.gl.scott@gmail.com" target="_blank" class="">ryan.gl.scott@gmail.com</a>> wrote:<br type="attribution" class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Personally, I'd be more inclined towards latter approach (in<br class="">
<a href="https://phabricator.haskell.org/D3837" rel="noreferrer" target="_blank" class="">https://phabricator.haskell.<wbr class="">org/D3837</a>). After all, one of the key<br class="">
properties of (==) (for which the Haddocks even make a special note)<br class="">
is that it does not attempt to provide an instance that works for<br class="">
every possible kind. Indeed, as you've discovered, there are cases<br class="">
when it doesn't make sense to use DefaultEq, such as for ().<br class="">
<br class="">
I'll tentatively give my support for D3837, although I'd be curious to<br class="">
hear what Richard has to say about this (since I'm reasonably<br class="">
confident he gave (==) its current implementation).<br class="">
<br class="">
Ryan S.<br class="">
______________________________<wbr class="">_________________<br class="">
Libraries mailing list<br class="">
<a href="mailto:Libraries@haskell.org" class="">Libraries@haskell.org</a><br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-<wbr class="">bin/mailman/listinfo/libraries</a><br class="">
</blockquote></div></div>
_______________________________________________<br class="">Libraries mailing list<br class=""><a href="mailto:Libraries@haskell.org" class="">Libraries@haskell.org</a><br class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries<br class=""></div></blockquote></div><br class=""></body></html>