
<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto"><div>I for one favor the HRefl constructor name for practical reasons. These types will commonly be used in similar scopes.</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">Also, there is a theoretical quibble for why this shouldn't just replace :~: directly in any code that would otherwise use both and why both will be used in much the same code going forward:</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">Heterogenous equality is a form of what Conor McBride calls "John Major" equality. In a more general type theory, HRefl doesn't imply Refl! You can't show HRefl implies Refl in MLTT. This extra power is granted by dependent pattern matching most dependent type theories or in Haskell by the way we implement ~. In Haskell, today, it works out because we have "uniqueness of identity proofs" or "axiom K". This means that anything going on in the world of homotopy type theory today can't be used in Haskell directly as univalence and axiom k are inconsistent. </div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">Some work has been put into pattern matching in Agda without axiom K. Do I expect that folks are going to run out and implement it in Haskell? No, but in general I want to be very clear in my code when I rely upon this extra power that Haskell grants us kinda by accident or fiat today as those results don't transfer, and could be dangerous to assume if we decide to go in a different direction in the far flung future.</div><div id="AppleMailSignature"><br></div><div id="AppleMailSignature">-Edward</div><div id="AppleMailSignature"><br>Sent from my iPad</div><div><br>On Jul 9, 2017, at 5:35 PM, Oleg Grenrus <<a href="mailto:oleg.grenrus@iki.fi">oleg.grenrus@iki.fi</a>> wrote:<br><br></div><blockquote type="cite"><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div><div style="direction: inherit;"><span style="background-color: rgba(255, 255, 255, 0);">It's not only a value, it's also a pattern. We have PatternSynonyms, but IMHO it's not a strong argument for having constructors with a same name.</span></div><div style="direction: inherit;"><span style="background-color: rgba(255, 255, 255, 0);"><br></span></div><div style="direction: inherit;">- Oleg</div><br>Sent from my iPhone</div><div><br>On 9 Jul 2017, at 22.47, Wolfgang Jeltsch <<a href="mailto:wolfgang-it@jeltsch.info">wolfgang-it@jeltsch.info</a>> wrote:<br><br></div><blockquote type="cite"><div><span>Hi!</span><br><span></span><br><span>I agree with you, Andrew, that types should have different names.</span><br><span>However, (H)Refl is not a type. It is a data constructor; so it is a</span><br><span>special kind of value and as such very similar to sym, trans, and</span><br><span>friends. The similarity of Refl to the ordinary functions of the</span><br><span>Heterogeneous module becomes even more obvious when considering that</span><br><span>Refl is a proof, like sym, trans, and so on.</span><br><span></span><br><span>All the best,</span><br><span>Wolfgang</span><br><span></span><br><span>Am Samstag, den 08.07.2017, 21:25 -0400 schrieb Andrew Martin:</span><br><blockquote type="cite"><span>Just wanted to weigh in with my two cents. I also prefer to use the</span><br></blockquote><blockquote type="cite"><span>module system for the most part rather than prefixing function names</span><br></blockquote><blockquote type="cite"><span>with something that indicates the data type they operate on. However,</span><br></blockquote><blockquote type="cite"><span>when it comes to types, I would much rather they have different names.</span><br></blockquote><blockquote type="cite"><span>I like that the data constructor of :~~: is HRefl. However, for the</span><br></blockquote><blockquote type="cite"><span>functions sym, trans, etc., I would rather have a</span><br></blockquote><blockquote type="cite"><span>Data.Type.Equality.Hetero that exports all of these without any kind</span><br></blockquote><blockquote type="cite"><span>of prefixes on them. Then there's the question of where we export :~~:</span><br></blockquote><blockquote type="cite"><span>from. It could be exported only from the Hetero module, or it could be</span><br></blockquote><blockquote type="cite"><span>exported from both.</span><br></blockquote><blockquote type="cite"><span></span><br></blockquote><blockquote type="cite"><span>Sent from my iPhone</span><br></blockquote><blockquote type="cite"><span></span><br></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>On Jul 8, 2017, at 7:56 PM, Wolfgang Jeltsch <<a href="mailto:wolfgang-it@jeltsch.in">wolfgang-it@jeltsch.in</a></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>fo> wrote:</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Hi!</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Unfortunately, my wish has not been granted, as I wanted the data</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>constructor of (:~~:) to be named Refl and (:~~:) to be defined in a</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>separate module. I see that there are no heterogeneous versions of</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>sym,</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>trans, and so on in base at the moment. If they will be available at</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>some time, how will they be called? Will they be named hsym, htrans,</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>and</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>so on? This would be awful, in my opinion.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>In Haskell, we have the module system for qualification. I very well</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>understand the issues Julien Moutinho pointed out. For example, you</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>cannot have a module that just reexports all the functions from</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Data.Sequence and Data.Map, because you would get name clashes.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>However, I think that the solution to these kinds of problems is to</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>fix</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>the module system. An idea would be to allow for exporting qualified</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>names. Then a module could import Data.Sequence and Data.Map</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>qualified</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>as Seq and Map, respectively, and export Seq.empty, Map.empty, and</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>so</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>on. </span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>If we try to work around those issues with the module system by</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>putting</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>qualification into the actual identifiers in the form of single</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>letters</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>(like in mappend, HRef, and so on), we will be stuck with this</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>workaround forever, even if the module system will be changed at</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>some</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>time, because identifiers in core libraries are typically not</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>changed.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Just imagine, we would have followed this practice for the</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>containers</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>package. We would have identifiers like “smap”, “munion”,</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>“imintersection”, and so on.</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>All the best,</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Wolfgang</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Am Freitag, den 07.07.2017, 08:15 -0700 schrieb Ryan Scott:</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Sorry for only just discovering this thread now. A lot of this</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>discussion is in fact moot, since (:~~:) already is in base!</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Specifically, it's landing in Data.Type.Equality [1] in the next</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>version of base (bundled with GHC 8.2). Moreover, it's constructor</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>is</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>named HRefl, so your wish has been granted ;)</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>As for why it's being introduced in base, it ended up being useful</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>for</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>the new Type-indexed Typeable that's also landing in GHC 8.2. In</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>particular, the eqTypeRep function [2] must return heterogeneous</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>equality (:~~:), not homogeneous equality (:~:), since it's</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>possible</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>that you'll compare two TypeReps with different kinds.</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span></span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>Ryan S.</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>-----</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>[1] <a href="http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5">http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5</a></span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>f718d18fcaa66a:/libraries/base/Data/Type/Equality.hs#l37</span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>[2] <a href="http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5">http://git.haskell.org/ghc.git/blob/99adcc8804e91161b35ff1d0e5</a></span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><blockquote type="cite"><span>f718d18fcaa66a:/libraries/base/Data/Typeable/Internal.hs#l311>; </span><br></blockquote></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>_______________________________________________</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span>Libraries mailing list</span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span><a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a></span><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><span><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a></span><br></blockquote></blockquote><span>_______________________________________________</span><br><span>Libraries mailing list</span><br><span><a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a></span><br><span><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a></span><br></div></blockquote></div></blockquote><blockquote type="cite"><div><span>_______________________________________________</span><br><span>Libraries mailing list</span><br><span><a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a></span><br><span><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a></span><br></div></blockquote></body></html>