Глава 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 работает аналогично; кроме того, оно позволяет физически изменять это поле. Неизменяемые поля ковариантны, изменяемые поля не имеют вариативности. Начиная с OCaml 5.4, изменяемые поля могут быть помечены атрибутом [@atomic] для параллельного доступа; см. 9.7.2.
Как изменяемые, так и неизменяемые поля могут иметь явно полиморфные типы. Полиморфизм содержимого статически проверяется при создании или изменении значения записи. Типы извлечённых значений могут быть инстанцированы.

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

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

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

Псевдоним типа: есть уравнение, нет представления.

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

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

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

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

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

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