rep*_*eat 4 ocaml gadt subtyping polymorphic-variants
我正在编写一个 Prolog 系统，并且使用多态变体来表示 Prolog 术语。
特别是，我使用多态变体（而不是常规变体），因此我可以进行子类型化，同时确保 OCaml 对子类型的匹配进行出色的详尽检查。
到目前为止，一切都很好！
我曾多次阅读过有关 GADT 的内容（在 Discuss.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), (#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 中大量使用它来表达格式良好的程序的复杂约束，例如，将位向量运算应用于相同长度的向量。这使我们能够在分析中忽略格式错误的程序，并节省几行代码和几个小时的调试时间。
即使是这个简单的例子，答案也已经变得太大了，所以我不得不停下来。我建议您访问discuss.ocaml.org并在那里搜索GADT和多态变体。我记得那里有一些更深入的讨论。