• Основной язык
• Система модулей
• Объекты в OCaml
• Именованные аргументы
• Полиморфные варианты
• Полиморфизм и его ограничения
• Обобщённые алгебраические типы
• Продвинутые примеры с классами и модулями
• Параллельное программирование
• Модель памяти: сложные аспекты

Глава 7. Обобщённые алгебраические типы

Обобщённые алгебраические типы, или GADT, расширяют обычные типы-суммы двумя способами: ограничения на параметры типа могут меняться в зависимости от конструктора значения, а некоторые переменные типа могут быть экзистенциально квантифицированы. Ограничения задаются с помощью явного возвращаемого типа, в котором параметры типа инстанцируются:

type _ term =
  | Int : int -> int term
  | Add : (int -> int -> int) term
  | App : ('b -> 'a) term * 'b term -> 'a term

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

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

1 Рекурсивные функции

Напишем функцию eval:

let rec eval : type a. a term -> a = function
  | Int n    -> n                 (* a = int *)
  | Add      -> (fun x y -> x+y)  (* a = int -> int -> int *)
  | App(f,x) -> (eval f) (eval x)
          (* eval called at types (b->a) and b for fresh b *)

И воспользуемся ею:

let two = eval (App (App (Add, Int 1), Int 1))

val two : int = 2

Важно отметить, что функция eval использует полиморфный синтаксис для локально абстрактных типов. При определении рекурсивной функции, работающей с GADT, обычно следует использовать явную полиморфную рекурсию. Например, следующее определение приводит к ошибке типа:

let rec eval (type a) : a term -> a = function
  | Int n    -> n
  | Add      -> (fun x y -> x+y)
  | App(f,x) -> (eval f) (eval x)

Error: The value f has type ($b -> a) term
       but an expression was expected of type 'a
       The type constructor $b would escape its scope
       Hint: $b is an existential type bound by the constructor App.

