TestEquality for references

[Edward Kmett]

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 <rae at cs.brynmawr.edu>
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 <ekmett at gmail.com> wrote:
>
> 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/20181204/54192bb6/attachment.html>