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

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

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

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

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

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

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: This expression 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 Вывод типа

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

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

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, чтобы проверить, что вывод типа является принципиальным.

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

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

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

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

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 в качестве первого элемента кортежа. Обратите внимание, что случай опровержения можно опустить здесь, потому что он автоматически добавляется, когда в сопоставлении с образцом есть только один случай.

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

4 Расширенные примеры

Тип term, который мы определили выше, является индексированным типом, где параметр типа отражает свойство содержимого значения. Другое использование GADTs — одноэлементные типы, где значение 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)

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

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 Имена экзистенциальных типов в сообщениях об ошибках

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

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

  type any = Any : 'name -> any
  let escape (Any x) = x
  
  Error: This expression 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 ...) и связаны с аннотацией типа снаружи аргумента конструктора.

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

Конечно, не все абстрактные типы могут быть уточнены, так как это противоречит проверке полноты. А именно, встроенные типы (определённые самим компилятором, такие как int или array) и абстрактные типы, определённые локальным модулем, не могут быть инстанцированы и, следовательно, вызывают ошибку типа, а не вводят уравнение.