Proxy, new Typeable, and type-level equality
Edward A Kmett
ekmett at gmail.com
Thu Apr 4 17:11:57 CEST 2013
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
More information about the Libraries
mailing list