用于将多态数据结构提升为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强制转换操作符是此作业所需的全部内容.当然,这是作弊,但安全包装作弊.