TestEquality for references

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

TestEquality for references

Edward Kmett-2
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward

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

Re: TestEquality for references

David Feuer
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

Re: TestEquality for references

Edward Kmett-2
On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.

-Edward 

 
On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

Re: TestEquality for references

Richard Eisenberg-4
Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.

Richard

On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:

On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.

-Edward 

 
On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


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

Re: TestEquality for references

Edward Kmett-2
Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)

-Edward

On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.

Richard

On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:

On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.

-Edward 

 
On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


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

Re: TestEquality for references

Andrew Martin
Given that each comes at the cost of the other, if I had to choose between which of these two STRef features I could have, I would pick being able to use it to recover equality over being able to lift newtype coercions through it. The former is increases expressivity while the latter accomplishes something that is achievable by simply using less newtypes in APIs where the need for this arises (not that I've ever actually needed to coerce an STRef in this way, but it would be interesting to hear from anyone who has needed this).

On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <[hidden email]> wrote:
Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)

-Edward

On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.

Richard

On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:

On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.

-Edward 

 
On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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


--
-Andrew Thaddeus Martin

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

Re: TestEquality for references

Edward Kmett-2
You actually would need both types for full generality. Both provide useful power under different circumstances.

Another thing I noticed when working on this is that TestEquality is missing TestCoercion as a superclass at present. This means you can't use the latter as merely a weaker TestEquality constraint, but have to plumb both independently. This feels wrong. Everything that can support TestEquality should be able to support TestCoercion.

I do at least want the TestCoercion instances.

-Edward

On Tue, Dec 4, 2018 at 7:46 AM Andrew Martin <[hidden email]> wrote:
Given that each comes at the cost of the other, if I had to choose between which of these two STRef features I could have, I would pick being able to use it to recover equality over being able to lift newtype coercions through it. The former is increases expressivity while the latter accomplishes something that is achievable by simply using less newtypes in APIs where the need for this arises (not that I've ever actually needed to coerce an STRef in this way, but it would be interesting to hear from anyone who has needed this).

On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <[hidden email]> wrote:
Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)

-Edward

On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.

Richard

On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:

On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.

-Edward 

 
On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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


--
-Andrew Thaddeus Martin

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

Re: TestEquality for references

Zemyla
I thought of this, but the problem is that Data.Type.Equality is Trustworthy, while Data.Type.Coercion is unsafe. Therefore, you can't define the superclass in a Safe module.

The solution to this would be to have Data.Type.Equality export TestCoercion but not testCoercion, and have a a default implementation (with DefaultSignatures) that requires TestEquality and just turns the equality into a coercion.

Another option is to include testCoercion, but not Coercion, and use the fact that Coercion is a Category here:

toId :: Category p => (a :~: b) -> p a b
toId Refl = id

And then testCoercion a b = fmap toId $ testEquality a b

On Tue, Dec 4, 2018, 19:50 Edward Kmett <[hidden email] wrote:
You actually would need both types for full generality. Both provide useful power under different circumstances.

Another thing I noticed when working on this is that TestEquality is missing TestCoercion as a superclass at present. This means you can't use the latter as merely a weaker TestEquality constraint, but have to plumb both independently. This feels wrong. Everything that can support TestEquality should be able to support TestCoercion.

I do at least want the TestCoercion instances.

-Edward

On Tue, Dec 4, 2018 at 7:46 AM Andrew Martin <[hidden email]> wrote:
Given that each comes at the cost of the other, if I had to choose between which of these two STRef features I could have, I would pick being able to use it to recover equality over being able to lift newtype coercions through it. The former is increases expressivity while the latter accomplishes something that is achievable by simply using less newtypes in APIs where the need for this arises (not that I've ever actually needed to coerce an STRef in this way, but it would be interesting to hear from anyone who has needed this).

On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <[hidden email]> wrote:
Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)

-Edward

On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.

Richard

On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:

On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.

-Edward 

 
On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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


--
-Andrew Thaddeus Martin
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

Re: TestEquality for references

Edward Kmett-2
I could live with that solution pretty well. Getting the default implementation would be a very nice bonus, as in most cases it is quite repetitive. 

Observation: In the second scenario is it really that exporting Coercion actually dangerous? 

