Сравнение типов во время выполнения для подъема полиморфных структур данных в GADT

Question

Предположим, мы определили GADT для сравнения типов:

data EQT a b where
  Witness :: EQT a a

Можно ли тогда объявить функцию eqt со следующей сигнатурой типа:

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

... так, что eqt xy оценивается как Just Witness , если typeOf x == typeOf y --- и в противном случае Nothing

Функция eqt позволит поднять обычные полиморфные структуры данных в GADT.

Answer 1

Да, это так.Вот один из способов:

Во-первых, тип равенства типов.

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

Обратите внимание, что он сам может быть создан как экземпляр Typeable.Это ключ.Теперь мне просто нужно взять в руки нужный мне Refl, вот так.

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

И теперь я могу попытаться превратить (Refl :: Eq aa) в нечто типа (Eq ab), используяОператор приведения Data.Typeable.Это сработает только тогда, когда a и b равны!

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

Тяжелая работа уже выполнена.

Дополнительные варианты этой темы можно найти в библиотеке Data.Witness, нооператор Data.Typeable - это все, что вам нужно для этой работы.Это, конечно, измена, но надежная измена.