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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
