Русская Википедия:Параметрический полиморфизм

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Шаблон:Полиморфизм Параметрический полиморфизм в языках программирования и теории типов — свойство семантики системы типов, позволяющее обрабатывать значения разных типов идентичным образом, то есть исполнять физически один и тот же код для данных разных типовШаблон:SfnШаблон:Sfn.

Параметрический полиморфизм считается «истинной» формой полиморфизмаШаблон:Sfn, делая язык более выразительным и существенно повышая коэффициент повторного использования кода. Традиционно ему противопоставляется ad-hoc-полиморфизмШаблон:Sfn, предоставляющий единый интерфейс к потенциально различному коду для разных допустимых в данном контексте типов, потенциально не совместимых (статически или динамически). В ряде исчислений, например, в теории квалифицированных типов, ad-hoc-полиморфизм рассматривается как частный случай параметрического.

Параметрический полиморфизм лежит в основе систем типов языков семейства ML; такие системы типов называют полиморфными. В сообществах языков с неполиморфными системами типов (потомки Алгола и BCPLШаблон:Sfn) параметрически полиморфные функции и типы называют «обобщёнными».

Полиморфизм типов

Термин «параметрический полиморфизм» традиционно используется для обозначения типобезопасного параметрического полиморфизма, хотя существуют и нетипизированные его формы (см. параметрический полиморфизм в Си и C++)Шаблон:Sfn. Ключевым понятием типобезопасного параметрического полиморфизма, помимо полиморфной функции, является полиморфный тип.

Полиморфный тип (Шаблон:Lang-en), или политип (Шаблон:Lang-en) — это тип, параметризованный другим типом. Параметр в слое типов называется переменной типа (или ти́повой переменной).

Формально полиморфизм типов изучается в полиморфно типизированном лямбда-исчислении, называемом Системой F.

Например, функция append, сцепляющая два списка в один, может быть построена независимо от типа элементов списка. Пусть ти́повая переменная a описывает тип элементов списка. Тогда функция append может быть типизирована как «forall a. [a] × [a] -> [a]» (здесь конструкция [a] означает тип «список, каждый элемент которого имеет тип a» — синтаксис, принятый в языке Haskell). В этом случае говорят, что тип параметризован переменной a для всех значений a. В каждом месте применения append к конкретным аргументам значение a разрешается, причём каждое её упоминание в Шаблон:Iw подменяется значением, соответствующим контексту применения. Таким образом, в данном случае сигнатура функционального типа требует идентичности типов элементов обоих списков и результата.

Множество допустимых значений переменной типа задаётся посредством квантификации. Простейшими кванторами являются универсальный (как в примере с append) и экзистенциальный (см. далее).

Квалифицированный тип (Шаблон:Lang-en) — это полиморфный тип, дополнительно снабжённый набором предикатов, регламентирующих спектр допустимых значений параметра этого типа. Иначе говоря, квалификация типа позволяет управлять квантификацией произвольным образом. Теорию квалифицированных типов построил Марк Джонс (Шаблон:Lang-en2) в 1992 годуШаблон:Sfn. Она предоставляет общее обоснование для самых экзотичных систем типов, включая классы типов, расширяемые записиШаблон:Переход и Шаблон:Iw и позволяет точно формулировать особые ограничения для конкретных полиморфных типов, устанавливая таким образом отношения между параметрическим и ad-hoc-полиморфизмом (перегрузкой), а также между явной и неявной перегрузкой. Связь типа с предикатом в этой теории называется свидетельством (Шаблон:Lang-en). Для свидетельств сформулирована алгебра, аналогичная лямбда-исчислению, включающая абстракцию свидетельств, применение свидетельств и т. д. Соотнесение терма этой алгебры с явно перегруженной функцией называется трансляцией свидетельства (Шаблон:Lang-en).

Мотивирующими примерами для разработки обобщённой теории послужили классы типов Вадлера — Блотта и типизация расширяемых записей посредством предикатов Харпера — ПирсаШаблон:SfnШаблон:Sfn.

Классификация полиморфных систем

Шаблон:Викиучебник

Параметрически полиморфные системы типов принципиально классифицируются по рангуШаблон:Переход и по свойству предикативностиШаблон:Переход. Кроме того, различаются явный и неявный полиморфизмШаблон:Sfn и ряд других свойств. Неявный полиморфизм обеспечивается за счёт выведения типов, что существенно повышает удобство использования, но имеет ограниченную выразительность. Многие практические параметрически полиморфные языки разделяют фазы внешнего неявно типизированного языка (Шаблон:Lang-en) и внутреннего явно типизированного (Шаблон:Lang-en).

Наиболее общей формой полиморфизма является «импредикативный полиморфизм высших рангов». Наиболее популярными ограничениями этой формы являются полиморфизм 1-го ранга, называемый «пренексным»Шаблон:Переход, и предикативный полиморфизмШаблон:Переход. Вместе они образуют «предикативный пренексный полиморфизм», близкий к реализованному в ML и в ранних версиях Хаскела.

С усложнением систем типов сигнатуры типов становятся настолько сложными, что полное или почти полное их выведение начинает рассматриваться многими исследователями как критичное свойство, отсутствие которого сделает язык непригодным для практикиШаблон:SfnШаблон:Sfn. Например, для традиционного комбинатора map полная сигнатура типа (с учётом родовой квантификации) в условиях типобезопасного отслеживания потока исключенийШаблон:Переход принимает следующий видШаблон:SfnШаблон:Sfn (как и вышеШаблон:Переход, [a] означает список элементов типа a):
<math>val\;map \colon \forall\alpha\colon\star _\cdot \forall\beta\colon\star _\cdot \forall\gamma\colon\emptyset _\cdot \forall\delta\colon\emptyset _\cdot (\; \alpha \xrightarrow{\gamma} \beta\; )\; \xrightarrow{\delta} \;(\; \left [ \alpha \right ] \xrightarrow{\gamma} \left [ \beta \right ] \;)</math>

Ранг

Ранг полиморфизма показывает допустимую в рамках системы глубину вложения кванторов переменных типа. «Полиморфизм ранга k» (при k > 1) позволяет конкретизировать переменные типа полиморфными типами ранга не выше (k — 1). «Полиморфизм высших рангов» позволяет ставить кванторы переменных типа слева от произвольного числа стрелок в типах высших порядков.

Джо Уэллс (Шаблон:Lang-en) доказалШаблон:Sfn, что выведение типов для Системы F, типизированной по Карри, неразрешимо для рангов выше 2-го, так что при использовании более высоких рангов необходимо использовать явное аннотирование типамиШаблон:Sfn.

Существуют системы типов с частичным выведением, требующие аннотирования только невыводимых ти́повых переменныхШаблон:SfnШаблон:SfnШаблон:Sfn.

Пренексный полиморфизм

Полиморфизм ранга 1 часто называется пренексным (от слова «пренекс» — см. Шаблон:Iw). В пренексно полиморфной системе переменные типа не могут конкретизироваться полиморфными типами. Это ограничение делает различие между мономорфными и полиморфными типами существенным, из-за чего в пренексной системе полиморфные типы нередко называют «схемами типизации» (Шаблон:Lang-en) для отличения их от «обычных» (мономорфных) типов (монотипов). Как следствие, все типы могут быть записаны в форме, когда все кванторы переменных типа вынесены в самую внешнюю (пренексную) позицию, что и называется Шаблон:Iw. Проще говоря, разрешается полиморфное определение функций, но запрещается передавать полиморфные функции в качестве аргументов другим функциямШаблон:Sfn[1] — полиморфно определённые функции должны быть инстанцированы монотипом перед использованием.

