Hi all,
Combining ideas from a number of people/threads ("Proxy and new-typeable" [on libraries] and "RFC: Singleton equality witnesses" [on ghc-devs]), I propose this: > module GHC.TypeReasoning where > > data a :~: b where > Refl :: a :~: a > > -- with credit to Conal Elliott for 'ty' and Erik Hesselink & Martijn van Steenbergen for 'type-equality' > sym :: (a :~: b) -> (b :~: a) > trans :: (a :~: b) -> (b :~: c) -> (a :~: c) > coerce :: (a :~: b) -> a -> b > liftEq :: (a :~: b) -> (f a :~: f b) > liftEq2 :: (a :~: a') -> (b :~: b') -> (f a b :~: f a' b') > liftEq3 :: ... > liftEq4 :: ... > > instance Eq (a :~: b) where ... > instance Show (a :~: b) where ... > instance Read (a :~: a) where ... > instance Ord (a :~: b) where ... > -- what other instances? > > data Void > -- instances as in Edward Kmett's 'void' package > > absurd :: Void -> a > > type Refuted a = a -> Void > type Decision a = Proved a > | Disproved (Refuted a) > > class EqT f where > eqT :: f a -> f b -> Maybe (a :~: b) > > class EqT f => DecideEqT f where > decideEqT :: f a -> f b -> Decision (a :~: b) > > defaultEqT :: DecideEqT f => f a -> f b -> Maybe (a :~: b) -- for easy writing of EqT instances > > instance EqT ((:~:) a) where ... > instance DecideEqT ((:~:) a) where ... > module Data.Proxy where > -- as in Ben Gamari's version > module Data.Typeable ( ? , Proxy(..), (:~:)(..) ) where > > ... > import GHC.TypeReasoning > import {-# SOURCE #-} Data.Proxy > > ... > eqTypeable :: (Typeable a, Typeable b) => Maybe (a :~: b) > decideEqTypeable :: (Typeable a, Typeable b) => Decision (a :~: b) > -- can't use EqT and DecideEqT because Typeable is in Constraint, not * > > gcast :: (Typeable a, Typeable b) => c a -> Maybe (c b) -- it is now polykinded > > {-# DEPRECATED gcast1 ... #-} > {-# DEPRECATED gcast2 ... #-} > ... On top of features others have proposed/written in packages, I have added DecideEqT and related definitions. I would indeed have use for this definition, and I imagine others will, too, once it's out there. We could theoretically hold off on that one, but it seems easy enough just to put it in now, while we're all thinking about it. I've tested the definition by writing instances of singletons, and it works as desired. If this proposal is accepted, we can then look at changing some of the definitions around TypeLits as well, linking in much of the ghc-devs thread "RFC: Singleton equality witnesses". I don't see any dependencies from the code above on the TypeLits/singleton stuff, so I think we can take those changes in a second round. One question in the above code: What other instances should there be for (:~:)? Comments? Thoughts? Thanks, Richard |
On Wed, Apr 3, 2013 at 6:08 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> > Comments? Thoughts? > > Thanks, > Richard Perhaps you could steal some ideas from my type-eq library: http://hackage.haskell.org/package/type-eq -- Your ship was destroyed in a monadic eruption. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130403/109e3642/attachment.htm> |
In reply to this post by Richard Eisenberg-2
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 > |
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 > > > > An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130424/71619443/attachment.htm> |
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/ghc-devs/attachments/20130424/49b58739/attachment.htm> |
Free forum by Nabble | Edit this page |