TypeRep与"Type"GADT的关系

Question

在Scrap中你的样板重新加载,作者描述了一个新的Scrap Your Boilerplate演示文稿,它应该与原版相同.

然而,一个不同之处在于它们假设一组有限的,基本的"基础"类型,用GADT编码

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

在原始SYB中,使用类型安全转换,使用Typeable类实现.

我的问题是:

• 这两种方法之间有什么关系？
• 为什么GADT表示被选为"SYB Reloaded"演示文稿？

Answer 1

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

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

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

在旧的 TypeRep 案例中，我们没有这样的证据，这取决于运行时字符串相等性，以及通过fromDynamic.

比较签名：

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

与 GADT 风格相比：

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

我不能伪造我的类型证据，并且稍后在重建事物时我可以使用它，例如当a我拥有的只是Type a.

Answer 2

[我是《SYB Reloaded》论文的作者之一。]

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

该论文在结论中指出：

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

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

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

事实上，我（以及我认为合著者）根本不太喜欢这门课Typeable。（事实上​​，我仍然没有，尽管它现在终于变得更加有纪律了，因为 GHC 添加了自动派生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)

正如我上面所说，如果我们现在想要定义一个对所有Int出现的情况进行求和的通用求和函数，我们就不能再进行模式匹配，而必须回退到mkQ, butmkQ纯粹是根据 定义的，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