Data.Type.Equality and coercions

[Edward Kmett]

That works for me.


On Thu, Oct 10, 2013 at 5:59 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>  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>
> 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/20131010/13927825/attachment.html>