TestEquality for references

[Richard Eisenberg]

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 <ekmett at gmail.com> wrote:
> 
> On Sun, Dec 2, 2018 at 7:55 PM David Feuer <david.feuer at gmail.com <mailto:david.feuer at gmail.com>> 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 <ekmett at gmail.com <mailto:ekmett at gmail.com> 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 <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
> Libraries at haskell.org <mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries <http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181203/2796eb48/attachment.html>