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

[Gábor Lehel]

On Sun, Sep 29, 2013 at 5:36 PM, Edward Kmett <ekmett at gmail.com> 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 <rhymoid at gmail.com>wrote:
>
>> What about (~~)?
>>
>>
>> On Sun, Sep 29, 2013 at 5:21 PM, Edward Kmett <ekmett at gmail.com> 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 <roma at ro-che.info>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
>>>>
>>>> * Richard Eisenberg <eir at cis.upenn.edu> [2013-09-29 00:10:46-0400]
>>>> > -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
>>>
>>>
>>
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
>


-- 
Your ship was destroyed in a monadic eruption.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130929/b617522e/attachment.html>