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

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

11.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 могут появляться в уравнении типа и в объявлении типа.

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