Модули в микроскопе более тонкие, чем кажется
(Если ваши глаза в какой-то момент застекляются, переходите ко второму разделу.)
Давайте посмотримчто произойдет, если вы положите все в один файл.Это должно быть возможным, поскольку отдельные вычислительные блоки не увеличивают мощность системы типов. (Примечание: используйте отдельные каталоги для этого и для любого теста с файлами a.* и b.*, в противном случае компилятор увидит единицы компиляции A и B, что может сбить с толку.)
module A = (struct
type t = { x : int }
let b = B.a
end : sig
type t = { x : int }
val b : t
end)
module B = (struct
let a : A.t = { A.x = 1 }
end : sig
val a : A.t
end)
О, ну, это не может работать.Очевидно, что B здесь не определено.Нам нужно быть более точным в отношении цепочки зависимостей: сначала определим интерфейс A, затем интерфейс B, затем реализации B и A.
module type Asig = sig
type t = { x : int }
type u = int
val b : t
end
module B = (struct
let a : Asig.t = { Asig.x = 1 }
end : sig
val a : Asig.t
end)
module A = (struct
type t = { x : int }
let b = B.a
end : Asig)
Хорошо., нет.
File "d.ml", line 7, characters 12-18:
Error: Unbound type constructor Asig.t
Видите ли, Asig это подпись.Подпись - это спецификация модуля, и не более;в Окамле нет исчисления подписей.Вы не можете ссылаться на поля подписи.Вы можете ссылаться только на поля модуля.Когда вы пишете A.t, это относится к полю типа t модуля A.
В Ocaml эта тонкость возникает довольно редко.Но вы пытались заглянуть в угол языка, и вот что там скрывается.
Так что же происходит, когда есть два модуля компиляции?Более близкая модель - видеть A как функтор, который принимает модуль B в качестве аргумента.Требуемая подпись для B - это подпись, описанная в файле интерфейса b.mli.Аналогично, B - это функция, которая принимает в качестве аргумента модуль A, сигнатура которого указана в a.mli.О, подождите, это немного сложнее: A появляется в сигнатуре B, так что интерфейс B действительно определяет функтор, который принимает A и производит, так сказать, B.
module type Asig = sig
type t = { x : int }
type u = int
val b : t
end
module type Bsig = functor(A : Asig) -> sig
val a : A.t
end
module B = (functor(A : Asig) -> (struct
let a : A.t = { A.x = 1 }
end) : Bsig)
module A = functor(B : Bsig) -> (struct
type t = { x : int }
let b = B.a
end : Asig)
И здесь, при определении A, мы сталкиваемся с проблемой: у нас еще нет A для передачи в качестве аргумента B.(Конечно, за исключением рекурсивных модулей, но здесь мы пытаемся понять, почему мы не можем обойтись без них.)
Определение порождающего типа является побочным эффектом
Фундаментальное прилипаниеДело в том, что type t = {x : int} является генеративным определением типа.Если этот фрагмент появляется дважды в программе, определяются два разных типа.(Ocaml предпринимает шаги и запрещает вам определять два типа с одинаковыми именами в одном модуле, за исключением верхнего уровня.)
Фактически, как мы видели выше, type t = {x : int} вМодуль реализации является генеративным определением типа.Это означает «определить новый тип с именем d, который представляет собой тип записи с полями…».Тот же синтаксис может присутствовать в интерфейсе модуля, но там он имеет другое значение: там он означает «модуль определяет тип t, который является типом записи…».
После определения порождающего типадважды создает два разных типа, конкретный порождающий тип, который определяется A, не может быть полностью описан спецификацией модуля A (его сигнатура).Следовательно, любая часть программы, которая использует этот порождающий тип, действительно использует реализацию A, а не только его спецификацию .
Когда вы приступаете к этому, определяя порождающий тип, этоэто форма побочного эффекта.Этот побочный эффект возникает во время компиляции или во время инициализации программы (различие между этими двумя появляется только тогда, когда вы начинаете смотреть на функторы, что я не буду здесь делать). Поэтому важно отслеживать, когда этот побочный эффект происходит:происходит, когда модуль A определен (скомпилирован или загружен).
Итак, чтобывыразите это более конкретно: определение типа type t = {x : int} в модуле A скомпилировано в «пусть t будет типом # 1729, новым типом, который является типом записи с полем…».(Тип fresh означает тип, который отличается от любого типа, который когда-либо был определен ранее.).Определение B определяет a для типа # 1729.
Поскольку модуль B зависит от модуля A, A должен быть загружен до B.Но реализация A явно использует реализацию B.Эти два являются взаимно рекурсивными.Сообщение об ошибке Окамла немного сбивает с толку, но вы действительно выходите за рамки языка.