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

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

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

$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 Явное именование экзистенциалов