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

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

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

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

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

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

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

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

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

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

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

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

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

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

С усложнением систем типов сигнатуры типов становятся настолько сложными, что полное или почти полное их выведение начинает рассматриваться многими исследователями как критичное свойство, отсутствие которого сделает язык непригодным для практики . Например, для традиционного комбинатора map полная сигнатура типа (с учётом родовой квантификации) в условиях типобезопасного отслеживания потока исключений принимает следующий вид (как и выше , [a] означает список элементов типа a ):
${\displaystyle 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]\;)}$

Ранг

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle \neg \lbrace a\land b\rbrace =\langle \neg a\lor \neg b\rangle }$

${\displaystyle \neg \langle a\lor b\rangle =\lbrace \neg a\land \neg b\rbrace }$

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

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

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

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

Классическим примером может служить язык Standard 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 => ...
      | _ => ...

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

if A
   then B
   else C

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

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

либо

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

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

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

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

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

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

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

Пример простейшего варианта конструкции реализован в 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 году предложил идею захватывать информацию об «оставшейся» (не указанной явно) части записи посредством того, что он назвал рядной ти́повой переменной ( row type variable ) .

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

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

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

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

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

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

Наиболее заметный след оставил Дидье́ Реми́ ( фр. Didier Rémy ). Он построил практичную систему типов с расширяемыми записями, включающую полный и эффективный алгоритм реконструкции типов . Реми расслаивает язык типов на , формулируя сортированную алгебру типов ( англ. sorted algebra of types, sorted language of types ). Различаются сорт собственно типов (в том числе типов полей) и сорт полей ; вводятся отображения между ними и на их основе формулируются правила типизации расширяемых записей как простое расширение классических правил ML . Информация о присутствии ( англ. presence ) поля определяется как отображение из сорта типов в сорт полей . Рядные ти́повые переменные переформулируются как переменные, принадлежащие сорту полей и равные константе отсутствия ( англ. absence ), являющейся элементом сорта полей , не имеющим соответствия в сорте типов . Операция вычисления типа для записи из n полей определяется как отображение 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) *)

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

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

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

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

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

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

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

Просвечивающие суммы обобщают слабые суммы за счёт меток и набора равенств, описывающих конструкторы типов . Термин « просвечивающие » ( англ. translucent ) означает, что в составе типа записи могут присутствовать как типы с явно экспортированной структурой, так и полностью абстрактные . Слой родо́в в исчислении имеет простой классический состав: различаются род всех типов ${\displaystyle \star }$ и функциональные рода́ вида ${\displaystyle k_{1}=>k_{2}}$ , типизирующие конструкторы типов ( ML не поддерживает полиморфизма в высших рода́х , все переменные типа принадлежат к роду ${\displaystyle \star }$ , и абстракция конструкторов типов возможна лишь посредством функторов ). Исчисление различает правила подтипизации для записей как основных типов и для полей записей как их составляющих, соответственно, рассматривая «подтипы» и «подполя», а затемнение (абстрагирование) сигнатур полей является отдельным от подтипизации понятием. Подтипизация здесь формализует сопоставление модулей с интерфейсами .

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

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

Ацуси Охори ( англ. Atsushi Ohori ) совместно со своим научным руководителем ( англ. ) в 1988 году предложил идею ограничивать спектр возможных значений обычных типовых переменных в полиморфной типизации самих записей . В дальнейшем Охори формализовал эту идею посредством родо́в записей , построив к 1995 году полноценное исчисление и способ его эффективной компиляции . Прототип реализации был создан в 1992 году как расширение компилятора , затем Охори возглавил разработку собственного компилятора SML# , реализующего одноимённый диалект языка Standard ML . В SML# полиморфизм записей служит основой для бесшовного встраивания конструкций на SQL в программы на SML . 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 *)

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

Исчисление Охори выделяется наиболее интенсивным использованием слоя родо́в . В записи ${\displaystyle t\colon \colon k}$ (отнесение типа ${\displaystyle t}$ к роду ${\displaystyle k}$ ) символ ${\displaystyle k}$ означает либо род всех типов ${\displaystyle U}$ ; либо род записей , имеющих форму ${\displaystyle \left\{\left\{l_{1}\colon t_{1},\dots ,l_{n}\colon t_{n}\right\}\right\}}$ , обозначающий множество всех записей, содержащих как минимум указанные поля; либо род вариантов , имеющих форму ${\displaystyle \left\langle \left\langle l_{1}:t_{1},\dots ,l_{n}\colon t_{n}\right\rangle \right\rangle }$ , обозначающий множество всех вариантных типов , содержащих как минимум указанные конструкторы . В плоском синтаксисе языка ограничение типа некоторым родом записи записывается как t#{...} (см. примеры выше). Решение в некоторой степени схоже с Карделли — Вегнера .

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

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

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

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

