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 <roma@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@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@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@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