Proxy, new Typeable, and type-level equality

[Richard Eisenberg]

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
>