当约束说类型应该匹配时模块签名不匹配

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

3. 因此，

   Z2.z

   是记录

   { s : int }

4. 因此，

   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

参数化的模块类型的空间：它要么全部要么没有。

---

更新

谢谢，回复很有帮助。使用 Andreas Rossberg 的观察，即 OCaml 看到类型 identity 被保留但类型 kind 没有保留，修复它所需要做的就是在外部定义适当种类的类型。下面是一个激励人心的例子：

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. Constraining functor argument types:

   AugmentedGraph

   can only be applied to a

   Graph

   or its subtypes.
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.

问题是传播记录或数据类型的identity不会传播它的representation（或“种类”，OCaml 在这里这样称呼它）。事实上，

A

hids 上的签名注释隐藏了该表示。为了保持透明，你需要写：

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)

这可能不是预期的行为。