• Ядро языка
• Система модулей
• Объекты в 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

Действительно, взглянув на тип хранилища, мы видим, что слабый тип '_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 для чтения этого содержимого как значения типа x, что нарушило бы систему типов.

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

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

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

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

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