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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
30 messages Options
12
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
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:


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

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Shachaf Ben-Kiki
On Sat, Sep 28, 2013 at 6:57 PM, Edward Kmett <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
-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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Carter Schonwald
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 <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Sebastiaan Joosten
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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
~ is used for the equality witness itself as a constraint.


On Sun, Sep 29, 2013 at 7:25 AM, Sebastiaan Joosten <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Roman Cheplyaka-2
In reply to this post by Richard Eisenberg-2
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 <[hidden email]> [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 <[hidden email]> 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
> > [hidden email]
> > http://www.haskell.org/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
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 <[hidden email]> 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 <[hidden email]> [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 <[hidden email]> 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
> > [hidden email]
> > http://www.haskell.org/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Stijn van Drongelen
What about (~~)?


On Sun, Sep 29, 2013 at 5:21 PM, Edward Kmett <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> [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 <[hidden email]> 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
> > [hidden email]
> > http://www.haskell.org/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
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?

-Edward


On Sun, Sep 29, 2013 at 11:29 AM, Stijn van Drongelen <[hidden email]> wrote:
What about (~~)?


On Sun, Sep 29, 2013 at 5:21 PM, Edward Kmett <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> [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 <[hidden email]> 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
> > [hidden email]
> > http://www.haskell.org/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries




_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Gábor Lehel



On Sun, Sep 29, 2013 at 5:36 PM, Edward Kmett <[hidden email]> 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 <[hidden email]> wrote:
What about (~~)?


On Sun, Sep 29, 2013 at 5:21 PM, Edward Kmett <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> [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 <[hidden email]> 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
> > [hidden email]
> > http://www.haskell.org/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries




_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries




--
Your ship was destroyed in a monadic eruption.

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Erik Hesselink
In reply to this post by Roman Cheplyaka-2
I agree. I would expect (==) to be something like:

type family (x :: k) == (y :: k) :: Bool where
  a == a = True
  a == b = False

As for the equality witness type, I think there's nothing wrong with
(:=:). This way, it can also have the same name as the constructor,
which still has to start with a colon, as far as I know. (:~:) would
also be fine by me, but I don't think a name without colons is
desirable.

Erik

On Sun, Sep 29, 2013 at 2:33 PM, Roman Cheplyaka <[hidden email]> 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 <[hidden email]> [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 <[hidden email]> 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
>> > [hidden email]
>> > http://www.haskell.org/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/libraries
>
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Simon Peyton Jones
In a constraint
        f :: (a ~ b) => [a] -> [b]
the "~" is nominal type equality, not representational equality. The data type we are discussing is simply the value-level representation of this constraint.  Thus

        data a :=: b where
          Ref :: (a~b) => a :=: b

So perhaps a variant on "~" is called for, maybe :~:, to make that link stronger.

As Edward says, there is representational equality too, and we want both a constraint and a data type for it.  Currently the constraint looks like
        Coercible a b
but and the data type is currently called EqR.  Linking them more tightly could be a Good Thing. For example, we could hav
        a ~~ b
for the constraint and
        a :~~: b
for the data type.  I do not have strongly feelings; just pointing out the correspondences.

Simon

| -----Original Message-----
| From: Libraries [mailto:[hidden email]] On Behalf Of Erik
| Hesselink
| Sent: 29 September 2013 18:46
| To: Roman Cheplyaka
| Cc: Haskell Libraries
| Subject: Re: [Proposal] Renaming (:=:) to (==)
|
| I agree. I would expect (==) to be something like:
|
| type family (x :: k) == (y :: k) :: Bool where
|   a == a = True
|   a == b = False
|
| As for the equality witness type, I think there's nothing wrong with
| (:=:). This way, it can also have the same name as the constructor,
| which still has to start with a colon, as far as I know. (:~:) would
| also be fine by me, but I don't think a name without colons is
| desirable.
|
| Erik
|
| On Sun, Sep 29, 2013 at 2:33 PM, Roman Cheplyaka <[hidden email]>
| 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 <[hidden email]> [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 <[hidden email]>
| 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
| >> > [hidden email]
| >> > http://www.haskell.org/mailman/listinfo/libraries
| >>
| >> _______________________________________________
| >> Libraries mailing list
| >> [hidden email]
| >> http://www.haskell.org/mailman/listinfo/libraries
| >
| > _______________________________________________
| > Libraries mailing list
| > [hidden email]
| > http://www.haskell.org/mailman/listinfo/libraries
| >
| _______________________________________________
| Libraries mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Gábor Lehel
On Sun, Sep 29, 2013 at 10:33 PM, Simon Peyton-Jones <[hidden email]> wrote:
As Edward says, there is representational equality too, and we want both a constraint and a data type for it.  Currently the constraint looks like
        Coercible a b
but and the data type is currently called EqR.  Linking them more tightly could be a Good Thing. For example, we could hav
        a ~~ b
for the constraint and
        a :~~: b
for the data type.  I do not have strongly feelings; just pointing out the correspondences.

Simon

I think `Coercible` and `coerce` (along with `unsafeCoerce`) are perfect as they are. Not everything has to be an operator. Things with names are self-documenting, which is good. For something that's going to show up very frequently, it makes sense to use an operator, because (a) by showing up very frequently, it becomes common knowledge, and (b) it's shorter. I think this is true for (~). If something shows up only occasionally, I think it makes more sense to use a name, because (a) widespread familiarity can't be assumed, and (b) brevity is less important. I think this is true for `Coercible`.

Of course, this doesn't answer the question of what to call the data type. :-) I don't have any great ideas. (Coerce? CanCoerce? IsCoercible?)

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
As an aside now that the conversation has drifted to the discussion of a data type for representational equivalence:

One of the things I was chasing after with Iavor, Richard, and Simon about at ICFP was how we can upgrade Coercible so that it can compose better. 

Currently you cannot derive Coercible a b from Coercible b a, and Coercible a b and Coercible b c do not entail Coercible a c. This means it isn't possible to compose these witnesses 'horizontally' at present. e.g. if we were to try to write say Data.Type.Equality.Representational, we could not (at present) write anything like the current combinators in Data.Type.Equality even just starting with the Category for composition.

I fully favor keeping coerce simple and just possibly upgrading the composition of Coercible or the internal witness ~R# that sits under Coercible so that we can write these compositions.

The first attempt at upgrading Coercible made it seem like perhaps the right path forward was to do more with the ~R#, at which point having two names at the constraint level seems to be problematic. We know how to upgrade the composition of ~R#, but Coercible as currently built is harder.

That however is probably a separate discussion about

a.) how to actually finish fixing things up so that they can compose better and 
b.) if we can do it without affecting the API we provide to the end user.

-Edward



On Sun, Sep 29, 2013 at 4:59 PM, Gábor Lehel <[hidden email]> wrote:
On Sun, Sep 29, 2013 at 10:33 PM, Simon Peyton-Jones <[hidden email]> wrote:
As Edward says, there is representational equality too, and we want both a constraint and a data type for it.  Currently the constraint looks like
        Coercible a b
but and the data type is currently called EqR.  Linking them more tightly could be a Good Thing. For example, we could hav
        a ~~ b
for the constraint and
        a :~~: b
for the data type.  I do not have strongly feelings; just pointing out the correspondences.

Simon

I think `Coercible` and `coerce` (along with `unsafeCoerce`) are perfect as they are. Not everything has to be an operator. Things with names are self-documenting, which is good. For something that's going to show up very frequently, it makes sense to use an operator, because (a) by showing up very frequently, it becomes common knowledge, and (b) it's shorter. I think this is true for (~). If something shows up only occasionally, I think it makes more sense to use a name, because (a) widespread familiarity can't be assumed, and (b) brevity is less important. I think this is true for `Coercible`.

Of course, this doesn't answer the question of what to call the data type. :-) I don't have any great ideas. (Coerce? CanCoerce? IsCoercible?)

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Conal Elliott
In reply to this post by Edward Kmett-2
-1.

I'm hoping we don't get more deeply invested in the syntactic change in GHC 7.6 that removed the possibility of symbolic type variables ("~>", "*", "+", etc). I had a new job and wasn't paying attention when SPJ polled the community. From my perspective, the loss has much greater scope than the gain for type level naturals. I'd like to keep the door open to the possibility of bringing back the old notation with the help of a language pragma. It would take a few of us to draft a proposal addressing details.

Not at all meaning to start a syntax debate on this thread. Just an explanation of my -1 for the topic at hand.

- Conal

-- Conal


On Sat, Sep 28, 2013 at 9:57 PM, Edward Kmett <[hidden email]> 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:


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

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
I think if someone went through the effort of writing a patch so you could at least introduce local operator names with an explicit forall, like with ScopedTypeVariables and the proposed explicit type applications then it'd probably be accepted.

Sent from my iPhone

On Sep 30, 2013, at 2:25 PM, Conal Elliott <[hidden email]> wrote:

-1.

I'm hoping we don't get more deeply invested in the syntactic change in GHC 7.6 that removed the possibility of symbolic type variables ("~>", "*", "+", etc). I had a new job and wasn't paying attention when SPJ polled the community. From my perspective, the loss has much greater scope than the gain for type level naturals. I'd like to keep the door open to the possibility of bringing back the old notation with the help of a language pragma. It would take a few of us to draft a proposal addressing details.

Not at all meaning to start a syntax debate on this thread. Just an explanation of my -1 for the topic at hand.

- Conal

-- Conal


On Sat, Sep 28, 2013 at 9:57 PM, Edward Kmett <[hidden email]> 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:


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

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Carter Schonwald
Agreed. 

On Monday, September 30, 2013, Edward A Kmett wrote:
I think if someone went through the effort of writing a patch so you could at least introduce local operator names with an explicit forall, like with ScopedTypeVariables and the proposed explicit type applications then it'd probably be accepted.

Sent from my iPhone

On Sep 30, 2013, at 2:25 PM, Conal Elliott <<a href="javascript:_e({}, &#39;cvml&#39;, &#39;conal@conal.net&#39;);" target="_blank">conal@...> wrote:

-1.

I'm hoping we don't get more deeply invested in the syntactic change in GHC 7.6 that removed the possibility of symbolic type variables ("~>", "*", "+", etc). I had a new job and wasn't paying attention when SPJ polled the community. From my perspective, the loss has much greater scope than the gain for type level naturals. I'd like to keep the door open to the possibility of bringing back the old notation with the help of a language pragma. It would take a few of us to draft a proposal addressing details.

Not at all meaning to start a syntax debate on this thread. Just an explanation of my -1 for the topic at hand.

- Conal

-- Conal


On Sat, Sep 28, 2013 at 9:57 PM, Edward Kmett <<a href="javascript:_e({}, &#39;cvml&#39;, &#39;ekmett@gmail.com&#39;);" target="_blank">ekmett@...> 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:


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

_______________________________________________
Libraries mailing list
<a href="javascript:_e({}, &#39;cvml&#39;, &#39;Libraries@haskell.org&#39;);" target="_blank">Libraries@...
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
GHC.TypeLits code looks to be using (<=?) as the boolean valued version of the predicate and (<=) for the assertion.

This points to a coming disagreement over style across the different parts of GHC itself, if we're saying that the principle reason for not using (==) is that we want it to be the boolean valued version.

-Edward


On Mon, Sep 30, 2013 at 4:03 PM, Carter Schonwald <[hidden email]> wrote:
Agreed. 


On Monday, September 30, 2013, Edward A Kmett wrote:
I think if someone went through the effort of writing a patch so you could at least introduce local operator names with an explicit forall, like with ScopedTypeVariables and the proposed explicit type applications then it'd probably be accepted.

Sent from my iPhone

On Sep 30, 2013, at 2:25 PM, Conal Elliott <[hidden email]> wrote:

-1.

I'm hoping we don't get more deeply invested in the syntactic change in GHC 7.6 that removed the possibility of symbolic type variables ("~>", "*", "+", etc). I had a new job and wasn't paying attention when SPJ polled the community. From my perspective, the loss has much greater scope than the gain for type level naturals. I'd like to keep the door open to the possibility of bringing back the old notation with the help of a language pragma. It would take a few of us to draft a proposal addressing details.

Not at all meaning to start a syntax debate on this thread. Just an explanation of my -1 for the topic at hand.

- Conal

-- Conal


On Sat, Sep 28, 2013 at 9:57 PM, Edward Kmett <[hidden email]> 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:


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

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries




_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-2
Thanks for pointing this out, Edward. I think consistency within the type level is more important than consistency between the type level and the term level. So, if we settle on a convention that a symbol ending in `?` means Boolean-valued and other symbols mean constraints, I'm all for making the change to (==).

I'm not aware of a wide poll on the names in TypeLits, so we shouldn't necessarily just follow that lead. That said, the above proposal about `?` seems sensible to me. If we decide to do this, we should find somewhere (where??) to articulate this.

Richard 

On Oct 2, 2013, at 9:28 PM, Edward Kmett <[hidden email]> wrote:

GHC.TypeLits code looks to be using (<=?) as the boolean valued version of the predicate and (<=) for the assertion.

This points to a coming disagreement over style across the different parts of GHC itself, if we're saying that the principle reason for not using (==) is that we want it to be the boolean valued version.

-Edward


On Mon, Sep 30, 2013 at 4:03 PM, Carter Schonwald <[hidden email]> wrote:
Agreed. 


On Monday, September 30, 2013, Edward A Kmett wrote:
I think if someone went through the effort of writing a patch so you could at least introduce local operator names with an explicit forall, like with ScopedTypeVariables and the proposed explicit type applications then it'd probably be accepted.

Sent from my iPhone

On Sep 30, 2013, at 2:25 PM, Conal Elliott <[hidden email]> wrote:

-1.

I'm hoping we don't get more deeply invested in the syntactic change in GHC 7.6 that removed the possibility of symbolic type variables ("~>", "*", "+", etc). I had a new job and wasn't paying attention when SPJ polled the community. From my perspective, the loss has much greater scope than the gain for type level naturals. I'd like to keep the door open to the possibility of bringing back the old notation with the help of a language pragma. It would take a few of us to draft a proposal addressing details.

Not at all meaning to start a syntax debate on this thread. Just an explanation of my -1 for the topic at hand.

- Conal

-- Conal


On Sat, Sep 28, 2013 at 9:57 PM, Edward Kmett <[hidden email]> 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:


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

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
12