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

** **