Кіріспе
Жалпылама бағдарламалау негіздері
Бағдарламалау тілдері мен типтер теориясында параметрлік полиморфизм кодтың бір бөлігіне нақты типтердің орнына айнымалыларды пайдалану арқылы "жалпы" тип беруге және қажет болған жағдайда нақты типтермен инстанциялауға мүмкіндік береді. Сәйкестік функциясы – бұл ерекше жағдай, бірақ көптеген басқа функциялар да параметрлік полиморфизмнен пайда көреді. Мысалы, екі тізімді біріктіретін функция тізім элементтерін тексермейді, тек тізімнің құрылымын ғана қарастырады. Сондықтан, оған ұқсас типтер отбасы беріледі, мысалы, `list a`, `list b` және т.б., мұнда `a` және `b` тип элементтерінің тізімін білдіреді. Ең жалпы тип, демек,
– бұл типтер отбасының кез келген типімен инстанциялануы мүмкін. `f` және `g` сияқты параметрлік полиморфтық функциялар кез келген тип бойынша параметрленген деп айтылады. Екі `f` және `g` функциялары бір тип бойынша параметрленген, бірақ функциялар кез келген саны типтер бойынша параметрленуі мүмкін. Мысалы, жұптың бірінші және екінші элементтерін қайтаратын `fst` және `snd` функцияларына келесі типтер берілуі мүмкін:
`fst a b : a -> (a, b)` және `snd a b : b -> (a, b)`. `fst a b` өрнегінде `a` типі `int` және `b` типі `string` болып инстанцияланады, ал `fst` функциясын шақыруда `fst int string`, сондықтан жалпы өрнектің типі `int` болады. Параметрлік полиморфизмді енгізу үшін қолданылатын синтаксис бағдарламалау тілдері арасында әртүрлі болады. Мысалы, кейбір бағдарламалау тілдерінде, мысалы, Haskell, ∀ квантификаторы ашық түрде жазылмауы мүмкін. Басқа тілдерде типтер параметрлік полиморфтық функцияның шақыру орындарында біріне немесе барлығына нақты түрде көрсетілуі керек.
The syntax used to introduce parametric polymorphism varies significantly between programming languages. For example, in some programming languages, such as Haskell, the quantifier is implicit and may be omitted. Other languages require types to be instantiated explicitly at some or all of a parametrically polymorphic function's call sites.
Тарих
Параметриялық полиморфизм алғаш рет 1975 жылы ML бағдарламалау тілінде пайда болды. Бүгінде ол Стандартты ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia, Python, TypeScript, C++ және тағы да басқа тілдерде қолданылады. Java, C#, Visual Basic NET және Delphi параметрлік полиморфизмді іске асыру үшін "генериктерді" енгізді. Тип полиморфизмінің кейбір нұсқалары сырттай параметрлік полиморфизмге ұқсас болғанымен, сонымен қатар арнайы мүмкіндіктерді де қосады. Мысалы, C++ үлгілерінің мамандануын қарастыруға болады.
1-ші (предикативті) полиморфизм
Предикативті типтік жүйеде (сонымен қатар пренекс полиморфты жүйе деп аталады) типтік айнымалылар полиморфты типтермен инстанцияланбауы мүмкін. Предикативті типтік теорияларға Мартин Лёфтың типтік теориясы және Nuprl жатады. Бұл "ML стилі" немесе "Let полиморфизмі" деп аталатын нәрсеге өте ұқсас (техникалық тұрғыдан алғанда, ML-дің Let полиморфизмі бірнеше қосымша синтаксистік шектеулерге ие). Бұл шектеу полиморфты және полиморфты емес типтерді ажыратуды өте маңызды етеді; сондықтан предикативті жүйелерде полиморфты типтерді кейде типтік схемалар деп атайды, оларды қарапайым (мономорфты) типтерден, кейде монотиптер деп аталатындардан ажырату үшін. Предикативтіліктің салдары – барлық типтерді сандық белгілердің барлығын ең сыртқы (пренекс) позицияға қоятын формада жазуға болады. Мысалы, жоғарыда сипатталған функцияның келесі типі бар: Бұл функцияны тізімдер жұбына қолдану үшін, нәтижесіндегі функция типі аргументтердің типтерімен сәйкес келетіндей, айнымалыға нақты тип қою қажет. Импредикативті жүйеде, тіпті өзі полиморфты тип болса да, кез келген тип болуы мүмкін; сондықтан оны кез келген типтегі элементтері бар тізімдер жұбына, тіпті өзі сияқты полиморфты функциялардың тізімдеріне де қолдануға болады. ML тіліндегі полиморфизм предикативті. Өйткені предикативтілік, басқа шектеулермен бірге, типтік жүйені толық типтік қорытындылау әрқашан мүмкін болатындай жеткілікті қарапайым етеді. Практикалық мысал ретінде, OCaml (ML-дің ұрпағы немесе диалектісі) типтік қорытындылауды жүзеге асырады және импредикативті полиморфизмді қолдайды, бірақ кейбір жағдайларда импредикативті полиморфизм қолданылғанда, егер бағдарламашы кейбір нақты типтік түсіндірмелер бермесе, жүйенің типтік қорытындылауы толық болмайды.
In order to apply this function to a pair of lists, a concrete type must be substituted for the variable such that the resulting function type is consistent with the types of the arguments. In an impredicative system, may be any type whatsoever, including a type that is itself polymorphic; thus can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as itself. Polymorphism in the language ML is predicative. This is because predicativity, together with other restrictions, makes the type system simple enough that full type inference is always possible. As a practical example, OCaml (a descendant or dialect of ML) performs type inference and supports impredicative polymorphism, but in some cases when impredicative polymorphism is used, the system's type inference is incomplete unless some explicit type annotations are provided by the programmer.
Жоғары дәрежелі полиморфизмдер
Кейбір типтік жүйелер басқа типтік конструкторлар болжамды болып қала бергенімен, алдын ала болжамды функция типтік конструкторды қолдайды. Мысалы, жоғары дәрежелі полиморфизмді қолдайтын жүйеде түрге рұқсат етіледі, тіпті мүмкін емес болса да. Тип k (к – тұрақты бүтін сан) деңгейіне ие деп айтылады, егер оның түбірінен кванторға дейінгі жол тип ағаш түрінде бейнеленгенде k немесе одан көп жебелерден солға өтпесе.