TestEquality for references

[Edward Kmett]

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 <andrew.thaddeus at gmail.com>
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 <ekmett at gmail.com> 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 <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
>>>>
>>>>
>>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>
>
> --
> -Andrew Thaddeus Martin
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20181204/cfbf0896/attachment.html>