Proxy, new Typeable, and type-level equality
eir at cis.upenn.edu
Wed Apr 24 15:34:04 CEST 2013
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.
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!
> 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.
> 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...
More information about the Libraries