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

• 9.10.1 Простые типы модулей
• 9.10.2 Подписи
• 9.10.3 Типы функторов
• 9.10.4 Оператор with

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

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

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

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

9.10.2 Подписи

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Спецификация одного или нескольких типов классов в сигнатуре записывается как class type classtype-def { and classtype-def } и состоит из последовательности взаимно рекурсивных определений имён типов классов. Спецификации типов классов описаны более подробно в разделе 9.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 должен ссылаться на тип модуля, который является сигнатурой, а не типом функтора.

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

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

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

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

9.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 может только добавить информацию о компонентах типа сигнатуры, но никогда не удалить информацию.