Параметрический полиморфизм

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

К предикативным системам относятся интуиционистская теория типов и .

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

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

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

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

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

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

 
 

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

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

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

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

Пример определения записи:
> 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, ...} *)
Мономорфизм записей делает их негибким, но эффективным средством: поскольку фактическое расположение в памяти каждого поля записи известно заранее (на этапе компиляции), обращение к нему по имени компилируется в прямую индексацию, что обычно вычисляется за одну машинную инструкцию. Однако, при разработке сложных масштабируемых систем желательно иметь возможность абстрагировать поля от конкретных записей — например, определить универсальный селектор полей:
fun select r l = #l r
Но компиляция полиморфного обращения к полям, которые могут располагаться в разном порядке в разных записях, представляет сложную проблему, как с точки зрения контроля безопасности операций на уровне языка, так и с точки зрения быстродействия на уровне машинного кода. Наивным решением может быть динамический поиск по словарю при каждом обращении (и скриптовые языки его применяют), однако, очевидно, что это чрезвычайно неэффективно.

Суммы типов составляют основу выражения ветвления, причём за счёт строгости системы типов компилятор обеспечивает контроль за полнотой разбора. Например, для следующего типа-суммы:
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 => ...
      | _ => ...
В некоторых языках (в , в Haskell) даже «более простая» конструкция if-then-else является лишь синтаксическим сахаром над частным случаем ветвления, то есть выражение
if A
   then B
   else C
уже на этапе грамматического разбора представляется в виде
case A of
     true => B
   | false => C
либо
case A of
     true => B
   | _ => C

Синтаксический сахар 
В  записи и варианты являются мономорфными, однако, поддерживается синтаксический сахар для работы с записями со множеством полей, называемый «универсальным образцом»:
> 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, ...}» означает, что в данной записи существуют и другие поля, помимо упомянутых. Однако полиморфизм записей как таковой отсутствует (даже пренексный): требуется полное статическое разрешение информации о мономорфном типе записи (посредством выведения или явного аннотирования).

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

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

Пример простейшего варианта конструкции реализован в Alice ML (согласно действующим соглашениям по ). Универсальный образец (многоточие) имеет расширенные возможности: посредством его можно осуществлять «захват ряда» с тем, чтобы работать с «оставшейся» частью записи как со значением:
> 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-х) были предложены различные варианты формализации расширяемых записей через операции конкатенации над неполиморфными записями (Харпер — Пирс, Ванд, Сальцманн).  даже использовал операции над записями вместо полиморфизма в языке Amber. Для этих исчислений нет известного способа эффективной компиляции; кроме того, эти исчисления весьма сложны и с точки зрения теоретико-ти́пового анализа.

Например:
val car = { name = "Toyota"; age = "old"; id = 6678 }
val truck = { name = "Toyota"; id = 19823235 }
...
val repaired_truck = { car and truck }
Ванд (автор рядного полиморфизма) показал, что посредством конкатенации записей можно моделировать множественное наследование.

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

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

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

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

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

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

Рядный полиморфизм Ванда 
 в 1987 году предложил идею захватывать информацию об «оставшейся» (не указанной явно) части записи посредством того, что он назвал рядной ти́повой переменной ().

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

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

Пример (язык OCaml; синтаксис постфиксный, record#field):
# let send_m a = a#m ;;
(* value send_m : < m : a; .. > -> a = <fun> *)
Здесь многоточие (из двух точек) — это принятый в OCaml синтаксис для безымянной рядной ти́повой переменной. За счёт такой типизации, функция send_m может быть применена к объекту любого (заранее ) объектного типа, в состав которого входит метод m соответствующей сигнатуры.

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

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

Упрощённо идею исчисления можно трактовать как расширение типа всякого поля записи флагом присутствия/отсутствия и представление записи в виде кортежа со слотом для каждого возможного поля. В прототипе реализации синтаксис языка типов был сделан приближенным к теоретико-ти́повой формулировке, например:
# 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) *)

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

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

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

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

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

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

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

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

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

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

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

Исчисление Охори выделяется наиболее интенсивным использованием слоя родо́в. В записи  (отнесение типа  к роду ) символ  означает либо род всех типов ; либо род записей, имеющих форму , обозначающий множество всех записей, содержащих как минимум указанные поля; либо род вариантов, имеющих форму , обозначающий множество всех вариантных типов, содержащих как минимум указанные конструкторы. В плоском синтаксисе языка ограничение типа некоторым родом записи записывается как t#{...} (см. примеры выше). Решение в некоторой степени схоже с  Карделли — Вегнера.

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

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

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

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

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

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

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

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

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

Матиас Блюм (, коллега , работающий над проектом ), его аспирант Вонсёк Чэй () и коллега Юмат Эйкар () решили обе проблемы, основываясь на  произведений и сумм. Воплощением их идей стал язык MLPolyR, основанный на простейшем подмножестве  и дополняющий его несколькими уровнями типобезопасности. Позже Вонсёк Чэй защитил на этих достижениях диссертацию.

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

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

 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-ветвления (в отличие от исчисления Гастера — Джонса), что важно для композиции первоклассных ветвлений. Завершение композиции ряда осуществляется с помощью слова 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-блоков). Таким образом, первоклассные расширяемые ветвления () являются принципиальным решением , позволяя говорить о парадигме расширяемого программирования. По словам Блюма, это является не чем-то принципиально новым, а просто интересным способом применения рядного полиморфизма, который уже поддерживается в системе типов, и в этом смысле достоинством такого технического решения является его концептуальная простота.

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

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

