在重新加载的废锅炉板中,作者描述了废锅炉板的新演示,该演示应该与原始演示等效。
然而,一个区别是,它们假设了一个有限的、封闭的"基本"类型集,用GADT 编码
data Type :: * -> * where
Int :: Type Int
List :: Type a -> Type [a]
...
在最初的SYB中,使用类型安全转换,使用Typeable
类实现。
我的问题是:
- 这两种方法之间有什么关系
- 为什么选择GADT代表作为"SYB Reloaded"演示
[我是"SYB Reloaded"论文的作者之一。]
TL;DR我们真的只是使用了它,因为它对我们来说更漂亮。基于类的Typeable
方法更实用。Spine
视图可以与Typeable
类组合,并且不依赖于Type
GADT。
论文在结论中指出了这一点:
我们的实现处理泛型编程的两个核心成分,这与最初的SYB论文不同:我们使用重载函数显式类型参数,而不是基于类型安全的重载函数cast 1或基于类的可扩展方案[20];我们使用显式脊椎视图,而不是基于组合子的方法。两项更改都是独立的我们认为SYB方法的结构在我们的环境中更为明显,并且对PolyP和Generic Haskell的理解变得更加清晰。我们已经透露spine视图仅限于可编写的泛型函数类适用于包括GADT在内的一大类数据类型。
我们的方法不能很容易地用作库,因为使用显式类型参数的重载函数需要Type数据类型和函数(如toSpine)。然而,可以将Spine合并到SYB库中,同时仍然使用SYB的技术对重载函数进行编码的纸张。
因此,我们选择使用GADT进行类型表示主要是为了清楚起见。正如Don在回答中所说,这种表示有一些明显的优势,即它维护了关于类型表示用于什么类型的静态信息,并且它允许我们在没有任何进一步魔法的情况下实现强制转换,特别是在不使用unsafeCoerce
的情况下。类型索引函数也可以通过对类型使用模式匹配来直接实现,而不需要回退到各种组合子,如mkQ
或extQ
。
事实上,我(以及我认为的合著者)只是不太喜欢Typeable
类。(事实上,我仍然没有,尽管GHC为Typeable
添加了自动派生,使其具有多态性,并最终消除了定义自己实例的可能性,这一点现在终于变得更加严格了。)此外,Typeable
可能还没有现在那么成熟和广为人知,所以使用GADT编码来"解释"它似乎很有吸引力。此外,当时我们还考虑向Haskell添加开放数据类型,从而减轻GADT关闭的限制。
因此,总结一下:如果你实际上只需要一个封闭的宇宙的动态类型信息,我总是选择GADT,因为你可以使用模式匹配来定义类型索引函数,而且你不必依赖unsafeCoerce
或高级编译器魔术。然而,如果宇宙是开放的,这是很常见的,当然对于通用编程设置来说,那么GADT方法可能很有指导意义,但并不实用,使用Typeable
是可行的。
然而,正如我们在论文结论中所指出的,选择Type
而不是Typeable
并不是我们正在做出的另一个选择的先决条件,即使用Spine
观点,我认为这更重要,也是论文的核心。
论文本身显示了(在第8节中)一个变体,其灵感来自"用类废弃锅炉板"论文,该论文使用了带有类约束的Spine
视图。但我们也可以做一个更直接的发展,我在下面展示。为此,我们将使用Data.Typeable
中的Typeable
,但定义我们自己的Data
类,为了简单起见,它只包含toSpine
方法:
class Typeable a => Data a where
toSpine :: a -> Spine a
Spine
数据类型现在使用Data
约束:
data Spine :: * -> * where
Constr :: a -> Spine a
(:<>:) :: (Data a) => Spine (a -> b) -> a -> Spine b
函数fromSpine
与其他表示形式一样微不足道
fromSpine :: Spine a -> a
fromSpine (Constr x) = x
fromSpine (c :<>: x) = fromSpine c x
Data
的实例对于平面类型(如Int
:)来说是微不足道的
instance Data Int where
toSpine = Constr
对于二叉树这样的结构化类型,它们仍然是完全简单的:
data Tree a = Empty | Node (Tree a) a (Tree a)
instance Data a => Data (Tree a) where
toSpine Empty = Constr Empty
toSpine (Node l x r) = Constr Node :<>: l :<>: x :<>: r
然后,本文继续定义了各种通用函数,如mapQ
。这些定义几乎没有改变。我们只得到Data a =>
的类约束,其中本文有Type a ->
:的函数自变量
mapQ :: Query r -> Query [r]
mapQ q = mapQ' q . toSpine
mapQ' :: Query r -> (forall a. Spine a -> [r])
mapQ' q (Constr c) = []
mapQ' q (f :<>: x) = mapQ' q f ++ [q x]
更高级别的函数,如everything
,也只是丢失了它们的显式类型参数(然后实际上看起来与原始SYB完全相同):
everything :: (r -> r -> r) -> Query r -> Query r
everything op q x = foldl op (q x) (mapQ (everything op q) x)
如上所述,如果我们现在想定义一个通用和函数来总结所有Int
的出现,我们就不能再进行模式匹配,而是必须回到mkQ
,但mkQ
纯粹是根据Typeable
定义的,并且完全独立于Spine
:
mkQ :: (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
(r `mkQ` br) a = maybe r br (cast a)
然后(同样与最初的SYB完全一样):
sum :: Query Int
sum = everything (+) sumQ
sumQ :: Query Int
sumQ = mkQ 0 id
对于本文后面的一些内容(例如,添加构造函数信息),还需要做更多的工作,但这些都可以完成。因此,使用Spine
实际上根本不依赖于使用Type
。
很明显,Typeable
的使用是开放的——可以在事后添加新的变体,而无需修改原始定义。
然而,重要的变化是TypeRep
是非类型化的。也就是说,运行时类型TypeRep
和它编码的静态类型之间没有连接。使用GADT方法,我们可以对类型a
与其Type
之间的映射进行编码,由GADTType a
给出。
因此,我们烘焙了类型rep静态链接到其原始类型的证据,并可以使用Type a
编写静态类型的动态应用程序(例如),作为我们有运行时a
的证据。
在旧的TypeRep案例中,我们没有这样的证据,它归结为运行时字符串相等,以及通过fromDynamic
实现最好的强制和希望。
比较签名:
toDyn :: Typeable a => a -> TypeRep -> Dynamic
与GADT风格:
toDyn :: Type a => a -> Type a -> Dynamic
我不能伪造我的类型证据,我可以在以后重建东西时使用它,例如,当我只有一个Type a
时,查找a
的类型类实例。