Глава 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. Например, мы можем определить другую ссылку на опцию и сохранить в ней целое число:
# 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} После сохранения целого числа в 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
Действительно, посмотрев на тип хранилища, мы видим, что слабый тип '_weak1 был заменён типом int
# store;;
- : int option ref = {contents = Some 3} Следовательно, после размещения целого числа в store мы не можем использовать его для хранения чего-либо, кроме целого числа. Более того, слабые типы защищают программу от нежелательных мутаций значений с полиморфным типом.
Кроме того, слабые типы не могут появляться в сигнатуре модулей верхнего уровня: типы должны быть известны во время компиляции. В противном случае разные модули компиляции могли бы заменить слабый тип на разные и несовместимые типы. По этой причине компиляция следующего небольшого фрагмента кода
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 воспринимается проверяющим типы как определение функции и, следовательно, может быть обобщён. Такая манипуляция называется eta-расширением в лямбда-исчислении и иногда упоминается под этим именем.
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, который должен был бы возникнуть с ограничением на значения, так как f () является применением функции.
Ограничение на значения в сочетании с этим обобщением для ковариативных параметров типа называется смягчённым ограничением на значения.
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/4.14/htmlman/polymorphism.html
