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

Question

При использовании взаимно рекурсивных определений модулей в OCaml необходимо давать подписи даже в файле .ml. Это раздражает, когда я также хочу выставить данный интерфейс из .mli, так как в итоге я повторяю подпись дважды. : (

module rec Client : sig
  type ('serv,'cli) t

  (* functions ... *)
end = struct
  type ('serv,'cli) t =
    { server: ('serv,'cli) Server.t
    ; (* other members ... *)
    }
end
and Server : sig
  type ('serv,'cli) t

  (* functions ... *)
end = struct
  type ('serv,'cli) t =
    { mutable clients: ('serv,'cli) Client.t list
    ; mutable state: 'serv
    }

  (* functions again ... *)
end

Это грубое приближение к тому, что я делаю (объекты типа Client знают Server, который их создал. Server s знают Client s).

Конечно, подписи повторяются в .mli. Почему это необходимо?

(Примечание: я не жалуюсь, но на самом деле хочу знать, есть ли для этого причина, связанная с теорией типов или "проблемой жесткого компилятора".)

Answer 1

Насколько я знаю, это никак не обойти. На очень высоком уровне, что касается компилятора, сигнатура типа Client является неполной, пока он не узнает сигнатуру типа Server, и наоборот. В принципе, есть способ обойти это: компилятор может перекрестно ссылаться на ваши файлы .mli во время компиляции. Но у этого подхода есть недостатки: он смешивает некоторые обязанности компилятора и компоновщика и усложняет модульную компиляцию (без каламбура).

Если вам интересно, я рекомендую оригинальное предложение Xavier Leroy для рекурсивных модулей.

Answer 2

Мое предположение: для компиляции рекурсивных модулей компилятору нужны аннотации типов для реализации.В mli-файле (если вы используете какой-либо) типы этих модулей могут быть дополнительно ограничены или скрыты, поэтому в общем случае компилятору не имеет смысла ожидать поиска полезных типов в mli по разрешению рекурсии типов.