В теории квалифицированных типов расширяемые записи описываются предикатами отсутствия поля ( «lacks» predicate ) и присутствия поля ( «has» predicate ). Бенедикт Гастер ( Benedict R. Gaster ) совместно с автором теории Марком Джонсом ( Mark P. Jones ) доработал её в части расширяемых записей до практичной системы типов неявно типизированных языков, в том числе, определив способ компиляции . Они вводят термин первоклассные метки ( first-class labels ), подчёркивающий возможность абстрагировать операции над полями от статически известных меток. В дальнейшем Гастер защитил на построенной системе диссертацию .

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

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

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

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

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

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

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

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

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

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

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

Как и в исчислении Гарриги , для полиморфных сумм в 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 -образец соответствовал бы множеству полей (и, соответственно, множеству смещений). Лейен называет эту конструкцию « первоклассными образцами для сопоставления » ( first-class patterns ).

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

Полиморфизм в высших рода́х ( англ. higher-kinded polymorphism ) означает абстракцию над конструкторами типов высших порядков, то есть ти́повыми операторами вида

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

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

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

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

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

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

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

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

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

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

Например, пусть требуется реализовать вместо обычного типа « вектор » (линейный массив) семейство типов « вектор длиной 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. Решение состоит в том, что все типы (за определёнными ограничениями) автоматически « продвигаются » ( англ. promote ) на уровень выше, формируя одноимённые рода́, которые можно использовать явным образом. С этой точки зрения, запись Vec :: * -> Nat -> * не является зависимой — она означает лишь, что второй параметр вектора должен принадлежать к именованному роду Nat , а в данном случае единственным элементом этого рода является одноимённый тип.

Решение является весьма простым, как с точки зрения реализации в компиляторе, так и с точки зрения практической доступности. А поскольку полиморфизм типов изначально является естественным элементом семантики Haskell, продвижение типов приводит к полиморфизму родо́в ( англ. kind polymorphism ), который одновременно повышает коэффициент повторного использования кода и обеспечивает более высокий уровень типобезопасности . Например, следующий 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Си и C++

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

См. также

• Конструктор типов
• Род (теория типов)

Примечания

Литература

• Christopher Strachey. . — 1967. 12 августа 2017 года.
  • Повторно опубликовано: Christopher Strachey. Fundamental Concepts in Programming Languages // . — 2000. — Т. 13 . — С. 11—49 . — doi : .

• J. Roger Hindley. The principal type scheme of an object in combinatory logic (англ.) // Transactions of the American Mathematical Society . — American Mathematical Society, 1969. — Vol. 146 . — P. 29—60 . — doi : .

• Jean-Yves Girard. Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types (фр.) // Proceedings of the Second Scandinavian Logic Symposium. — Amsterdam, 1971. — P. 63—92 . — doi : .

• Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (фр.) . — Université Paris 7, 1972.

• John C. Reynolds. Towards a Theory of Type Structure // . — Paris: Colloque sur la programmation, 1974. — Т. 19 . — С. 408—425 . — doi : .

• Milner R. , Morris L., Newey M. A Logic for Computable Functions with reflexive and polymorphic types // Arc-et-Senans. — Proc. Conference on Proving and Improving Programs, 1975.

• Robin Milner . A Theory of Type Polymorphism in Programming. — , 1978. — Т. 17 , вып. 3 . — С. 348—375 . — doi : .

• , John С. Mitchell. // Mathematical Structures in Computer Science. — 1991. — Т. 1 , вып. 1 .

• , Peter Wegner. // . — New York, USA: ACM , 1985. — Т. 17 , вып. 4 . — С. 471—523 . — ISSN . — doi : .

• . Введение в Стандартный ML (рус.) . — Carnegie Mellon University, 1986. — 97 с. — ISBN PA 15213-3891.

• John M. Lucassen, David K. Gifford. . — 1986.

• . . — 1987.

• . (англ.) // In Proc. 2nd IEEE Symposium on Logic in Computer Science. — 1987. — P. 37—44 .

• Martín Abadi, , Pierre-Louis Curien. . — POPL, 1993.

• . (англ.) // Inf. Comput. 76. — 1988. — P. 138—164 .

• John M. Lucassen, David K. Gifford. . — , 1988.

• Didier Rémy. // Research Report 1431. — Institut National de Recherche en Informatique et Automatisme, 1991.

• . (англ.) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — Iss. Formal Description of Programming Concepts . — P. 431—507 .

• , Benjamin Pierce. // CMU-CS-90-157R. — Carnegie Mellon University, supported and monitored by Naval Research, 1991.

• . // Selections from 1989 IEEE Symposium on Logic in Computer Science. — Information and Computation,, 1991. — Т. 93 , вып. 1 . — doi : .

