11.10 Типы модулей (спецификации модулей)

• 11.10.1 Простые типы модулей
• 11.10.2 Подписи
• 11.10.3 Типы функторов
• 11.10.4 Оператор with

Типы модулей являются модульными аналогами выражений типов: они определяют общую форму и свойства типов модулей.

См. также следующие расширения языка: восстановление типа модуля, подстановка внутри подписи, алиасы модулей на уровне типов, атрибуты, узлы расширения, генеративные функторы и подстановки типов модулей.

11.10.1 Простые типы модулей

Выражение modtype-path эквивалентно типу модуля, связанному с именем modtype-path. Выражение ( module-type ) обозначает тот же тип, что и module-type.

11.10.2 Подписи

Подписи — это спецификации типов для структур. Подписи sig … end — это наборы спецификаций типов для имён значений, имён типов, исключений, имён модулей и имён типов модулей. Структура будет соответствовать подписи, если структура предоставляет определения (реализации) для всех имён, указанных в подписи (и, возможно, ещё больше), и эти определения соответствуют требованиям типа, заданным в подписи.

После каждой спецификации в подписи разрешено необязательное ;;. Оно служит синтаксическим разделителем без семантического смысла.

Спецификации значений

Спецификация компонента значения в подписи записывается как val value-name : typexpr, где value-name — имя значения, а typexpr — его ожидаемый тип.

Форма external value-name : typexpr = external-declaration аналогична, за исключением того, что дополнительно требуется, чтобы имя было реализовано как внешняя функция, указанная в external-declaration (см. главу 22).

Спецификации типов

Спецификация одного или нескольких компонентов типа в подписи записывается как type typedef { and typedef } и состоит из последовательности взаимно рекурсивных определений имён типов.

Каждое определение типа в сигнатуре указывает необязательное уравнение типа = typexpr и необязательное представление типа = constr-decl … или = { field-decl … }. Реализация имени типа в соответствующей структуре должна быть совместима с выражением типа, указанным в уравнении (если задано), и иметь указанное представление (если задано). Обратно, пользователи этой сигнатуры смогут полагаться на уравнение типа или представление типа, если они заданы. Более точно, у нас есть следующие четыре ситуации:

Абстрактный тип: без уравнения, без представления.

Имена, определенные как абстрактные типы в сигнатуре, могут быть реализованы в соответствующей структуре любым типом определения (при условии, что у него такое же количество параметров типа). Точная реализация типа будет скрыта от пользователей структуры. В частности, если тип реализован как тип варианта или тип записи, связанные конструкторы и поля не будут доступны пользователям; если тип реализован как сокращение, то равенство типов между именем типа и правой частью сокращения будет скрыто от пользователей структуры. Пользователи структуры рассматривают этот тип как несовместимый с любым другим типом: был сгенерирован новый тип.

Сокращение типа: уравнение = typexpr, без представления.

Имя типа должно быть реализовано типом, совместимым с typexpr. Все пользователи структуры знают, что имя типа совместимо с typexpr.

Новый тип варианта или тип записи: без уравнения, представление.

Имя типа должно быть реализовано типом варианта или типом записи с ровно теми конструкторами или полями, которые указаны. Все пользователи структуры имеют доступ к конструкторам или полям и могут использовать их для создания или проверки значений этого типа. Однако пользователи структуры рассматривают этот тип как несовместимый с любым другим типом: был сгенерирован новый тип.

Переэкспортированный тип варианта или тип записи: уравнение, представление.

Этот случай объединяет два предыдущих: представление типа становится видимым для всех пользователей, и новый тип не генерируется.

Спецификация исключений

Спецификация exception constr-decl в сигнатуре требует от соответствующей структуры предоставления исключения с именем и аргументами, указанными в определении, и делает исключение доступным для всех пользователей структуры.

Спецификации классов

Спецификация одного или нескольких классов в сигнатуре записывается как class class-spec { and class-spec } и состоит из последовательности взаимно рекурсивных определений имен классов.

Спецификации классов более подробно описаны в разделе 11.9.4.

Спецификации типов классов

