<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Sep 29, 2013 at 5:36 PM, Edward Kmett <span dir="ltr"><<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hrmm. <div><br></div><div>There is another wrinkle to consider. <div><br></div><div>Soon there will likely be another type coming along for a representational equality witness. So perhaps it would be best to use an = somewhere in the name and ~ in the other? To indicate this one is real equality and the other is only an equivalence?</div>
</div></div></blockquote><div><br></div><div style>I think this falls down because we already have (~) as a constraint meaning real equality, not only an equivalence.</div><div style><br></div><div style>I still like (:~:) for the real equality witness, to parallel the constraint. (~~) sounds OK too, along similar lines.</div>
<div style><br></div><div style>The representational equality could perhaps not be an operator, but something with a normal name, just like `Coercible` is not an operator either (which AFAIK is the constraint form of it).</div>
<div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><span class="HOEnZb"><font color="#888888">
<div><br></div><div>-Edward</div></font></span></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Sep 29, 2013 at 11:29 AM, Stijn van Drongelen <span dir="ltr"><<a href="mailto:rhymoid@gmail.com" target="_blank">rhymoid@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>What about (~~)?</div></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Sun, Sep 29, 2013 at 5:21 PM, Edward Kmett <span dir="ltr"><<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I can appreciate the objections to (==) and I'm absolutely open to other names. </div><div><br>
</div><div>I just rather dislike (:=:).<div><br></div><div>Lets throwing this open to bikeshedding. Alternatives?</div><span><font color="#888888">
<div><br></div></font></span></div><span><font color="#888888"><div>-Edward</div></font></span></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Sep 29, 2013 at 8:33 AM, Roman Cheplyaka <span dir="ltr"><<a href="mailto:roma@ro-che.info" target="_blank">roma@ro-che.info</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I agree with Richard here — this overloading of == doesn't seem<br>
intuitive to me. Using it for type-level boolean equality would be much<br>
more natural.<br>
<br>
That said, :=: could probably benefit from the relaxed rules for type<br>
operators; I just don't think == is a good choice.<br>
<br>
Roman<br>
<br>
* Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>> [2013-09-29 00:10:46-0400]<br>
<div><div>> -1 from me.<br>
><br>
> Shachaf stated my argument correctly -- I think that the (:=:) operator means something quite different from the term-level (==) operator, and the name should reflect this. I do like thinking about a better name, though, and I'm happy enough if I'm outvoted here.<br>
><br>
> Richard<br>
><br>
> On Sep 28, 2013, at 10:08 PM, Shachaf Ben-Kiki wrote:<br>
><br>
> > On Sat, Sep 28, 2013 at 6:57 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>> wrote:<br>
> >> As part of the discussion about Typeable, GHC 7.8 is going to include a<br>
> >> Data.Type.Equality module that provides a polykinded type equality data<br>
> >> type.<br>
> >><br>
> >> I'd like to propose that we rename this type to (==) rather than the (:=:)<br>
> >> it was developed under.<br>
> >><br>
> >> We are already using (+), (-), (*), etc. at the type level in type-nats, so<br>
> >> it would seem to fit the surrounding convention.<br>
> >><br>
> >> I've done the work of preparing a patch, visible here:<br>
> >><br>
> >> <a href="https://github.com/ekmett/packages-base/commit/fb47f8368ad3d40fdd79bdeec334c0554fb17110" target="_blank">https://github.com/ekmett/packages-base/commit/fb47f8368ad3d40fdd79bdeec334c0554fb17110</a><br>
> >><br>
> >> Thoughts?<br>
> >><br>
> >> Normally, I'd let this run the usual 2 week course, but we're getting down<br>
> >> to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with<br>
> >> the current name forever.<br>
> >><br>
> >> Discussion Period: 1 week<br>
> >><br>
> >> -Edward Kmett<br>
> >><br>
> ><br>
> > +1. For what it's worth, I suggested that name before, and Richard<br>
> > Eisenberg suggested that == should be for type-level Boolean equality:<br>
> > <<a href="http://markmail.org/message/3yifytgt2k3cfwws" target="_blank">http://markmail.org/message/3yifytgt2k3cfwws</a>>. I'm not convinced,<br>
> > though -- this seems fundamental enough to deserve the simplest name<br>
> > possible.<br>
> ><br>
> > (I'm using that link because the <a href="http://haskell.org" target="_blank">haskell.org</a> mailing list archive<br>
> > seems to be gone... Hopefully that comes back, eventually.)<br>
> ><br>
> > Shachaf<br>
> > _______________________________________________<br>
> > Libraries mailing list<br>
> > <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
> > <a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
><br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
</div></div><br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br><br clear="all"><div><br></div>-- <br>Your ship was destroyed in a monadic eruption.
</div></div>