<div dir="ltr"><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">david.feuer@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="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">    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">  let x = [1, 2]</font></div><div dir="auto"><font face="sans-serif">  foo :: STRef s [Int] <- newSTRef x</font></div><div dir="auto"><font face="sans-serif">  let bar :: STRef s (ZipList Int) = coerce foo</font></div><div dir="auto"><font face="sans-serif">  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:0 0 0 .8ex;border-left:1px #ccc solid;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> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;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> 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><br>
</blockquote></div></div></div>
</blockquote></div></div>