Проблема проверки типов OCaml при использовании двух параметризованных модулей

Question

У меня есть два модуля, Graph и Game, которые параметризованы другими модулями. Они также содержат функции f и g, которые вызывают проблемы проверки типов, когда я использую их в модуле тестирования. Я пропустил много кода, который не важен для этой проблемы.

Вот модуль Graph, который имеет некоторый модуль 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, которая позднее будет введена для функции f из модуля Graph.

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

Затем у вас остается «проблема», которую определяют 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