• Andrew W. Appel. . — Princeton University, 1992.

• Mark P. Jones. . — ESOP , Springer-Verlag Lecture Notes in Computer Science, 1992.

• Atsushi Ohori. // POPL: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages,. — Kyoto University, ACM , 1992. — С. 154—165 . — doi : .

• J.-P. Talpin, P. Jouvelot. // 2(3):245271. — , 1992.

• , John С. Mitchell. . — ACM TOPLAS, 1993. — С. 211—252 .

• , Mark Lillibridge. (англ.) . — ACM Press, , 1993. — ISBN CMU-CS-93-197. — doi : .

• Didier Rémy. . — International Symposium on Theoretical Aspects of Computer Software, Springer-Verlag, 1994. — С. 321—346 .

• J. B. Wells. (англ.) // Proceedings of the 9th Annual IEEE . — Symposium on Logic in Computer Science (LICS), 1994. — P. 176—185 .

• , . Compiling Polymorphism Using Intensional Type Analysis. — 1995.

• Atsushi Ohori. . — Kyoto University, ACM , 1995. — С. 844—895 .

• Mark P. Jones. . — Springer-Verlag Lecture Notes, 1995. — doi : .

• Didier Rémy. // Presented at the workshop on Advances in types for computer science at the Newton Institute. — Cambridge, UK, 1995.

• . ML for the Working Programmer. — 2nd. — Cambridge, Great Britain: Cambridge University Press, 1996. — 492 с. — ISBN 0-521-57050-6 (hardback), 0-521-56543-X (paperback).

• Benedict R. Gaster, Mark P. Jones. // Technical Report NOTTCS-TR-96-3. — University of Nottingham, 1996.

• Jacques Garrigue, Didier Rémy. // Academic Press. — Information and Computation, 1997.

• M. Sulzmann. // Technical Report YALEU/DCS/RR-1128. — Yale University, 1997. — doi : .

• Karl Crary, Stephanie Weirich, J. Gregory Morrisett. . — , 1998.

• Benedict R. Gaster. // Technical report NOTTCS-TR-98-3. — Ph.D. Thesis, 1998.

• Jacques Garrigue. . — Kyoto University, 1998.

• Didier Rémy, Jérôme Vouillon. . — Theory And Practice of Object Systems, ACM , 1998. — Т. 4(1) . — С. 27—50 .

• John C. Reynolds. . — Cambridge University Press, 1998. — ISBN 978-0-521-59414-1 (hardback), 978-0-521-10697-9 (paperback).

• The ML2000 Working Group. (англ.) . — 1999.

• Benjamin Pierce. . — MIT Press , 2002. — ISBN 0-262-16209-1 .
  • Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — , 2012. — 680 с. — ISBN 978-5-7913-0082-9 .

• John C. Mitchell. Concepts in Programming Languages. — Cambridge University Press, 2004. — ISBN 0-511-04091-1 (eBook in netLibrary); 0-521-78098-5 (hardback).

• Jens Palsberg, Tian Zhao. . — 2004. 16 сентября 2016 года.

• Daan Leijen. // TechReport UU-CS-2004-51. — Universiteit Utrecht, 2004.

• Matthias Blume, Umut A. Acar, Wonseok Chae. . — , 2006.

• Matthew Fluet, Riccardo Pucella. (англ.) . — , 2006.

• Stephen Weeks. (англ.) . — 2006. 29 июня 2007 года.

• Matthias Blume. : speech video. — Microsoft, 2007.

• Matthias Blume, Umut A. Acar, Wonseok Chae. . — Toyota Technological Institute at Chicago, APLAS, 2008.

• Wonseok Chae. // Ph.D. Thesis. — Toyota Technological Institute at Chicago, 2009.

• Роман Душкин. . — 2010.

• Jeremy Yallop, Leo White. . — International Symposium on Functional and Logic Programming, 2014.

• . . — version 1.37 (revised 01.11.2014). — licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License., 2012. — 544 с. от 24 октября 2015 на Wayback Machine

• Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and Jose P. Magalhães. // In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation. — NY, USA: , 2012. — С. 53—66 .

• Minsky, Madhavapeddy, Hickey. (англ.) . — O'Reilly Media, 2013. — 510 p. — ISBN 9781449324766 .
  • Перевод на русский язык:
    Мински, Мадхавапедди, Хикки. Программирование на языке OCaml (рус.) . — ДМК, 2014. — 536 с. — ISBN 978-5-97060-102-0 .

• Andreas Rossberg. . — , 2015.

• Andreas Rossberg. . — WadlerFest, Google, 2016.

• (неопр.) .

• (неопр.) .

• (неопр.) .

• Jacques Garrigue. (неопр.) .