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. Richard On Apr 24, 2013, at 9:11 AM, José Pedro Magalhães wrote:

Hi all,

I've started working on implementing what's described on that wikipage to a base library branch: https://github.com/ghc/packages-base/tree/data-proxy

Some code (and lots of documentation) is still missing; feel free to help!

Cheers, Pedro

On Fri, Apr 12, 2013 at 2:01 PM, Richard Eisenberg wrote: I have updated the wiki page at http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning 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!

My timeline for implementing all of this (not hard, but it needs to be done) is around the end of the month.

Thanks, Richard

On Apr 4, 2013, at 11:11 AM, Edward A Kmett wrote:

...

Note the eq lib and the type-eq/(:~:) GADT-based approach are interchangeable.

You can upgrade a Leibnizian equality to a type equality by applying the Leibnizian substitution to an a :~: a.

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.

The only reason eq exists is to showcase this approach, but in practice I recommend just using the GADT, modulo mutterings about the name. :)

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.

Sent from my iPhone

On Apr 4, 2013, at 3:01 AM, Erik Hesselink wrote:

...

On Wed, Apr 3, 2013 at 6:08 PM, Richard Eisenberg wrote:

...

Comments? Thoughts?

Edward Kmett 'eq' library uses a different definition of equality, but can also be an inspiration for useful functions. Particularly, it includes:

lower :: (f a :~: f b) -> a :~: b

Another question is where all this is going to live? In a separate library? Or in base? And should it really be in a GHC namespace? The functionality is not bound to GHC. Perhaps something in data would be more appropriate.

Erik

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries