如何解决多态变体-> GADT？

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

尤其是，我使用了 polymorphic 变体（而不是常规变体），因此我可以进行子类型化，同时确保OCaml对子类型匹配进行出色的穷举性检查。

到目前为止，太好了！

我已经多次阅读有关GADT的信息（在describe.ocaml.org和realworldocaml.org中）。对我来说，GADT似乎提供了类似的功能，但具有较小的内存占用空间：具有多个自变量的个案的多态变体需要常规变体不需要的额外指针。

到目前为止，我无法成功使用GADT，所以这是我的问题：

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

提前谢谢！

解决方法

是否存在使用多态变体将代码转换为GADT的简单明了的方法？在一般情况下甚至有可能吗？

不，因为它们通常用于完全不同的目的。

多态变体为求和类型提供子类型。 GADT为总和类型变体启用了约束。

但是，您可以同时使用两种技术将求和类型划分为构成您的超级类型的商的类型集。您甚至可以将幻影多态变体用作每个子集的见证类型。

让我们做一些编码，假设我们有一组图形，我们希望将它们细分为两个不相交的圆和矩形子集。

使用多态变体，

  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

看起来与poly例子相同，但语法上的差异很小。该类型看起来也很精确val equal_circle : circle figure -> circle figure -> bool。不需要额外的约束，类型检查器正在为我们完成工作。

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

  (* 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),(#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,(Rectangle _ as y) ->
        equal_rectangle x y
      | Rectangle _,Circle _
      | Circle _,Rectangle _ -> false

我们立即发现，对于我们而言，GADT是功能更强大的工具，可让我们对约束进行更多控制。并且考虑到我们可以使用多态变体和对象类型作为类型索引来表达约束，我们可以从两个世界中获得最好的选择：细粒度约束和子类型化。

说实话，您可以使用tagless-final style获得与GADT相同但没有GADT的结果。但这是一个实现细节，有时在实践中很重要。 GADT的主要问题是它们不可序列化。确实，您无法存储幻像类型。

总而言之，无论您使用的是GADT还是Tagless-Final Style，您都可以更好地控制类型约束，并且可以更清楚地表达您的意图（并让类型检查器强制实施）。我们在BAP中经常使用它来表达格式良好的程序的复杂约束，例如，bitvector operations被应用于相同长度的向量。这使我们能够在分析中忽略格式错误的程序，并节省了几行代码和几小时的调试。

即使有一个简单的例子，答案也已经变得太大了，所以我必须停下来。建议您访问discuss.ocaml.org，然后在其中搜索GADT和多态变体。我记得那里有一些更详尽的讨论。

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