<div dir="ltr">~ is used for the equality witness itself as a constraint.</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Sep 29, 2013 at 7:25 AM, Sebastiaan Joosten <span dir="ltr"><<a href="mailto:sjcjoosten@gmail.com" target="_blank">sjcjoosten@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 style="word-wrap:break-word">I'd like to go for ~, but unfortunately it is in use as a prefix operator (for Lazy pattern matching) and it would be a lot more work to implement than the current :=: / ==. Someone would have to use the same trick as was used for unary/binary minus. I've no idea on how to change the lexer for that, so I'll just go with +1 on Edward's suggestion: ==<div>
<div class="h5"><div><br></div><div><br><div><div>On Sep 29, 2013, at 7:21 , Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>> wrote:</div><br><blockquote type="cite">
<div dir="ltr">so a term of type a==b lets you locally introduce the hypothesis that a~b in the local types?<div>(just making sure i understand this).</div><div><br></div><div>whats use case for the type level boolean equality? Naively, it seems like that could be derived from a typelevel " Maybe (a==b)'' plus a type level version of the "maybe" combinator</div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Sep 29, 2013 at 12:10 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">-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>
<span><font color="#888888"><br>
Richard<br>
</font></span><div><div><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></blockquote></div><br></div>
_______________________________________________<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>
</blockquote></div><br></div></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></div>