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

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

9.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 ведет себя аналогично; кроме того, оно позволяет физически изменять это поле. Неизменяемые поля являются ковариантными, изменяемые поля — нековариантными. Как изменяемые, так и неизменяемые поля могут иметь явно полиморфные типы. Полиморфизм содержимого статически проверяется при создании или изменении значения записи. Извлеченные значения могут иметь свои типы, которые могут быть инстанцированы.

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

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

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

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

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

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

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

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

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

Переменные типа, появляющиеся в качестве параметров типа, могут необязательно предваряться + или -, чтобы указать, что конструктор типа является ковариантным или контравариантным по отношению к этому параметру. Эта информация о вариативности используется для принятия решений о подтипах при проверке корректности приведений :> (см. раздел 9.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 могут появляться в уравнении типа и объявлении типа.

9.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