多态变异-> GADT？

Question

我正在编写一个Prolog系统，并且使用多态变体来表示Prolog术语。

特别是，我使用多态变体(而不是常规变量)，以便在确保OCaml对子类型的匹配进行出色的穷尽性检查的同时进行子类型。

到现在为止还好!

我曾多次阅读关于GADT(在discuss.ocaml.org和realworldocaml.org上)的文章。在我看来，GADT似乎提供了类似的特性，但内存占用却更小:多态变体在有多个参数的情况下，需要一个常规变量不需要的额外指针。

到目前为止，我还不能成功地使用GADT，所以我的问题是：

是否有一种简单、直接的方法将使用多态变体的代码转换为GADT？这在一般情况下都有可能吗？

提前谢谢你！

Answer 1

是否有一种简单、直接的方法将使用多态变体的代码转换为GADT？这在一般情况下可能吗？

不，因为一般来说，它们的用途完全不同。

多态变体为sum类型提供子类型。GADT为sum类型变体启用约束。

但是，您可以使用这两种技术将sum类型划分为包含超级类型的商数类型集。您甚至可以使用幻影多态变体作为每个子集的见证类型。

让我们做一些编码，假设我们有一组数字，我们想细分成两个不相交的圆和矩形子集。

使用多态变体，

  type circle = [ `circle of int]
  type rectangle = [`rectangle of int * int]
  type figure = [circle | rectangle]

和使用GADT的相同

  type circle = Is_circle
  type rectangle = Is_rectangle
  type _ figure =
    | Circle : int -> circle figure
    | Rectangle : int * int -> rectangle figure

注意，约束是如何用circle和rectangle类型显式表示的。我们甚至可以使用多态变量来见证约束。只要类型检查器能够区分约束中的两种类型(即，抽象类型不能工作，因为它们的实现可能是相等的)，任何东西都会工作。

现在让我们来做一些涉及子类型的操作。让我们从多态变体开始

  let equal_circle (`circle r1) (`circle r2) = r1 = r2

  let equal_rectangle (`rectangle (x1,y1)) (`rectangle (x2,y2)) =
    x1 = x2 && y1 = y2

  let equal_figure x y = match x,y with
    | (#circle as x), (#circle as y) ->
      equal_circle x y
    | (#rectangle as x), (#rectangle as y) ->
      equal_rectangle x y
    | #rectangle, #circle
    | #circle, #rectangle -> false 

到目前一切尚好。一个小小的警告是，我们的equal_circle和equal_rectangle函数有点多态，但是可以通过添加适当的类型约束或具有模块签名(我们总是使用模块签名，对吗？)来轻松地解决这个问题。

现在让我们用GADT实现同样的，慢慢地，

  let equal_circle (Circle x) (Circle y) = x = y

  let equal_rectangle (Rectangle (x1,y1)) (Rectangle (x2,y2)) =
    x1 = x2 && y1 = y2

看起来和多义的例子一样，模组小的句法差异。val equal_circle : circle figure -> circle figure -> bool，这种类型看起来也很不错，也很精确。不需要额外的约束，类型检查器正在为我们做我们的工作。

好的，现在让我们尝试编写超级方法，第一次尝试将不起作用：

  (* not accepted by the typechecker *)
  let equal_figure x y = match x,y with
    | (Circle _ as x), (Circle _ as y) ->
      equal_circle x y
    | (Rectangle _ as x), (Rectangle _ as y) ->
      equal_rectangle x y

对于GADT，默认情况下类型检查器将选择一个具体的类型索引，因此类型检查器将选择任意一个索引，而不是指定'a figure -> 'b figure -> bool类型，在我们的示例中，它是circle，并抱怨rectangle figure不是circle figure。没问题，我们可以直截了当地说，我们要允许任意数字的比较，

  let equal_figure : type k. k figure -> k figure -> bool =
    fun x y -> match x,y with
      | (Circle _ as x), (Circle _ as y) ->
        equal_circle x y
      | (Rectangle _ as x), (Rectangle _ as y) ->
        equal_rectangle x y

这个type k对类型检查器说：“概括所有出现的k”。因此，我们现在有了一个方法，它的类型与用多态变量实现的相应方法略有不同。它可以比较相同类型的图形，但不能比较不同类型的图形，即它具有'a figure -> 'a figure -> bool类型。你不能用多态变体来表达的东西，事实上，多态变体的相同实现并不是详尽无遗的，

  let equal_figure x y = match x,y with (* marked as non-exhaustive *)
    | (#circle as x), (#circle as y) ->
      equal_circle x y
    | (#rectangle as x), (#rectangle as y) ->
      equal_rectangle x y

当然，我们可以实现一种更通用的方法，它可以使用GADT对任意图形进行比较，例如，下面的定义具有'a figure -> 'b figure -> bool类型

  let equal_figure' : type k1 k2. k1 figure -> k2 figure -> bool =
    fun x y -> match x,y with
      | (Circle _ as x), (Circle _ as y) ->
        equal_circle x y
      | (Rectangle _ as x), (Rectangle _ as y) ->
        equal_rectangle x y
      | Rectangle _, Circle _
      | Circle _, Rectangle _ -> false

我们立即看到，就我们的目的而言，GADT是一个更强大的工具，可以让我们更好地控制约束。考虑到我们可以使用多态变量和对象类型作为表示约束的类型索引，我们可以从这两个世界中得到最好的结果--细粒度约束和子类型。

老实说，您可以使用无标记-最终风格实现与GADT相同的结果，但不使用GADT。但这是一个实现细节，有时在实践中很重要。GADT的主要问题是它们不能序列化。实际上，你不能存储幻影类型。

总之，无论您使用的是GADT还是无标记的最终样式，您都可以更好地控制类型约束，并且可以更清楚地表达您的意图(并让类型检查器强制执行它)。我们在BAP中经常使用它来表示格式良好的程序的复杂约束，例如，将位向量运算应用于相同长度的向量。这使我们能够在分析中忽略格式错误的程序，并节省了几行代码和几个小时的调试时间。

答案，即使是简单的例子，已经变得太大了，所以我必须停止。我建议您访问discuss.ocaml.org并在那里搜索GADT和多态变体。我记得在那里进行了一些更彻底的讨论。

dicuss.ocaml.org的一些更深入的讨论

1. https://discuss.ocaml.org/t/do-i-need-polymorphic-variants/
2. https://discuss.ocaml.org/t/what-is-the-right-way-to-add-constraints-on-a-type-to-handle-recursive-structures-with-variants-and-to-combine-fragments-of-types/
3. https://discuss.ocaml.org/t/narrowing-variant-types-alternatives/