使用两个参数化模块时的 OCaml 类型检查问题

Question

我有两个模块，Graph 和 Game，它们由其他模块参数化。它们还包含函数 f 和 g，当我在测试模块中使用它们时会导致类型检查问题。我遗漏了很多对这个问题不重要的代码。

这是一个具有某些模块 AbstractUSet 的图形模块。 AbstractUSet.t在原代码中使用较多。函数 f 稍后将采用另一个函数并做一些工作。问题是，另一个函数来自另一个模块并且具有不同的类型。

module UTYPE = sig
  type t
  val compare : t -> t -> int
end

module type GRAPH = sig
  module U : UTYPE
  module AbstractUSet : Set.S
  val f : (AbstractUSet.t -> AbstractUSet.t) -> AbstractUSet.t -> AbstractUSet.t
end

module Graph (UA : UTYPE) : (GRAPH with module U=UA) = struct
  module U=UA
  module AbstractUSet = Set.Make(struct type t=U.t let compare=U.compare end)
  let f g uset = g uset
end

另一个模块是Game模块。它用 AbstractVSet.t 做了很多事情。它包含函数 g，稍后将从 Graph 模块输入函数 f。

module type GAME_PIECE = sig
  type t
  val compare : t -> t -> int
end

module type GAME = sig
  module P : GAME_PIECE
  module AbstractVSet : Set.S
  val g : AbstractVSet.t -> AbstractVSet.t
end

module GameInstance (NA : GAME_PIECE) : (GAME with module P=NA) = struct
  module P = NA
  module AbstractVSet = Set.Make(struct type t=P.t let compare=P.compare end)
  let g vset = vset
end

这是我的测试模块。最后，UTYPE 和 GAME_PIECE 是相同的，但我无法向 OCaml 说明这一点。我已经评论了不进行类型检查的行。编译器说 MyGame.AbstractVSet.t 和 MyGraph.AbstractUSet.t 之间存在冲突。

module TestGame = struct
  include(Game(struct type t=string let compare=compare end))
end

module TestGraph = struct
  include(Graph(struct type t=string let compare=compare end))
end

module Test = struct
  module MyGame = TestGame
  module MyGraph = TestGraph
  let stringlist = ["a";"b"]
  let uset = MyGraph.uset_from_ulist stringlist // works fine
  let vset = MyGame.vset_from_vlist stringlist // works fine
  let result = MyGraph.f (MyGame.g) vset // does not typecheck!
end

如果你问，为什么我要使用这么多模块：这个项目比这个代码摘录要大得多，它的目的是这样的；）谁能帮助我如何让 OCaml 编译器清楚地知道 UTYPE 和 GAME_PIECE 在 Test 模块中是相同的？非常感谢您的帮助！！！

Answer 1

第一个问题是您的抽象集模块不同：OCaml 中的两个仿函数应用程序的结果仅当仿函数应用程序应用于完全相同的情况下才相等命名模块。例如，在

module A = struct type t = int end
module F(X:sig type t end) = struct type t end
module FA = F(A)
module B = A
module FA' = F(B)
module C = F(struct type t end)

类型FA.t和Fa'.t相同

let f (x:FA.t): FA'.t = x

但是类型C.t和FA.t是不同的：

let f (x:C.t): FA'.t = x
Error: This expression has type C.t but an expression was expected of type
         FA'.t

但这部分可以通过在不需要时不使用匿名结构来修复：

module Graph (UA : UTYPE) : (GRAPH with module U=UA) = struct
  module U=UA
  module AbstractUSet = Set.Make(U)
  let f g uset = g uset
end

然后，您剩下的 "problem" 即 Game(M).AbstractUSet 和 Graph(M).AbstractUSet 定义了两种不同的类型。（请注意，这可能是测试之外的正确行为）。对于测试，一种选择是简单地公开这些模块是函子应用程序的结果的信息。例如，可以将 GAME 模块类型（和 GameInstance 仿函数）重新定义为：


module type GAME = sig
  type set
  module P : GAME_PIECE
  module AbstractVSet: Set.S with type t = set
  val g : AbstractVSet.t -> AbstractVSet.t
end

module GameInstance (NA : GAME_PIECE) :
(GAME with type set:= Set.Make(NA).t and module P=NA) = struct
  module P = NA
  module AbstractVSet = Set.Make(NA)
  let g vset = vset
end

在这里，我们得到了 GameInstance(M).AbstractVSet.t 是与 Set.Make(M).t.

类型相同

结合图形部分的相同操作：

module type GRAPH = sig
  type set
  module U : UTYPE
  module AbstractUSet : Set.S with type t = set
  val f : (AbstractUSet.t -> AbstractUSet.t) -> AbstractUSet.t -> AbstractUSet.t
end

module Graph (UA : UTYPE) :
(GRAPH with type set := Set.Make(UA).t and module U=UA) = struct
  module U=UA
  module AbstractUSet = Set.Make(UA)
  let f g uset = g uset
end

我们保留了足够的类型信息以保持测试的相等性：

module TestGame = GameInstance(String)
module TestGraph = Graph(String)

module Test = struct
  module MyGame = TestGame
  module MyGraph = TestGraph
  let result vset = MyGraph.f (MyGame.g) vset (* does typecheck *)
end

使用两个参数化模块时的 OCaml 类型检查问题

OCaml Typechecking Problem When Using Two Parameterized Modules

ocaml

q

typechecking