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@gmail.com> wrote:
On Sun, Sep 29, 2013 at 10:33 PM, Simon Peyton-Jones <simonpj@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@haskell.org
http://www.haskell.org/mailman/listinfo/libraries