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

[Edward Kmett]

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 <illissius at gmail.com> wrote:

> On Sun, Sep 29, 2013 at 10:33 PM, Simon Peyton-Jones <
> simonpj at 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 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/20130929/f6839e29/attachment.html>