Not in the sense that we should revisit the stance, but rather it seems that the things it exports that can actually use Coercible to coerce that are the problem point. 

Without coerce or coerceWith, everything in Data.Type.Coercion seems perfectly Trustworthy. 

We should just be able to split off the Trustworthy parts of Data.Type.Coercion via an Internal module and use them to put the superclass in place. Even gcoerceWith requires you to have access to coerce to do anything with it other than manipulate Coercible instances.

The whole module is currently unsafe because of one combinator in it.

GHC is even smart enough that you don't need `coerce` to implement sym, trans, etc. so `coerce` and `coerceWith` aren't even used when implementing the instances.
 
-Edward

On Tue, Dec 4, 2018 at 9:08 PM Zemyla <[hidden email]> wrote:
I thought of this, but the problem is that Data.Type.Equality is Trustworthy, while Data.Type.Coercion is unsafe. Therefore, you can't define the superclass in a Safe module.

The solution to this would be to have Data.Type.Equality export TestCoercion but not testCoercion, and have a a default implementation (with DefaultSignatures) that requires TestEquality and just turns the equality into a coercion.

Another option is to include testCoercion, but not Coercion, and use the fact that Coercion is a Category here:

toId :: Category p => (a :~: b) -> p a b
toId Refl = id

And then testCoercion a b = fmap toId $ testEquality a b

On Tue, Dec 4, 2018, 19:50 Edward Kmett <[hidden email] wrote:
You actually would need both types for full generality. Both provide useful power under different circumstances.

Another thing I noticed when working on this is that TestEquality is missing TestCoercion as a superclass at present. This means you can't use the latter as merely a weaker TestEquality constraint, but have to plumb both independently. This feels wrong. Everything that can support TestEquality should be able to support TestCoercion.

I do at least want the TestCoercion instances.

-Edward

On Tue, Dec 4, 2018 at 7:46 AM Andrew Martin <[hidden email]> wrote:
Given that each comes at the cost of the other, if I had to choose between which of these two STRef features I could have, I would pick being able to use it to recover equality over being able to lift newtype coercions through it. The former is increases expressivity while the latter accomplishes something that is achievable by simply using less newtypes in APIs where the need for this arises (not that I've ever actually needed to coerce an STRef in this way, but it would be interesting to hear from anyone who has needed this).

On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <[hidden email]> wrote:
Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)

-Edward

On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.

Richard

On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:

On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.

    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

  let x = [1, 2]
  foo :: STRef s [Int] <- newSTRef x
  let bar :: STRef s (ZipList Int) = coerce foo
  case testEquality foo bar of UH-OH

I suspect testCoercion actually will work here.

You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:

type role STRef nominal nominal

That might not break enough code to worry about; I'm not sure.

That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.

-Edward 

 
On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.

With these you can learn about the equality of the types of elements of an STRef when you go to

     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)

I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/

With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).

This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.

Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.

-Edward
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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


--
-Andrew Thaddeus Martin
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

Re: TestEquality for references

David Feuer
I *do* think we should revisit that stance. Anyone who's still relying
on coerce not existing to guard their otherwise *unsafe* operations
without using role annotations is way behind the times and needs to
fix their code.
On Wed, Dec 5, 2018 at 12:22 AM Edward Kmett <[hidden email]> wrote:

