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 <ekmett at gmail.com 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 <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
>>
> _______________________________________________
> 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/0de24b42/attachment.html>