gds (gds) wrote,
gds
gds

subtyping / подтипизация / ocaml

В окамловском чятике ocaml@conference.jabber.ru dimitrykakadu спросил, что же такое "+'a" в определении типовых параметров. На страницах нашей уютненькой жыжыцы редакция сейчас будет отвечать за базар.
Итак, кратко: +'a означает, что данный параметр ковариантно входит в тип. -'a — соответственно, контрвариантно. Просто 'a — ни так, ни эдак (инвариантно).
Под катом — объяснение подтипизации за 21 день.

Типы обозначим заглавными буквами.
Факт того, что везде, где применимо значение с типом B, применимо значение с типом A, назовём "A является подтипом B", и обозначим как A ⊆ B.
Обычно подразумевают, что ∀A, A ⊆ A.

Если Ssub ⊆ Ssup и Tsub ⊆ Tsup, то (Ssup → Tsub) ⊆ (Ssub → Tsup).
(Смотрите внимательно на эти затейливые индексы!)
На русском языке это формулируется так: если есть функция, то вместо неё можно использовать функцию, которая берёт аргумент с более "широким" типом, и возвращает значение с более "узким" типом. То есть, если функция должна брать узкий тип, вместо неё можно подсунуть функцию, которая берёт широкий тип (всё равно, значения из "разницы" между типами по-любому не будут переданы). Если функция должна возвращать значение с широким типом, то вместо неё можно подсунуть функцию, возвращающую значение с более узким типом — тот, кто получит это значение, если уж умеет обрабатывать значения широкого типа, уж точно обработает значение узкого типа.

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

Если возьмём тип U, населённый ровно одним значением (я про окамловский тип unit например), то существует изоморфизм между типом T и типом U→T (то есть, любое значение x:T можно однозначно представить как fun () -> x, и из любой функции с типом unit -> T можно однозначно получить значение с типом T). Далее, так как U ⊆ U, то из правила подтипизации функций следует, что Tsub ⊆ Tsup ⇒ (U → Tsub) ⊆ (U → Tsup), что вполне согласуется с интуицией.

