Data.Type.Equality and coercions

[Simon Peyton-Jones]

I?m afraid that ?subst? really isn?t a good name.

Data.Type.Coercion
coerce :: Coercible a b => a -> b
coerceWith :: Coercion a b -> a -> b

Data.Typeable
cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b

So ?cast? is to do with genuine, nominal type equality.    With that in mind, how about

castWith :: (a :~: b) -> a -> b

Simon

From: Libraries [mailto:libraries-bounces at haskell.org] On Behalf Of Edward Kmett
Sent: 09 October 2013 18:19
To: Richard Eisenberg
Cc: Joachim Breitner; Haskell Libraries
Subject: Re: Data.Type.Equality and coercions

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<mailto: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<mailto: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/20131010/33f57364/attachment-0001.html>