Coercible questions

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

Coercible questions

Michal Terepeta
Hi,

I've started looking into using `Data.Coerce` (and the `Coercible` type-class) for a personal project and was wondering why coercing between `Int` and `Word` is not allowed? I don't see any fundamental reason why this shouldn't work...

Perhaps, it's just a matter of GHC's implementation details leaking out? IIRC internally GHC has separate `RuntimeRep`/`PrimRep` for a `Word#` and for an `Int#`. If that's the case, would it make sense to unify these? Their actual runtime representation should be the same and I'd expect most (all?) of their differences should be attached to `PrimOp`s.

And that leads me to another question--what exactly goes wrong here:
```
data Foo = Foo Int#
data Bar = Bar Int#

test :: Bar
test = coerce (Foo 42#)
```
Which fails with: "Couldn't match representation of type ‘Foo’ with that of ‘Bar’ arising from a use of ‘coerce’"

Perhaps I'm just misunderstanding exactly how `Coercible` works?

Thanks in advance!

- Michal

PS. The ability to coerce through things like lists is amazing :)

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Coercible questions

Michal Terepeta
Adding [hidden email] to continue the thread

Hi Sandy,

Thanks for the answer! Do you think there is some fundamental reason for this? Or just a matter of implementing this in GHC? It seems to me that this should work just fine as long as the runtime representation is the same.

And a related question--is it safe to `unsafeCoerce` an `Int` to a `Word`? The only reason for why this could be problematic that comes to my mind is that there could be an assumption that different `data`s do not alias each other (although `newtype`s can due to `Coercible` functionality). But I'm not sure this is ever used by GHC? Are there any other reasons why this could be problematic?

Thanks!

- Michal



On Sat, Oct 5, 2019 at 5:27 PM Sandy Maguire <[hidden email]> wrote:
Hi Michal,

Datas aren't coercible, only newtypes. This is why you can't coerce Ints and Words, and why Foo and Bar don't work.

Sandy

On Sat, Oct 5, 2019 at 4:17 PM Michal Terepeta <[hidden email]> wrote:
Hi,

I've started looking into using `Data.Coerce` (and the `Coercible` type-class) for a personal project and was wondering why coercing between `Int` and `Word` is not allowed? I don't see any fundamental reason why this shouldn't work...

Perhaps, it's just a matter of GHC's implementation details leaking out? IIRC internally GHC has separate `RuntimeRep`/`PrimRep` for a `Word#` and for an `Int#`. If that's the case, would it make sense to unify these? Their actual runtime representation should be the same and I'd expect most (all?) of their differences should be attached to `PrimOp`s.

And that leads me to another question--what exactly goes wrong here:
```
data Foo = Foo Int#
data Bar = Bar Int#

test :: Bar
test = coerce (Foo 42#)
```
Which fails with: "Couldn't match representation of type ‘Foo’ with that of ‘Bar’ arising from a use of ‘coerce’"

Perhaps I'm just misunderstanding exactly how `Coercible` works?

Thanks in advance!

- Michal

PS. The ability to coerce through things like lists is amazing :)
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


--
I'm currently travelling the world, sleeping on people's couches and doing full-time collaboration on Haskell projects. If this seems interesting to you, please consider signing up as a host! https://isovector.github.io/erdos/

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Coercible questions

Brandon Allbery
I think there's some work going on to expose the representations, which would enable some ability to coerce. But possibly not this much, as they're separate RuntimeReps so you don't combine signed and unsigned numbers inadvertently; currently that's a little magical inside ghc iirc, with the RuntimeRep the only way to distinguish at all and that vanishing post-typechecking.

On Sat, Oct 5, 2019 at 12:30 PM Michal Terepeta <[hidden email]> wrote:
Adding [hidden email] to continue the thread

Hi Sandy,

Thanks for the answer! Do you think there is some fundamental reason for this? Or just a matter of implementing this in GHC? It seems to me that this should work just fine as long as the runtime representation is the same.

And a related question--is it safe to `unsafeCoerce` an `Int` to a `Word`? The only reason for why this could be problematic that comes to my mind is that there could be an assumption that different `data`s do not alias each other (although `newtype`s can due to `Coercible` functionality). But I'm not sure this is ever used by GHC? Are there any other reasons why this could be problematic?

Thanks!

- Michal



On Sat, Oct 5, 2019 at 5:27 PM Sandy Maguire <[hidden email]> wrote:
Hi Michal,

Datas aren't coercible, only newtypes. This is why you can't coerce Ints and Words, and why Foo and Bar don't work.

Sandy

On Sat, Oct 5, 2019 at 4:17 PM Michal Terepeta <[hidden email]> wrote:
Hi,

I've started looking into using `Data.Coerce` (and the `Coercible` type-class) for a personal project and was wondering why coercing between `Int` and `Word` is not allowed? I don't see any fundamental reason why this shouldn't work...

