Re: Proxy, new Typeable, and type-level equality

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