ocaml - 参数化模块类型

Question

我正在尝试构建相互依赖的模块类型的层次结构。在 Coq 中我可以写这样的东西:

Module Type Foo.
  Parameter t:Type.
End Foo.

Module Type Bar1 (T:Foo).
  Parameter f1: T.t -> T.t.
End Bar1.

Module Type Bar2 (T:Foo).
  Parameter f2: T.t -> T.t.
End Bar2.

Module Ex (F:Foo) (B1: Bar1 F) (B2:Bar2 F).

End Ex.

我该如何用 OCaml 表达它？

Answer 1

不幸的是，Ocaml 不直接支持参数化模块类型。但是，您可以通过将参数化模块包装在它们周围来模拟它们:

module type Foo =
sig
  type t
end

module Bar (X : Foo) =
struct
  module type T =
  sig
    val f : X.t -> X.t
  end
end

module Ex (F : Foo) (B : Bar(F).T) = ...

有点笨拙，但效果相同。