haskell - 将多态数据结构提升为 GADT 的类型的运行时比较

Question

假设我们定义一个 GADT 来比较类型:

data EQT a b where
  Witness :: EQT a a

是否可以使用以下类型签名声明函数eqt:

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

...如果 typeOf x == typeOf y，eqt x y 的计算结果为 Just Witness --- 否则为 >什么都没有？

函数 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 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 强制转换运算符就足以完成此工作。它是当然是作弊，但要安全地包装作弊。