Parametrisk polymorfisme - Parametric polymorphism

Polymorfisme
Ad hoc polymorfisme
Parametrisk polymorfisme
Subtyping

I programmeringssprog og typeteori er parametrisk polymorfisme en måde at gøre et sprog mere udtryksfuldt på, samtidig med at den opretholder fuld statisk typesikkerhed . Ved hjælp af parametrisk polymorfisme kan en funktion eller en datatype skrives generisk, så den kan håndtere værdier identisk uden at afhænge af deres type. Sådanne funktioner og datatyper kaldes henholdsvis generiske funktioner og generiske datatyper og danner grundlaget for generisk programmering .

For eksempel kan en funktion, appendder forbinder to lister, konstrueres, så den ikke er ligeglad med typen af ​​elementer: den kan tilføje lister med heltal , lister over reelle tal , lister over strenge osv. Lad typevariablen a betegne typen af ​​elementer på listerne. Så appendkan det skrives

forall a. [a] × [a] -> [a]

hvor [a]betegner typen af ​​lister med elementer af type a . Vi siger, at den type appender parametreres af en for alle værdier af en . (Bemærk, at da der kun er en typevariabel, kan funktionen ikke anvendes på bare et par lister: parret såvel som resultatlisten skal bestå af den samme type elementer) For hvert sted, hvor appendder anvendes, skal en værdi bestemmes for en .

Efter Christopher Strachey kan parametrisk polymorfisme stå i kontrast med ad hoc polymorfisme , hvor en enkelt polymorf funktion kan have en række forskellige og potentielt heterogene implementeringer afhængigt af den eller de argumenter, den anvendes på. Således kan ad hoc polymorfisme generelt kun understøtte et begrænset antal af sådanne forskellige typer, da der skal tilvejebringes en separat implementering for hver type.

Historie

Parametrisk polymorfisme blev først introduceret til programmeringssprog i ML i 1975. I dag findes den i Standard ML , OCaml , F# , Ada , Haskell , Mercury , Visual Prolog , Scala , Julia , Python , TypeScript , C ++ og andre. Java , C# , Visual Basic .NET og Delphi har hver introduceret "generika" til parametrisk polymorfisme. Nogle implementeringer af type polymorfisme ligner overfladisk parametrisk polymorfisme, samtidig med at de introducerer ad hoc -aspekter. Et eksempel er C ++ skabelonspecialisering .

Den mest generelle form for polymorfisme er "højere rang impredikativ polymorfisme". To populære begrænsninger af denne form er begrænset rangpolymorfisme (for eksempel rang-1 eller prenexpolymorfisme ) og prædikativ polymorfisme. Tilsammen giver disse begrænsninger "prædikativ prenexpolymorfisme", som i det væsentlige er den form for polymorfisme, der findes i ML og tidlige versioner af Haskell.

Højere rangeret polymorfisme

Rang-1 (prenex) polymorfisme

I et prenex polymorft system kan typevariabler muligvis ikke instantieres med polymorfe typer. Dette ligner meget det, der kaldes "ML-stil" eller "Let-polymorfisme" (teknisk set har ML's Let-polymorfisme et par andre syntaktiske begrænsninger). Denne begrænsning gør sondringen mellem polymorfe og ikke-polymorfe typer meget vigtig; Således kaldes polymorfe typer i predikative systemer undertiden som typeskemaer for at skelne dem fra almindelige (monomorfe) typer, som undertiden kaldes monotyper . En konsekvens er, at alle typer kan skrives i en form, der placerer alle kvantificatorer yderst (prenex). Overvej f.eks. appendFunktionen beskrevet ovenfor, som har type

forall a. [a] × [a] -> [a]

For at anvende denne funktion på et par lister, skal en type erstattes af variablen a i funktionstypen, således at typen af ​​argumenterne matcher den resulterende funktionstype. I et impredikativt system kan den type, der erstattes, være hvilken som helst type, herunder en type, der i sig selv er polymorf; således appendkan anvendes til par af lister med elementer af enhver type-even til lister af polymorfe funktioner som appendsig selv. Polymorfisme i sproget ML er prædikativt. Dette skyldes, at prædikativitet sammen med andre restriktioner gør typesystemet så simpelt, at der altid er mulighed for fuld inferens .

Som et praktisk eksempel udfører OCaml (en efterkommer eller dialekt af ML ) typeinferens og understøtter impredicative polymorphism, men i nogle tilfælde, når der anvendes impredicative polymorphism, er systemets typeafstand ufuldstændig, medmindre nogle eksplicitte typeanmærkninger leveres af programmereren.

Rank- k polymorfisme

For nogle faste værdier k er rank- k polymorfisme et system, hvor en kvantificator muligvis ikke vises til venstre for k eller flere pile (når typen tegnes som et træ).

Typeinferens for rang-2 polymorfisme kan afgøres, men rekonstruktion for rang-3 og derover er ikke.

Rank- n ("højere rang") polymorfisme

Rank- n polymorfi er polymorfi, hvori kvantorer kan vises til venstre for vilkårligt mange pile.

Predikativitet og upredikativitet

Forudsigende polymorfisme

I et predikativt parametrisk polymorft system må en type, der indeholder en typevariabel , ikke anvendes på en sådan måde, at den instantieres til en polymorf type. Prædikative typeteorier omfatter Martin-Löf-teori og NuPRL .

Impredikativ polymorfisme

Impredikativ polymorfisme (også kaldet førsteklasses polymorfisme ) er den mest kraftfulde form for parametrisk polymorfisme. En definition siges at være uhensigtsmæssig, hvis den er selvrefererende; i typeteori muliggør dette instantiering af en variabel i en type med enhver type, herunder polymorfe typer, såsom sig selv. Et eksempel på dette er System F med typevariablen X i typen , hvor X endda kunne referere til T selv.

I typen teori , den hyppigst undersøgte impredicative maskinskrevne λ-calculus er baseret på de af lambda terning , især System F .

Afgrænset parametrisk polymorfisme

Hovedartikel: Begrænset kvantificering

I 1985 erkendte Luca Cardelli og Peter Wegner fordelene ved at tillade grænser for typeparametrene. Mange operationer kræver en vis viden om datatyperne, men kan ellers fungere parametrisk. For eksempel for at kontrollere, om et element er inkluderet på en liste, skal vi sammenligne emnerne for lighed. I Standard ML er typeparametre i formen '' a begrænset, så ligestillingsoperationen er tilgængelig, så funktionen ville have typen '' a × '' a liste → bool og '' a kan kun være en type med definerede lighed. I Haskell opnås afgrænsning ved at kræve, at typer tilhører en typeklasse ; således har den samme funktion typen i Haskell. I de fleste objektorienterede programmeringssprog, der understøtter parametrisk polymorfisme, kan parametre begrænses til at være undertyper af en given type (se undertype polymorfisme og artiklen om generisk programmering ).

Se også

Noter

Referencer