Edward Kmett | 29 Sep 03:57 2013
Picon

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

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
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Shachaf Ben-Kiki | 29 Sep 04:08 2013
Picon

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

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
Richard Eisenberg | 29 Sep 06:10 2013

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

-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
Carter Schonwald | 29 Sep 07:21 2013
Picon

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

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
Sebastiaan Joosten | 29 Sep 13:25 2013
Picon

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

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
Edward Kmett | 29 Sep 14:11 2013
Picon

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

~ 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


_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Roman Cheplyaka | 29 Sep 14:33 2013

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

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
Edward Kmett | 29 Sep 17:21 2013
Picon

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

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
Stijn van Drongelen | 29 Sep 17:29 2013
Picon

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

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
Edward Kmett | 29 Sep 17:36 2013
Picon

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

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 <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
Gábor Lehel | 29 Sep 18:22 2013
Picon

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




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.
_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Erik Hesselink | 29 Sep 19:46 2013
Picon

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 <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
>
Simon Peyton-Jones | 29 Sep 22:33 2013
Picon

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

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:libraries-bounces <at> haskell.org] 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 <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
Gábor Lehel | 29 Sep 22:59 2013
Picon

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

On Sun, Sep 29, 2013 at 10:33 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> 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
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Edward Kmett | 29 Sep 23:29 2013
Picon

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

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 <illissius <at> gmail.com> wrote:
On Sun, Sep 29, 2013 at 10:33 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> 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
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
Conal Elliott | 30 Sep 20:25 2013
Picon

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

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


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
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
Edward A Kmett | 30 Sep 21:05 2013
Picon

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

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 <conal <at> conal.net> 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 <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:


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
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
Carter Schonwald | 30 Sep 22:03 2013
Picon

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

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 <conal <at> conal.net> 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 <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:


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
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
Edward Kmett | 3 Oct 03:28 2013
Picon

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

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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:


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
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
Richard Eisenberg | 3 Oct 05:07 2013

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

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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:


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
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
Simon Peyton-Jones | 3 Oct 10:10 2013
Picon

RE: [Proposal] Renaming (:=:) 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.

 

Negotiating names is not much fun, but they stay with us for a long time.  And Richard, might you find 20 mins to throw up a wiki page (on the GHC Trac or Haskell wiki, doesn’t matter too much) giving the exported signature of TypeLits and related modules (singletons?), together with a summary of the main open naming issues?  Should be mainly cut-and-paste.  That would be really helpful.

 

Simon

 

From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 03 October 2013 04:07
To: Edward Kmett
Cc: Haskell Libraries
Subject: Re: [Proposal] Renaming (:=:) to (==)

 

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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:

 

 

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
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
Simon Peyton-Jones | 3 Oct 10:16 2013
Picon

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

PS: on the specifics of (:=:) vs (==), I am alive to the fact that all these different sorts of equality are quite confusing to our poor programmers.  We might have

 

                f :: (a~b) => (c == d) -> blah

 

where the (a~b) is an implicitly-passed witness and the (c == d) is an explicitly-passed one.  But both witness the same sort of equality.  There seems to be a reasonable case for making them look related.  Currently I lean towards (:~:) thus

 

                f :: (a~b) => (c :~: d) -> blah

 

Simon

 

From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Simon Peyton-Jones
Sent: 03 October 2013 09:10
To: Richard Eisenberg; Edward Kmett
Cc: Haskell Libraries
Subject: RE: [Proposal] Renaming (:=:) 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.

 

Negotiating names is not much fun, but they stay with us for a long time.  And Richard, might you find 20 mins to throw up a wiki page (on the GHC Trac or Haskell wiki, doesn’t matter too much) giving the exported signature of TypeLits and related modules (singletons?), together with a summary of the main open naming issues?  Should be mainly cut-and-paste.  That would be really helpful.

 

Simon

 

From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 03 October 2013 04:07
To: Edward Kmett
Cc: Haskell Libraries
Subject: Re: [Proposal] Renaming (:=:) to (==)

 

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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:

 

 

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
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
Edward Kmett | 4 Oct 21:30 2013
Picon

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

The main concern that I would have with the (:~:) notation is that it doesn't extend well, and doesn't fit existing practice elsewhere.

TypeLits is already also using (<=), etc. That follows pretty common practice in languages like Agda of using (<=), (==), (>=) as the type of proofs of equality. It'd be a shame to eventually wind up with a second (==) out of there crippled to only work with Nat, or to wind up with everything but (==), which then switches to a very different notation.