При отсутствии явной полиморфной аннотации для рекурсивной функции выводится мономорфный тип. Если внутри определения функции рекурсивный вызов выполняется с типом, содержащим экзистенциальную переменную типа GADT, эта переменная переходит в тип рекурсивной функции и, следовательно, выходит за пределы своей области видимости. В приведённом выше примере это происходит в ветви App(f,x), когда eval вызывается с аргументом f. В этой ветви тип f — ($App_'b -> a) term. Префикс $ в $App_'b обозначает экзистенциальный тип, названный компилятором (см. 7.5). Поскольку тип eval — 'a term -> 'a, вызов eval f приводит к тому, что экзистенциальный тип $App_'b переходит в переменную типа 'a и выходит за пределы своей области видимости. Это и вызывает описанную выше ошибку.

2 Вывод типов

Вывод типов для GADT общеизвестно сложен. Причина в том, что некоторые типы могут стать неоднозначными, выходя за пределы ветви. Например, в приведённом выше случае Int значение n может иметь тип int или a, а за пределами этой ветви эти типы неэквивалентны. В качестве первого приближения можно сказать, что вывод типов всегда работает, если сопоставление с образцом аннотировано типами, не содержащими свободных переменных типа (как для проверяемого выражения, так и для возвращаемого типа). Именно так устроен приведённый выше пример: аннотация типа содержит только локально абстрактные типы.

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

let rec sum : type a. a term -> _ = fun x ->
  let y =
    match x with
    | Int n -> n
    | Add   -> 0
    | App(f,x) -> sum f + sum x
  in y + 1

val sum : 'a term -> int = 

Здесь возвращаемый тип int никогда не объединяется с a, поэтому он считается неоднозначным, и его можно вывести. При использовании таких частичных аннотаций типов мы настоятельно рекомендуем включать режим -principal, чтобы проверить, что вывод является главным.

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

let get_int : int term -> int = function
  | Int n    -> n
  | App(_,_) -> 0

3 Случаи-опровержения

Обычно проверка полноты лишь пытается определить, можно ли проверить типы пропущенных в сопоставлении с образцом случаев. Однако можно заставить её выполнить более тщательную проверку, добавив случаи-опровержения, записываемые в виде точки. При наличии случая-опровержения проверка полноты сначала вычисляет пересечение образца с дополнением предшествующих ему случаев. Затем она проверяет, могут ли полученные образцы действительно соответствовать каким-либо конкретным значениям, пытаясь проверить их типы. Подстановочные символы в сгенерированных образцах обрабатываются особым образом: если их тип — вариантный тип, содержащий только конструкторы GADT, образец разбивается на отдельные конструкторы, чтобы проверить, возможен ли какой-либо из них (такое разбиение не выполняется для аргументов этих конструкторов во избежание бесконечной рекурсии). Также разбиваются кортежи и вариантные типы, содержащие только один случай, поскольку внутри них могут находиться GADT. Например, следующий код считается полным:

type _ t =
  | Int : int t
  | Bool : bool t

let deep : (char t * int) option -> char = function
  | None -> 'c'
  | _ -> .

В частности, выведенный оставшийся случай — Some _, который разбивается на Some (Int, _) и Some (Bool, _). Ни один из них не имеет допустимого типа, поскольку deep ожидает в качестве первого элемента кортежа несуществующий тип char t. Обратите внимание: здесь можно было бы опустить случай-опровержение, поскольку он добавляется автоматически, если в сопоставлении с образцом имеется только один случай.

Ещё одно изменение: проверка избыточности теперь учитывает GADT — случай будет признан избыточным, если его можно заменить случаем-опровержением с тем же образцом.

4 Продвинутые примеры

Определённый выше тип term — это индексированный тип, параметр типа которого отражает свойство содержимого значения. Ещё одно применение GADT — синглтонные типы, в которых значение GADT представляет ровно один тип. Это значение можно использовать как представление этого типа во время выполнения, а функция, получающая его, может вести себя полиморфно по типу.

Вот пример полиморфной функции, которая получает представление некоторого типа t во время выполнения и значение того же типа, а затем выводит это значение в виде строки в удобном для чтения формате:

type _ typ =
  | Int : int typ
  | String : string typ
  | Pair : 'a typ * 'b typ -> ('a * 'b) typ

let rec to_string: type t. t typ -> t -> string =
  fun t x ->
  match t with
  | Int -> Int.to_string x
  | String -> Printf.sprintf "%S" x
  | Pair(t1,t2) ->
      let (x1, x2) = x in
      Printf.sprintf "(%s,%s)" (to_string t1 x1) (to_string t2 x2)

Ещё одно распространённое применение GADT — свидетельства равенства.

type (_,_) eq = Eq : ('a,'a) eq

let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x

Здесь у типа eq только один конструктор, и сопоставление с ним добавляет локальное ограничение, позволяющее преобразование между a и b. Создавая такие свидетельства равенства, можно получить равные типы, синтаксически различающиеся.

Вот пример использования как синглтонных типов, так и свидетельств равенства для реализации динамических типов.

let rec eq_type : type a b. a typ -> b typ -> (a,b) eq option =
  fun a b ->
  match a, b with
  | Int, Int -> Some Eq
  | String, String -> Some Eq
  | Pair(a1,a2), Pair(b1,b2) ->
      begin match eq_type a1 b1, eq_type a2 b2 with
      | Some Eq, Some Eq -> Some Eq
      | _ -> None
      end
  | _ -> None

type dyn = Dyn : 'a typ * 'a -> dyn

let get_dyn : type a. a typ -> dyn -> a option =
  fun a (Dyn(b,x)) ->
  match eq_type a b with
  | None -> None
  | Some Eq -> Some x

5 Имена экзистенциальных типов в сообщениях об ошибках

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

• Во-первых, имена типов, начинающиеся с $, обозначают экзистенциальные типы.
• $a обозначает экзистенциальный тип, введённый для переменной типа 'a конструктора GADT:

  type any = Any : 'name -> any
  let escape (Any x) = x
  
  Error: The value x has type $name but an expression was expected of type 'a
         The type constructor $name would escape its scope
         Hint: $name is an existential type bound by the constructor Any.

• $'a используется, если во время проверки типов экзистенциальная переменная была объединена с переменной типа 'a:

  type ('arg,'result,'aux) fn =
    | Fun: ('a ->'b) -> ('a,'b,unit) fn
    | Mem1: ('a ->'b) * 'a * 'b -> ('a, 'b, 'a * 'b) fn
  let apply: ('arg,'result, _ ) fn -> 'arg -> 'result = fun f x ->
    match f with
    | Fun f -> f x
    | Mem1 (f,y,fy) -> if x = y then fy else f x
  
  Error: This pattern matches values of type
           ($'arg, 'result, $'arg * 'result) fn
         but a pattern was expected which matches values of type
           ($'arg, 'result, unit) fn
         The type constructor $'arg would escape its scope

• $n (где n — число) обозначает экзистенциальный тип, сгенерированный внутри компилятора, которому нельзя присвоить имя по одному из предыдущих правил.

Как показывает последний пункт, текущая реализация несовершенна и может быть улучшена в будущих версиях.

6 Явное именование экзистенциальных типов

Как было объяснено выше, сопоставление с образцом конструктора GADT может вводить экзистенциальные типы. Для явного задания их имён был введён специальный синтаксис. Например, следующий код задаёт имя типа аргумента f и использует его.

type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure
let eval = fun (Closure (type a) (f, x : (a -> _) * _)) -> f (x : a)

Все экзистенциальные переменные типа конструктора должны быть объявлены с помощью конструкции (type ...) и связаны с аннотацией типа, заданной снаружи аргумента конструктора.

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

type _ ty =
  | Int : int ty
  | Pair : 'b ty * 'c ty -> ('b * 'c) ty
let rec default : type a. a ty -> a = function
  | Int -> 0
  | Pair (type b c) (b, c : b ty * c ty) ->
      (default b : b), (default c : c)

7 Уравнения для нелокальных абстрактных типов

Сопоставление с образцом GADT может также добавлять уравнения типов для нелокальных абстрактных типов. Поведение такое же, как и для локальных абстрактных типов. Повторно используя определённый выше тип eq, можно написать:

module M : sig type t val x : t val e : (t,int) eq end = struct
  type t = int
  let x = 33
  let e = Eq
end

let x : int = let Eq = M.e in M.x

8 Типы, используемые в качестве индексов GADT

При обсуждении случаев-опровержений (7.3) мы использовали следующий пример:

type _ t =
  | Int : int t
  | Bool : bool t

let deep : (char t * int) option -> char = function
  | None -> 'c'
  | _ -> .

Проверка типов может установить, что случай Some _ невозможен, поскольку тип char t пуст. Это основано на том, что типы, встречающиеся в индексе GADT, заведомо различны: конструктор Int возвращает тип int t, и мы знаем, что типы int и char различны, поэтому Int невозможен для типа char t; то же верно и для Bool. Иными словами, проверка невозможности случая GADT для конкретного типа требует рассуждений о неравенстве типов.

По этой причине использование абстрактных типов в качестве индексов GADT не работает так, как предполагалось. Рассмотрим, например:

(* type-level natural numbers, in unary notation *)
module TypeNat = struct
  type zero
  type !'a succ
end

type ('a, _) sized_list =
  | Nil : ('a, TypeNat.zero) sized_list
  | Cons : 'a * ('a, 'n) sized_list -> ('a, 'n TypeNat.succ) sized_list

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

let of_singleton : ('a, TypeNat.(zero succ)) sized_list -> 'a = function
  | Cons (v, Nil) -> v
  | _ -> .

Error: This match case could not be refuted.
       Here is an example of a value that would reach it: Nil

Поскольку zero и succ — абстрактные типы, компилятор считает, что их определения неизвестны и что на самом деле они могут быть одним и тем же типом. В частности, из этой сигнатуры не следует, что типы zero и zero succ различны (даже если их реализации различаются), поэтому компилятор не может согласиться с тем, что случай Nil невозможен для типа zero succ:¹

Это можно объяснить так: модуль с такой же сигнатурой мог бы иметь следующую реализацию, в которой zero и zero succ, очевидно, совместимы:

module OtherTypeNat : sig
  type zero
  type !'a succ
end = struct
  type zero = unit
  type 'a succ = 'a
end

Чтобы избежать этой проблемы, рекомендуется задать конкретные определения для таких типов, как zero и succ, предназначенных только для использования в индексах GADT. (Это может показаться нелогичным, поскольку значения этого типа мы никогда не будем обрабатывать.) Например, можно использовать:

module TypeNat = struct
  type zero = Zero
  type 'a succ = Succ
end

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

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

module TypeNat = struct
  type zero = private Zero
  type 'a succ = private Succ
end

Примечание. Обычно private используется в интерфейсах, а не в реализациях; см. документацию о приватных типах в разделе 12.3. Конструкторы типа данных, определённого как private, нельзя использовать для создания значений, поэтому такой тип фактически пуст. Благодаря этому становится яснее, что эти типы предназначены только для использования в качестве индексов GADT.

8.1 Прежнее поведение: типы в текущем модуле

В ранних версиях OCaml, вплоть до OCaml 5.4, для типов, определённых в текущем модуле, использовалась особая обработка. Это исключение не применяется к обсуждавшимся выше определениям succ и zero, которые находятся в отдельных подмодулях.

Поэтому раньше следующих определений было достаточно для определения sized_list: компилятор принимал, что zero и 'a succ всегда различны:

type zero
type !'a succ

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

Это исключение усложняло систему и делало её менее модульной. Например, примеры с GADT работали хорошо, когда всё было определено в одном модуле, но определения функций, находившиеся в другом модуле, приводили к ошибкам, что очень сбивало пользователей с толку.

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

type zero = private Zero
type 'a succ = private Succ

1

Нам также потребовалась явная аннотация инъективности type !'a succ; иначе определение sized_list также будет отвергнуто, поскольку succ — абстрактный тип.