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

Thoughts?

Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.

Discussion Period: 1 week

-Edward Kmett

+1. For what it's worth, I suggested that name before, and Richard Eisenberg suggested that == should be for type-level Boolean equality: http://markmail.org/message/3yifytgt2k3cfwws. I'm not convinced, though -- this seems fundamental enough to deserve the simplest name possible.

(I'm using that link because the haskell.org mailing list archive seems to be gone... Hopefully that comes back, eventually.)

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

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

Thoughts?

Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.

Discussion Period: 1 week

-Edward Kmett

+1. For what it's worth, I suggested that name before, and Richard Eisenberg suggested that == should be for type-level Boolean equality: http://markmail.org/message/3yifytgt2k3cfwws. I'm not convinced, though -- this seems fundamental enough to deserve the simplest name possible.

(I'm using that link because the haskell.org mailing list archive seems to be gone... Hopefully that comes back, eventually.)

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

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

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

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 [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 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/fb47f8368ad3d40fdd79bdeec334c...

Thoughts?

Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.

Discussion Period: 1 week

-Edward Kmett

+1. For what it's worth, I suggested that name before, and Richard Eisenberg suggested that == should be for type-level Boolean equality: http://markmail.org/message/3yifytgt2k3cfwws. I'm not convinced, though -- this seems fundamental enough to deserve the simplest name possible.

(I'm using that link because the haskell.org mailing list archive seems to be gone... Hopefully that comes back, eventually.)

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

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

What about (~~)? On Sun, Sep 29, 2013 at 5:21 PM, Edward Kmett wrote:

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

I just rather dislike (:=:).

Lets throwing this open to bikeshedding. Alternatives?

-Edward

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

...

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

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

Roman

* Richard Eisenberg [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 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/fb47f8368ad3d40fdd79bdeec334c...

...

Thoughts?

Normally, I'd let this run the usual 2 week course, but we're

getting down

...

to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.

Discussion Period: 1 week

-Edward Kmett

+1. For what it's worth, I suggested that name before, and Richard Eisenberg suggested that == should be for type-level Boolean equality: http://markmail.org/message/3yifytgt2k3cfwws. I'm not convinced, though -- this seems fundamental enough to deserve the simplest name possible.

(I'm using that link because the haskell.org mailing list archive seems to be gone... Hopefully that comes back, eventually.)

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

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

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

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

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

Hrmm.

There is another wrinkle to consider.

Soon there will likely be another type coming along for a representational equality witness. So perhaps it would be best to use an = somewhere in the name and ~ in the other? To indicate this one is real equality and the other is only an equivalence?

I think this falls down because we already have (~) as a constraint meaning real equality, not only an equivalence. I still like (:~:) for the real equality witness, to parallel the constraint. (~~) sounds OK too, along similar lines. The representational equality could perhaps not be an operator, but something with a normal name, just like `Coercible` is not an operator either (which AFAIK is the constraint form of it).

-Edward

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

...

What about (~~)?

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

...

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

I just rather dislike (:=:).

Lets throwing this open to bikeshedding. Alternatives?

-Edward

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

...

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

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

Roman

...

-1 from me.

Shachaf stated my argument correctly -- I think that the (:=:) operator means something quite different from the term-level (==) operator, and the name should reflect this. I do like thinking about a better name,

* Richard Eisenberg [2013-09-29 00:10:46-0400] though, and I'm happy enough if I'm outvoted here.

...

Richard

On Sep 28, 2013, at 10:08 PM, Shachaf Ben-Kiki wrote:

...

On Sat, Sep 28, 2013 at 6:57 PM, Edward Kmett

...

...

> As part of the discussion about Typeable, GHC 7.8 is going to include a > Data.Type.Equality module that provides a polykinded type equality data > type. > > I'd like to propose that we rename this type to (==) rather than

wrote: the (:=:)

...

...

> it was developed under. > > We are already using (+), (-), (*), etc. at the type level in type-nats, so > it would seem to fit the surrounding convention. > > I've done the work of preparing a patch, visible here: > > https://github.com/ekmett/packages-base/commit/fb47f8368ad3d40fdd79bdeec334c... > > Thoughts? > > Normally, I'd let this run the usual 2 week course, but we're getting down > to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with > the current name forever. > > Discussion Period: 1 week > > -Edward Kmett >

+1. For what it's worth, I suggested that name before, and Richard Eisenberg suggested that == should be for type-level Boolean equality: http://markmail.org/message/3yifytgt2k3cfwws. I'm not convinced, though -- this seems fundamental enough to deserve the simplest name possible.

(I'm using that link because the haskell.org mailing list archive seems to be gone... Hopefully that comes back, eventually.)

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

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

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

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

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

-- Your ship was destroyed in a monadic eruption.

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@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 | 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 [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 | wrote: | >> >> As part of the discussion about Typeable, GHC 7.8 is going to | include a | >> >> Data.Type.Equality module that provides a polykinded type equality | data | >> >> type. | >> >> | >> >> I'd like to propose that we rename this type to (==) rather than | the (:=:) | >> >> it was developed under. | >> >> | >> >> We are already using (+), (-), (*), etc. at the type level in | type-nats, so | >> >> it would seem to fit the surrounding convention. | >> >> | >> >> I've done the work of preparing a patch, visible here: | >> >> | >> >> https://github.com/ekmett/packages- | base/commit/fb47f8368ad3d40fdd79bdeec334c0554fb17110 | >> >> | >> >> Thoughts? | >> >> | >> >> Normally, I'd let this run the usual 2 week course, but we're | getting down | >> >> to the wire for 7.8's release. Once 7.8 ships, we'd basically be | stuck with | >> >> the current name forever. | >> >> | >> >> Discussion Period: 1 week | >> >> | >> >> -Edward Kmett | >> >> | >> > | >> > +1. For what it's worth, I suggested that name before, and Richard | >> > Eisenberg suggested that == should be for type-level Boolean | equality: | >> > http://markmail.org/message/3yifytgt2k3cfwws. I'm not convinced, | >> > though -- this seems fundamental enough to deserve the simplest | name | >> > possible. | >> > | >> > (I'm using that link because the haskell.org mailing list archive | >> > seems to be gone... Hopefully that comes back, eventually.) | >> > | >> > Shachaf | >> > _______________________________________________ | >> > Libraries mailing list | >> > Libraries@haskell.org | >> > http://www.haskell.org/mailman/listinfo/libraries | >> | >> _______________________________________________ | >> Libraries mailing list | >> Libraries@haskell.org | >> http://www.haskell.org/mailman/listinfo/libraries | > | > _______________________________________________ | > Libraries mailing list | > Libraries@haskell.org | > http://www.haskell.org/mailman/listinfo/libraries | > | _______________________________________________ | Libraries mailing list | Libraries@haskell.org | http://www.haskell.org/mailman/listinfo/libraries

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

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

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

Thoughts?

Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.

Discussion Period: 1 week

-Edward Kmett

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

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@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 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 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/fb47f8368ad3d40fdd79bdeec334c...

Thoughts?

Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.

Discussion Period: 1 week

-Edward Kmett

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

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@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 mailto:ekmett@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 mailto:carter.schonwald@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 mailto:conal@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 mailto:ekmett@gmail.com> wrote: As part of the discussion about Typeable, GHC 7.8 is going to include a Data.Type.Equality module that provides a polykinded type equality data type. I'd like to propose that we rename this type to (==) rather than the (:=:) it was developed under. We are already using (+), (-), (*), etc. at the type level in type-nats, so it would seem to fit the surrounding convention. I've done the work of preparing a patch, visible here: https://github.com/ekmett/packages-base/commit/fb47f8368ad3d40fdd79bdeec334c... Thoughts? Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever. Discussion Period: 1 week -Edward Kmett _______________________________________________ Libraries mailing list Libraries@haskell.orgmailto:Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries _______________________________________________ Libraries mailing list Libraries@haskell.orgmailto:Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

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 Blindnesshttp://existentialtype.wordpress.com/2011/03/15/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 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@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@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 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@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 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 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/fb47f8368ad3d40fdd79bdeec334c... ****

** **

Thoughts?****

** **

Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.****

** **

Discussion Period: 1 week****

** **

-Edward Kmett****

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

** **

** **

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

** **

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 http://ghc.haskell.org/trac/ghc/wiki/TypeLevelNamingIssues

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

https://github.com/ekmett/packages-base/commit/fb47f8368ad3d40fdd79bdeec334c... **** ** ** Thoughts?**** ** ** Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.**** ** ** Discussion Period: 1 week**** ** ** -Edward Kmett****

_______________________________________________ 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****

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@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 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 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 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 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/fb47f8368ad3d40fdd79bdeec334c...

Thoughts?

Normally, I'd let this run the usual 2 week course, but we're getting down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck with the current name forever.

Discussion Period: 1 week

-Edward Kmett

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

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