Спецификация одного или нескольких типов классов в сигнатуре записывается как class type classtype-def { and classtype-def } и состоит из последовательности взаимно рекурсивных определений имен типов классов. Спецификации типов классов более подробно описаны в разделе 11.9.5.

Спецификации модулей

Спецификация компонента модуля в сигнатуре записывается как module module-name : module-type, где module-name — имя компонента модуля, а module-type — его ожидаемый тип. Модули могут быть вложены произвольным образом; в частности, функторы могут появляться как компоненты структур, а типы функторов — как компоненты сигнатур.

Для указания компонента модуля, являющегося функтором, можно записать

вместо

Спецификации типов модулей

Компонент типа модуля в сигнатуре может быть указан либо как явный тип модуля, либо как абстрактный тип модуля.

Спецификация абстрактного типа модуля module type modtype-name позволяет имени modtype-name быть реализованным любым типом модуля в соответствующей сигнатуре, но скрывает реализацию типа модуля от всех пользователей сигнатуры.

Спецификация явного типа модуля module type modtype-name = module-type требует, чтобы имя modtype-name было реализовано типом модуля module-type в соответствующей сигнатуре, но делает равенство между modtype-name и module-type очевидным для всех пользователей сигнатуры.

Открытие пути модуля

Выражение open module-path в сигнатуре не задает никаких компонентов. Оно просто влияет на обработку последующих элементов сигнатуры, позволяя компонентам модуля, обозначенному module-path, ссылаться на простые имена name вместо обращений к пути module-path . name. Сфера действия open заканчивается в конце выражения сигнатуры.

Включение сигнатуры

Выражение include module-type в сигнатуре выполняет текстовое включение компонентов сигнатуры, обозначенной module-type. Оно ведет себя так, как если бы компоненты включенной сигнатуры были скопированы в место расположения include. Аргумент module-type должен ссылаться на тип модуля, который является сигнатурой, а не типом функтора.

11.10.3 Типы функторов

Выражение типа модуля functor ( имя-модуля : тип-модуля₁ ) -> тип-модуля₂ является типом функторов (функций от модулей к модулям), которые принимают в качестве аргумента модуль типа тип-модуля₁ и возвращают в качестве результата модуль типа тип-модуля₂. Тип модуля тип-модуля₂ может использовать имя имя-модуля для ссылки на компоненты типа фактического аргумента функтора. Если тип тип-модуля₂ не зависит от компонентов типа имя-модуля, выражение типа модуля может быть упрощено с помощью альтернативной краткой записи тип-модуля₁ -> тип-модуля₂. Ограничения на тип аргумента функтора не накладываются; в частности, функтор может принимать другой функтор в качестве аргумента («функтор высшего порядка»).

Когда тип результирующего модуля является функтором,

можно использовать сокращённую форму

11.10.4 Оператор with

Предполагая, что тип-модуля обозначает сигнатуру, выражение тип-модуля with ограничение-модуля { and ограничение-модуля } обозначает ту же сигнатуру, где к некоторым спецификациям типов добавлены уравнения типов, как описано в ограничениях, следующих за ключевым словом with. Ограничение type [параметры-типов] имя-типа = выражение-типа добавляет уравнение типа = выражение-типа к спецификации компонента типа, имеющего имя имя-типа в ограниченной сигнатуре. Ограничение module путь-к-модулю = расширенный-путь-к-модулю добавляет уравнения типов ко всем компонентам типа подструктуры, обозначаемой путь-к-модулю, делая их эквивалентными соответствующим компонентам типа структуры, обозначаемой расширенный-путь-к-модулю.

Например, если имя типа модуля S привязано к сигнатуре

        sig type t module M: (sig type u end) end

тогда S with type t=int обозначает сигнатуру

        sig type t=int module M: (sig type u end) end

и S with module M = N обозначает сигнатуру

        sig type t module M: (sig type u=N.u end) end

Функтор, принимающий два аргумента типа S, которые разделяют свой компонент t, записывается

        functor (A: S) (B: S with type t = A.t) ...

Ограничения добавляются слева направо. После применения каждого ограничения результирующая сигнатура должна быть подтипом сигнатуры до применения ограничения. Таким образом, оператор with может только добавлять информацию о компонентах типа сигнатуры, но никогда не удалять информацию.