-Edward

P.S. In Agda they of accommodate a stronger notion of the Bool-valued equalities by using ?'s overhead when they want to talk about the Dec-based versions that correspond to the (<=?) in TypeLits, that carry proof of the equality or proof that the equality is unsatisfiable. Carrying the proof lets them avoid Boolean Blindness, and lets you actually compute with the result. That said, even if we later decided we wanted to upgrade (==?) to carry witnesses I think we should skip the unicode. ;) 

On Thu, Oct 3, 2013 at 4:16 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

PS: on the specifics of (:=:) vs (==), I am alive to the fact that all these different sorts of equality are quite confusing to our poor programmers.  We might have

 

                f :: (a~b) => (c == d) -> blah

 

where the (a~b) is an implicitly-passed witness and the (c == d) is an explicitly-passed one.  But both witness the same sort of equality.  There seems to be a reasonable case for making them look related.  Currently I lean towards (:~:) thus

 

                f :: (a~b) => (c :~: d) -> blah

 

Simon

 

From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Simon Peyton-Jones
Sent: 03 October 2013 09:10
To: Richard Eisenberg; Edward Kmett
Cc: Haskell Libraries
Subject: RE: [Proposal] Renaming (:=:) 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.

 

Negotiating names is not much fun, but they stay with us for a long time.  And Richard, might you find 20 mins to throw up a wiki page (on the GHC Trac or Haskell wiki, doesn’t matter too much) giving the exported signature of TypeLits and related modules (singletons?), together with a summary of the main open naming issues?  Should be mainly cut-and-paste.  That would be really helpful.

 

Simon

 

From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 03 October 2013 04:07
To: Edward Kmett
Cc: Haskell Libraries
Subject: Re: [Proposal] Renaming (:=:) to (==)

 

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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:

 

 

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
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
Richard Eisenberg | 11 Oct 21:03 2013

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

I've done this (summarizing the issues discussed in this thread) and posted at

The color on the bikeshed may only be cosmetic, but we (and others) will be looking at it for a long time. And, besides, I imagine many Haskellers are aesthetes at heart. What else drew us to such a beautiful language? :)

Thanks,
Richard

On Oct 3, 2013, at 4:10 AM, Simon Peyton-Jones wrote:

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.

 

Negotiating names is not much fun, but they stay with us for a long time.  And Richard, might you find 20 mins to throw up a wiki page (on the GHC Trac or Haskell wiki, doesn’t matter too much) giving the exported signature of TypeLits and related modules (singletons?), together with a summary of the main open naming issues?  Should be mainly cut-and-paste.  That would be really helpful.

 

Simon

 

From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 03 October 2013 04:07
To: Edward Kmett
Cc: Haskell Libraries
Subject: Re: [Proposal] Renaming (:=:) to (==)

 

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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:

 

 

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
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
Edward Kmett | 11 Oct 21:54 2013
Picon

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

On Fri, Oct 11, 2013 at 3:03 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
I've done this (summarizing the issues discussed in this thread) and posted at

The color on the bikeshed may only be cosmetic, but we (and others) will be looking at it for a long time. And, besides, I imagine many Haskellers are aesthetes at heart. What else drew us to such a beautiful language? :)


Thoughts on my first reading:

Re Sym in Data.Type.Coercion:

Sym shouldn't be (and at last check wasn't) exported by Data.Type.Coercion. 
It is only used to implement 

sym :: Coercion a b -> Coercion b a

internally. It does so by using the supplied Coercion to coerce Sym a a into Sym a b and unwrapping it to get Coercion b a. 

This is an adaptation of the pretty standard standard trick for implementing sym with Leibnizian equality.

Similarly `trans` / (.) are implementing by using coerce on a Coercion, since its arguments are representational.

This lets us get away with using Coercible directly as it stands, and still gives us the right groupoid structure for the witness.

Simon's suggestion of castWith sounds fine to me, and is much nicer than subst.

Re: The need for SomeNat and SomeSymbol

They are currently impossible to implement without using very deep voodoo. See the magicSingIId note.
 
