haskell - 为 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/boilerplate/

无论如何，Typeable 几乎完全是机械的。即使对于 GADT，您也可以通过 DeriveDataTypeable 扩展来派生它。至少当类型为 * -> * 时，如您的示例所示。

我还可以给出手动提供 Typeable1 实例的示例，但它将在下一版本的 GHC 中弃用。用于手动创建实例的接口(interface)正在更改。

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

instance Typeable1 V where
    typeOf1 _ = mkTyConApp vTyCon []

NOINLINE 编译指示实际上很重要，因为 mkTyCon 在幕后做了不安全的事情。这就是为什么最好让 GHC 手动派生实例(如果可能的话)。

我的理解是，GHC future 版本中将要更改的部分是您应该使用不同的函数 mkTyCon3，它将包名称、模块名称和类型名称作为单独的参数。这是一个明显的改进，即使使支持多个版本的 GHC 变得更加困难。请参阅:Changes to Data.Typeable .

以上所有内容都非常旧。

来自 GHC 文档:

Also since GHC 7.8.1, handwritten (ie. not derived) instances of Typeable are forbidden, and will result in an error.

您永远不需要甚至被允许使用任何现代版本的 GHC 手动编写 Typeable 实例。事实上，您甚至不需要告诉 GHC 来导出它们 - 它会自动执行此操作。