为GADT定义自己的Typeable实例

Question

有人能指出我在Haskell中为GADT定义Typeable或Typeable1实例的一组很好的例子.

或者,有人可以向我展示如何为以下GADT定义Typeable(手动).

data V a where
    Unit :: V () 
    Pair :: V a -> V b -> V (a, b) 
    L :: V a -> V (Either a b) 
    R :: V b -> V (Either a b) 
    Fresh :: Int -> V a

或者,指向介绍该想法的论文的指针也会有所帮助.

Answer 1

看起来这个网站现在已经不见了,但是这个回归机器仍然有链接到所有原始论文的网站:http://web.archive.org/web/20080622204226/http: //www.cs.vu.nl/样板/

无论如何,Typeable几乎是完全机械的.你可以通过DeriveDataTypeable扩展来派生它,甚至是GADT.至少在那种情况下* -> *,如你的例子.

我还举一个手动提供Typeable1实例的例子,但它将在下一版本的GHC中弃用.用于手动创建实例的接口正在发生变化.

{-# NOINLINE vTyCon #-}
vTyCon :: TyCon
vTyCon = mkTyCon "ModuleName.V"

instance Typeable1 V where
    typeOf1 _ = mkTyConApp vTyCon []

该NOINLINEpragma实际上很重要,因为mkTyCon在引擎盖下做了不安全的事情.这就是为什么最好让GHC手动派生实例,如果可能的话.

我的理解是GHC未来版本中将要改变的部分是你应该使用一个不同的函数mkTyCon3,它将包名,模块名和类型名作为单独的参数.这是一个明显的改进,即使支持多个版本的GHC更加强硬.请参阅:对Data.Typeable的更改.