TestEquality for references

Thu Dec 13 09:14:36 UTC 2018

I'm definitely open to revisiting it as well.

-Edward

On Mon, Dec 10, 2018 at 5:54 PM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

> I put my 2¢ with David here. Though I agreed with the decision to make
> coerce Unsafe at first, I think we can revise that now.
>
> Richard
>
> > On Dec 5, 2018, at 12:46 AM, David Feuer <david.feuer at gmail.com> wrote:
> >
> > I *do* think we should revisit that stance. Anyone who's still relying
> > on coerce not existing to guard their otherwise *unsafe* operations
> > without using role annotations is way behind the times and needs to
> > fix their code.
> > On Wed, Dec 5, 2018 at 12:22 AM Edward Kmett <ekmett at gmail.com> wrote:
> >>
> >> I could live with that solution pretty well. Getting the default
> implementation would be a very nice bonus, as in most cases it is quite
> repetitive.
> >>
> >> Observation: In the second scenario is it really that exporting
> Coercion actually dangerous?
> >>
> >> Not in the sense that we should revisit the stance, but rather it seems
> that the things it exports that can actually use Coercible to coerce that
> are the problem point.
> >>
> >> Without coerce or coerceWith, everything in Data.Type.Coercion seems
> perfectly Trustworthy.
> >>
> >> We should just be able to split off the Trustworthy parts of
> Data.Type.Coercion via an Internal module and use them to put the
> superclass in place. Even gcoerceWith requires you to have access to coerce
> to do anything with it other than manipulate Coercible instances.
> >>
> >> The whole module is currently unsafe because of one combinator in it.
> >>
> >> GHC is even smart enough that you don't need `coerce` to implement sym,
> trans, etc. so `coerce` and `coerceWith` aren't even used when implementing
> the instances.
> >>
> >> -Edward
> >>
> >> On Tue, Dec 4, 2018 at 9:08 PM Zemyla <zemyla at gmail.com> wrote:
> >>>
> >>> 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
> >>>
> >>> _______________________________________________
> >>> 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
> > _______________________________________________
> > 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/20181213/15bbae82/attachment.html>