<div dir="ltr">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).</div><br><div class="gmail_quote"><div dir="ltr">On Tue, Dec 4, 2018 at 12:26 AM Edward Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Mostly because it means I wind up needing another construction to make it all go and can't just kick it all upstream. ;)<div><br></div><div>-Edward</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Dec 3, 2018 at 10:11 PM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank">rae@cs.brynmawr.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space">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.<div><br></div><div>Richard<br><div><br><blockquote type="cite"><div>On Dec 2, 2018, at 5:04 PM, Edward Kmett <<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>> wrote:</div><br class="m_-7098737273766701547m_7384271164395299066Apple-interchange-newline"><div><div dir="ltr" style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none"><div class="gmail_quote"><div dir="ltr">On Sun, Dec 2, 2018 at 7:55 PM David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="auto"><div>Unfortunately, testEquality for STRef is not at all safe, for reasons we've previously discussed in another context.</div><div dir="auto"><br></div><div dir="auto">   <span class="m_-7098737273766701547m_7384271164395299066Apple-converted-space"> </span>testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)</div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><font face="sans-serif"> <span class="m_-7098737273766701547m_7384271164395299066Apple-converted-space"> </span>let x = [1, 2]</font></div><div dir="auto"><font face="sans-serif"> <span class="m_-7098737273766701547m_7384271164395299066Apple-converted-space"> </span>foo :: STRef s [Int] <- newSTRef x</font></div><div dir="auto"><font face="sans-serif"> <span class="m_-7098737273766701547m_7384271164395299066Apple-converted-space"> </span>let bar :: STRef s (ZipList Int) = coerce foo</font></div><div dir="auto"><font face="sans-serif"> <span class="m_-7098737273766701547m_7384271164395299066Apple-converted-space"> </span>case testEquality foo bar of UH-OH</font></div><div dir="auto"><font face="sans-serif"><br></font></div><div dir="auto"><font face="sans-serif">I suspect testCoercion actually will work here.</font></div><div dir="auto"><br></div><div dir="auto">You could patch up the problem by giving STRef (and perhaps MutVar#) a stricter role signature:</div><div dir="auto"><br></div><div dir="auto">type role STRef nominal nominal</div><div dir="auto"><br></div><div dir="auto">That might not break enough code to worry about; I'm not sure.</div></div></blockquote><div><br></div><div>That is rather unfortunate, as it means most if not all of these would be limited to TestCoercion.</div><div><br></div><div>-Edward </div><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="auto"><div dir="auto"><div class="gmail_quote" dir="auto"><div dir="ltr">On Sun, Dec 2, 2018, 7:16 PM Edward Kmett <<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a><span class="m_-7098737273766701547m_7384271164395299066Apple-converted-space"> </span>wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr">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.</div><div dir="ltr"><br></div><div dir="ltr"><div dir="ltr">With these you can learn about the equality of the types of elements of an STRef when you go to</div><div dir="ltr"><br></div><div dir="ltr">     testEquality :: STRef s a -> STRef s b -> Maybe (a :~: b)<br><div><br></div><div>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: <a href="https://dl.acm.org/citation.cfm?id=2976008" rel="noreferrer" target="_blank">https://dl.acm.org/citation.cfm?id=2976008</a><span class="m_-7098737273766701547m_7384271164395299066Apple-converted-space"> </span>and currently I get by by unsafeCoercing reallyUnsafePointerEquality# and unsafeCoercing the witness that I get back in turn. =/</div><div><br></div><div>With this the notion of a "Key" introduced there can be safely modeled with an STRef s (Proxy a).</div><div><br></div><div>This would make it {-# LANGUAGE Safe #-} for users to construct heterogeneous container types that don't need Typeable information about the values.</div></div></div><div dir="ltr"><br></div><div dir="ltr">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.</div><div dir="ltr"><br></div><div>-Edward</div><div dir="ltr"><div></div></div></div>_______________________________________________<br>Libraries mailing list<br><a href="mailto:Libraries@haskell.org" rel="noreferrer" target="_blank">Libraries@haskell.org</a><br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a></blockquote></div></div></div></blockquote></div></div></div></blockquote></div><br></div></div></blockquote></div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">-Andrew Thaddeus Martin</div>