Data.Type.Equality and coercions

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Data.Type.Equality and coercions

Richard Eisenberg-2
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
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Data.Type.Equality and coercions

Stijn van Drongelen
On Wed, Oct 9, 2013 at 5:25 PM, Richard Eisenberg <[hidden email]> wrote:

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.

Why not keep the name `coerce` for both functions, and require qualified imports? 

-Stijn

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Data.Type.Equality and coercions

Edward Kmett-2
In reply to this post by Richard Eisenberg-2
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 <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Data.Type.Equality and coercions

Joachim Breitner-2
Hi,


Am Mittwoch, den 09.10.2013, 13:18 -0400 schrieb Edward Kmett:
> 'subst' may be a better name for gcoerce than it is for coerce,
> anyways, so there is plenty of room for discussion.

not a very constructive comment, but subst certainly is a better name,
for, well, subst:
http://hackage.haskell.org/package/type-equality-0.1.2/docs/Data-Type-Equality.html#v:subst

Greetings,
Joachim


--
Joachim “nomeata” Breitner
  [hidden email]http://www.joachim-breitner.de/
  Jabber: [hidden email]  • GPG-Key: 0x4743206C
  Debian Developer: [hidden email]

_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

signature.asc (205 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

RE: Data.Type.Equality and coercions

Simon Peyton Jones
In reply to this post by Edward Kmett-2

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:[hidden email]] 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 <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

 


_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Data.Type.Equality and coercions

Edward Kmett-2
That works for me.


On Thu, Oct 10, 2013 at 5:59 AM, Simon Peyton-Jones <[hidden email]> 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:[hidden email]] 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 <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries

 



_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Data.Type.Equality and coercions

Bertram Felgenhauer-2
In reply to this post by Joachim Breitner-2
Hi,
> Am Mittwoch, den 09.10.2013, 13:18 -0400 schrieb Edward Kmett:
> > 'subst' may be a better name for gcoerce than it is for coerce,
> > anyways, so there is plenty of room for discussion.
>
> not a very constructive comment, but subst certainly is a better name,
> for, well, subst:
> http://hackage.haskell.org/package/type-equality-0.1.2/docs/Data-Type-Equality.html#v:subst

The pattern of type signatures for subst (= subst1) and subst2
suggests

   subst0 :: (a :=: b) -> a -> b

Unfortunately, that's not a very intuitive name.

Cheers,

Bertram
_______________________________________________
Libraries mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/libraries