我正在编写一个 Prolog 系统，并且我正在使用多态变体来表示 Prolog 术语。
特别是，我使用多态变体（而不是常规变体），因此我可以进行子类型化，同时确保 OCaml 对子类型匹配的出色详尽性检查。
到目前为止，一切都很好！
在多个场合，我一直在阅读有关 GADT 的信息（在讨论.ocaml.org 和 realworldocaml.org 上）。对我来说，GADT 似乎提供了类似的功能，但内存占用更小：具有多个参数的案例的多态变体需要一个常规变体不需要的额外指针。
到目前为止，我还没有成功使用 GADT，所以这是我的问题：
是否有一种简单、直接的方法可以将使用多态变体的代码转换为 GADT？在一般情况下这甚至可能吗？
先感谢您！
是否有一种简单、直接的方法可以将使用多态变体的代码转换为 GADT？在一般情况下这甚至可能吗？
不，因为它们通常用于完全不同的目的。
多态变体为总和类型提供子类型。GADT 启用总和类型变体的约束。
但是，您可以使用这两种技术将 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_circleandequal_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. 不需要额外的约束，类型检查器正在为我们做我们的工作。
OK，现在我们尝试写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”。所以我们现在有一个方法，它的类型与使用多态变体实现的相应方法略有不同。它可以比较相同种类的图形，但不能比较不同种类的图形，即它有 type '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 是一个更强大的工具，可以让我们更好地控制约束。鉴于我们可以使用多态变体和对象类型作为类型索引来表达约束，我们可以从两个世界中获得最好的——细粒度约束和子类型。
老实说，使用 tagless -final 样式，您可以获得与使用 GADT 但没有 GADT 相同的结果。但这是一个实现细节，在实践中有时很重要。GADT 的主要问题是它们不可序列化。实际上，您不能存储幻像类型。
总而言之，无论您使用的是 GADT 还是 Tagless-Final Style，您都可以更好地控制类型约束，并且可以更清楚地表达您的意图（并让类型检查器强制执行它）。我们在 BAP 中大量使用它来表达格式良好的程序的复杂约束，例如，位向量操作应用于相同长度的向量。这使我们能够在分析中忽略格式错误的程序，并为我们节省几行代码和几个小时的调试时间。
答案，即使是这个简单的例子，已经变得太大了，所以我不得不停下来。我建议您访问讨论.ocaml.org 并在那里搜索 GADT 和多态变体。我记得那里有一些更深入的讨论。