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

Fri Oct 4 19:30:07 UTC 2013

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<http://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 <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<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/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****
>
>  ** **
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131004/2a375aa6/attachment-0001.html>