MLPolyR использует нетривиальное сочетание нескольких исчислений и двухстадийную трансляцию. Для выведения и согласования типов он использует исчисление Реми, одновременно используя принцип  для представления сумм как произведений, далее транслирует язык в промежуточный явно типизированный язык с полиморфными записями, и затем использует эффективный способ компиляции, построенный Охори. Иначе говоря, модель компиляции Охори была обобщена до поддержки исчисления Реми. На теоретико-ти́повом уровне Блюм вводит сразу несколько новых синтаксических нотаций, позволяющих записывать правила для типизации исключений и первоклассных ветвлений. Система типов 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-образец соответствовал бы множеству полей (и, соответственно, множеству смещений). Лейен называет эту конструкцию «первоклассными образцами для сопоставления» ().

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

Например, если определить следующую функцию (язык Haskell):
when b m = if b then m else return ()
то для неё будет выведен такой функциональный тип:
when :: forall (m :: * -> *). Monad m => Bool -> m () -> m ()
Сигнатура m :: * -> * говорит о том, ти́повая переменная m является переменной типа, принадлежащего к высшему роду (). Это значит, что она абстрагируется над конструкторами типов (в данном случае унарными, такими как Maybe или []), которые могут применяться к конкретным типам, таким как Int или (), для построения новых типов.

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

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

Например, пусть требуется реализовать вместо обычного типа «вектор» (линейный массив) семейство типов «вектор длиной n», иначе говоря, определить тип «вектор, индексированный длиной». Классическая реализация на Haskell выглядит так:
data Zero
data Succ n
data Vec :: * -> * -> * where
    Nil  :: Vec a Zero
    Cons :: a -> Vec a n -> Vec a (Succ n)
Здесь вначале определяются фантомные типы, то есть типы, не имеющие динамического представления. Конструкторы Zero и Succ служат «значениями слоя типов», а переменная n обеспечивает неравенство разных конкретных типов, построенных конструктором Succ. Тип Vec определён как обобщённый алгебраический тип данных (GADT).

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

Более развитое исчисление позволило бы задать область значений параметра типа более точно:
data Nat = Zero | Succ Nat
data Vec :: * -> Nat -> * where
   VNil  :: Vec a Zero
   VCons :: a -> Vec a n -> Vec a (Succ n)
Но обычно такой выразительностью обладают лишь узко-специализированные системы с зависимыми типами, реализованные в таких языках, как Agda, Coq и другими. Например, с позиции языка Agda запись Vec :: * -> Nat -> * означала бы, что род типа Vec зависит от типа Nat (то есть элемент одного сорта зависит от элемента другого, более низкого сорта).

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

Решение является весьма простым, как с точки зрения реализации в компиляторе, так и с точки зрения практической доступности. А поскольку полиморфизм типов изначально является естественным элементом семантики Haskell, продвижение типов приводит к полиморфизму родо́в (), который одновременно повышает коэффициент повторного использования кода и обеспечивает более высокий уровень типобезопасности. Например, следующий GADT, используемый для верификации равенства типов:
data EqReﬂ a b where
   Reﬂ :: EqReﬂ a a
в классическом Haskell имеет род * -> * -> *, что не позволяет использовать его для проверки равенства конструкторов типов, таких как Maybe. Система родов, основанная на продвижении типов, выводит полиморфный род forall X. X -> X -> *, делая тип EqReﬂ более универсальным. Это можно записать явно:
data EqReﬂ (a :: X) (b :: X) where
   Reﬂ :: forall X. forall(a :: X). EqReﬂ a a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Язык 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++ является неизбежной, так как в системе типов языка отсутствует поддержка полиморфизма — полиморфный язык здесь является  надстройкой над мономорфным ядром языка. Это приводит к кратному увеличению объёма получаемого машинного кода, что получило известность как «раздувание кода''».

История 

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

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

См. также 
 Конструктор типов
 Род (теория типов)

Примечания

Литература 
 
 Повторно опубликовано: 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 
 Перевод на русский язык: 

 

 

 

 

 

 

 

 

 

 

 

  

 

 
 Перевод на русский язык: 

 

 

 

 

 

 

Теория типов
Типы данных
Функциональное программирование