Data.Type.Equality and coercions

[Edward Kmett]

I sent Austin a patch about 4 hours before your post that included the code
for the resolution to the (:~:) vs (==) Proposal that included a renaming
of Data.Type.Equality.coerce.

Notably, the core libraries committee decided to take Simon's suggestion
that the witness should be (:~:) rather than (:=:), and I observed that
(==) was never the right name, because (a <= b) is a constraint, but a data
type, which removed any objections I had.

As a knock-on effect of that discussion, I implemented a Category for
Data.Type.Coercion. (It turned out to be trivially implementable with the
existing Coercible with no changes needed, by borrowing some tricks from my
old eq package) and wound up needing to import Data.Type.Equality inside it
and noticed the conflict.

I renamed 'Data.Type.Equality.coerce' it to 'subst' somewhat arbitrarily,
though, as we're getting down close to the wire and we're starting to try
to avoid base exporting multiple functions with the same name but different
signatures to reduce confusion.

If you still want this bikeshed to have a different color, by all means
carry on!

'subst' may be a better name for gcoerce than it is for coerce, anyways, so
there is plenty of room for discussion.

-Edward


On Wed, Oct 9, 2013 at 11:25 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> I've noticed two infelicities with the Data.Type.Equality module that I
> added this summer (according to this proposal:
> http://ghc.haskell.org/trac/ghc/wiki/TypeLevelReasoning)  For those of
> you unfamiliar, the key definition is this:
>
> > data a :=: b where
> >   Refl :: a :=: a
>
> This is essentially just like (~), but in * instead of Constraint.
>
> 1. There is a function
> > coerce :: (a :=: b) -> a -> b
>
> This function conflicts with the new function of the same name in the
> Coercible class (defined in GHC.Prim), with the type
> > coerce :: Coercible a b => a -> b
>
> So, these functions are very similar. The first uses explicit nominal
> equality, while the second uses implicit representational equality. Neither
> quite subsumes the other.
>
> (Disclaimer: I may or may not have named both of these myself, albeit
> separated by several months. If I did, sorry for creating this problem.)
>
> My slight inclination: rename the Coercible version to `coerceRep`, as it
> really is doing a runtime coercion, as opposed to `coerce`. But, I'm quite
> happy for someone else to have a better idea.
>
>
> 2. There is a useful function that should be added to Data.Type.Equality:
>
> > gcoerce :: (a :=: b) -> ((a ~ b) => r) -> r
> > gcoerce Refl x = x
>
> For an example of this in action, see
> https://gist.github.com/goldfirere/6902431, which is related to #8423 but
> can be read standalone.
>
> I don't think that gcoerce can subsume coerce because they have different
> type inference implications. In particular, the types of the coercion in
> `coerce` can improve the type of the equality witness, whereas this is not
> possible in `gcoerce`.
>
> Discussion time: 1 week.
>
> Thanks!
> Richard
>
> _______________________________________________
> 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/20131009/3e2a51dc/attachment.html>