If we bring in GHC.Reflection. (I've almost finished a patch for it, my only remaining hangups are in the wiredIn itself) then the code in GHC.TypeLits for KnownNat and KnownSymbol can go away, and those two definitions can use reflection internally.

We'd pick up

module GHC.Reflection
  ( Reifying(..)
  , reify#
  ) where

import GHC.Prim (Proxy#, proxy#, unsafeCoerce#)

class Reifying s where
  type Reified s :: *
  -- | Recover a reified value.
  reflect# :: Proxy# s -> Reified s

-- wiredIn
reify# :: forall k a r. a -> (forall (s :: k). (Reifying s, Reified s ~ a) => Proxy# s -> r) -> r

Then the current instances for KnownNat and KnownSymbol become the substantially identical actual instances we currently have for them in the reflection package:

-- | This instance gives the integer associated with a type-level natural.
-- There are instances for every concrete literal: 0, 1, 2, etc.
instance SingI n => Reifying (n :: Nat) where
  type Reified n = Integer
  reflect# _ = case sing :: Sing n of
    SNat x -> x

-- | This instance gives the string associated with a type-level symbol.
-- There are instances for every concrete literal: "hello", etc.
instance SingI n => Reifying (n :: Symbol) where
  type Reified (n :: Symbol) = String
  reflect# _ = case sing :: Sing n of
    SSym x -> x

Those classes can melt away and disappear and internally the implementation of someNatVal, and someSymbolVal become much less horrific:

-- | This type represents unknown type-level natural numbers.
data SomeNat = forall (n :: Nat). Reifying n => SomeNat (Proxy# n)

-- | This type represents unknown type-level symbols.
data SomeSymbol = forall (n :: Symbol). Reifying n => SomeSymbol (Proxy# n)

-- | Convert an integer into an unknown type-level natural.
someNatVal :: Integer -> Maybe SomeNat
someNatVal n
  | n >= 0 = Just (reify# n SomeNat)
  | otherwise = Nothing

-- | Convert a string into an unknown type-level symbol.
someSymbolVal :: String -> SomeSymbol
someSymbolVal n = reify# n SomeSymbol

The combinators then can just use reflect#. 

instance Eq SomeNat where
  SomeNat x == SomeNat y = reflect# x == reflect# y

instance Ord SomeNat where
  compare (SomeNat x) (SomeNat y) = compare (reflect# x) (reflect# y)

instance Show SomeNat where
  showsPrec p (SomeNat x) = showsPrec p (reflect# x)

This minimalist version of GHC.Reflection seems to actually result in a net reduction in the amount of code. It also makes both of those types candidates for moving out, as they don't rely on a terrifying builtin with a fake type.

-Edward

On Oct 3, 2013, at 4:10 AM, Simon Peyton-Jones wrote:

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.
 
Negotiating names is not much fun, but they stay with us for a long time.  And Richard, might you find 20 mins to throw up a wiki page (on the GHC Trac or Haskell wiki, doesn’t matter too much) giving the exported signature of TypeLits and related modules (singletons?), together with a summary of the main open naming issues?  Should be mainly cut-and-paste.  That would be really helpful.
 
Simon
 
From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 03 October 2013 04:07
To: Edward Kmett
Cc: Haskell Libraries
Subject: Re: [Proposal] Renaming (:=:) to (==)
 
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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:
 
 
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
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
Edward Kmett | 11 Oct 22:12 2013
Picon

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

Dan just asked me what unsafeCoerce# was doing in the GHC.Reflection imports above. unsafeCoerce# was only imported there while I was testing this as a base only change to make sure I had the API right before I started switching over to the wiredIn. 

That won't be there in the final product.

-Edward


On Fri, Oct 11, 2013 at 3:54 PM, Edward Kmett <ekmett <at> gmail.com> wrote:
On Fri, Oct 11, 2013 at 3:03 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:

I've done this (summarizing the issues discussed in this thread) and posted at

The color on the bikeshed may only be cosmetic, but we (and others) will be looking at it for a long time. And, besides, I imagine many Haskellers are aesthetes at heart. What else drew us to such a beautiful language? :)


Thoughts on my first reading:

Re Sym in Data.Type.Coercion:

Sym shouldn't be (and at last check wasn't) exported by Data.Type.Coercion. 
It is only used to implement 

sym :: Coercion a b -> Coercion b a

internally. It does so by using the supplied Coercion to coerce Sym a a into Sym a b and unwrapping it to get Coercion b a. 

This is an adaptation of the pretty standard standard trick for implementing sym with Leibnizian equality.

Similarly `trans` / (.) are implementing by using coerce on a Coercion, since its arguments are representational.

This lets us get away with using Coercible directly as it stands, and still gives us the right groupoid structure for the witness.

Simon's suggestion of castWith sounds fine to me, and is much nicer than subst.

Re: The need for SomeNat and SomeSymbol

They are currently impossible to implement without using very deep voodoo. See the magicSingIId note.
 
If we bring in GHC.Reflection. (I've almost finished a patch for it, my only remaining hangups are in the wiredIn itself) then the code in GHC.TypeLits for KnownNat and KnownSymbol can go away, and those two definitions can use reflection internally.

We'd pick up

module GHC.Reflection
  ( Reifying(..)
  , reify#
  ) where

import GHC.Prim (Proxy#, proxy#, unsafeCoerce#)

class Reifying s where
  type Reified s :: *
  -- | Recover a reified value.
  reflect# :: Proxy# s -> Reified s

-- wiredIn
reify# :: forall k a r. a -> (forall (s :: k). (Reifying s, Reified s ~ a) => Proxy# s -> r) -> r

Then the current instances for KnownNat and KnownSymbol become the substantially identical actual instances we currently have for them in the reflection package:

-- | This instance gives the integer associated with a type-level natural.
-- There are instances for every concrete literal: 0, 1, 2, etc.
instance SingI n => Reifying (n :: Nat) where
  type Reified n = Integer
  reflect# _ = case sing :: Sing n of
    SNat x -> x

-- | This instance gives the string associated with a type-level symbol.
-- There are instances for every concrete literal: "hello", etc.
instance SingI n => Reifying (n :: Symbol) where
  type Reified (n :: Symbol) = String
  reflect# _ = case sing :: Sing n of
    SSym x -> x

Those classes can melt away and disappear and internally the implementation of someNatVal, and someSymbolVal become much less horrific:

-- | This type represents unknown type-level natural numbers.
data SomeNat = forall (n :: Nat). Reifying n => SomeNat (Proxy# n)

-- | This type represents unknown type-level symbols.
data SomeSymbol = forall (n :: Symbol). Reifying n => SomeSymbol (Proxy# n)

-- | Convert an integer into an unknown type-level natural.
someNatVal :: Integer -> Maybe SomeNat
someNatVal n
  | n >= 0 = Just (reify# n SomeNat)
  | otherwise = Nothing

-- | Convert a string into an unknown type-level symbol.
someSymbolVal :: String -> SomeSymbol
someSymbolVal n = reify# n SomeSymbol

The combinators then can just use reflect#. 

instance Eq SomeNat where
  SomeNat x == SomeNat y = reflect# x == reflect# y

instance Ord SomeNat where
  compare (SomeNat x) (SomeNat y) = compare (reflect# x) (reflect# y)

instance Show SomeNat where
  showsPrec p (SomeNat x) = showsPrec p (reflect# x)

This minimalist version of GHC.Reflection seems to actually result in a net reduction in the amount of code. It also makes both of those types candidates for moving out, as they don't rely on a terrifying builtin with a fake type.

-Edward

On Oct 3, 2013, at 4:10 AM, Simon Peyton-Jones wrote:

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.
 
Negotiating names is not much fun, but they stay with us for a long time.  And Richard, might you find 20 mins to throw up a wiki page (on the GHC Trac or Haskell wiki, doesn’t matter too much) giving the exported signature of TypeLits and related modules (singletons?), together with a summary of the main open naming issues?  Should be mainly cut-and-paste.  That would be really helpful.
 
Simon
 
From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 03 October 2013 04:07
To: Edward Kmett
Cc: Haskell Libraries
Subject: Re: [Proposal] Renaming (:=:) to (==)
 
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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:
 
 
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
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
Richard Eisenberg | 12 Oct 04:58 2013

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


On Oct 11, 2013, at 3:54 PM, Edward Kmett wrote:


Re Sym in Data.Type.Coercion:

Sym shouldn't be (and at last check wasn't) exported by Data.Type.Coercion. 
It is only used to implement 

Right -- of course.


Simon's suggestion of castWith sounds fine to me, and is much nicer than subst.

Given the various murmurs in agreement here, I'm going to go ahead and just make this change.


Re: The need for SomeNat and SomeSymbol

They are currently impossible to implement without using very deep voodoo. See the magicSingIId note.

Right -- of course.

Thanks for answering my (stupid) questions!
Richard

 

On Oct 3, 2013, at 4:10 AM, Simon Peyton-Jones wrote:

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.
 
Negotiating names is not much fun, but they stay with us for a long time.  And Richard, might you find 20 mins to throw up a wiki page (on the GHC Trac or Haskell wiki, doesn’t matter too much) giving the exported signature of TypeLits and related modules (singletons?), together with a summary of the main open naming issues?  Should be mainly cut-and-paste.  That would be really helpful.
 
Simon
 
From: Libraries [mailto:libraries-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 03 October 2013 04:07
To: Edward Kmett
Cc: Haskell Libraries
Subject: Re: [Proposal] Renaming (:=:) to (==)
 
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 <ekmett <at> gmail.com> 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 <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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:
 
 
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
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
Iavor Diatchki | 12 Oct 07:29 2013
Picon

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

Hello,

I am not sure what version of GHC.TypeLits you looked at, but as of the other day the code in there is almost the same as what you propose (except for the use of different classes).

On Fri, Oct 11, 2013 at 12:54 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

They are currently impossible to implement without using very deep voodoo. See the magicSingIId note.

The `magicSingI` has been redone and is quite a bit simpler now.  Note [magicDictId magic] describes the current approach. Still, if we can think of a way to get rid of it, I'm strongly in support.
 
 
If we bring in GHC.Reflection. (I've almost finished a patch for it, my only remaining hangups are in the wiredIn itself) then the code in GHC.TypeLits for KnownNat and KnownSymbol can go away, and those two definitions can use reflection internally.


`KnowNat` and `KnownSymbol` are the basic classes that provide the built-in instances for type-level literals (SingI is gone).  I don't see any way around having some built-in code like that.  


 
Then the current instances for KnownNat and KnownSymbol become the substantially identical actual instances we currently have for them in the reflection package:

-- | This instance gives the integer associated with a type-level natural.
-- There are instances for every concrete literal: 0, 1, 2, etc.
instance SingI n => Reifying (n :: Nat) where
  type Reified n = Integer
  reflect# _ = case sing :: Sing n of
    SNat x -> x

Indeend, `natVal` is implemented almost exactly like this.  It'd be trivial to provide an instance for the `Reify` class if we needed to:

  instance KnowNat n => Reifying (n :: Nat) where type Reified n = Integer; reflect# = natVal


Those classes can melt away and disappear

Do you mean by providing built-in instances for `Reify` instead? If so, this is mostly a renaming, and I am not so keen on making the change as I like the simplicity of `KnownSym` and `KnownNat`.  Also---and this is an implementation detail---their dictionaries are simpler than the one for `Reify`: they just carry around the actual value, integer or string, while the dictionaries for `Reify` have to store a whole function.  I think this matters when you package them in existentials, no?


 
and internally the implementation of someNatVal, and someSymbolVal become much less horrific:

-- | This type represents unknown type-level natural numbers.
data SomeNat = forall (n :: Nat). Reifying n => SomeNat (Proxy# n)


-- | Convert an integer into an unknown type-level natural.
someNatVal :: Integer -> Maybe SomeNat
someNatVal n
  | n >= 0 = Just (reify# n SomeNat)
  | otherwise = Nothing

Well, the current implementation is almost exactly this! I don't really know how `reify#` is supposed to work, but it certainly seems to do something very similar to what `magicDict` does, so we should probably make sure that there is only one implementation.  I would guess that you can use `magicDict` to implement `reify#`.  The other way around would also be OK with me as long as I don't have to use the `Reify` class, and can use directly the simpler (no type functions, no kind polymorphism) `KnownSymbol` and `KnownNat` classes.

Also, doesn't `reify#` introduce a coherence issue?  `someNatVal` and the instances for `KnownNat` are carefully engineered to provide a consistent view to the programmer, but as far as understand, this is not the case with `Reifying`.  For example, consider the following code:

data {- kind -} K

instance Reifying (a :: K) where
  type Reified a = Integer
  reflect# _ = 5

getK :: Reifying a => Proxy (a :: K) -> Integer
getK = reflect#

test :: Integer
test = reify# 6 getK

It is not at all obvious if `test` should evaluate 5 (using the global instance) or 6 (using the locally supplied evidence), and the choice seems highly dependent on the mood of the constraint solver.

-Iavor







_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Edward Kmett | 12 Oct 20:22 2013
Picon

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

On Sat, Oct 12, 2013 at 1:29 AM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:
Hello,

I am not sure what version of GHC.TypeLits you looked at, but as of the other day the code in there is almost the same as what you propose (except for the use of different classes).

My copy of the code was a couple of days out of date, from when I started the patch. 

On Fri, Oct 11, 2013 at 12:54 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

They are currently impossible to implement without using very deep voodoo. See the magicSingIId note.

The `magicSingI` has been redone and is quite a bit simpler now.  Note [magicDictId magic] describes the current approach. Still, if we can think of a way to get rid of it, I'm strongly in support.
 
If we bring in GHC.Reflection. (I've almost finished a patch for it, my only remaining hangups are in the wiredIn itself) then the code in GHC.TypeLits for KnownNat and KnownSymbol can go away, and those two definitions can use reflection internally.
 
`KnowNat` and `KnownSymbol` are the basic classes that provide the built-in instances for type-level literals (SingI is gone).  I don't see any way around having some built-in code like that.  

Indeend, `natVal` is implemented almost exactly like this.  It'd be trivial to provide an instance for the `Reify` class if we needed to:

  instance KnowNat n => Reifying (n :: Nat) where type Reified n = Integer; reflect# = natVal

If those are the classes being generated now, then I can use that to generate the instances for Reifying at those kinds.
 
Those classes can melt away and disappear

Do you mean by providing built-in instances for `Reify` instead? If so, this is mostly a renaming, and I am not so keen on making the change as I like the simplicity of `KnownSym` and `KnownNat`.  Also---and this is an implementation detail---their dictionaries are simpler than the one for `Reify`: they just carry around the actual value, integer or string, while the dictionaries for `Reify` have to store a whole function.  I think this matters when you package them in existentials, no?

The instance for Reifying holds a function from Proxy# a which is of unlifted kind and has no representation. Behind the scenes they should look substantially identical. 

Using something like the Tagged newtype could make them definitely identical behind the scenes.

I'm okay with leaving them as it is. I mostly was noting that if we did consolidate then we'd get a slight code reduction. 
 
and internally the implementation of someNatVal, and someSymbolVal become much less horrific:
-- | This type represents unknown type-level natural numbers.
data SomeNat = forall (n :: Nat). Reifying n => SomeNat (Proxy# n)

-- | Convert an integer into an unknown type-level natural.
someNatVal :: Integer -> Maybe SomeNat
someNatVal n
  | n >= 0 = Just (reify# n SomeNat)
  | otherwise = Nothing

Well, the current implementation is almost exactly this! I don't really know how `reify#` is supposed to work, but it certainly seems to do something very similar to what `magicDict` does, so we should probably make sure that there is only one implementation.  I would guess that you can use `magicDict` to implement `reify#`.  The other way around would also be OK with me as long as I don't have to use the `Reify` class, and can use directly the simpler (no type functions, no kind polymorphism) `KnownSymbol` and `KnownNat` classes. 
 
In core, stripping away the newtypes and coercions reify# winds up looking like

reify a k = k (\_ -> a) proxy#

The lambda there is ignoring a Proxy#, which is an unlifted argument without representation, and the proxy# argument at the end is similar.

Also, doesn't `reify#` introduce a coherence issue?  `someNatVal` and the instances for `KnownNat` are carefully engineered to provide a consistent view to the programmer, but as far as understand, this is not the case with `Reifying`.  For example, consider the following code:

data {- kind -} K

instance Reifying (a :: K) where
  type Reified a = Integer
  reflect# _ = 5

getK :: Reifying a => Proxy (a :: K) -> Integer
getK = reflect#

test :: Integer
test = reify# 6 getK

It is not at all obvious if `test` should evaluate 5 (using the global instance) or 6 (using the locally supplied evidence), and the choice seems highly dependent on the mood of the constraint solver.

Fair point. I was attempting to generalize reify# to allow it to instantiate at kinds other than *, to enable it to subsume your existing usecase. 

When restricted to * there isn't a coherence issue, as there is no such overarching instance, but also simply by providing any concrete instance of Reifying under kind * means that any attempt by the user to define such an instance Reifying (a :: *) would overlap, preventing this conflict.

I'll go back to the simpler version of reify#, which doesn't attempt to let you reify at other kinds, and leave TypeLits alone.

This simplifies my task considerably.

-Edward

_______________________________________________
Libraries mailing list
Libraries <at> haskell.org
http://www.haskell.org/mailman/listinfo/libraries
Erik Hesselink | 3 Oct 10:53 2013
Picon

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

I still think there's a case to be made for having type and value
level functions have the same name. We'll already have things like (+)
have the same name on both levels. It might be confusing if other
things don't have the same name on both levels.

Erik

On Thu, Oct 3, 2013 at 5:07 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
> 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 <ekmett <at> gmail.com> 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
> <carter.schonwald <at> gmail.com> 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 <conal <at> conal.net> 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 <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
>>>>
>>>> _______________________________________________
>>>> 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
>

Gmane