Близким эквивалентом является так называемый «Let-полиморфизм» или «полиморфизм в стиле ML» Дамаса — Милнера. Технически, Let-полиморфизм в ML имеет дополнительные синтаксические ограничения, такие как «ограничение на значения» (Шаблон:Lang-en2), связанное с проблемой типобезопасности при использовании ссылок (не возникающих в чистых языках, таких как Haskell и Clean)Шаблон:SfnШаблон:Sfn.

Предикативность

Предикативный полиморфизм

Предикативный (ограниченный условием) полиморфизм требует, чтобы переменная типа была конкретизирована монотипом (не политипом).

К предикативным системам относятся интуиционистская теория типов и Шаблон:Iw.

Импредикативный полиморфизм

Импредикативный (безусловный) полиморфизм разрешает конкретизировать переменную типа произвольным типом — как мономорфным, так и полиморфным, включая сам определяемый тип. (Разрешение в рамках некоего исчисления рекурсивного включения системы в саму себя называется Шаблон:Iw. Потенциально это может приводить к парадоксам типа Расселовского или КанторовскогоШаблон:Sfn, но в случае с тщательно продуманной системой типов этого не происходитШаблон:Sfn.)

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

Примером импредикативной системы является Система F и её расширения (см. лямбда-куб)Шаблон:Sfn.

Поддержка рекурсии

Шаблон:Main

Традиционно в потомках ML функция может быть полиморфной только при взгляде «извне» (то есть её можно применять к аргументам различных типов), но её определение может содержать только мономорфную рекурсию (то есть разрешение типов осуществляется до вызова). Распространение реконструкции типов по ML на рекурсивные типы не представляет серьезных трудностей. С другой стороны, сочетание реконструкции типов с рекурсивно определёнными термами порождает сложную проблему, известную под названием Шаблон:Iw. Майкрофт (Шаблон:Lang-en2) и Мейртенс (Шаблон:Lang-en2) предложили полиморфное правило типизации, позволяющее конкретизировать различными типами рекурсивные вызовы рекурсивной функции из её собственного тела. В этом исчислении, известном как исчисление Милнера — Майкрофта, выведение типов неразрешимо.Шаблон:Sfn

Полиморфизм структурных типов

Типы-произведения (также известные как «записи») служат формальной базой для объектно-ориентированного и модульного программирования. Их Шаблон:Iw пару составляют типы-суммы (также известные как «Шаблон:Iw»)Шаблон:SfnШаблон:SfnШаблон:Sfn:

<math>\neg \lbrace a \land b \rbrace = \langle \neg a \lor \neg b \rangle</math>
<math>\neg \langle a \lor b \rangle = \lbrace \neg a \land \neg b \rbrace</math>

Вместе они являются средством выражения любых сложных структур данных и некоторых аспектов поведения программШаблон:Переход.

Исчисление записей (Шаблон:Lang-en) — обобщённое название проблемы и ряда её решений, касающихся вопросов гибкости типов-произведений в языках программирования при условии типобезопасностиШаблон:SfnШаблон:SfnШаблон:Sfn. Термин нередко распространяется и на типы-суммы, а границы понятия «тип записи» могут варьироваться от исчисления к исчислению (как и само понятие «тип»). Применяются также термины «полиморфизм записей» (что, опять же, зачастую включает в себя полиморфизм вариантов)Шаблон:Sfn, «исчисление модулей»Шаблон:Sfn и «структурный полиморфизм».

Общие сведения

Произведения и суммы типов (записи и Шаблон:Iw) обеспечивают гибкость при построении сложных структур данных, но ограничения многих реальных систем типов зачастую не позволяют использовать их по-настоящему гибко. Эти ограничения обычно возникают в связи с вопросами эффективности, выведения типов или просто удобства использования.Шаблон:Sfn

Классическим примером может служить язык Шаблон:Nowrap, система типов которого была умышленно ограничена ровно настолько, чтобы сочетать простоту реализуемости с выразительностью и математически доказуемой типобезопасностью.

Пример определения записи: 

> val r = {name = "Foo", used = true};
(* val r : {name : string, used : bool} = {name = "Foo", used = true} *)

Доступ к значению поля по его имени осуществляется префиксной конструкцией вида #field record: 

> val r1 = #name r;
(* val r1 : string = "Foo" *)

Следующее определение функции над записью является корректным: 

> fun name1 (x: {name : string, age : int}) = #name x

А следующее порождает ошибку компилятора о том, что тип не разрешён полностью: 

