Введение

Основа обобщённого программирования

В языках программирования и теории типов параметрический полиморфизм позволяет присвоить единому фрагменту кода "обобщённый" тип, используя переменные вместо конкретных типов, а затем инстанцировать его конкретными типами по мере необходимости. Функция идентичности является особенно крайним примером, но многие другие функции также выигрывают от параметрического полиморфизма. Например, функция, которая объединяет два списка, не проверяет элементы списка, а только структуру списка. Поэтому ей можно присвоить семейство типов, например, `list a`, `list b`, и так далее, где `list a` обозначает список элементов типа `a`. Наиболее общий тип, следовательно,

который может быть инстанцирован для любого типа из этого семейства. Параметрически полиморфные функции, такие как `f` и `g`, говорят, параметризованы по произвольному типу. И `f`, и `g` параметризованы по одному типу, но функции могут быть параметризованы по произвольно большому числу типов. Например, функции `first` и `second`, возвращающие первый и второй элементы пары соответственно, могут иметь следующие типы:

В выражении `h x y`, `a` инстанцируется как `int`, а `b` инстанцируется как `string` в вызове `h`, поэтому тип всего выражения равен `bool`. Синтаксис, используемый для введения параметрического полиморфизма, значительно различается в разных языках программирования. Например, в некоторых языках программирования, таких как Haskell, квантор является неявным и может быть опущен. Другие языки требуют явной инстанциации типов в некоторых или всех точках вызова параметрически полиморфной функции.

История

Параметрический полиморфизм был впервые представлен в языках программирования ML в 1975 году. Сегодня он поддерживается в Standard ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia, Python, TypeScript, C++ и других. Java, C#, Visual Basic .NET и Delphi внедрили "обобщения" (generics) для реализации параметрического полиморфизма. Некоторые реализации полиморфизма типов кажутся похожими на параметрический полиморфизм, но при этом включают в себя ad hoc элементы. Примером является специализация шаблонов в C++.

Полиморфизм ранга-1 (предсказательный)

В предикативной системе типов (также известной как полиморфная система prenex) переменные типа не могут быть инстанцированы полиморфными типами. Теории предикативных типов включают теорию типов Мартина Лёфа и Nuprl. Это очень похоже на то, что называется "стиль ML" или "Let-полиморфизм" (технически Let-полиморфизм ML имеет несколько других синтаксических ограничений). Это ограничение делает различие между полиморфными и не полиморфными типами очень важным; таким образом, в предикативных системах полиморфные типы иногда называют схемами типов, чтобы отличить их от обычных (мономорфных) типов, которые иногда называют монотипами. Следствием предикативности является то, что все типы могут быть записаны в форме, помещающей все кванторы на самую внешнюю (prenex) позицию. Например, рассмотрим функцию, описанную выше, которая имеет следующий тип:

Чтобы применить эту функцию к паре списков, необходимо подставить конкретный тип вместо переменной таким образом, чтобы полученный тип функции был согласован с типами аргументов. В импредикативной системе может быть любым типом, включая тип, который сам по себе является полиморфным; таким образом, может применяться к парам списков с элементами любого типа – даже к спискам полиморфных функций, таких как она сама. Полиморфизм в языке ML является предикативным. Это связано с тем, что предикативность, вместе с другими ограничениями, делает систему типов достаточно простой, чтобы полный вывод типов всегда был возможен. В качестве практического примера, OCaml (потомок или диалект ML) выполняет вывод типов и поддерживает импредикативный полиморфизм, но в некоторых случаях, когда используется импредикативный полиморфизм, вывод типов системы неполный, если программист не предоставит некоторые явные аннотации типов.

Полиморфизм высшего ранга

Некоторые системы типов поддерживают импредикативный конструктор типа функции, даже если другие конструкторы типов остаются предикативными. Например, тип `∀a. a -> a` разрешен в системе, поддерживающей полиморфизм высшего ранга, даже если `∀a. ∀b. a -> b` может быть запрещен. Ранг типа определяется как k (для некоторого фиксированного целого числа k), если при представлении типа в виде дерева ни один путь от корня к квантору не проходит через k или более стрелок слева.