Perhaps, it's just a matter of GHC's implementation details leaking out? IIRC internally GHC has separate `RuntimeRep`/`PrimRep` for a `Word#` and for an `Int#`. If that's the case, would it make sense to unify these? Their actual runtime representation should be the same and I'd expect most (all?) of their differences should be attached to `PrimOp`s.

And that leads me to another question--what exactly goes wrong here:
```
data Foo = Foo Int#
data Bar = Bar Int#

test :: Bar
test = coerce (Foo 42#)
```
Which fails with: "Couldn't match representation of type ‘Foo’ with that of ‘Bar’ arising from a use of ‘coerce’"

Perhaps I'm just misunderstanding exactly how `Coercible` works?

Thanks in advance!

- Michal

PS. The ability to coerce through things like lists is amazing :)
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


--
I'm currently travelling the world, sleeping on people's couches and doing full-time collaboration on Haskell projects. If this seems interesting to you, please consider signing up as a host! https://isovector.github.io/erdos/
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


--
brandon s allbery kf8nh

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Coercible questions

Richard Eisenberg-5
Hi devs,

In a perfect world, Coercible would relate any two types with the same representation. But the world is not perfect! So we fall well short of this goal.

Specifically, Coercible allows conversions between a newtype and its representation, and additionally between datatypes where the roles work out. Section 2 of the JFP paper (https://repository.brynmawr.edu/cgi/viewcontent.cgi?referer=&httpsredir=1&article=1010&context=compsci_pubs) is an accessible description of how this works.

In the specific cases of Int and Word: there is no guarantee (that I know of) that the tags on the sole constructors of these types are the same. So we don't know that they have the same representation. Even if we did know that the tags are the same, there is no guarantee that Int# and Word# have the same representation. I *think* GHC is general enough that it could cope on a system that used, say, different registers to store signed and unsigned machine integers.

More generally, it might be nice if we could coerce between

> data Booly = Bad | Good

and Bool, but we can't. It would additionally be good to coerce between A and B, where:

> data A = A1 | A2 | A3
> data B = B1 | B2 !C
> data C = C1 | C2

Both A and B have precisely 3 possibilities. But we don't do that yet either. Maybe someday.

In contrast to Brandon, I don't know of anyone working on this. That's not to say that it's no good to work on it, of course!

Richard

On Oct 5, 2019, at 5:51 PM, Brandon Allbery <[hidden email]> wrote:

I think there's some work going on to expose the representations, which would enable some ability to coerce. But possibly not this much, as they're separate RuntimeReps so you don't combine signed and unsigned numbers inadvertently; currently that's a little magical inside ghc iirc, with the RuntimeRep the only way to distinguish at all and that vanishing post-typechecking.

On Sat, Oct 5, 2019 at 12:30 PM Michal Terepeta <[hidden email]> wrote:
Adding [hidden email] to continue the thread

Hi Sandy,

Thanks for the answer! Do you think there is some fundamental reason for this? Or just a matter of implementing this in GHC? It seems to me that this should work just fine as long as the runtime representation is the same.

And a related question--is it safe to `unsafeCoerce` an `Int` to a `Word`? The only reason for why this could be problematic that comes to my mind is that there could be an assumption that different `data`s do not alias each other (although `newtype`s can due to `Coercible` functionality). But I'm not sure this is ever used by GHC? Are there any other reasons why this could be problematic?

Thanks!

- Michal



On Sat, Oct 5, 2019 at 5:27 PM Sandy Maguire <[hidden email]> wrote:
Hi Michal,

Datas aren't coercible, only newtypes. This is why you can't coerce Ints and Words, and why Foo and Bar don't work.

Sandy

On Sat, Oct 5, 2019 at 4:17 PM Michal Terepeta <[hidden email]> wrote:
Hi,

I've started looking into using `Data.Coerce` (and the `Coercible` type-class) for a personal project and was wondering why coercing between `Int` and `Word` is not allowed? I don't see any fundamental reason why this shouldn't work...

Perhaps, it's just a matter of GHC's implementation details leaking out? IIRC internally GHC has separate `RuntimeRep`/`PrimRep` for a `Word#` and for an `Int#`. If that's the case, would it make sense to unify these? Their actual runtime representation should be the same and I'd expect most (all?) of their differences should be attached to `PrimOp`s.

And that leads me to another question--what exactly goes wrong here:
```
data Foo = Foo Int#
data Bar = Bar Int#

test :: Bar
test = coerce (Foo 42#)
```
Which fails with: "Couldn't match representation of type ‘Foo’ with that of ‘Bar’ arising from a use of ‘coerce’"

Perhaps I'm just misunderstanding exactly how `Coercible` works?

Thanks in advance!

- Michal

PS. The ability to coerce through things like lists is amazing :)
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


--
I'm currently travelling the world, sleeping on people's couches and doing full-time collaboration on Haskell projects. If this seems interesting to you, please consider signing up as a host! https://isovector.github.io/erdos/
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


--
brandon s allbery kf8nh
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs