参数化模块类型

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) = ...

有点笨拙,但有相同的效果.