Глава 6 Полиморфизм и его ограничения
В этой главе рассматриваются более сложные вопросы, связанные с ограничениями полиморфных функций и типов. В OCaml есть ситуации, когда тип, выведенный проверяющим типом, может быть менее универсальным, чем ожидалось. Такая не универсальность может происходить как из-за взаимодействия побочных эффектов и типизации, так и из-за трудностей с неявной полиморфной рекурсией и полиморфизмом высшего порядка.
В этой главе подробно рассматриваются каждая из этих ситуаций и, если это возможно, способы восстановления универсальности.
6.1 Слабый полиморфизм и мутации
6.1.1 Слабо полиморфные типы
Возможно, наиболее частые примеры не универсальности происходят из-за взаимодействия полиморфных типов и мутаций. Простой пример появляется при типизации следующего выражения
# let store = ref None ;;
val store : '_weak1 option ref = {contents = None} Поскольку тип None — 'a option, а функция ref имеет тип 'b -> 'b ref, естественным выводом для типа store был бы 'a option ref. Однако выведенный тип '_weak1 option ref отличается. Переменные типов, имена которых начинаются с _weak, например, '_weak1, являются слабо полиморфными переменными типов, иногда сокращаемыми до «слабых переменных типов». Слабая переменная типа — это заполнитель для единственного типа, который в настоящее время неизвестен. После того, как конкретный тип t за местоимением типа '_weak1 станет известен, все вхождения '_weak1 будут заменены на t. Например, мы можем определить еще одну ссылку на опцию и сохранить в ней int:
# let another_store = ref None ;;
val another_store : '_weak2 option ref = {contents = None} # another_store := Some 0;
another_store ;;
- : int option ref = {contents = Some 0} После сохранения int в another_store, тип another_store был обновлен с '_weak2 option ref до int option ref. Это различие между слабо и универсально полиморфными переменными типов защищает программы OCaml от некорректности и ошибок во время выполнения. Чтобы понять, откуда может возникнуть некорректность, рассмотрите простую функцию, которая меняет значение x со значением, сохраненным в ссылке store, если такое значение есть:
# let swap store x = match !store with
| None -> store := Some x; x
| Some y -> store := Some x; y;;
val swap : 'a option ref -> 'a -> 'a = Мы можем применить эту функцию к нашему хранилищу
# let one = swap store 1 let one_again = swap store 2 let two = swap store 3;; val one : int = 1 val one_again : int = 1 val two : int = 2
После этих трех обменов сохраненное значение равно 3. Все в порядке до сих пор. Затем мы можем попробовать поменять 3 на более интересное значение, например, функцию:
# let error = swap store (fun x -> x);; Error: This expression should not be a function, the expected type is int
На этом этапе проверяющий тип обоснованно жалуется, что нельзя поменять целое число и функцию, и что целое число всегда должно обмениваться на другое целое число. Кроме того, проверяющий тип предотвращает ручную смену типа хранимого значения store:
# store := Some (fun x -> x);; Error: This expression should not be a function, the expected type is int
Действительно, взглянув на тип store, мы видим, что слабый тип '_weak1 был заменен типом int
# store;;
- : int option ref = {contents = Some 3} Следовательно, после помещения int в store, мы не можем использовать его для хранения других значений, кроме int. В более общем плане, слабые типы защищают программу от необоснованной мутации значений с полиморфным типом.
Кроме того, слабые типы не могут появиться в сигнатуре модулей верхнего уровня: типы должны быть известны во время компиляции. В противном случае разные модули компиляции могли бы заменить слабый тип различными и несовместимыми типами. По этой причине компиляция следующего небольшого фрагмента кода
let option_ref = ref None
вызывает ошибку компиляции
Error: The type of this expression, '_weak1 option ref,
contains type variables that cannot be generalized
Для решения этой ошибки достаточно добавить явную аннотацию типа, чтобы указать тип во время объявления:
let option_ref: int option ref = ref None
В любом случае это хорошая практика для таких глобальных переменных. В противном случае они будут выбирать тип первого использования. Если в этот момент допущена ошибка, это может привести к путанице с ошибками типов, когда позже корректные использования отмечаются как ошибки.
6.1.2 Ограничение значений
Идентификация точного контекста, в котором полиморфные типы должны быть заменены слабыми типами модульным способом, является сложной задачей. Действительно, система типов должна учитывать возможность того, что функции могут скрывать постоянные состояния мутаций. Например, следующая функция использует внутреннюю ссылку для реализации функции задержки тождества
# let make_fake_id () =
let store = ref None in
fun x -> swap store x ;;
val make_fake_id : unit -> 'a -> 'a = # let fake_id = make_fake_id();; val fake_id : '_weak3 -> '_weak3 =
Неправильно применять эту функцию fake_id к значениям с различными типами. Функция fake_id поэтому обоснованно присваивается тип '_weak3 -> '_weak3 вместо 'a -> 'a. В то же время, должно быть возможно использовать локальное состояние мутации без влияния на тип функции.
Чтобы обойти эти двойственные трудности, проверяющий тип считает, что любое значение, возвращаемое функцией, может опираться на скрытые постоянные состояния мутации и должно иметь слабый тип. Это ограничение на тип мутабельных значений и результатов применения функций называется ограничением значения. Обратите внимание, что это ограничение значений является консервативным: есть ситуации, когда ограничение значений слишком осторожно и присваивает слабый тип значению, которое можно безопасно обобщить до полиморфного типа:
# let not_id = (fun x -> x) (fun x -> x);; val not_id : '_weak4 -> '_weak4 =
Это довольно часто происходит при определении функций с помощью функций высшего порядка. Чтобы избежать этой проблемы, решением является добавление явного аргумента в функцию:
# let id_again = fun x -> (fun x -> x) (fun x -> x) x;; val id_again : 'a -> 'a =
С этим аргументом id_again рассматривается проверяющим типом как определение функции и, следовательно, может быть обобщено. Этот вид манипуляций называется эта-расширением в лямбда-исчислении и иногда упоминается под этим именем.
6.1.3 Смягченное ограничение значений
Существует еще одно частичное решение проблемы ненужных слабых типов, реализованное непосредственно в проверяющем типе. Вкратце, можно доказать, что слабые типы, которые появляются только как параметры типов в ковариантных позициях — также называемых позитивными позициями — можно безопасно обобщить до полиморфных типов. Например, тип 'a list ковариантен в 'a:
# let f () = [];; val f : unit -> 'a list =
# let empty = f ();; val empty : 'a list = []
Обратите внимание, что тип, выведенный для empty, равен 'a list, а не '_weak5 list, который должен был появиться с ограничением значений.
Ограничение значений в сочетании с этим обобщением для ковариантных параметров типа называется смягченным ограничением значений.
6.1.4 Ковариантность и ограничение значений
Ковариантность описывает, как конструкторы типов ведут себя по отношению к подтипированию. Рассмотрим, например, пару типа x и xy, где x является подтипом xy, обозначаемым x :> xy:
# type x = [ `X ];; type x = [ `X ]
# type xy = [ `X | `Y ];; type xy = [ `X | `Y ]
Поскольку x является подтипом xy, мы можем преобразовать значение типа x в значение типа xy:
# let x:x = `X;; val x : x = `X
# let x' = ( x :> xy);; val x' : xy = `X
Аналогично, если у нас есть значение типа x list, мы можем преобразовать его в значение типа xy list, поскольку мы можем преобразовать каждый элемент по одному:
# let l:x list = [`X; `X];; val l : x list = [`X; `X]
# let l' = ( l :> xy list);; val l' : xy list = [`X; `X]
Другими словами, x :> xy подразумевает, что x list :> xy list, поэтому конструктор типа 'a list является ковариантным (он сохраняет суботипизацию) в своём параметре 'a.
Напротив, если у нас есть функция, которая может обрабатывать значения типа xy
# let f: xy -> unit = function
| `X -> ()
| `Y -> ();;
val f : xy -> unit = то она также может обрабатывать значения типа x:
# let f' = (f :> x -> unit);; val f' : x -> unit =
Обратите внимание, что мы можем переписать тип f и f' как
# type 'a proc = 'a -> unit
let f' = (f: xy proc :> x proc);;
type 'a proc = 'a -> unit
val f' : x proc = В этом случае, x :> xy подразумевает xy proc :> x proc. Обратите внимание, что второе отношение суботипизации меняет порядок x и xy: конструктор типа 'a proc является контравариантным относительно своего параметра 'a. Более общим образом, конструктор типа функции 'a -> 'b является ковариантным относительно своего возвращаемого типа 'b и контравариантным относительно своего аргументного типа 'a.
Конструктор типа также может быть инвариантным по некоторым из своих типов-параметров, ни ковариантным, ни контравариантным. Типичным примером является ссылка:
# let x: x ref = ref `X;;
val x : x ref = {contents = `X} Если бы мы могли привести x к типу xy ref как переменную xy, мы могли бы использовать xy для хранения значения `Y внутри ссылки, а затем использовать значение x для чтения этого содержимого как значения типа x, что нарушило бы систему типов.
Более общим образом, как только переменная типа появляется в позиции, описывающей изменяемое состояние, она становится инвариантной. Вследствие этого, ковариантные переменные никогда не будут обозначать изменяемые местоположения и могут быть безопасно обобщены. Для более подробного описания заинтересованные читатели могут обратиться к оригинальной статье Жака Гарриге на http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf
Вместе, ослабленное ограничение на значения и ковариативность типов-параметров помогают избежать eta-расширения во многих ситуациях.
6.1.5 Абстрактные типы данных
Кроме того, когда определения типов доступны, система проверки типов может сама вывести информацию о ковариации, и можно извлечь выгоду из ослабленного ограничения на значения даже неосознанно. Однако это больше не так при определении новых абстрактных типов. В качестве иллюстрации, мы можем определить тип модуля collection как:
# module type COLLECTION = sig
type 'a t
val empty: unit -> 'a t
end
module Implementation = struct
type 'a t = 'a list
let empty ()= []
end;;
module type COLLECTION = sig type 'a t val empty : unit -> 'a t end
module Implementation :
sig type 'a t = 'a list val empty : unit -> 'a list end # module List2: COLLECTION = Implementation;; module List2 : COLLECTION
В этой ситуации, при приведении модуля List2 к типу модуля COLLECTION, система проверки типов забывает, что 'a List2.t был ковариантным по 'a. Вследствие этого, ослабленное ограничение на значения больше не применяется:
# List2.empty ();; - : '_weak5 List2.t =
Чтобы сохранить ослабленное ограничение на значения, нам нужно объявить абстрактный тип 'a COLLECTION.t как ковариантный по 'a:
# module type COLLECTION = sig
type +'a t
val empty: unit -> 'a t
end
module List2: COLLECTION = Implementation;;
module type COLLECTION = sig type +'a t val empty : unit -> 'a t end
module List2 : COLLECTION Затем мы восстанавливаем полиморфизм:
# List2.empty ();; - : 'a List2.t =
6.2 Полиморфная рекурсия
Второй основной класс не-обобщенности напрямую связан с проблемой вывода типа для полиморфных функций. В некоторых случаях, выводимый OCaml тип может быть недостаточно общим, чтобы позволить определение некоторых рекурсивных функций, особенно для рекурсивных функций, действующих на нерегулярных алгебраических типах данных.
С регулярным полиморфным алгебраическим типом данных, типы параметров конструктора типа являются постоянными в рамках определения типа. Например, мы можем посмотреть на произвольно вложенные списки, определенные как:
# type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list
let l = Nested[ List [1]; Nested [List[2;3]]; Nested[Nested[]] ];;
type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list
val l : int regular_nested =
Nested [List [1]; Nested [List [2; 3]]; Nested [Nested []]] Обратите внимание, что конструктор типа regular_nested всегда появляется как 'a regular_nested в определении выше, с тем же параметром 'a.
С этим типом можно вычислить максимальную глубину с помощью классической рекурсивной функции:
# let rec maximal_depth = function
| List _ -> 1
| Nested [] -> 0
| Nested (a::q) -> 1 + max (maximal_depth a) (maximal_depth (Nested q));;
val maximal_depth : 'a regular_nested -> int = Нерегулярные рекурсивные алгебраические типы данных соответствуют полиморфным алгебраическим типам данных, чьи типы параметров меняются между левой и правой стороной определения типа. Например, может быть интересно определить тип данных, который гарантирует, что все списки вложены на одной и той же глубине:
# type 'a nested = List of 'a list | Nested of 'a list nested;; type 'a nested = List of 'a list | Nested of 'a list nested
Интуитивно, значение типа 'a nested представляет собой список списков …списка элементов a с k вложенными списками. Мы можем затем адаптировать функцию maximal_depth, определенную для regular_depth, в функцию depth, которая вычисляет это k. В качестве первой попытки, мы можем определить:
# let rec depth = function
| List _ -> 1
| Nested n -> 1 + depth n;;
Error: This expression has type 'a list nested
but an expression was expected of type 'a nested
The type variable 'a occurs inside 'a list Ошибка типа здесь происходит от того, что при определении depth, система проверки типов сначала присваивает depth тип 'a -> 'b . При типизации сопоставления с образцом, 'a -> 'b превращается в 'a nested -> 'b, затем в 'a nested -> int после типизации ветви List. Однако, при типизации применения depth n в ветви Nested, система проверки типов сталкивается с проблемой: depth n применяется к 'a list nested, поэтому она должна иметь тип 'a list nested -> 'b. Объединение этого ограничения с предыдущим приводит к невозможному ограничению 'a list nested = 'a nested. Другими словами, в своем определении, рекурсивная функция depth применяется к значениям типа 'a t с разными типами 'a из-за нерегулярности конструктора типа nested. Это создает проблему, потому что система проверки типов ввела новую переменную типа 'a только при определении функции depth, тогда как здесь нам нужна различная переменная типа для каждого применения функции depth.
6.2.1 Явно полиморфные аннотации
Решение этой проблемы — использование явно полиморфной аннотации типа для типа 'a:
# let rec depth: 'a. 'a nested -> int = function
| List _ -> 1
| Nested n -> 1 + depth n;;
val depth : 'a nested -> int = # depth ( Nested(List [ [7]; [8] ]) );; - : int = 2
В типе depth, 'a.'a nested -> int, переменная типа 'a является универсально квантифицированной. Другими словами, 'a.'a nested -> int читается как «для всех типов 'a, depth отображает значения 'a nested в целые числа». В то время как стандартный тип 'a nested -> int может быть интерпретирован как «пусть будет переменная типа 'a, тогда depth отображает значения 'a nested в целые числа». Существует два основных различия между этими двумя выражениями типа. Во-первых, явно полиморфная аннотация сообщает системе проверки типов, что она должна вводить новую переменную типа каждый раз, когда функция depth применяется. Это решает нашу проблему с определением функции depth.
Во-вторых, она также уведомляет систему проверки типов о том, что тип функции должен быть полиморфным. Действительно, без явно полиморфной аннотации, следующая аннотация типа является совершенно корректной:
# let sum: 'a -> 'b -> 'c = fun x y -> x + y;; val sum : int -> int -> int =
так как 'a,'b и 'c обозначают переменные типа, которые могут или не могут быть полиморфными. В то время как объединение явно полиморфного типа с не-полиморфным типом является ошибкой:
# let sum: 'a 'b 'c. 'a -> 'b -> 'c = fun x y -> x + y;;
Error: This definition has type int -> int -> int which is less general than
'a 'b 'c. 'a -> 'b -> 'c Важное замечание здесь заключается в том, что нет необходимости явно указывать тип depth: достаточно добавить аннотации только для универсально квантифицированных переменных типа:
# let rec depth: 'a. 'a nested -> _ = function
| List _ -> 1
| Nested n -> 1 + depth n;;
val depth : 'a nested -> int = # depth ( Nested(List [ [7]; [8] ]) );; - : int = 2
6.2.2 Дополнительные примеры
С явными полиморфными аннотациями становится возможным реализовать любую рекурсивную функцию, которая зависит только от структуры вложенных списков, а не от типа элементов. Например, более сложным примером было бы вычисление общего количества элементов вложенных списков:
# let len nested =
let map_and_sum f = List.fold_left (fun acc x -> acc + f x) 0 in
let rec len: 'a. ('a list -> int ) -> 'a nested -> int =
fun nested_len n ->
match n with
| List l -> nested_len l
| Nested n -> len (map_and_sum nested_len) n
in
len List.length nested;;
val len : 'a nested -> int = # len (Nested(Nested(List [ [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ])));; - : int = 7
Аналогично, может потребоваться использовать более одной явно полиморфной переменной типа, например, для вычисления длины вложенных списков вложенных списков:
# let shape n =
let rec shape: 'a 'b. ('a nested -> int nested) ->
('b list list -> 'a list) -> 'b nested -> int nested
= fun nest nested_shape ->
function
| List l -> raise
(Invalid_argument "shape requires nested_list of depth greater than 1")
| Nested (List l) -> nest @@ List (nested_shape l)
| Nested n ->
let nested_shape = List.map nested_shape in
let nest x = nest (Nested x) in
shape nest nested_shape n in
shape (fun n -> n ) (fun l -> List.map List.length l ) n;;
val shape : 'a nested -> int nested = # shape (Nested(Nested(List [ [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ])));; - : int nested = Nested (List [[2; 1]; [0; 1; 3]; [0]])
6.3 Полиморфные функции высшего порядка
Однако явные полиморфные аннотации недостаточно для покрытия всех случаев, когда выведенный тип функции менее общий, чем ожидалось. Аналогичная проблема возникает при использовании полиморфных функций в качестве аргументов функций высшего порядка. Например, мы можем захотеть вычислить среднюю глубину или длину двух вложенных списков:
# let average_depth x y = (depth x + depth y) / 2;; val average_depth : 'a nested -> 'b nested -> int =
# let average_len x y = (len x + len y) / 2;; val average_len : 'a nested -> 'b nested -> int =
# let one = average_len (List [2]) (List [[]]);; val one : int = 1
Естественно было бы разделить эти два определения как:
# let average f x y = (f x + f y) / 2;;
val average : ('a -> int) -> 'a -> 'a -> int = Однако тип average len менее общий, чем тип average_len, поскольку он требует, чтобы тип первого и второго аргумента был одинаковым:
# average_len (List [2]) (List [[]]);; - : int = 1
# average len (List [2]) (List [[]]);;
Error: This expression has type 'a list
but an expression was expected of type int Как и ранее с полиморфной рекурсией, проблема связана с тем, что переменные типа вводятся только в начале определений let. Когда мы вычисляем как f x, так и f y, типы x и y объединяются вместе. Чтобы избежать этого объединения, нам нужно указать проверяющему тип, что f полиморфен по своему первому аргументу. В некотором смысле, мы хотели бы, чтобы average имел тип
val average: ('a. 'a nested -> int) -> 'a nested -> 'b nested -> int
Обратите внимание, что этот синтаксис недействителен в OCaml: average имеет универсально квантифицированный тип 'a внутри типа одного из его аргументов, тогда как для полиморфной рекурсии универсально квантифицированный тип вводился до остальной части типа. Это положение универсально квантифицированного типа означает, что average является функцией полиморфного второго ранга. Этот тип функций высшего ранга напрямую не поддерживается OCaml: вывод типов для полиморфных функций второго и более высоких рангов неразрешим; поэтому для использования таких функций высшего ранга необходимо вручную обрабатывать эти универсально квантифицированные типы.
В OCaml есть два способа введения этого типа явных универсально квантифицированных типов: универсально квантифицированные поля записей,
# type 'a nested_reduction = { f:'elt. 'elt nested -> 'a };;
type 'a nested_reduction = { f : 'elt. 'elt nested -> 'a; } # let boxed_len = { f = len };;
val boxed_len : int nested_reduction = {f = } и универсально квантифицированные методы объектов:
# let obj_len = object method f:'a. 'a nested -> 'b = len end;; val obj_len : < f : 'a. 'a nested -> int > =
Для решения нашей проблемы мы можем использовать либо решение для записей:
# let average nsm x y = (nsm.f x + nsm.f y) / 2 ;; val average : int nested_reduction -> 'a nested -> 'b nested -> int =
или решение для объектов:
# let average (obj:<f:'a. 'a nested -> _ > ) x y = (obj#f x + obj#f y) / 2 ;; val average : < f : 'a. 'a nested -> int > -> 'b nested -> 'c nested -> int =
© 1995-2022 INRIA.
https://v2.ocaml.org/releases/5.0/htmlman/polymorphism.html