Если рассмотрим параметризованные типы вида T A B .. Z (что соответствует окамловскому type t 'a 'b .. 'z = ..), то отношение подтипизации типов-параметров (A, B, .. Z) может вызывать отношение подтипизации параметризованных типов в целом. Мы можем рассматривать каждый параметр отдельно, поэтому для простоты рассмотрим тип с одним параметром, T A.
Могут быть три варианта. Если Asub ⊆ Asup, то:
1. Тип A входит ковариантно: Asub ⊆ Asup ⇒ T Asub ⊆ T Asup.
2. Тип A входит контрвариантно: Asub ⊆ Asup ⇒ T Asup ⊆ T Asub.
3. Тип A входит ни ковариантно, ни контрвариантно: из Asub ⊆ Asup мы не можем сделать вывод об отношении подтипизации между T Asub и T Asup. (можем также говорить "инвариантно".)
Первый случай обозначается в окамле как type t +'a = .., второй — type t -'a = .., третий — type t 'a = ...

Аналог вариантности в алгебре — монотонность функции. Может быть монотонная: a<b ⇒ f(a)<f(b), может быть антимонотонная: a<b ⇒ f(a)>f(b), а может быть так, что из a<b не следует ни то, ни другое.

Типы-произведения ковариантны по обоим аргументам: type pair +'a +'b = ('a * 'b);

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

В качестве примера рассмотрим классические списки, type list 'a = [ Nil | Cons of 'a and list 'a ];. Для каждого из его конструкторов рассмотрим его подтипизацию.
∀'a, 'b, (Nil : list 'a) ⊆ (Nil : list 'b), так как он не содержит типового параметра, и этот конструктор ничем не ограничивает подтипизацию значений с типом list 'a (то есть, можно считать, что он как ковариантен, так и контрвариантен по 'a).
Конструктор Cons of 'a and list 'a изоморфен произведению ('a * list 'a), которое вариантно по 'a, но вариантность list 'a мы пока не знаем (так как собственно её и вычисляем). В данном случае нам надо предположить, какой может быть вариантность list 'a (ко-, контра- или никакой), и согласовать уравнение "вариантность list 'a = вариантность ('a * list 'a) = ковариантно по a и ?вариантно по list 'a". (Если бы записать тип как type list 'a = μ β . [ Nil | Cons of 'a and β ] или как-то наподобие того, рассуждения про вариантность становятся гораздо стройнее, но это не является моей целью.) Так вот, уравнение сходится в случае, когда list 'a либо ковариантно, либо инвариантно по 'a. На практике гораздо удобнее, когда list 'a ковариантно по 'a.

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

Конструктор "стрелка" или "лямбда-абстракция" можно также выписать явно:
type app -'s +'t = 's -> 't;
Обратите внимание, что вариантности расставлены ровно согласно определениям выше.
В функциональном программировании контрвариантность обычно является следствием того, что значение находится слева от стрелки. Так как всегда можно сделать uncurrying и преобразовать функцию с многими аргументами в функцию над аргументом-туплом (который ковариантен по всем аргументам), и этот аргумент будет в контрвариантной позиции, то каждый из аргументов будет контрвариантен: type app3 -'s1 -'s2 +'t = 's1 -> 's2 -> 't;.
Вариантность меняется на противоположную, когда тип стоит слева от стрелки: type appapp +'a -'b +'c = ('a -> 'b) -> 'c;

Далее рассмотрим ссылки, ref 'a. У них есть две операции: взятие текущего значения и присвоение нового значения.
В случае, когда мы берём значение из ссылки, тип ref 'a ковариантен по типовому параметру. Это значит, что если 'a ⊆ 'b, то по отношении к операции взятия будет ref 'a ⊆ ref 'b. Единственное нормальное объяснение, которое я могу придумать, таково: если контекст ожидает значение с типом 'b, то он может вместо него получить значение с типом 'a, и, следовательно, если перед этим берём это значение из ссылки с типом ref 'b, то вместо этого можем взять значение из ссылки с типом ref 'a.
Если же присваиваем, ref 'a контрвариантен. Если 'a ⊆ 'b, то присваивать мы можем значение только более "узкого" типа (логика та же, как в объяснении контрвариантности аргументов функции), то есть ref 'b ⊆ ref 'a.
Таким образом, ref 'a ⊆ ref 'b может выполняться тогда и только тогда, когда 'a ⊆ 'b и 'b ⊆ 'a. (В некоторых системах типов это достигается только при 'a = 'b, но не во всех.) А если в целом, то ref 'a инвариантно по 'a.
Интересным, но на практике мало нужным экспериментом будет изобразить такие типы type sink -'a; и type source +'a;, которые в свою очередь были бы подтипами type ref 'a;.

Всё, сказанное про ссылки, относится и к массивам.

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

Так-то!

upd1/
В редакцию поступила телеграмма о том, что неплохо бы рассказать про LSP — принцип подстановки им. Барбары Лисков. Редакция продолжает отвечать за базар, прямо в этом посте.

Оригинально этот принцип формулируется так:
Пусть q(x) является свойством, верным относительно объектов x некоторого типа T. Тогда q(y) также должно быть верным для объектов y типа S, где S является подтипом типа T.

То есть, принцип говорит о том, что свойства программы (корректность, например) не должны измениться, если вместо значения x с типом T мы подсунем значение y с типом S.
С другой стороны, подтипизация полиморфных вариантов и объектов — это штука серьёзная, не для fp-kiddies, которые довольствуются только индуктивными типами данных и записями. Как и всякий сложный инструмент, подтипизацию надо использовать с умом. Заменителем ума в данном случае может стать тот самый принцип подстановки.
Однако трансляторы языков программирования не могут доказать выполнения всех свойств программы для любых подтипов, которые существуют или будут существовать в программе, поэтому подтипизация отдана на откуп программисту, и подтипизация с принципом подстановки, в общем-то, ортогональны. (там, где подтипизация осуществляется номинально, а не структурно, и нет индуктивных типов данных, читать как "наследование и принцип подстановки ортогональны".)
Примеры несоблюдения принципа подстановки для номинальной подтипизации объектов смотрите, например, в статье про Квадрат-Прямоугольник.
В случае подтипизации вариантов история ещё хуже, так как код, работающий со значениями вариантного типа, разбросан по всему коду, знающему структуру вариантного типа, и при изменении структуры придётся менять весь код, который эту структуру использует. Поэтому зачастую предпочитают скрывать структуру вариантного типа (даже обычного sum type, без подтипизации), выводя наружу только интерфейс для работы со значениями абстрактного типа. В случае, когда меняется только представление значений типа данных (вариантный тип), но не операции над значениями типа, это помогает. (кроме того, это слегка помогает даже в тех случаях, когда меняются операции и логика в целом.)

Можно как иметь осуществлённой подтипизацию между двумя типами данных, так и не иметь её из-за свойств языка или чего-либо другого (архитектуры, может быть). Для двух типов данных может как выполняться принцип подстановки, так и не выполняться (при этом не важно, являются ли они подтипами с точки зрения языка).

 

Принцип не выполняется

Принцип выполняется

Нет подтипизации

Живите с миром, у вас всё хорошо (1)

Для удобства можно эмулировать подтипизацию (2)

Есть подтипизация

Будьте аккуратны с подтипизацией! (3)

"Всё правильно сделал" (4)


(1) — не нужно натягивать подтипизацию туда, где она не нужна.
(2) — вот тут вам придётся или дублировать код, или оборачивать разные типы в значения одного типа. Классический секс, который ожидает любителей функционального программирования, где нет подтипизации сумм и произведений (т.е. индуктивных типов данных и объектов).
(3) — вот тут вам придётся худо, если будете расширять архитектуру наследованием — классический секс для фанбоев ООП. И даже хуже: в тех языках, где есть неявное приведение типов, существует отношение подтипизации между такими типами, для которых соблюдение принципа подстановки — скорее редчайшая случайность, нежели закон. (рассмотрите сишное приведение типов, как бы дающее подтипизацию double ⊆ int, по отношению к законам арифметических операций, например.)
(4) — используйте подтипизацию, соблюдайте LSP, будьте счастливы в личной жизни. Если же подтипизация мешает — для того же окамла всегда можно откатиться до варианта (2).

Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 6 comments
А что насчет вывода вариантности? Есть ли он? Возможен ли он?
Для случаев, когда указывается "тело" типа, окамл всегда выводит вариантности сам, и при явно указанных вариантностях только проверяет их (например, можно попробовать определить тип с неправильной вариантностью, но его не пропустит). Вариантности нужно указывать вроде бы только для абстрактных типов (например, в сигнатурах, когда пишут type someabstract +'a -'b;;). То есть, при сокрытии тела типа программист должен указать, хочет ли он скрыть также вариантности, или их надо протащить так, чтобы пользователи этого типа их знали и использовали.
Спасибо!

Отличный пост. Еще бы примеров из народного хозяйства.
И ещё момент. Когда есть тело типа даже с указанными вариантностями, при печати этого типа (в топлевеле либо через ocamlc -i) вариантности не указываются (хотя они есть). Это связано с тем, что при "парсинге" данного определения типа они будут вычислены на основании тела типа, и их указывать не надо (видимо, пугает людей). Неочевидный момент такой.
Я правильно понял, что в mliшке надо прописывать плюсики руками? Что бы сторонние люди, читающие мой код не задавались, поставленными выше вопросами?

Для полноты картины, возможно, стоит добавить кусок кода, который не компилится, но если добавить +, то компилится. А я пока попытаюсь найти простой пример в Core и Core_extended.
#use "topfind";;
#camlp4r;;

module Lst
 :
  sig
    type lst +'a;
    value of_list : list 'a -> lst 'a;
    value iter : ('a -> unit) -> lst 'a -> unit;
  end
 =
  struct
    type lst 'a = list 'a;
    value of_list x = x;
    value iter = List.iter;
  end
;

type my_sub = [= `A | `B ]
;

type my_sup = [= my_sub | `C ]
;

value my_sub_val : my_sub = `A
;

value (my_sub_list : Lst.lst my_sub) = Lst.of_list [`A; `B]
;

value my_sup_printer (x : my_sup) =
  print_string
    (match x with
     [ `A -> "A"
     | `B -> "B"
     | `C -> "C"
     ]
    )
;

(* обламывается без явного coercion:
value () = my_sup_printer my_sub_val;
*)

(* получается, так как между типами можно провести
   отношение подтипизации: *)
value () = my_sup_printer (my_sub_val :> my_sup);

value () = print_newline ();

(* обламывается без явного coercion:
value () = Lst.iter my_sup_printer my_list;
*)

(*
Если Lst.lst инвариантный, то подтипизацию вывести нельзя,
и возникает ошибка:
Error: Type Lst.lst my_sub is not a subtype of Lst.lst my_sup
*)
value () = Lst.iter my_sup_printer (my_sub_list :> Lst.lst my_sup);