> fun name2 x = #name x
(* unresolved type in declaration:
      {name : '1, ...} *)

Мономорфизм записей делает их негибким, но эффективным средствомШаблон:Sfn: поскольку фактическое расположение в памяти каждого поля записи известно заранее (на этапе компиляции), обращение к нему по имени компилируется в прямую индексацию, что обычно вычисляется за одну машинную инструкцию. Однако, при разработке сложных масштабируемых систем желательно иметь возможность абстрагировать поля от конкретных записей — например, определить универсальный селектор полей: 

fun select r l = #l r

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

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

datatype 'a foo = A of 'a
                | B of ('a * 'a)
                | C

всякая функция над ним будет иметь вид 

fun bar (p:'a foo) =
   case p of
        A x => ...
      | B (x,y) => ...
      | C => ...

и при удалении любого из предложений компилятор выдаст предупреждение о неполноте разбора («match nonexhaustive»). Для случаев, когда из множества вариантов лишь некоторые требуют анализа в данном контексте, можно организовать default-ветвление при помощи т. н. «джокера» — универсального образца, с которым сопоставимы все допустимые (согласно типизации) значения. Для его записи используется символ подчёркивания («_»). Например: 

fun bar (p:'a foo) =
   case p of
        C => ...
      | _ => ...

В некоторых языках (в Шаблон:Nowrap, в Haskell) даже «более простая» конструкция if-then-else является лишь синтаксическим сахаром над частным случаем ветвления, то есть выражение 

if A
   then B
   else C

уже на этапе грамматического разбора представляется в виде 

case A of
     true => B
   | false => C

либо 

case A of
     true => B
   | _ => C

Синтаксический сахар

В Шаблон:Nowrap записи и варианты являются мономорфными, однако, поддерживается синтаксический сахар для работы с записями со множеством полей, называемый «универсальным образцом»Шаблон:Sfn: 

> val r = {name = "Foo", used = true};
(* val r : {name : string, used : bool} = {name = "Foo", used = true} *)
> val {used = u, ...} = r;
(* val u : bool = true *)

Многоточие в типе «{used, ...}» означает, что в данной записи существуют и другие поля, помимо упомянутых. Однако полиморфизм записей как таковой отсутствует (даже пренексныйШаблон:Переход): требуется полное статическое разрешение информации о мономорфном типе записи (посредством выведения или явного аннотирования).

Расширение и функциональное обновление записей

Термин расширяемые записи (Шаблон:Lang-en2) используется для обобщённого обозначения таких операций, как расширение (построение новой записи на основе имеющейся с добавлением новых полей), обрезание (взятие указанной части от имеющейся записи) и др. В частности, он подразумевает возможность так называемого «функционального обновления записей» (Шаблон:Lang-en2) — операции построения нового значения записи на основе имеющегося путём копирования имён и типов его полей, при которой одно или несколько полей в новой записи получают новые значения, отличающиеся от исходных (и, возможно, имеющие другой тип).Шаблон:SfnШаблон:SfnШаблон:Sfn[2][3][4]

Сами по себе операции функционального обновления и расширения ортогональны полиморфизму записей, но их полиморфное использование представляет особый интерес. Даже для мономорфных записей приобретает большое значение возможность опускать явное упоминание полей, копируемых без изменений, а это фактически представляет собой полиморфизм записей в чисто синтаксической формеШаблон:Переход. С другой стороны, если рассматривать все записи в системе как расширяемые, то это позволяет типизировать функции над записями как полиморфные.

Пример простейшего варианта конструкции реализован в Alice ML (согласно действующим соглашениям по successor ML)[3]. Универсальный образец (многоточиеШаблон:Переход) имеет расширенные возможности: посредством его можно осуществлять «захват ряда» с тем, чтобы работать с «оставшейся» частью записи как со значением: 

> val r = {a = 1, b = true, c = "hello"}
(* r = {a = 1, b = true, c = "hello"} *)
> val {a = n, ... = r1} = r
(* r1 = {b=true, c="hello"} *)
> val r2 = {d = 3.14, ... = r1}
(* r2 = {b=true, c="hello", d=3.14} *)

Функциональное обновление реализуется как производная форма от захвата ряда с помощью служебного слова where. Например, следующий код: 

> let
     val r = { a = 1, c = 3.0, d = "not a list", f = [1], p = ["not a string"], z = NONE }
  in
     { r where d = nil, p = "hello" }
  end

будет автоматически переписан в форме: 

> let
     val r = { a = 1, c = 3.0, d = "not a list", f = [1], p = ["not a string"], z = NONE }
     val { d = _, p = _, ... = tmp } = r
  in
     { ... = tmp, d = nil, p = "hello" }
  end

Конкатенация записей

Одними из первых (конец 1980-х — начало 1990-х) были предложены различные варианты формализации расширяемых записей через операции конкатенации над неполиморфными записями (Харпер — ПирсШаблон:Sfn, ВандШаблон:Sfn, СальцманнШаблон:Sfn). Шаблон:Iw даже использовал операции над записями вместо полиморфизма в языке Amber. Для этих исчислений нет известного способа эффективной компиляции; кроме того, эти исчисления весьма сложны и с точки зрения теоретико-ти́пового анализа.Шаблон:SfnШаблон:SfnШаблон:SfnШаблон:Sfn

НапримерШаблон:Sfn: 

val car = { name = "Toyota"; age = "old"; id = 6678 }
val truck = { name = "Toyota"; id = 19823235 }
...
val repaired_truck = { car and truck }

Ванд (автор рядного полиморфизмаШаблон:Переход) показал, что посредством конкатенации записей можно моделировать множественное наследованиеШаблон:SfnШаблон:Sfn.

Структурная подтипизация Карделли

Шаблон:Нп2 исследовал возможность формализовать «полиморфизм записей» посредством отношений подтипизации на записях: для этого запись рассматривается как «универсальный подтип», то есть разрешается отнесение её значения ко всему множеству её супертипов. Этот подход также поддерживает наследование методов и служит теоретико-ти́повой базой для наиболее распространённых форм объектно-ориентированного программирования.Шаблон:SfnШаблон:SfnШаблон:Sfn

Карделли представил вариант метода компиляции полиморфизма записей через их подтипы посредством предопределения смещения всех возможных меток в потенциально огромной структуре со множеством пустых слотовШаблон:Sfn.

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

> if true then {A = 1, B = true} else {B = false, C = "Cat"}
(* val it : {B : bool} *)

имеет тип {B : bool}, но его динамическое значение равно {A = 1, B = true}, то есть информация о типе расширяемой записи теряетсяШаблон:Sfn, что представляет серьёзную проблему для проверки операций, требующих для своего исполнения полной информации о структуре значения (таких как сравнение на равенство)Шаблон:Sfn. Наконец, при наличии подтипов выбор между упорядоченным и неупорядоченным представлением записей серьёзно влияет на производительностьШаблон:Sfn.

Популярность подтипизации обусловлена тем, что она предоставляет простые и наглядные решения для многих задач. Например, объекты разных типов можно помещать в единый список, если они имеют общий супертипШаблон:Sfn.

Рядный полиморфизм Ванда

Шаблон:Нп2 в 1987 году предложил идею захватывать информацию об «оставшейся» (не указанной явно) части записи посредством того, что он назвал рядной ти́повой переменной (Шаблон:Lang-en2)Шаблон:Sfn.

Рядная переменная — это переменная типа, пробегающая множество конечных наборов (рядов) типизированных полей (пар «(значение : тип)»). В результате появляется возможность реализовать «наследование вширину» непосредственно на основе параметрического полиморфизма, лежащего в основе ML,— без усложнения системы типов правилами Шаблон:Iw. Получаемую разновидность полиморфизма называют рядным полиморфизмом (Шаблон:Lang-en2). Рядный полиморфизм распространяется как на произведения типов, так и на суммы типов.

Ванд заимствовал термин Шаблон:Lang-en (ряд, цепочка, строка) из Алгола-68, где он означал набор представлений. В русскоязычной литературе этот термин в контексте Алгола традиционно переводился как «мультивид». Встречается также вариант перевода «row variables» как «строчные переменные»Шаблон:Sfn, который может вызвать путаницу со строчными буквами в строковых типах.

Пример (язык OCaml; синтаксис постфиксный, record#field)Шаблон:Sfn: 

# let send_m a = a#m ;;
(* value send_m : < m : a; .. > -> a = <fun> *)

Здесь многоточие (из двух точек) — это принятый в OCaml синтаксис для безымянной рядной ти́повой переменной. За счёт такой типизации, функция send_m может быть применена к объекту любого (заранее не известного) объектного типа, в состав которого входит метод m соответствующей сигнатуры.

Выведение типов для исчисления Ванда в первоначальной версии было неполным: из-за отсутствия ограничений на расширение ряда, добавление поля при совпадении имени подменит существующее — в результате не все программы имеют главный типШаблон:SfnШаблон:Sfn. Однако, эта система была первым конкретным предложением по расширению ML записями, поддерживающими наследованиеШаблон:Sfn. В последующие годы был предложен целый ряд различных доработок, в том числе, делающих его полнымШаблон:SfnШаблон:Sfn.

Наиболее заметный след оставил Дидье́ Реми́ (Шаблон:Lang-fr). Он построил практичную систему типов с расширяемыми записями, включающую полный и эффективный алгоритм реконструкции типовШаблон:SfnШаблон:Sfn. Реми расслаивает язык типов на сорта, формулируя сортированную алгебру типов (Шаблон:Lang-en). Различаются сорт собственно типов (в том числе типов полей) и сорт полей; вводятся отображения между ними и на их основе формулируются правила типизации расширяемых записей как простое расширение классических правил ML. Информация о присутствии (Шаблон:Lang-en) поля определяется как отображение из сорта типов в сорт полей. Рядные ти́повые переменные переформулируются как переменные, принадлежащие сорту полей и равные константе отсутствия (Шаблон:Lang-en), являющейся элементом сорта полей, не имеющим соответствия в сорте типов. Операция вычисления типа для записи из n полей определяется как отображение n-арного поля в тип (где каждое поле в кортеже либо вычисляется функцией присутствия, либо задаётся константой отсутствия).

Упрощённо идею исчисления можно трактовать как расширение типа всякого поля записи флагом присутствия/отсутствия и представление записи в виде кортежа со слотом для каждого возможного поляШаблон:Sfn. В прототипе реализации синтаксис языка типов был сделан приближенным к теоретико-ти́повой формулировке, напримерШаблон:Sfn: 

# let car = { name = "Toyota"; age = "old"; id = 7866 } ;;
(* car : ∏ (name : pre (string); id : pre (num); age : pre (string); abs) *)

# let truck = { name = "Blazer"; id = 6587867567 } ;;
(* truck : ∏ (name : pre (string); id : pre (num); abs) *)

# let person = { name = "Tim"; age = 31; id = 5656787 } ;;
(* person : ∏ (name : pre (string); id : pre (num); age : pre (num); abs) *)

(символ ∏ у Реми означает операцию вычисления типа)

Добавление нового поля записывается с помощью конструкции with: 

# let driver = { person with vehicle = car } ;;
(* driver : ∏ (vehicle : pre (∏ (name : pre (string); id : pre (num); age : pre (string); abs));
              name : pre (string); id : pre (num); age : pre (num); abs) *)

Функциональное обновлениеШаблон:Переход записывается идентично, с той разницей, что упоминание уже существующего поля переопределяет его: 

#let truck_driver = { driver with vehicle = truck };;
(* truck driver : ∏ (vehicle : pre (∏ (name : pre (string); id : pre (num); abs));
                    name : pre (string); id : pre (num); age : pre (num); abs) *)

Эта схема формализует ограничение, необходимое для проверки операций над записями и выведения главного типа, но не ведёт к очевидной и эффективной реализацииШаблон:SfnШаблон:Sfn. Реми использует хеширование, что довольно эффективно в среднем, но увеличивает издержки во время исполнения даже для исходно мономорфных программ и плохо подходит для записей с большим числом полейШаблон:Sfn.

В дальнейшем Реми исследовал использование рядного полиморфизма совместно с Шаблон:Iw, подчеркнув, что это ортогональные понятия, и показав, что записи становятся наиболее выразительными при их одновременном использованииШаблон:Sfn. На этой основе он совместно с Жеромом Вуйоном (Шаблон:Lang-fr) предложил легковесное объектно-ориентированное расширение для MLШаблон:Sfn. Это расширение было реализовано в языке «Caml Special Light» Ксавье Леруа, превратив его в OCamlШаблон:Sfn. Объектная модель OCaml тесно сплетает использование структурной подтипизацииШаблон:Переход и рядного полиморфизмаШаблон:Sfn, из-за чего порой их ошибочно отождествляют. Рядный полиморфизм произведений в OCaml лежит в основе выведения типов; отношения подтипизации не являются необходимыми в языке с его поддержкой, но дополнительно повышают гибкость на практикеШаблон:SfnШаблон:SfnШаблон:Sfn. В OCaml реализован более простой и наглядный синтаксис для информации о типах.

Жак Гарри́га (Шаблон:Lang-fr) реализовалШаблон:Sfn практичную систему полиморфных сумм. Он совместил теоретические работы Реми и ОхориШаблон:Переход, построив систему, пролегающую посередине: информация о наличии меток в записи представляется посредством использования родо́в, а информация об их типах использует рядные переменные. Чтобы компилятор мог отличать полиморфные суммы от мономорфных, Гаррига использует специальный синтаксис (обратный апостроф, предваряющий тег). При этом исчезает необходимость в объявлении типа — можно сразу писать функции над ним, и компилятор будет выводить минимальный список тегов по мере композиции этих функций. Эта система стала частью OCaml около 2000 года, но не вместо, а в дополнение к мономорфным суммам, так как они несколько менее эффективны, и из-за невозможности контроля полноты разбора затрудняют поиск ошибок (в отличие от решения БлюмаШаблон:Переход).Шаблон:SfnШаблон:Sfn

Недостатки рядного полиморфизма Ванда — неочевидность реализации (нет единого систематичного способа его компилировать, каждая конкретная система типов на основе рядных переменных имеет свою реализацию) и неоднозначное соотношение с теорией (нет единообразной формулировки для проверки и выведения типов, поддержка выведения решалась отдельно и потребовала экспериментов с наложением различных ограничений)Шаблон:Sfn.

Просвечивающие суммы Харпера — Лилибриджа

Наиболее сложной разновидностью записей являются зависимые записи. Такие записи могут включать в себя типы наравне с «обычными» значениями (материализованные типы, Шаблон:IwШаблон:Sfn), причём термы и типы, следующие далее по порядку в теле записи, могут быть определены на основе предшествующих им. Такие записи соответствуют «слабым суммам» из теории зависимых типов, также известным как «экзистенциалы», и служат наиболее общим обоснованием систем модулей языков программированияШаблон:SfnШаблон:Sfn. Шаблон:Iw рассматривалШаблон:Sfn аналогичные по свойствам типы как один из основных типов в полнотиповом программировании (но называл их «кортежами»).

Шаблон:Нп2 и Марк Лилибридж (Шаблон:Lang-en2) построилиШаблон:SfnШаблон:Sfn исчисление просвечивающих сумм (Шаблон:Lang-en) для формального обоснования языка модулей первого класса высшего порядка — наиболее развитой системы модулей среди известных. Это исчисление, в том числе, применяется в семантике Харпера — Стоуна, представляющей теоретико-ти́повое обоснование для Шаблон:Nowrap.

Просвечивающие суммы обобщают слабые суммы за счёт меток и набора равенств, описывающих конструкторы типов. Термин «просвечивающие» (Шаблон:Lang-en) означает, что в составе типа записи могут присутствовать как типы с явно экспортированной структурой, так и полностью абстрактные. Слой родо́в в исчислении имеет простой классический состав: различаются род всех типов <math>\star</math> и функциональные рода́ вида <math>k_1 => k_2</math>, типизирующие конструкторы типов (ML не поддерживает полиморфизма в высших рода́хШаблон:Переход, все переменные типа принадлежат к роду <math>\star</math>, и абстракция конструкторов типов возможна лишь посредством функторовШаблон:Sfn). Исчисление различает правила подтипизации для записей как основных типов и для полей записей как их составляющих, соответственно, рассматривая «подтипы» и «подполя», а затемнение (абстрагирование) сигнатур полей является отдельным от подтипизации понятием. Подтипизация здесь формализует сопоставление модулей с интерфейсами.Шаблон:SfnШаблон:Sfn

Исчисление Харпера — Лилибриджа неразрешимо даже в части проверки согласования типов (диалекты языка модулей, реализованные в Шаблон:Nowrap и OCaml, используют ограниченные подмножества этого исчисления). Однако позже Андреас Россберг (Шаблон:Lang-en) на основе их идей построил язык «1ML», в котором традиционные записи уровня ядра языка и структуры уровня модулей являются одной и той же первоклассной конструкциейШаблон:Sfn (существенно более выразительной, чем у Карделли — см. критика языка модулей ML). За счёт подключения идеи Харпера и МитчелаШаблон:Sfn о подразделении всех типов на Шаблон:Iw «маленьких» и «больших» типов (упрощённо, это похоже на фундаментальное разделение типов на простые и агрегатные, с неодинаковыми правилами типизации), Россберг обеспечил разрешимость не только проверки согласования, но и почти полного выведения типов. Более того, 1ML допускает импредикативныйШаблон:Переход полиморфизмШаблон:Sfn. При этом внутренний языкШаблон:Переход в 1ML основан на плоской Шаблон:Iw и не требует использования зависимых типов в качестве метатеории. На 2015 год Россберг оставил открытым вопрос о возможности добавления в 1ML рядного полиморфизмаШаблон:Переход, отметив лишь, что это должно обеспечить более полное выведение типовШаблон:Sfn. Спустя год он добавилШаблон:Sfn в 1ML полиморфизм эффектовШаблон:Переход.

Полиморфное исчисление записей Охори

Ацуси Охори (Шаблон:Lang-en) совместно со своим научным руководителем Шаблон:Нп2 в 1988 году предложил идею ограничивать спектр возможных значений обычных типовых переменных в полиморфной типизации самих записей. В дальнейшем Охори формализовал эту идею посредством родо́в записей, построив к 1995 году полноценное исчисление и способ его эффективной компиляцииШаблон:SfnШаблон:Sfn. Прототип реализации был создан в 1992 году как расширение компилятора Шаблон:IwШаблон:Sfn, затем Охори возглавил разработку собственного компилятора SML#, реализующего одноимённый диалект языка Шаблон:Nowrap. В SML# полиморфизм записей служит основой для бесшовного встраивания конструкций на SQL в программы на Шаблон:Nowrap. SML# применяется крупными японскими компаниями для решения бизнес-задач, связанных с нагруженными базами данных[5]. Пример такого рода сессии (REPL)Шаблон:Sfn: 

fun wealthy { Salary = s, ... } = s > 100000;
(* val wealthy = fn : 'a#{ Salary:int, ... } -> bool *)

fun young x = #Age x < 24;
(* val young = fn : 'a#{ Age:int, ... } -> bool *)

fun youngAndWealthy x = wealthy x andalso young x;
(* val youngAndWealthy = fn : 'a#{ Age:int, Salary:int, ... } -> bool *)

fun select display l pred = fold (fn (x,y) => if pred x then (display x)::y else y) l nil;
(* val select = fn : ('a -> 'b) -> 'a list -> ('a -> bool) -> 'b list *)

fun youngAndWealthyEmployees l = select #Name l youngAndWealthy;
(* val youngAndWealthyEmployees = fn : 'b#{ Age:int, Name:'a, Salary:int, ... } list -> 'a list *)

Охори назвал своё исчисление «полиморфизмом записей» (Шаблон:Lang-en) или «полиморфным исчислением записей» (Шаблон:Lang-en), одновременно подчеркнув, что он, как и Ванд, рассматривает полиморфизм не только типов-произведений, но и типов-суммШаблон:Sfn.

Исчисление Охори выделяется наиболее интенсивным использованием слоя родо́вШаблон:Sfn. В записи <math>t \colon\colon k</math> (отнесение типа <math>t</math> к роду <math>k</math>) символ <math>k</math> означает либо род всех типов <math>U</math>; либо род записей, имеющих форму <math>\left \{ \left \{ l_1\colon t_1, \dots, l_n\colon t_n \right \} \right \}</math>, обозначающий множество всех записей, содержащих как минимум указанные поля; либо род вариантов, имеющих форму <math>\left \langle \left \langle l_1: t_1, \dots, l_n\colon t_n \right \rangle \right \rangle</math>, обозначающий множество всех вариантных типов, содержащих как минимум указанные конструкторы. В плоском синтаксисе языка ограничение типа некоторым родом записи записывается как t#{...} (см. примеры выше). Решение в некоторой степени схоже с Шаблон:Iw Карделли — ВегнераШаблон:Sfn.

Единственная полиморфная операция, предусмотренная этим исчислением — операция извлечения поляШаблон:Sfn. Однако Охори был первым, кто представил для полиморфизма записей простую и эффективную схему компиляцииШаблон:Sfn. Он назвал её «исчислением реализаций» (Шаблон:Lang-en2). Запись представляется вектором, упорядоченным лексикографически по именам полей исходной записи; обращение к полю по имени транслируется в вызов промежуточной функции, возвращающей номер данного поля в данном векторе по запрашиваемому имени, и последующую индексацию вектора по вычисленному номеру позиции. Функция вызывается только при инстанцировании полиморфных термов, что накладывает минимальный оверхед на рантайм при использовании полиморфизма и не накладывает никакого оверхеда при работе с мономорфными типами. Метод работает одинаково хорошо с произвольно большими записями и вариантами. Исчисление обеспечивает выведение типов и находит строгое соответствие с теорией (родовая квантификация напрямую соотносится с обычной индексацией вектора), представляя собой непосредственно расширение лямбда-исчисление второго порядка Жирара — Рейнольдса, что позволяет переносить различные известные свойства полиморфной типизации на полиморфизм записейШаблон:Sfn.

На практике, поддержка полиморфных вариантов в SML# не была реализована из-за её несовместимости с механизмом определения типов-сумм в Шаблон:Nowrap (требуется синтаксическое разделение сумм и рекурсивных типов)Шаблон:Sfn.

Недостатком исчисления Охори является отсутствие поддержки операций расширения или обрезания записейШаблон:SfnШаблон:SfnШаблон:Sfn.

Первоклассные метки Гастера — Джонса

В теории квалифицированных типовШаблон:Переход расширяемые записи описываются предикатами отсутствия поля (Шаблон:Lang-en2) и присутствия поля (Шаблон:Lang-en2). Бенедикт Гастер (Шаблон:Lang-en2) совместно с автором теории Марком Джонсом (Шаблон:Lang-en2) доработал её в части расширяемых записей до практичной системы типов неявно типизированных языков, в том числе, определив способ компиляцииШаблон:Sfn. Они вводят термин первоклассные метки (Шаблон:Lang-en2), подчёркивающий возможность абстрагировать операции над полями от статически известных меток. В дальнейшем Гастер защитил на построенной системе диссертациюШаблон:Sfn.

Исчисление Гастера — Джонса не обеспечивает полное выведение типов. Кроме того, из-за проблем разрешимости было наложено искусственное ограничение: запрет на пустые рядыШаблон:Sfn. Сульцманн предпринял попытку реформулирования исчисленияШаблон:Sfn, однако построенная им система не может быть расширена до поддержки полиморфного расширения записей, и не имеет универсального метода эффективной компиляцииШаблон:Sfn.

Да́ан Ле́йен (Шаблон:Lang-en2) добавил в исчисление Гастера — Джонса предикат рядного равенства (или равенства ряда, Шаблон:Lang-en) и переместил язык рядов в язык предикатов — это обеспечило полное выведение типов и сняло запрет на пустые рядыШаблон:Sfn. При компиляции записи преобразуются в лексикографически упорядоченный кортеж и применяется трансляция свидетельствШаблон:Переход по схеме Гастера — Джонса. Система Лейена позволяет выражать такие идиомы, как Шаблон:Iw (наиболее мощную форму объектно-ориентированного программирования) и первоклассные ветвленияШаблон:Переход.

На основе этих работ реализованы расширения языка Haskell[6].

Результаты Гастера — Джонса очень близки к результатам ОхориШаблон:Переход, несмотря на существенные различия в теоретико-ти́повом обосновании, и основным преимуществом является поддержка операций расширения и обрезания записейШаблон:Sfn. Недостатком исчисления является то, что оно опирается на свойства системы типов, которые отсутствуют в большинстве языков программирования. Кроме того, выведение типов для него представляет серьёзную проблему, из-за чего авторы наложили дополнительные ограничения. И хотя Лейен устранил многие недостатки, использование default-ветвленияШаблон:Переход невозможно.Шаблон:Sfn

Полиморфизм управляющих конструкций

С развитием программных систем может увеличиваться количество вариантов в типе-сумме, и добавление каждого варианта требует добавления соответствующего ветвления в каждую функцию над этим типом, даже если эти ветвления в разных функциях идентичны. Таким образом, трудоёмкость наращивания функциональности в большинстве языков программирования нелинейно зависит от декларативных изменений в техническом задании. Эта закономерность известна как Шаблон:Iw. Другой известной проблемой является обработка исключений: на протяжении десятилетий исследования систем типов, все языки, относимые к типобезопасным, могли, тем не менее, завершать работу порождением непойманного исключения — поскольку, несмотря на типизацию самих исключений, механизм их порождения и обработки не типизировался. И хотя были построены средства анализа потока исключений, эти средства всегда являлись внешними по отношению к языку.

Матиас Блюм (Шаблон:Lang-en, коллега Шаблон:Iw, работающий над проектом successor ML[7]), его аспирант Вонсёк Чэй (Шаблон:Lang-en2) и коллега Юмат Эйкар (Шаблон:Lang-en2) решили обе проблемы, основываясь на Шаблон:Iw произведений и сумм. Воплощением их идей стал язык MLPolyRШаблон:SfnШаблон:SfnШаблон:Sfn, основанный на простейшем подмножестве Шаблон:Nowrap и дополняющий его несколькими уровнями типобезопасностиШаблон:Sfn. Позже Вонсёк Чэй защитил на этих достижениях диссертациюШаблон:Sfn.

Решение состоит в следующем. Согласно принципу двойственности, вводная форма (Шаблон:Lang-en) для некоего понятия соответствует устраняющей форме (Шаблон:Lang-en) двойственного емуШаблон:Sfn. Таким образом, устраняющая форма сумм (разбор ветвлений) соответствует вводной форме записей. Это побуждает наделить ветвления теми же свойствами, что уже доступны для записей — сделать их первоклассными объектами и допустить их расширение.

Например, простейший интерпретатор языка выражений: 

fun eval e = case e of
                  `Const i => i
                | `Plus (e1,e2) => eval e1 + eval e2

с введением первоклассной конструкции cases может быть переписан в виде: 

fun eval e = match e with
                cases `Const i => i
                    | `Plus (e1,e2) => eval e1 + eval e2

после чего cases-блок может быть вынесен: 

fun eval_c eval = cases `Const i => i
                      | `Plus (e1,e2) => eval e1 + eval e2

fun eval e = match e with (eval_c eval)

Это решение допускает default-ветвления (в отличие от исчисления Гастера — ДжонсаШаблон:Переход), что важно для композиции первоклассных ветвленийШаблон:Sfn. Завершение композиции ряда осуществляется с помощью слова nocases. 

fun const_c d =
    cases `Const i => i
    default: d

fun plus_c eval d =
    cases `Plus (e1,e2) => eval e1 + eval e2
    default: d

fun eval e = match e with
    const_c (plus_c eval nocases)


fun bind env v1 x v2 =
    if v1 = v2 then x else env v2

fun var_c env d =
    cases `Var v => env v
    default: d

fun let_c eval env d =
    cases `Let (v,e,b) => eval (bind env v (eval env e)) b
    default: d

fun eval_var env e = match e with
    const_c (plus_c (eval_var env) (var_c env (let_c eval_var env nocases)))

Как видно, новый код, который необходимо дописывать при качественном усложнении системы, не требует изменения уже написанного кода (функции const_c и plus_c «ничего не знают» о последующем добавлении в интерпретатор языка поддержки переменных и let-блоков). Таким образом, первоклассные расширяемые ветвления (Шаблон:Lang-en2) являются принципиальным решением Шаблон:Iw, позволяя говорить о парадигме расширяемого программированияШаблон:SfnШаблон:Sfn. По словам Блюма, это является не чем-то принципиально новым, а просто интересным способом применения рядного полиморфизмаШаблон:Переход, который уже поддерживается в системе типов, и в этом смысле достоинством такого технического решения является его концептуальная простотаШаблон:Sfn.

Однако расширение программных систем требует также контроля над обработкой исключений, которые могут порождаться на произвольной глубине вложения вызовов. И здесь Блюм с коллегами провозглашают новый слоган типобезопасности в развитие слогана Милнера: «Программы, прошедшие проверку типов, не порождают необработанных исключений». Проблема состоит в том, что если сигнатура функционального типа включает информацию о типах исключений, которые эта функция потенциально может порождать, и эта информация в сигнатуре передаваемой функции должна быть строго согласована с информацией о параметре функции высшего порядка (в том числе, если это пустое множество) — типизация механизма обработки исключений немедленно требует полиморфности типов самих исключений — в противном случае функции высшего порядка перестают быть полиморфными. В то же время, в безопасном языке исключения являются расширяемой суммойШаблон:SfnШаблон:SfnШаблон:Sfn, то есть вариантным типом, конструкторы которого добавляются по ходу программы. Соответственно, типобезопасность потока исключений означает необходимость поддержки типов-сумм, которые являются одновременно расширяемыми и полиморфными. И здесь вновь решением является рядный полиморфизмШаблон:Переход.

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

MLPolyR использует нетривиальное сочетание нескольких исчислений и двухстадийную трансляцию. Для выведения и согласования типов он использует исчисление РемиШаблон:Переход, одновременно используя принцип Шаблон:Iw для представления сумм как произведений, далее транслирует язык в промежуточный явно типизированный язык с полиморфными записями, и затем использует эффективный способ компиляции, построенный ОхориШаблон:Переход. Иначе говоря, модель компиляции Охори была обобщена до поддержки исчисления РемиШаблон:Sfn. На теоретико-ти́повом уровне Блюм вводит сразу несколько новых синтаксических нотаций, позволяющих записывать правила для типизации исключений и первоклассных ветвлений. Система типов MLPolyR обеспечивает полное выведение типов, так что авторы отказались от разработки плоского синтаксиса для явной записи типов и от поддержки сигнатур в языке модулей.

В системе типов ЛейенаШаблон:Переход также возникает вариант полиморфизма ветвлений: конструкция case может быть представлена в виде функции высшего порядка, получающей запись из функций, каждая из которых соответствует определённой ветви вычислений (синтаксис Хаскела подходит для этого изменения и не требует пересмотра). Например: 

data List a = nil :: {}
            | cons :: { hd :: a, tl :: List a }

snoc xs r = case (reverse xs) r

last xs = snoc xs { nil = \r -> _|_,
                      cons = \r -> r.hd }

Поскольку записи в системе Лейена являются расширяемыми, разбор ветвлений обретает гибкость на уровне динамических решений (например, цепочки проверок или использования ассоциативного массива), но обеспечивает гораздо более эффективную реализацию (метка варианта соответствует смещению в записи). Однако, от поддержки ветвления по умолчанию (default) в данном случае приходится отказаться, поскольку единственный default-образец соответствовал бы множеству полей (и, соответственно, множеству смещений). Лейен называет эту конструкцию «первоклассными образцами для сопоставления» (Шаблон:Lang-en2).

Полиморфизм в высших рода́х

Полиморфизм в высших рода́х (Шаблон:Lang-en) означает абстракцию над конструкторами типов высших порядков, то есть ти́повыми операторами вида 

* -> * -> ... -> *

Поддержка этой возможности поднимает полиморфизм на более высокий уровень, обеспечивая абстракцию как над типами, так и над конструкторами типов — подобно тому как функции высших порядков обеспечивают абстракцию как над значениями, так и над другими функциями. Полиморфизм в высших рода́х является естественным компонентом многих идиом функционального программирования, включая монады, свёртки и встраиваемые языки.Шаблон:SfnШаблон:Sfn

НапримерШаблон:Sfn, если определить следующую функцию (язык Haskell): 

when b m = if b then m else return ()

то для неё будет выведен такой функциональный тип: 

when :: forall (m :: * -> *). Monad m => Bool -> m () -> m ()

Сигнатура m :: * -> * говорит о том, ти́повая переменная m является переменной типа, принадлежащего к высшему роду (Шаблон:Lang-en). Это значит, что она абстрагируется над конструкторами типов (в данном случае унарными, такими как Maybe или []), которые могут применяться к конкретным типам, таким как Int или (), для построения новых типов.

В языках, поддерживающих полную абстракцию типа (Standard ML, OCaml), все ти́повые переменные должны принадлежать к роду *, в противном случае система типов была бы небезопасной. Полиморфизм в высших рода́х, таким образом, обеспечивается за счёт самого механизма абстракции в сочетании с явным аннотированием при инстанцировании, что несколько неудобно. Тем не менее, возможна идиоматическая реализация полиморфизма в высших рода́х, не требующая явного аннотирования — для этого на уровне типов применяется техника, аналогичная дефункционализации.Шаблон:Sfn

Полиморфизм родо́в

Системы родо́в (Шаблон:Lang-en) обеспечивают безопасность самих систем типов, позволяя контролировать смысл ти́повых выражений.

Например, пусть требуется реализовать вместо обычного типа «вектор» (линейный массив) семейство типов «вектор длиной n», иначе говоря, определить тип «вектор, индексированный длиной». Классическая реализация на Haskell выглядит такШаблон:Sfn: 

data Zero
data Succ n
data Vec :: * -> * -> * where
    Nil  :: Vec a Zero
    Cons :: a -> Vec a n -> Vec a (Succ n)

Здесь вначале определяются фантомные типыШаблон:Sfn, то есть типы, не имеющие динамического представления. Конструкторы Zero и Succ служат «значениями слоя типов», а переменная n обеспечивает неравенство разных конкретных типов, построенных конструктором Succ. Тип Vec определён как обобщённый алгебраический тип данных (GADT).

Решение условно предполагает, что фантомный тип n будет использоваться для моделирования целочисленного параметра вектора на основе аксиом Пеано — то есть будут строиться только такие выражения, как Succ Zero, Succ Succ Zero, Succ Succ Succ Zero и т. д. Однако, хотя определения записаны на языке типов, сами по себе они сформулированы бестиповым образом. Это видно по сигнатуре Vec :: * -> * -> *, означающей, что конкретные типы, передаваемые в качестве параметров, принадлежат роду *, а значит, могут быть любым конкретным типом. Иначе говоря, здесь не запрещаются бессмысленные ти́повые выражения вроде Succ Bool или Vec Zero Int.Шаблон:Sfn

Более развитое исчисление позволило бы задать область значений параметра типа более точно: 

data Nat = Zero | Succ Nat
data Vec :: * -> Nat -> * where
   VNil  :: Vec a Zero
   VCons :: a -> Vec a n -> Vec a (Succ n)

Но обычно такой выразительностью обладают лишь узко-специализированные системы с зависимыми типамиШаблон:Sfn, реализованные в таких языках, как Agda, Coq и другими. Например, с позиции языка Agda запись Vec :: * -> Nat -> * означала бы, что род типа Vec зависит от типа Nat (то есть элемент одного сорта зависит от элемента другого, более низкого сорта).

В 2012 году было построеноШаблон:Sfn расширение языка Haskell, реализующее более развитую систему родо́в и делающее вышеприведённый код корректным кодом на Haskell. Решение состоит в том, что все типы (за определёнными ограничениями) автоматически «продвигаются» (Шаблон:Lang-en) на уровень выше, формируя одноимённые рода́, которые можно использовать явным образом. С этой точки зрения, запись Vec :: * -> Nat -> * не является зависимой — она означает лишь, что второй параметр вектора должен принадлежать к именованному роду Nat, а в данном случае единственным элементом этого рода является одноимённый тип.

Решение является весьма простым, как с точки зрения реализации в компиляторе, так и с точки зрения практической доступности. А поскольку полиморфизм типов изначально является естественным элементом семантики Haskell, продвижение типов приводит к полиморфизму родо́в (Шаблон:Lang-en), который одновременно повышает коэффициент повторного использования кода и обеспечивает более высокий уровень типобезопасности. Например, следующий GADT, используемый для верификации равенства типов: 

data EqRefl a b where
   Refl :: EqRefl a a

в классическом Haskell имеет род * -> * -> *, что не позволяет использовать его для проверки равенства конструкторов типов, таких как Maybe. Система родов, основанная на продвижении типов, выводит полиморфный род forall X. X -> X -> *, делая тип EqRefl более универсальным. Это можно записать явно: 

data EqRefl (a :: X) (b :: X) where
   Refl :: forall X. forall(a :: X). EqRefl a a

Полиморфизм эффектов

Системы эффектов (Шаблон:Lang-en) были предложены Гиффордом и Лукассеном во второй половине 1980-хШаблон:SfnШаблон:SfnШаблон:Sfn с целью обособления побочных эффектов для более тонкого контроля за безопасностью и эффективностью в конкурентном программировании.

Полиморфизм эффектов (Шаблон:Lang-en) при этом означает квантификацию над чистотой конкретной функции, то есть включение в функциональный тип флага, характеризующего функцию как чистую либо нечистую. Такое расширение типизации позволяет абстрагировать чистоту функций высшего порядка от чистоты функций, передаваемых им в качестве аргументов.

Это приобретает особое значение при переходе к функциям над модулями (записями, включающими в свой состав абстрактные типы) — функторам — поскольку в условиях чистоты они имеют право быть аппликативными, но в присутствии побочных эффектов они обязаны быть порождающими для обеспечения типобезопасности (подробнее об этом см. эквивалентность типов в языке модулей ML). Таким образом, в языке модулей первого класса высшего порядка полиморфизм эффектов оказывается необходимой основой для поддержки полиморфизма порождаемости (Шаблон:Lang-en): передача флага чистоты в функтор обеспечивает выбор между аппликативной и порождающей семантикой в единой системе.Шаблон:Sfn

Поддержка в языках программирования

Типобезопасный параметрический полиморфизм доступен в языках, типизированных по Хиндли — МилнеруШаблон:Переход — в диалектах ML (Standard ML, OCaml, Alice, F#) и их потомках (Haskell, Clean, Idris, Mercury, Agda) — а также в наследованных от них гибридных языках (Scala, Nemerle).

Обобщённые типы данных (дженерики) отличаются от параметрически полиморфных систем тем, что используют Шаблон:Iw, и потому не могут иметь ранг выше 1-гоШаблон:Переход. Они доступны в Ada, Eiffel, Java, C#, D, Rust; а также в Delphi, начиная с 2009-й версии. Впервые они появились в CLU.

Интенсиональный полиморфизм

Интенсиональный полиморфизм (Шаблон:Lang-en) представляет собой технику оптимизирующей компиляции параметрического полиморфизма на основе сложного теоретико-ти́пового анализа, которая состоит в вычислениях над типами во время выполнения программы. Интенсиональный полиморфизм позволяет реализовывать бестеговую сборку мусора, необёрнутую (Шаблон:Lang-en2) передачу аргументов в функции и упакованные (оптимизированные по памяти) плоские структуры данных.Шаблон:SfnШаблон:SfnШаблон:Sfn

Мономорфизация

Мономорфизация (Шаблон:Lang-en) представляет собой технику оптимизирующей компиляции параметрического полиморфизма, которая заключается в порождении мономорфного экземпляра для каждого случая использования полиморфной функции или типа. Другими словами, параметрический полиморфизм на уровне исходного кода транслируется в Шаблон:Nowrap полиморфизм на уровне целевой платформы. Мономорфизация повышает быстродействие (точнее, делает полиморфизм «бесплатным»), но вместе с тем может увеличивать размер выходного машинного кода.Шаблон:Sfn

Хиндли — Милнер

В классическом варианте система типов Хиндли — Милнера (а также просто «Хиндли — Милнер» или «Х-М», Шаблон:Lang-en)Шаблон:SfnШаблон:Sfn, положенная в основу языка ML, представляет собой подмножество Системы F, ограниченное предикативнымШаблон:Переход пренекснымШаблон:Переход полиморфизмом с целью обеспечения возможности автоматического выведения типов, для чего в состав Хиндли — Милнера традиционно также включался так называемый «Шаблон:Iw», разработанный Робином Милнером.

Многие реализации Х-М являются улучшенной версией системы, представляя собой «систему главной типизации» (Шаблон:Lang-en)Шаблон:SfnШаблон:Sfn, которая за один проход с почти линейной сложностью одновременно выводит наиболее общие полиморфные типы для каждого выражения и строго проверяет их согласование.

С момента своего появления система типов Хиндли — Милнера была расширена по нескольким направлениямШаблон:Sfn. Одним из наиболее известных расширений является поддержка ad-hoc-полиморфизма посредством классов типов, дальнейшим обобщением которых стали квалифицированные типыШаблон:Переход.

Автоматическое выведение типов было сочтено необходимостью при первоначальной разработке языка ML в качестве интерактивной системы доказательства теорем «Logic for Computable Functions», из-за чего и были наложены соответствующие ограничения. В дальнейшем на основе ML был разработан целый ряд эффективно компилируемых языков общего назначения, ориентированных на Шаблон:Iw, а в этом случае необходимость поддержки выведения типов резко снижается, так как интерфейсы модулей в промышленной практике в любом случае необходимо явно аннотировать типамиШаблон:Sfn. Поэтому было предложено множество вариантов расширения Хиндли — Милнера, отказывающихся от выведения типов ради расширения возможностей, вплоть до поддержки полной Системы F с импредикативнымШаблон:Переход полиморфизмом, таких как язык модулей высшего порядка, изначально основанный на явном аннотировании типов модулей и имеющий множество расширений и диалектов, а также расширения языка Haskell (Rank2Types, RankNTypes и ImpredicativeTypes).

Компилятор MLton языка Standard ML осуществляет мономорфизациюШаблон:Переход, но за счёт других применимых к Standard ML оптимизаций результирующее увеличение выходного кода не превышает 30 %Шаблон:Sfn.

Си и C++

В языке Си функции не являются объектами первого класса, но возможно определение указателей на функции, что позволяет строить функции высших порядков[8]. Также доступен небезопасный параметрический полиморфизм за счёт явной передачи необходимых свойств типа через бестиповое подмножество языка, представленное нетипизированным указателем void*Шаблон:Sfn (называемым в сообществе языка «обобщённым указателем» (Шаблон:Lang-en). Назначение и удаление информации о типе при приведении типа к void* и обратно не является ad-hoc-полиморфизмом, так как не меняет представление указателя, однако, его записывают явно для обхода системы типов компилятора[8].

Например, стандартная функция qsort способна обрабатывать массивы элементов любого типа, для которого определена функция сравнения[8]. 

struct segment { int start; int end; };

int seg_cmpr( struct segment *a, struct segment *b )
{ return abs( a->end - a->start ) - abs( b->end - b->start ); }

int str_cmpr( char **a, char **b )
{ return strcmp( *a, *b ); }

struct segment segs[] = { {2,5}, {4,3}, {9,3}, {6,8} };
char* strs[] = { "three", "one", "two", "five", "four" };

main()
{
    qsort( strs, sizeof(strs)/sizeof(char*), sizeof(char*),
                 (int (*)(void*,void*))str_cmpr );

    qsort( segs, sizeof(segs)/sizeof(struct segment), sizeof(struct segment),
                 (int (*)(void*,void*))seg_cmpr );
    ...
}

Тем не менее, в Си возможно идиоматическое воспроизведение типизированного параметрического полиморфизма без использования void*[9].

Язык C++ предоставляет подсистему шаблонов, использование которых внешне похоже на параметрический полиморфизм, но семантически реализуется сочетанием ad hoc-механизмов: 

template <typename T> T max(T x, T y)
{
    if (x < y)
        return y;
    else
        return x;
}

int main()
{
    int a = max(10,15);
    double f = max(123.11, 123.12);
    ...
}

МономорфизацияШаблон:Переход при компиляции шаблонов C++ является неизбежной, так как в системе типов языка отсутствует поддержка полиморфизма — полиморфный язык здесь является Шаблон:Iw надстройкой над мономорфным ядром языкаШаблон:Sfn. Это приводит к кратному увеличению объёма получаемого машинного кода, что получило известность как «раздувание кода»[10].

История

Шаблон:Заготовка раздела

Нотацию параметрического полиморфизма как развитие лямбда-исчисления (названную полиморфным лямбда-исчислением или Системой F) формально описал логик Шаблон:IwШаблон:SfnШаблон:Sfn (1971 год), независимо от него похожую систему описал информатик Шаблон:IwШаблон:Sfn (1974 год)Шаблон:Sfn.

Впервые параметрический полиморфизм был представлен в языке ML в 1973Шаблон:SfnШаблон:Sfn. Независимо от него параметрические типы были реализованы под руководством Барбары Лисков в CLU (1974 год)Шаблон:Sfn.

См. также

Примечания

Шаблон:Примечания

Литература

Внешние ссылки

  1. ↑ Шаблон:Cite web
  2. ↑ Шаблон:Cite web
  3. ↑ 3,0 3,1 Шаблон:Cite web
  4. ↑ Шаблон:Cite web
  5. ↑ Шаблон:Cite web
  6. ↑ Extensible records on Haskell-WikiШаблон:Недоступная ссылка
  7. ↑ Шаблон:Cite web
  8. ↑ 8,0 8,1 8,2 Шаблон:Книга, Глава 5.11. Указатели на функции
  9. ↑ Шаблон:Cite web
  10. ↑ Шаблон:Cite web

Шаблон:Выбор языка Шаблон:Типы данных

Партнерские ресурсы
Криптовалюты
Магазины
Хостинг
Разное

Источник — http://wikihandbk.com/ruwiki/index.php?title=Русская_Википедия:Параметрический_полиморфизм&oldid=10557224