>
> I could live with that solution pretty well. Getting the default implementation would be a very nice bonus, as in most cases it is quite repetitive.
>
> Observation: In the second scenario is it really that exporting Coercion actually dangerous?
>
> Not in the sense that we should revisit the stance, but rather it seems that the things it exports that can actually use Coercible to coerce that are the problem point.
>
> Without coerce or coerceWith, everything in Data.Type.Coercion seems perfectly Trustworthy.
>
> We should just be able to split off the Trustworthy parts of Data.Type.Coercion via an Internal module and use them to put the superclass in place. Even gcoerceWith requires you to have access to coerce to do anything with it other than manipulate Coercible instances.
>
> The whole module is currently unsafe because of one combinator in it.
>
> GHC is even smart enough that you don't need `coerce` to implement sym, trans, etc. so `coerce` and `coerceWith` aren't even used when implementing the instances.
>
> -Edward
>
> On Tue, Dec 4, 2018 at 9:08 PM Zemyla <[hidden email]> wrote:
>>
>> I thought of this, but the problem is that Data.Type.Equality is Trustworthy, while Data.Type.Coercion is unsafe. Therefore, you can't define the superclass in a Safe module.
>>
>> The solution to this would be to have Data.Type.Equality export TestCoercion but not testCoercion, and have a a default implementation (with DefaultSignatures) that requires TestEquality and just turns the equality into a coercion.
>>
>> Another option is to include testCoercion, but not Coercion, and use the fact that Coercion is a Category here:
>>
>> toId :: Category p => (a :~: b) -> p a b
>> toId Refl = id
>>
>> And then testCoercion a b = fmap toId $ testEquality a b
>>
>> On Tue, Dec 4, 2018, 19:50 Edward Kmett <[hidden email] wrote:
>>>
>>> You actually would need both types for full generality. Both provide useful power under different circumstances.
>>>
>>> Another thing I noticed when working on this is that TestEquality is missing TestCoercion as a superclass at present. This means you can't use the latter as merely a weaker TestEquality constraint, but have to plumb both independently. This feels wrong. Everything that can support TestEquality should be able to support TestCoercion.
>>>
>>> I do at least want the TestCoercion instances.
>>>
>>> -Edward
>>>
>>> On Tue, Dec 4, 2018 at 7:46 AM Andrew Martin <[hidden email]> wrote:
>>>>
>>>> Given that each comes at the cost of the other, if I had to choose between which of these two STRef features I could have, I would pick being able to use it to recover equality over being able to lift newtype coercions through it. The former is increases expressivity while the latter accomplishes something that is achievable by simply using less newtypes in APIs where the need for this arises (not that I've ever actually needed to coerce an STRef in this way, but it would be interesting to hear from anyone who has needed this).
>>>>
>>>> On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <[hidden email]> wrote:
>>>>>
>>>>> Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)
>>>>>
>>>>> -Edward
>>>>>
>>>>> On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
>>>>>>
>>>>>> Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.
>>>>>>
>>>>>> Richard
>>>>>>
>>>>>> On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:
>>>>>>
>>>>>> On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
>>>>>>>
>>>>>>> Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.
>>>>>>>
>>>>>>>     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)
>>>>>>>
>>>>>>>   let x = [1, 2]
>>>>>>>   foo :: STRef s [Int] <- newSTRef x
>>>>>>>   let bar :: STRef s (ZipList Int) = coerce foo
>>>>>>>   case testEquality foo bar of UH-OH
>>>>>>>
>>>>>>> I suspect testCoercion actually will work here.
>>>>>>>
>>>>>>> You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:
>>>>>>>
>>>>>>> type role STRef nominal nominal
>>>>>>>
>>>>>>> That might not break enough code to worry about; I'm not sure.
>>>>>>
>>>>>>
>>>>>> That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.
>>>>>>
>>>>>> -Edward
>>>>>>
>>>>>>
>>>>>>>
>>>>>>> On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
>>>>>>>>
>>>>>>>> I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.
>>>>>>>>
>>>>>>>> With these you can learn about the equality of the types of elements of an STRef when you go to
>>>>>>>>
>>>>>>>>      testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)
>>>>>>>>
>>>>>>>> I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/
>>>>>>>>
>>>>>>>> With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).
>>>>>>>>
>>>>>>>> This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.
>>>>>>>>
>>>>>>>> Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.
>>>>>>>>
>>>>>>>> -Edward
>>>>>>>> _______________________________________________
>>>>>>>> Libraries mailing list
>>>>>>>> [hidden email]
>>>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>>
>>>>>>
>>>>> _______________________________________________
>>>>> Libraries mailing list
>>>>> [hidden email]
>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>
>>>>
>>>>
>>>> --
>>>> -Andrew Thaddeus Martin
>>>
>>> _______________________________________________
>>> Libraries mailing list
>>> [hidden email]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: TestEquality for references

Richard Eisenberg-4
I put my 2¢ with David here. Though I agreed with the decision to make coerce Unsafe at first, I think we can revise that now.

Richard

