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

[Simon Peyton-Jones]

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

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

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

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

Simon

| -----Original Message-----
| From: Libraries [mailto: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