haskell - TypeRep和 "Type"GADT之间的关系

Question

在Scrap your boilerplate reloaded中，作者描述了Scrap Your Boilerplate的新表示形式，它应该与原始版本等效。

但是，不同之处在于，它们假设使用GADT编码的一组有限，封闭的“基本”类型

data Type :: * -> * where
  Int :: Type Int
  List :: Type a -> Type [a]
  ...

在原始SYB中，使用类型安全的强制类型转换，并使用 Typeable类实现。

我的问题是:

这两种方法之间的关系是什么？

为什么为“SYB重新加载”演示文稿选择了GADT表示形式？

Answer 1

[我是“SYB Reloaded”论文的作者之一。]

TL; DR 我们真的只是使用它，因为它对我们来说似乎更漂亮。基于类的Typeable方法更实用。 Spine View 可以与Typeable类结合使用，并且不依赖于Type GADT。

本文在结论中对此进行了陈述:

Our implementation handles the two central ingredients of generic programming differently from the original SYB paper: we use overloaded functions with explicit type arguments instead of overloaded functions based on a type-safe cast 1 or a class-based extensible scheme [20]; and we use the explicit spine view rather than a combinator-based approach. Both changes are independent of each other, and have been made with clarity in mind: we think that the structure of the SYB approach is more visible in our setting, and that the relations to PolyP and Generic Haskell become clearer. We have revealed that while the spine view is limited in the class of generic functions that can be written, it is applicable to a very large class of data types, including GADTs.

Our approach cannot be used easily as a library, because the encoding of overloaded functions using explicit type arguments requires the extensibility of the Type data type and of functions such as toSpine. One can, however, incorporate Spine into the SYB library while still using the techniques of the SYB papers to encode overloaded functions.

因此，主要是为了清楚起见，我们选择使用GADT进行类型表示。正如Don在回答中所说的那样，此表示形式有一些明显的优点，即它保持有关类型表示形式的静态信息，并且使我们无需任何进一步的魔术，尤其是无需使用，即可实现强制类型转换。的 unsafeCoerce。类型索引函数也可以通过在类型上使用模式匹配来直接实现，而不会退回到各种组合器，例如 mkQ或 extQ。

事实是，我(我认为是合著者)根本不喜欢 Typeable类。 (实际上，我仍然没有，尽管现在终于变得更加严格了，因为GHC为 Typeable添加了自动派生功能，使其具有多态性，并最终消除了定义自己的实例的可能性。)此外， Typeable可能还不像现在那样成熟和广为人知，因此似乎很有吸引力，可以使用GADT编码对其进行“解释”。而且，这是我们还考虑将Hastell添加 open datatypes，从而减轻GADT关闭的限制的时候。

因此，总结一下:如果您实际上只需要一个封闭的Universe的动态类型信息，那么我总是会选择GADT，因为您可以使用模式匹配来定义类型索引的函数，而不必依赖 unsafeCoerce或高级编译器魔术。但是，如果对于通用编程设置来说，宇宙是很普遍的(这很普遍)，那么GADT方法可能是有启发性的，但不切实际，并且使用 Typeable是可行的方法。

但是，正如我们在论文的结论中也指出的那样，选择 Type而不是 Typeable并不是我们正在做出其他选择的先决条件，即使用 Spine View ，我认为这是更重要的，而且实际上是核心的纸。

论文本身(在第8节中)展示了一种受 "Scrap your Boilerplate with Class"论文启发的变体，该论文使用了带有类约束的 Spine View 。但是我们也可以进行更直接的开发，下面我将进行演示。为此，我们将使用 Typeable中的 Data.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。