Глава 11 Язык программирования OCaml

8 Определения типов и исключений

• 8.1 Определения типов
• 8.2 Определения исключений

8.1 Определения типов

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

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

Определения типов вводятся ключевым словом type и состоят из одного или нескольких простых определений, возможно, взаимно рекурсивных, разделенных ключевым словом and. Каждое простое определение определяет один конструктор типа.

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

Идентификатор — это имя определяемого конструктора типа.

type colour =
  | Red | Green | Blue | Yellow | Black | White
  | RGB of {r : int; g : int; b : int}

type 'a tree = Lf | Br of 'a * 'a tree * 'a;;

type t = {decoration : string; substance : t'}
and t' = Int of int | List of t list

В правой части определений типов ссылки на одно из имен определяемого конструктора типа рассматриваются как рекурсивные, если type не сопровождается nonrec. Ключевое слово nonrec было введено в OCaml 4.02.2.

Необязательные параметры типа представляют собой либо одну переменную типа ' ident для конструкторов типов с одним параметром, либо список переменных типа ('ident₁,…,'ident_n) для конструкторов типов с несколькими параметрами. Каждый параметр типа может быть префиксен ограничением вариативности + (соответственно -), указывающим, что параметр является ковариативным (соответственно контравариантным), и аннотацией инъективности !, указывающей, что параметр может быть выведен из всего типа. Эти параметры типа могут появляться в выражениях типов правой части определения, необязательно ограниченные ограничением вариативности; т.е. ковариативный параметр может появляться только справа от функциональной стрелки (точнее, следовать левой ветви четного числа стрелок), а контравариантный параметр — только слева (левая ветвь нечетного числа стрелок). Если тип имеет представление или уравнение, и параметр свободен (т.е. не связан через ограничение типа с построенным типом), его ограничение вариативности проверяется, но подтипизация и т.д. будут использовать выведенную вариативность параметра, которая может быть менее ограниченной; в противном случае (т.е. для абстрактных типов или не свободных параметров) ограничение вариативности должно быть указано явно, а параметр является инвариантным, если вариативность не указана.

Необязательное уравнение типа = typexpr делает определенный тип эквивалентным выражению типа typexpr: один может быть заменен другим во время типизации. Если уравнение типа не указано, генерируется новый тип: определенный тип несовместим ни с каким другим типом.

Необязательное представление типа описывает структуру данных, представляющую определённый тип, при помощи списка связанных конструкторов (если это тип-вариант) или связанных полей (если это тип-запись). Если представление типа не указано, о структуре типа не делается никаких предположений, кроме того, что указано в необязательном уравнении типа.

Представление типа = [|] constr-decl { | constr-decl } описывает тип-вариант. Объявления конструкторов constr-decl₁, …, constr-decl_n описывают конструкторы, связанные с этим типом-вариантом. Объявление конструктора constr-name of typexpr₁ * … * typexpr_n объявляет имя constr-name как неконстантный конструктор, аргументы которого имеют типы typexpr₁ …typexpr_n. Объявление конструктора constr-name объявляет имя constr-name как константный конструктор. Имена конструкторов должны быть заглавными.

Представление типа = { field-decl { ; field-decl } [;] } описывает тип-запись. Объявления полей field-decl₁, …, field-decl_n описывают поля, связанные с этим типом-записью. Объявление поля field-name : poly-typexpr объявляет field-name как поле, аргумент которого имеет тип poly-typexpr. Объявление поля mutable field-name : poly-typexpr аналогично; в дополнение к этому, оно позволяет физическое изменение этого поля. Неизменяемые поля ковариантны, изменяемые поля нековариантны. И изменяемые, и неизменяемые поля могут иметь явно полиморфные типы. Полиморфизм содержимого статически проверяется при создании или изменении значения записи. Извлеченные значения могут иметь свои типы, которые подставляются.

Два компонента определения типа, необязательное уравнение и необязательное представление, могут быть объединены независимо, что приводит к четырём типичным ситуациям:

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

‍
При появлении в сигнатуре модуля, это определение не указывает ничего о конструкторе типа, кроме его количества параметров: его представление скрыто, и предполагается несовместимым с любым другим типом.

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

‍
Это определяет конструктор типа как сокращение для выражения типа справа от знака =.

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

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

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

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

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

Например, type +'a t объявляет t как абстрактный тип, который ковариантен относительно своего параметра; это означает, что если тип τ является подтипом типа σ, то τ t является подтипом σ t. Аналогично, type -'a t объявляет, что абстрактный тип t контравариантен по отношению к своему параметру: если τ является подтипом σ, то σ t является подтипом τ t. Если аннотация вариативности + или - не указана, конструктор типа предполагается невариантным в соответствующем параметре. Например, объявление абстрактного типа type 'a t означает, что τ t не является ни подтипом, ни надтипом σ t, если τ является подтипом σ.

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

Аннотации инъективности необходимы только для абстрактных типов и приватных типов строк, так как в противном случае их можно вывести из объявления типа: все параметры являются инъективными для объявлений типов-записей и типов-вариантов (включая расширяемые типы); для сокращений типа параметр является инъективным, если он имеет инъективное вхождение в его определяющем уравнении (будь то приватное или нет). Для ограниченных параметров типа в сокращениях типа, они являются инъективными, если либо они появляются в инъективной позиции в теле, или если все их переменные типа инъективны; в частности, если ограниченный параметр типа содержит переменную, которая не появляется в теле, он не может быть инъективным.

Конструкция constraint ' ident = typexpr позволяет указать параметры типа. Любой фактический аргумент типа, соответствующий параметру типа ident, должен быть экземпляром typexpr (точнее, ident и typexpr унифицируются). Переменные типа typexpr могут появляться в уравнении типа и в объявлении типа.

8.2 Определения исключений

Определения исключений добавляют новые конструкторы к встроенному типу-варианту exn значений исключений. Конструкторы объявляются так же, как и при определении типа-варианта.

# exception E of int * string;;

exception E of int * string

Форма exception constr-decl генерирует новое исключение, отличное от всех других исключений в системе. Форма exception constr-name = constr даёт альтернативное имя существующему исключению.

# exception E of int * string

  exception F = E

  let eq =
     E (1, "one") = F (1, "one");;

exception E of int * string
exception F of int * string
val eq : bool = true