Proxy, new Typeable, and type-level equality

3 Apr 2013

      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

Richard Eisenberg

Bas van Dijk

Edward Kmett

Gábor Lehel

Erik Hesselink

Edward A Kmett

Richard Eisenberg

José Pedro Magalhães

Richard Eisenberg

Twan van Laarhoven

tags

participants (8)