9

在Scrap your Boilerplate reloaded 中，作者描述了Scrap Your Boilerplate的新演示文稿，它应该与原版等效。

但是，一个区别是它们假设了一组有限的、封闭的“基本”类型，用 GADT 编码

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

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

我的问题是：

  • 这两种方法之间有什么关系？
  • 为什么为“SYB Reloaded”演示选择了 GADT 表示？
4

2 回答 2

5

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

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

该论文在其结论中指出了这一点：

我们的实现处理泛型编程的两个核心要素与原始 SYB 论文不同：我们使用具有显式类型参数的重载函数，而不是基于类型安全强制转换1或基于类的可扩展方案 [20] 的重载函数；我们使用显式脊椎视图而不是基于组合器的方法。这两个变化是相互独立的，并且是在明确的基础上做出的：我们认为 SYB 方法的结构在我们的环境中更加明显，并且与 PolyP 和 Generic Haskell 的关系变得更加清晰。我们发现，虽然脊椎视图仅限于可编写的通用函数类，但它适用于包括 GADT 在内的非常大的数据类型。

我们的方法不能轻易地用作库，因为使用显式类型参数对重载函数的编码需要 Type 数据类型和函数（如 toSpine）的可扩展性。但是，可以将 Spine 合并到 SYB 库中，同时仍然使用 SYB 论文的技术来编码重载函数。

因此，我们选择使用 GADT 进行类型表示主要是为了清楚起见。正如 Don 在他的回答中所说，这种表示有一些明显的优势，即它维护关于类型表示的类型的静态信息，并且它允许我们实现强制转换而无需任何进一步的魔法，特别是无需使用的unsafeCoerce。类型索引函数也可以通过在类型上使用模式匹配直接实现，而无需回退到各种组合器，例如mkQor extQ。

事实是我（我认为是合著者）根本就不是很喜欢这Typeable门课。（事实上​​，我仍然没有，尽管它现在终于变得更加自律了，因为 GHC 添加了自动派生 for Typeable，使其具有多态性，并最终消除了定义您自己的实例的可能性。）此外,Typeable并没有现在那么成熟和广为人知，因此使用 GADT 编码来“解释”它似乎很有吸引力。而且，这个时候我们也在考虑给 Haskell 添加开放数据类型，从而缓解 GADT 封闭的限制。

所以，总结一下：如果你真的只需要一个封闭宇宙的动态类型信息，我总是选择 GADT，因为你可以使用模式匹配来定义类型索引函数，你不必依赖unsafeCoerce也不需要高级编译器魔术。但是，如果宇宙是开放的，这很常见，当然对于通用编程设置，那么 GADT 方法可能是有指导意义的，但不实用，使用Typeable是要走的路。

然而，正如我们在论文的结论中所说的那样，选择TypeoverTypeable并不是我们正在做出的另一个选择的先决条件，即使用Spine视图，我认为这是更重要的，也是论文的核心.

论文本身（在第 8 节中）展示了一个受“Scrap your Boilerplate with Class”论文启发的变体，它使用了一个Spine带有类约束的视图。但是我们也可以做一个更直接的开发，我将在下面展示。为此，我们将使用Typeablefrom 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)

正如我上面所说，如果我们现在想要定义一个通用的 sum 函数来总结所有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。

于 2013-03-01T17:30:13.147 回答
5

好吧，显然Typeable使用是开放的——事后可以添加新的变体，而无需修改原始定义。

不过，重要的变化是它TypeRep是无类型的。也就是说，运行时类型 ,TypeRep和它编码的静态类型之间没有任何联系。使用 GADT 方法，我们可以对类型a与其之间的映射进行编码Type，由 GADT 给出Type a。

因此，我们为类型 rep 静态链接到其原始类型提供证据，并且可以使用Type a作为我们有运行时的证据来编写静态类型的动态应用程序（例如） a。

在较旧的 TypeRep 案例中，我们没有这样的证据，它归结为运行时字符串相等，以及通过fromDynamic.

比较签名：

toDyn :: Typeable a => a -> TypeRep -> Dynamic

与 GADT 风格相比：

toDyn :: Type a => a -> Type a -> Dynamic

我不能伪造我的类型证据，我可以稍后在重建事物时使用它，例如查找类型类实例，以了解a我只有一个Type a.

于 2013-03-01T15:33:11.873 回答