结合参数多态性和多态变体（反引号类型）

Question

假设我有一个由多个多态变体（协变）组成的类型，如下所示：

[> `Ok of int | `Error of string]

让我们进一步假设我想将此定义分解为某种类型构造函数和一个具体类型int。我的第一次尝试如下：

type 'a error = [> `Ok of 'a | `Error of string]

然而，使用这样的定义会产生一个非常奇怪的类型错误，提到一个'b没有出现在定义中任何地方的类型变量。

$ ocaml
        OCaml version 4.07.0

# type 'a error = [> `Ok of 'a | `Error of string ];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound

这'b是一个自动生成的名称，添加一个显式'b将变量转换为'c.

$ ocaml
        OCaml version 4.07.0

# type ('a, 'b) error = [> `Ok of 'a | `Error of 'b ];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of 'b | `Ok of 'a ] as 'c the variable 'c is unbound

[ `Thing1 of type1 | `Thing2 of type 2 ]在这种情况下，使用不变构造似乎可以正常工作。

$ ocaml
        OCaml version 4.07.0

# type 'a error = [ `Ok of 'a | `Error of string ] ;;
type 'a error = [ `Error of string | `Ok of 'a ]
#

但是，将类型参数显式标记为协变并不能挽救原始示例。

$ ocaml
        OCaml version 4.07.0

# type +'a error = [> `Ok of 'a | `Error of string];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound

而且，为了更好的衡量，添加逆变注释也不起作用。

$ ocaml
        OCaml version 4.07.0

# type -'a error = [> `Ok of 'a | `Error of string];;
Error: A type variable is unbound in this type declaration.
In type [> `Error of string | `Ok of 'a ] as 'b the variable 'b is unbound

试图猜测编译器将用于未绑定类型变量的名称并将其添加为左侧的参数也不起作用，并会产生非常奇怪的错误消息。

$ ocaml
        OCaml version 4.07.0

# type ('a, 'b) string = [> `Ok of 'a | `Error of string] ;;
Error: The type constructor string expects 2 argument(s),
       but is here applied to 0 argument(s)

有没有办法制作一个类型构造函数，可以有效地“替换不同类型”的 int in [> `Ok of int | `Error of string]？

Answer 1

这不是方差或参数多态性的问题，而是行多态性的问题。当您添加>或<同时添加一个隐式类型变量时，行变量将保存“完整”类型。您可以在错误中看到此类型变量显式：

[> `Error of string | `Ok of 'a ] as 'b

注意最后的as 'b部分。

为了给类型添加别名，您必须使类型变量显式，以便您可以将其作为别名上的类型参数引用：

type ('a, 'r) error = [> `Ok of 'a | `Error of string ] as 'r

另请注意，如果您遇到或何时遇到对象，这也适用于那里。一个对象类型..有一个隐式类型变量，你需要显式地为它设置别名：

type 'r obj = < foo: int; .. > as 'r