Runtime comparison of types for lifting polymorphic data structures into GADTs.

Question

Suppose we define a GADT for comparison of types:

data EQT a b where
  Witness :: EQT a a

Is it then possible to declare a function eqt with the following type signature:

eqt :: (Typeable a, Typeable b) => a -> b -> Maybe (EQT a b)

...such that eqt x y evaluates to Just Witness if typeOf x == typeOf y --- and otherwise to Nothing?

The function eqt would make it possible to lift ordinary polymorphic data structures into GADTs.

Answer 1

Yes it is. Here's one way:

First, the type-equality type.

data EQ :: * -> * -> * where
  Refl :: EQ a a  -- is an old traditional name for this constructor
  deriving Typeable

Note that it can itself be made an instance of Typeable. That's the key. Now I just need to get my hands on the Refl I need, like this.

refl :: a -> EQ a a
refl _ = Refl

And now I can try to turn (Refl :: Eq a a) into something of type (Eq a b) by using Data.Typeable's cast operator. That will work just when a and b are equal!

eq :: (Typeable a, Typeable b) => a -> b -> Maybe (EQ a b)
eq a _ = cast (refl a)

The hard work has already been done.

More variations on this theme can be found in the Data.Witness library, but the Data.Typeable cast operator is all you need for this job. It's cheating, of course, but safely packaged cheating.