抽象型协方差/反方差

Question

我在玩这个代码，但我不明白。

type t1 = [ `A ];;
type t2 = [ t1 | `B ] ;;
type t3 = [ t2 | `C ] ;;

module type MT =
sig
  type ('a,'b) fct
  val create : ('a -> 'b) -> ('a,'b) fct
end;;

module Mt : MT =
struct
    type ('a,'b) fct = 'a -> 'b
    let create f = f
end;;

let f = (fun x -> x : t2 -> t2) ;;
let af = Mt.create (fun x -> x : t2 -> t2);;

(f :> t1 -> t3);;
(af :> (t1, t3) Mt.fct);;

像这样，它不起作用，因为编译器不知道Mt.fct的类型参数是协变的还是反差的。但是，如果将模块签名中的类型声明替换为：

type (-'a,'+b) fct

告诉编译器b是协变量和反变体，现在它起作用了。因为我是一个棘手的小烦人的男孩，我试图欺骗编译器，告诉他，a也是协变的！

type (+'a,'+b) fct

他比我聪明，他注意到我在骗他。

Type declarations do not match:
         type ('a, 'b) fct = 'a -> 'b
       is not included in
         type (+'a, +'b) fct
       Their variances do not agree.

我的问题是:如果他知道类型参数的变化，为什么它不直接将它用于我的模块，而不是强迫我添加那些+和-。这又是一个决定性的问题吗？

Answer 1

类型归属Mt : MT是不透明的。因此编译器不能使用有关类型定义的信息，因为您可以随时更改定义(可以单独编译)。看这个，如果你看到

module type MT =
sig
  type ('a,'b) fct = 'a -> 'b
  val create : ('a -> 'b) -> ('a,'b) fct
end;;

然后，您编写的代码编译得很好。

Answer 2

虽然编译器可以在特定的参数位置上检查您的类型实际上是协变还是反变体，但它并不立即假定这是您希望在抽象类型中公开的信息。毕竟，一旦编译器知道了参数的变化，那么它就可以根据需要对该参数执行强制--这可能根本不是您的公共API的一部分！