<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>I've updated the wiki page to remove the Void/Refuted/DecideEqT code, as discussed in a conversation among Pedro, Simon, and me yesterday. This code can easily be put in a library, but Typeable won't support decidable equality directly. Instead, a library could easily use unsafeCoerce to implement the behavior. If that scares you, note that Data.Typeable would have to use unsafeCoerce to implement it, anyway.</div><div><br></div><div>Richard</div><br><div><div>On Apr 24, 2013, at 9:11 AM, José Pedro Magalhães <<a href="mailto:jpm@cs.uu.nl">jpm@cs.uu.nl</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi all,<br><br>I've started working on implementing what's described on that wikipage to a base library<br>branch: <a href="https://github.com/ghc/packages-base/tree/data-proxy">https://github.com/ghc/packages-base/tree/data-proxy</a><br>
<br>Some code (and lots of documentation) is still missing; feel free to help!<br><br><br>Cheers,<br>Pedro<br><br><div class="gmail_quote">On Fri, Apr 12, 2013 at 2:01 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I have updated the wiki page at <a href="http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning</a><br>
with these ideas. If you have further thoughts on all of this, please update that page and send an email out so we know to look at the changes!<br>
<br>
My timeline for implementing all of this (not hard, but it needs to be done) is around the end of the month.<br>
<br>
Thanks,<br>
Richard<br>
<div class="HOEnZb"><div class="h5"><br>
On Apr 4, 2013, at 11:11 AM, Edward A Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br>
<br>
> Note the eq lib and the type-eq/(:~:) GADT-based approach are interchangeable.<br>
><br>
> You can upgrade a Leibnizian equality to a type equality by applying the Leibnizian substitution to an a :~: a.<br>
><br>
> lens also has a notion of an Equality family at the bottom of the type semilattice for lens-like constructions, which is effectively a naked Leibnizian equality sans newtype wrapper.<br>
><br>
> The only reason eq exists is to showcase this approach, but in practice I recommend just using the GADT, modulo mutterings about the name. :)<br>
><br>
> That said those lowerings are particularly useful, if subtle -- Oleg wrote the first version of them, which I simplified to the form in that lib and they provide functionality that is classically not derivable for Leibnizian equality.<br>
><br>
> Sent from my iPhone<br>
><br>
> On Apr 4, 2013, at 3:01 AM, Erik Hesselink <<a href="mailto:hesselink@gmail.com">hesselink@gmail.com</a>> wrote:<br>
><br>
>> On Wed, Apr 3, 2013 at 6:08 PM, Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br>
>>> Comments? Thoughts?<br>
>><br>
>> Edward Kmett 'eq' library uses a different definition of equality, but<br>
>> can also be an inspiration for useful functions. Particularly, it<br>
>> includes:<br>
>><br>
>> lower :: (f a :~: f b) -> a :~: b<br>
>><br>
>> Another question is where all this is going to live? In a separate<br>
>> library? Or in base? And should it really be in a GHC namespace? The<br>
>> functionality is not bound to GHC. Perhaps something in data would be<br>
>> more appropriate.<br>
>><br>
>> Erik<br>
>><br>
>> _______________________________________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
>> <a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
><br>
<br>
</div></div></blockquote></div><br>
</blockquote></div><br></body></html>