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 <e...@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 <ekm...@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 <hessel...@gmail.com> wrote: > > > >> On Wed, Apr 3, 2013 at 6:08 PM, Richard Eisenberg <e...@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 > >> librar...@haskell.org > >> http://www.haskell.org/mailman/listinfo/libraries > > > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
