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

Предположим, мы определяем 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.


haskell gadt
person Community    schedule 30.10.2010    source источник

Ответы (1)


arrow_upward
11
arrow_downward

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

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

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 a a) в нечто типа (Eq a b) с помощью оператора приведения Data.Typeable. Это будет работать только тогда, когда a и b равны!

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

Тяжелая работа уже сделана.

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

person Conor McBride    schedule 31.10.2010
comment
Надежно упаковано, пока никто не сделал неправильный экземпляр Data.Typeable для чего-либо. (deriving Typeable всегда в безопасности.) - person GS - Apologise to Monica; 31.10.2010
comment
Обратите внимание, что в настоящее время eq доступен в модуле Data.Typeable как eqT - person Benjamin Hodgson♦; 05.09.2016