Proxy, new Typeable, and type-level equality

[Richard Eisenberg]

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 <jpm at cs.uu.nl> 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 <eir at cis.upenn.edu> 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 <ekmett at gmail.com> 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 <hesselink at gmail.com> wrote:
> >
> >> On Wed, Apr 3, 2013 at 6:08 PM, Richard Eisenberg <eir at cis.upenn.edu> 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 at haskell.org
> >> http://www.haskell.org/mailman/listinfo/libraries
> >
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130424/49b58739/attachment.htm>