TestEquality for references

[Edward Kmett]

On Sun, Dec 2, 2018 at 7:55 PM David Feuer <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 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
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181202/599038f0/attachment.html>