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@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@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@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@haskell.org
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://www.haskell.org/mailman/listinfo/libraries