[Proposal] Renaming (:=:) to (==)

[Edward Kmett]

~ is used for the equality witness itself as a constraint.


On Sun, Sep 29, 2013 at 7:25 AM, Sebastiaan Joosten <sjcjoosten at gmail.com>wrote:

> 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: ==
>
>
> On Sep 29, 2013, at 7:21 , Carter Schonwald <carter.schonwald at gmail.com>
> wrote:
>
> so a term of type a==b lets you locally introduce the hypothesis that a~b
> in the local types?
> (just making sure i understand this).
>
> 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
>
>
> On Sun, Sep 29, 2013 at 12:10 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
>
>> -1 from me.
>>
>> 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.
>>
>> Richard
>>
>> On Sep 28, 2013, at 10:08 PM, Shachaf Ben-Kiki wrote:
>>
>> > On Sat, Sep 28, 2013 at 6:57 PM, Edward Kmett <ekmett at gmail.com> wrote:
>> >> As part of the discussion about Typeable, GHC 7.8 is going to include a
>> >> Data.Type.Equality module that provides a polykinded type equality data
>> >> type.
>> >>
>> >> I'd like to propose that we rename this type to (==) rather than the
>> (:=:)
>> >> it was developed under.
>> >>
>> >> We are already using (+), (-), (*), etc. at the type level in
>> type-nats, so
>> >> it would seem to fit the surrounding convention.
>> >>
>> >> I've done the work of preparing a patch, visible here:
>> >>
>> >>
>> https://github.com/ekmett/packages-base/commit/fb47f8368ad3d40fdd79bdeec334c0554fb17110
>> >>
>> >> Thoughts?
>> >>
>> >> Normally, I'd let this run the usual 2 week course, but we're getting
>> down
>> >> to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck
>> with
>> >> the current name forever.
>> >>
>> >> Discussion Period: 1 week
>> >>
>> >> -Edward Kmett
>> >>
>> >
>> > +1. For what it's worth, I suggested that name before, and Richard
>> > Eisenberg suggested that == should be for type-level Boolean equality:
>> > <http://markmail.org/message/3yifytgt2k3cfwws>. I'm not convinced,
>> > though -- this seems fundamental enough to deserve the simplest name
>> > possible.
>> >
>> > (I'm using that link because the haskell.org mailing list archive
>> > seems to be gone... Hopefully that comes back, eventually.)
>> >
>> >    Shachaf
>> > _______________________________________________
>> > Libraries mailing list
>> > Libraries at haskell.org
>> > http://www.haskell.org/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://www.haskell.org/mailman/listinfo/libraries
>>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130929/2edbb3ce/attachment.html>