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

Глава 6. Полиморфизм и его ограничения

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

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

1 Слабый полиморфизм и мутация

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

На этом этапе проверяющая типы система справедливо сообщает, что нельзя обменять целое число и функцию, а значение типа int всегда должно заменяться другим значением типа 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

В любом случае, это хорошая практика для таких глобальных изменяемых переменных. Иначе их тип будет определяться первым использованием. Если здесь допущена ошибка, позднее правильные варианты использования могут быть отмечены как ошибочные, что приведёт к запутанным сообщениям об ошибках типов.

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 как определение функции и поэтому может обобщить её тип. Этот приём в лямбда-исчислении называется эта-расширением; иногда его называют просто эта-расширением.

1.3 Ослабленное ограничение значений

Существует и другое частичное решение проблемы ненужных слабых типов, реализованное непосредственно в проверяющей типы системе. Кратко говоря, слабые типы, встречающиеся только в качестве параметров типов в ковариантных позициях (также называемых положительными позициями), можно безопасно обобщить до полиморфных типов. Например, тип 'a list ковариантен по 'a:

#   let f () = [];;

val f : unit -> 'a list = 

#   let empty = f ();;

val empty : 'a list = []

Обратите внимание, что для empty выведен тип 'a list, а не '_weak5 list, который возник бы при обычном ограничении значений.

Ограничение значений в сочетании с таким обобщением ковариантных параметров типов называется ослабленным ограничением значений.

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

В общем случае, как только переменная типа появляется в позиции, описывающей изменяемое состояние, она становится инвариантной. Следовательно, ковариантные переменные никогда не обозначают изменяемые ячейки памяти, и их можно безопасно обобщать. За более подробным описанием заинтересованные читатели могут обратиться к оригинальной статье Жака Гаррига: http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf

В сочетании ослабленное ограничение значений и ковариантность параметров типов позволяют во многих случаях избежать эта-расширения.

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 = 

2 Полиморфная рекурсия

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

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

# type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list;;

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[]] ];;

val l : int regular_nested =
  Nested [List [1]; Nested [List [2; 3]]; Nested [Nested []]]

Обратите внимание, что конструктор типа regular_nested в приведённом выше определении всегда имеет вид 'a regular_nested и использует один и тот же параметр 'a. С таким типом можно вычислить глубину с помощью классической рекурсивной функции:

# let rec regular_depth = function
    | List _ -> 1
    | Nested n -> 1 + List.fold_left max 1 (List.map regular_depth n);;

val regular_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 уровней вложенных списков. Затем можно адаптировать функцию regular_depth, определённую для regular_nested, получив функцию depth, вычисляющую это значение k. Для начала попробуем определить её так:

# let rec depth = function
    | List _ -> 1
    | Nested n -> 1 + depth n;;

Error: The value n has type 'a list nested
       but an expression was expected of type 'a nested
       The type variable 'a occurs inside 'a list

Ошибка типа возникает потому, что при определении depth проверяющая типы система сначала присваивает ей тип 'a -> 'b . При типизации сопоставления с образцом он становится 'a nested -> 'b, а после типизации ветви List — 'a nested -> int. Однако при типизации применения 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.

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
       The type int is not a type variable.
       The type int is not a type variable.
       The type int is not a type variable.

Здесь важно отметить, что полностью указывать тип 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

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]])

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 should not be a list literal, the expected type is 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 =