约束要求类型应该匹配时模块签名不匹配

Question

考虑以下代码:

module A = struct
module type ZType = sig
type z
end
end
module B = struct
module M (InputZ : A.ZType) = struct
module OutputZ = InputZ
end
end
module C = struct
module type CZType = sig
type z = { s : int }
end
module M (Z1 : CZType) = struct
module B1 = B.M(Z1)
module Z2 : A.ZType with type z = Z1.z = B1.OutputZ
module Z3 : CZType = Z2 (* This line gives a signature mismatch error *)
end
end

可以看到，C.CZType是A.ZType的一个更具体的版本，唯一的区别是C.CZType.z被指定为记录类型。

我本以为下面的推理链会允许这段代码进行类型检查:

1. Z2.z与Z1.z相同(由于签名约束with type z = Z1.z)
2. Z1为CZType类型
因此，Z2.z为记录{ s : int }
3. 因此Z3为CZType类型。

但这不起作用。相反，编译器报错:

Signature mismatch:
Modules do not match: sig type z = Z1.z end is not included in CZType
Type declarations do not match:
type z = Z1.z
is not included in
type z = { s : int; }
Their kinds differ.

如何让编译器相信B1.OutputZ是CZType类型?

---

Andreas Rossberg正确地识别了问题。棘手的是，在我的例子中，B不"知道"。关于C，所以它不能约束OutputZ.z有正确的类型。

为了解决这个问题，我尝试在所需的输出模块类型上进一步参数化B:

module A = struct
module type ZType = sig
type z
end
end
module type TypeModType = sig
(* It is seemingly not possible to constrain T to be a subtype of A.ZType *)
module type T
end
module B = struct
module M (TypeMod : TypeModType) = struct
module M (InputZ : TypeMod.T) = struct
module OutputZ = InputZ
type z = InputZ.z (* Now this line gives an error *)
end
end
end
module C = struct
module type CZType = sig
type z = { s : int }
end
module M (Z1 : CZType) = struct
module B1 = B.M(struct module type T = CZType end)
module B2 = B1.M(Z1)
(* This line is now fine thanks to extra parameterization *)
module Z2: CZType = B2.OutputZ
end
end

当然，现在的问题是不可能限制B参数化的模块类型的空间:它要么是all，要么是none。

---

更新

谢谢你，你的回答很有帮助。根据Andreas rosssberg的观察，OCaml发现类型标识被保留，而类型类型类型没有保留，因此修复它所需要的就是在外部定义一个适当类型的类型。下面是一个激励的例子:

module type Graph = sig
type id
type attrs
type node = {
neighbors : id list;
attrs : attrs
}
end
type point = { x: int; y: int }
module type LocatedGraph = sig
type id
type attrs = point
type node = {
neighbors : id list;
attrs : attrs
}
end
module AugmentedGraph (OrigGraph : Graph) = struct
type id = Orig of OrigGraph.id | Added of int
type attrs = OrigGraph.attrs
type node = {
neighbors : id list;
attrs : attrs
}
end
module IntLocatedGraph = struct
type id = int
type attrs = point
type node = {
neighbors : id list;
attrs : attrs
}
end
module AugmentedIntLocatedGraph = AugmentedGraph(IntLocatedGraph)
module AugmentedIntLocatedGraphIsLocatedGraph : LocatedGraph = AugmentedIntLocatedGraph

同时实现三个属性:

1. Parametricity:如果给AugmentedGraph一个LocatedGraph，结果是LocatedGraph。
2. 约束函子参数类型:AugmentedGraph只能应用于Graph或其子类型。
3. 封装:AugmentedGraph不需要知道LocatedGraph来产生LocatedGraph.

Answer 1

更简单的版本是:

module A = struct type t = {a : int} end
module B : sig type t = A.t end = A
module C : sig type t = {a : int} end = B;;
Error: Signature mismatch:
Modules do not match:
sig type t = A.t end
is not included in
sig type t = { a : int; } end
Type declarations do not match:
type t = A.t
is not included in
type t = { a : int; }
Their kinds differ.

问题是传播记录或数据类型的标识不会传播其表示(或OCaml在这里称之为"kind")。事实上，B上的签名注释隐藏了这种表示。为了保持透明，你需要写:

module A = struct type t = {a : int} end
module B : sig type t = A.t = {a : int} end = A
module C : sig type t = {a : int} end = B

推断的签名也显示如下:

module A : sig type t = { a : int; } end
module B : sig type t = A.t = { a : int; } end
module C : sig type t = { a : int; } end

现在，将这个观察结果应用到您的示例中需要做更多的工作，我将其作为练习。:)

Answer 2

在我看来，根本问题在于函子

module M (InputZ : A.ZType) = struct
module OutputZ = InputZ
end

创建一个InputZ模块的副本，该副本被限制为A.ZType模块类型，完全独立于原始模块InputZ。特别是，这意味着所有额外的信息都丢失了。这种对其参数进行限制复制的函子目前是OCaml的反模式(在某些时候将通过透明归属来解决)。

事实上，如果我们从代码中删除此副本(并修复Z2上的模块类型约束)，我们将删除类型错误:

module B = struct
module M (InputZ : A.ZType) = struct
end
end
module M (Z1 : CZType) = struct
module B = B(Z1)
module Z2 : sig type z = Z1.z = { s : int} end = Z1
module Z3 : CZType = Z2 (* we didn't lose any information, and thus this works *)
end

此外，避免函子实参复制还可以避免将来在使用应用函子时遇到麻烦。特别是，对于任何可应用的函子F，在你的实现中F(B(Z1).OutputZ)≠F(Z1)，这可能不是预期的行为。