> On Dec 5, 2018, at 12:46 AM, David Feuer <[hidden email]> wrote:
>
> I *do* think we should revisit that stance. Anyone who's still relying
> on coerce not existing to guard their otherwise *unsafe* operations
> without using role annotations is way behind the times and needs to
> fix their code.
> On Wed, Dec 5, 2018 at 12:22 AM Edward Kmett <[hidden email]> wrote:
>>
>> I could live with that solution pretty well. Getting the default implementation would be a very nice bonus, as in most cases it is quite repetitive.
>>
>> Observation: In the second scenario is it really that exporting Coercion actually dangerous?
>>
>> Not in the sense that we should revisit the stance, but rather it seems that the things it exports that can actually use Coercible to coerce that are the problem point.
>>
>> Without coerce or coerceWith, everything in Data.Type.Coercion seems perfectly Trustworthy.
>>
>> We should just be able to split off the Trustworthy parts of Data.Type.Coercion via an Internal module and use them to put the superclass in place. Even gcoerceWith requires you to have access to coerce to do anything with it other than manipulate Coercible instances.
>>
>> The whole module is currently unsafe because of one combinator in it.
>>
>> GHC is even smart enough that you don't need `coerce` to implement sym, trans, etc. so `coerce` and `coerceWith` aren't even used when implementing the instances.
>>
>> -Edward
>>
>> On Tue, Dec 4, 2018 at 9:08 PM Zemyla <[hidden email]> wrote:
>>>
>>> I thought of this, but the problem is that Data.Type.Equality is Trustworthy, while Data.Type.Coercion is unsafe. Therefore, you can't define the superclass in a Safe module.
>>>
>>> The solution to this would be to have Data.Type.Equality export TestCoercion but not testCoercion, and have a a default implementation (with DefaultSignatures) that requires TestEquality and just turns the equality into a coercion.
>>>
>>> Another option is to include testCoercion, but not Coercion, and use the fact that Coercion is a Category here:
>>>
>>> toId :: Category p => (a :~: b) -> p a b
>>> toId Refl = id
>>>
>>> And then testCoercion a b = fmap toId $ testEquality a b
>>>
>>> On Tue, Dec 4, 2018, 19:50 Edward Kmett <[hidden email] wrote:
>>>>
>>>> You actually would need both types for full generality. Both provide useful power under different circumstances.
>>>>
>>>> Another thing I noticed when working on this is that TestEquality is missing TestCoercion as a superclass at present. This means you can't use the latter as merely a weaker TestEquality constraint, but have to plumb both independently. This feels wrong. Everything that can support TestEquality should be able to support TestCoercion.
>>>>
>>>> I do at least want the TestCoercion instances.
>>>>
>>>> -Edward
>>>>
>>>> On Tue, Dec 4, 2018 at 7:46 AM Andrew Martin <[hidden email]> wrote:
>>>>>
>>>>> Given that each comes at the cost of the other, if I had to choose between which of these two STRef features I could have, I would pick being able to use it to recover equality over being able to lift newtype coercions through it. The former is increases expressivity while the latter accomplishes something that is achievable by simply using less newtypes in APIs where the need for this arises (not that I've ever actually needed to coerce an STRef in this way, but it would be interesting to hear from anyone who has needed this).
>>>>>
>>>>> On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <[hidden email]> wrote:
>>>>>>
>>>>>> Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)
>>>>>>
>>>>>> -Edward
>>>>>>
>>>>>> On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
>>>>>>>
>>>>>>> Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.
>>>>>>>
>>>>>>> Richard
>>>>>>>
>>>>>>> On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:
>>>>>>>
>>>>>>> On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
>>>>>>>>
>>>>>>>> Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.
>>>>>>>>
>>>>>>>>    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)
>>>>>>>>
>>>>>>>>  let x = [1, 2]
>>>>>>>>  foo :: STRef s [Int] <- newSTRef x
>>>>>>>>  let bar :: STRef s (ZipList Int) = coerce foo
>>>>>>>>  case testEquality foo bar of UH-OH
>>>>>>>>
>>>>>>>> I suspect testCoercion actually will work here.
>>>>>>>>
>>>>>>>> You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:
>>>>>>>>
>>>>>>>> type role STRef nominal nominal
>>>>>>>>
>>>>>>>> That might not break enough code to worry about; I'm not sure.
>>>>>>>
>>>>>>>
>>>>>>> That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.
>>>>>>>
>>>>>>> -Edward
>>>>>>>
>>>>>>>
>>>>>>>>
>>>>>>>> On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
>>>>>>>>>
>>>>>>>>> I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.
>>>>>>>>>
>>>>>>>>> With these you can learn about the equality of the types of elements of an STRef when you go to
>>>>>>>>>
>>>>>>>>>     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)
>>>>>>>>>
>>>>>>>>> I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/
>>>>>>>>>
>>>>>>>>> With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).
>>>>>>>>>
>>>>>>>>> This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.
>>>>>>>>>
>>>>>>>>> Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.
>>>>>>>>>
>>>>>>>>> -Edward
>>>>>>>>> _______________________________________________
>>>>>>>>> Libraries mailing list
>>>>>>>>> [hidden email]
>>>>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>>>
>>>>>>>
>>>>>> _______________________________________________
>>>>>> Libraries mailing list
>>>>>> [hidden email]
>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>
>>>>>
>>>>>
>>>>> --
>>>>> -Andrew Thaddeus Martin
>>>>
>>>> _______________________________________________
>>>> Libraries mailing list
>>>> [hidden email]
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>> _______________________________________________
>>> Libraries mailing list
>>> [hidden email]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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

