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

On Sun, Sep 29, 2013 at 5:36 PM, Edward Kmett wrote:

Hrmm.

There is another wrinkle to consider.

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?

I think this falls down because we already have (~) as a constraint meaning real equality, not only an equivalence. I still like (:~:) for the real equality witness, to parallel the constraint. (~~) sounds OK too, along similar lines. 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).

-Edward

On Sun, Sep 29, 2013 at 11:29 AM, Stijn van Drongelen wrote:

...

What about (~~)?

On Sun, Sep 29, 2013 at 5:21 PM, Edward Kmett wrote:

...

I can appreciate the objections to (==) and I'm absolutely open to other names.

I just rather dislike (:=:).

Lets throwing this open to bikeshedding. Alternatives?

-Edward

On Sun, Sep 29, 2013 at 8:33 AM, Roman Cheplyaka wrote:

...

I agree with Richard here — this overloading of == doesn't seem intuitive to me. Using it for type-level boolean equality would be much more natural.

That said, :=: could probably benefit from the relaxed rules for type operators; I just don't think == is a good choice.

Roman

...

-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,

* Richard Eisenberg [2013-09-29 00:10:46-0400] 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

...

...

> 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

wrote: 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/fb47f8368ad3d40fdd79bdeec334c... > > 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

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

-- Your ship was destroyed in a monadic eruption.