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

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

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

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

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

7.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 ($App_'b -> a) term
       but an expression was expected of type 'a
       The type constructor $App_'b would escape its scope

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

7.2 Вывод типов

Вывод типов для GADTs является непростой задачей. Это связано с тем, что некоторые типы могут стать неоднозначными при выходе из ветви. Например, в случае 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

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

Обычно проверка полноты пытается только проверить, могут ли быть типизированы пропущенные случаи сопоставления с образцом или нет. Однако вы можете заставить её работать усерднее, добавив случаи опровержения, написанные как точка. При наличии случая опровержения, проверка полноты сначала вычислит пересечение образца с дополнением случаев, предшествующих ему. Затем она проверяет, могут ли полученные образцы действительно соответствовать каким-либо конкретным значениям, пытаясь типизировать их. Дикие карты в сгенерированных образцах обрабатываются специальным образом: если их тип является типом варианта с только конструкторами GADT, то образец разбивается на разные конструкторы, чтобы проверить, возможен ли какой-либо из них (это разбиение не выполняется для аргументов этих конструкторов, чтобы избежать не завершающейся работы). Мы также разбиваем кортежи и типы вариантов с одним случаем, так как они могут содержать 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: случай будет обнаружен как избыточный, если его можно заменить случаем опровержения с использованием того же образца.

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

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

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

Во-первых, типы, чьё имя начинается с $, являются экзистенциальными.

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

type any = Any : 'name -> any
let escape (Any x) = x

Error: This expression has type $Any_'name
       but an expression was expected of type 'a
       The type constructor $Any_'name would escape its scope

$Constr обозначает экзистенциальный тип, введённый для анонимной переменной типа в конструкторе GADT Constr:

type any = Any : _ -> any
let escape (Any x) = x

Error: This expression has type $Any but an expression was expected of type
         'a
       The type constructor $Any would escape its scope

$'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 — число) — это внутренне сгенерированный экзистенциальный тип, который нельзя было назвать с помощью предыдущих схем.

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

7.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.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), и абстрактные типы, определённые локальным модулем, не могут быть инстанцированы и, следовательно, вызывают ошибку типа, а не вводят уравнение.

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

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

﻿7.2 Вывод типов

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

﻿7.4 Дополнительные примеры

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

﻿7.6 Явное именование экзистенциалов