Re: TestEquality for references

Edward Kmett-2
I'm definitely open to revisiting it as well.

-Edward

On Mon, Dec 10, 2018 at 5:54 PM Richard Eisenberg <[hidden email]> wrote:
I put my 2¢ with David here. Though I agreed with the decision to make coerce Unsafe at first, I think we can revise that now.

Richard

> On Dec 5, 2018, at 12:46 AM, David Feuer <[hidden email]> wrote:
>
> I *do* think we should revisit that stance. Anyone who's still relying
> on coerce not existing to guard their otherwise *unsafe* operations
> without using role annotations is way behind the times and needs to
> fix their code.
> On Wed, Dec 5, 2018 at 12:22 AM Edward Kmett <[hidden email]> wrote:
>>
>> I could live with that solution pretty well. Getting the default implementation would be a very nice bonus, as in most cases it is quite repetitive.
>>
>> Observation: In the second scenario is it really that exporting Coercion actually dangerous?
>>
>> Not in the sense that we should revisit the stance, but rather it seems that the things it exports that can actually use Coercible to coerce that are the problem point.
>>
>> Without coerce or coerceWith, everything in Data.Type.Coercion seems perfectly Trustworthy.
>>
>> We should just be able to split off the Trustworthy parts of Data.Type.Coercion via an Internal module and use them to put the superclass in place. Even gcoerceWith requires you to have access to coerce to do anything with it other than manipulate Coercible instances.
>>
>> The whole module is currently unsafe because of one combinator in it.
>>
>> GHC is even smart enough that you don't need `coerce` to implement sym, trans, etc. so `coerce` and `coerceWith` aren't even used when implementing the instances.
>>
>> -Edward
>>
>> On Tue, Dec 4, 2018 at 9:08 PM Zemyla <[hidden email]> wrote:
>>>
>>> I thought of this, but the problem is that Data.Type.Equality is Trustworthy, while Data.Type.Coercion is unsafe. Therefore, you can't define the superclass in a Safe module.
>>>
>>> The solution to this would be to have Data.Type.Equality export TestCoercion but not testCoercion, and have a a default implementation (with DefaultSignatures) that requires TestEquality and just turns the equality into a coercion.
>>>
>>> Another option is to include testCoercion, but not Coercion, and use the fact that Coercion is a Category here:
>>>
>>> toId :: Category p => (a :~: b) -> p a b
>>> toId Refl = id
>>>
>>> And then testCoercion a b = fmap toId $ testEquality a b
>>>
>>> On Tue, Dec 4, 2018, 19:50 Edward Kmett <[hidden email] wrote:
>>>>
>>>> You actually would need both types for full generality. Both provide useful power under different circumstances.
>>>>
>>>> Another thing I noticed when working on this is that TestEquality is missing TestCoercion as a superclass at present. This means you can't use the latter as merely a weaker TestEquality constraint, but have to plumb both independently. This feels wrong. Everything that can support TestEquality should be able to support TestCoercion.
>>>>
>>>> I do at least want the TestCoercion instances.
>>>>
>>>> -Edward
>>>>
>>>> On Tue, Dec 4, 2018 at 7:46 AM Andrew Martin <[hidden email]> wrote:
>>>>>
>>>>> Given that each comes at the cost of the other, if I had to choose between which of these two STRef features I could have, I would pick being able to use it to recover equality over being able to lift newtype coercions through it. The former is increases expressivity while the latter accomplishes something that is achievable by simply using less newtypes in APIs where the need for this arises (not that I've ever actually needed to coerce an STRef in this way, but it would be interesting to hear from anyone who has needed this).
>>>>>
>>>>> On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <[hidden email]> wrote:
>>>>>>
>>>>>> Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)
>>>>>>
>>>>>> -Edward
>>>>>>
>>>>>> On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <[hidden email]> wrote:
>>>>>>>
>>>>>>> Why is it unfortunate? This looks like desired behavior to me. That is: I think these reference types should allow coercions between representationally equal types. Of course, that means that TestEquality is out.
>>>>>>>
>>>>>>> Richard
>>>>>>>
>>>>>>> On Dec 2, 2018, at 5:04 PM, Edward Kmett <[hidden email]> wrote:
>>>>>>>
>>>>>>> On Sun, Dec 2, 2018 at 7:55 PM David Feuer <[hidden email]> wrote:
>>>>>>>>
>>>>>>>> Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.
>>>>>>>>
>>>>>>>>    testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)
>>>>>>>>
>>>>>>>>  let x = [1, 2]
>>>>>>>>  foo :: STRef s [Int] <- newSTRef x
>>>>>>>>  let bar :: STRef s (ZipList Int) = coerce foo
>>>>>>>>  case testEquality foo bar of UH-OH
>>>>>>>>
>>>>>>>> I suspect testCoercion actually will work here.
>>>>>>>>
>>>>>>>> You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:
>>>>>>>>
>>>>>>>> type role STRef nominal nominal
>>>>>>>>
>>>>>>>> That might not break enough code to worry about; I'm not sure.
>>>>>>>
>>>>>>>
>>>>>>> That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.
>>>>>>>
>>>>>>> -Edward
>>>>>>>
>>>>>>>
>>>>>>>>
>>>>>>>> On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <[hidden email] wrote:
>>>>>>>>>
>>>>>>>>> I'd like to propose adding a bunch of instances for TestEquality and TestCoercion to base and primitive types such as: IORef, STRef s, MVar as well as MutVar and any appropriately uncoercible array types we have in primitive.
>>>>>>>>>
>>>>>>>>> With these you can learn about the equality of the types of elements of an STRef when you go to
>>>>>>>>>
>>>>>>>>>     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)
>>>>>>>>>
>>>>>>>>> I've been using an ad hoc versions of this on my own for some time, across a wide array of packages, based on Atze van der Ploeg's paper: https://dl.acm.org/citation.cfm?id=2976008 and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/
>>>>>>>>>
>>>>>>>>> With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).
>>>>>>>>>
>>>>>>>>> This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.
>>>>>>>>>
>>>>>>>>> Implementation wise, these can either use the value equality of those underlying primitive types and then produce a witness either by unsafeCoerce, or by adding new stronger primitives in ghc-prim to produce the witness in a type-safe manner, giving us well typed core all the way down.
>>>>>>>>>
>>>>>>>>> -Edward
>>>>>>>>> _______________________________________________
>>>>>>>>> Libraries mailing list
>>>>>>>>> [hidden email]
>>>>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>>>
>>>>>>>
>>>>>> _______________________________________________
>>>>>> Libraries mailing list
>>>>>> [hidden email]
>>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>>>
>>>>>
>>>>>
>>>>> --
>>>>> -Andrew Thaddeus Martin
>>>>
>>>> _______________________________________________
>>>> Libraries mailing list
>>>> [hidden email]
>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>>> _______________________________________________
>>> Libraries mailing list
>>> [hidden email]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


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