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 xy评估为Just Witness ，否则为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

现在我可以尝试使用 Data.Typeable 的强制转换运算符将 (Refl :: Eq aa) 转换为类型 (Eq ab) 的东西。只有当 a 和 b 相等时才会起作用！

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

艰苦的工作已经完成。

可以在 Data.Witness 库中找到有关此主题的更多变体，但 Data.Typeable 转换运算符是这项工作所需要的。当然，这是作弊，但安全包装的作弊。