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

Параметрический полиморфизм считается «истинной» формой полиморфизма, делая язык более выразительным и существенно повышая коэффициент повторного использования кода. Традиционно ему противопоставляется 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