Polymorfi (datalogi)

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 25. marts 2021; checks kræver 11 redigeringer .

Polymorfi i programmeringssprog og typeteori  er en funktions evne til at behandle data af forskellige typer [1] [2] [3] .

Der er flere typer polymorfi. To fundamentalt forskellige blev beskrevet af Christopher Strachey i 1967 : disse er parametrisk polymorfi og ad-hoc polymorfi , andre former er deres underarter eller kombinationer. Parametrisk polymorfi er sand, fordi indebærer udførelse af den samme kode for alle gyldige argumenttyper, og ad-hoc polymorfi er imaginær, fordi er at sikre kosmetisk ensartethed af potentielt forskellig eksekverbar kode for hver bestemt type argument [1] [4] . Samtidig er der situationer, hvor det er nødvendigt at bruge præcis ad-hoc polymorfi, og ikke parametrisk [5] . Teorien om kvalificerede typer kombinerer alle former for polymorfi i en enkelt model.

Der er en udbredt definition af polymorfi tilskrevet Björn Stroustrup : " en grænseflade (som en liste over erklæringer) - mange implementeringer (definitioner forbundet med disse erklæringer) " [6] , men kun ad-hoc polymorfi (imaginær polymorfi) falder ind under denne definition.

Generel information

Den grundlæggende mulighed for den samme kode til at behandle data af forskellige typer er bestemt af egenskaberne for sprogets typesystem . Fra dette synspunkt skelner man [7] statisk ikke-polymorf typning (efterkommere af Algol og BCPL ), dynamisk typning (efterkommere af Lisp , Smalltalk , APL ) og statisk polymorf typning (efterkommere af ML ). Brugen af ​​ad-hoc polymorfi er mest karakteristisk for ikke-polymorf typning. Parametrisk polymorfi og dynamisk typning øger kodegenbrug meget mere end ad-hoc polymorfi, da en funktion, der er defineret én gang, implementerer den specificerede adfærd uden duplikering for et uendeligt antal nydefinerede typer, der opfylder de betingelser, der kræves i funktionen. På den anden side bliver det nogle gange nødvendigt at give en anden funktionsadfærd afhængigt af typen af ​​parameteren, og så er speciel polymorfi nødvendig.

Parametrisk polymorfi er synonymt med typeabstraktion [8] . Det er allestedsnærværende i funktionel programmering , hvor det normalt blot omtales som "polymorfi".

I det objektorienterede programmeringsfællesskab betyder udtrykket "polymorfi" normalt arv , og brugen af ​​parametrisk polymorfi kaldes generisk programmering [9] eller nogle gange "statisk polymorfi".

Klassifikation

For første gang blev klassificeringen af ​​varianter af polymorfi udført af Christopher Strachey .

Hvis præcis én type er knyttet til en funktionsparameter, kaldes en sådan funktion monomorf. Mange programmeringssprog giver en syntaktisk mekanisme til at tildele et enkelt navn (identifikator) til flere monomorfe funktioner. I dette tilfælde bliver det i kildekoden muligt at kalde en funktion med faktiske parametre af forskellige typer, men i den kompilerede kode kaldes der faktisk forskellige funktioner (se procedure og funktionsoverbelastning ). Strachey kaldte denne mulighed for "ad-hoc polymorfi".

Hvis mere end én type er knyttet til en funktionsparameter, kaldes en sådan funktion polymorf . Selvfølgelig kan kun én type associeres med hver faktisk værdi, men en polymorf funktion overvejer parametre baseret på eksterne egenskaber, ikke deres egen organisation og indhold. Strachey kaldte denne mulighed for "parametrisk polymorfi".

Senere blev klassifikationen forfinet af Luca Cardelli [10] , der fremhævede fire typer polymorfi:

I nogle værker skelnes parametrisk, ad-hoc- og subtype polymorfi som tre uafhængige klasser af polymorfi [11] .

Dualiteten af ​​betydningen af ​​udtrykket "ad hoc" (på den ene side - "spontan, dårligt tænkt, lavet ved lejligheden", på den anden side - "særlig, arrangeret specifikt til et givet formål eller en given lejlighed") har været fortjent i mange år [5] . Strachey valgte dette udtryk ud fra den første betydning, idet han understregede, at der med ad-hoc polymorfi ikke er nogen enkelt systematisk måde at udlede typen af ​​resultatet ud fra typen af ​​argumenter, og selvom det er muligt at opbygge et bestemt sæt regler for at indsnævre søgespektret, disse regler er spontane i naturen, både i indhold og kontekst af anvendelsen [1] .

Faktisk er ad-hoc polymorfi ikke sand polymorfi [12] . Funktionsoverbelastning giver ikke "værdi, der har flere typer", men "tegn, der har flere typer ", men værdierne identificeret med dette symbol er af forskellige (potentielt inkompatible) typer. På samme måde er støbning ikke sand polymorfi: Operatøren ser ud til at acceptere værdier af mange typer, men værdierne skal konverteres til en vis repræsentation, før den kan bruge dem, så operatøren faktisk kun opererer på én type (dvs. har én type). Desuden afhænger typen af ​​returværdien her ikke af typen af ​​inputparameteren , som i tilfældet med parametrisk polymorfi.

Men at definere specifikke funktionsimplementeringer for forskellige typer er i nogle tilfælde en nødvendighed, ikke en ulykke. Klassiske eksempler er implementeringen af ​​aritmetiske operationer (fysisk forskellige for heltal og flydende kommatal ) og typelighed, som i årtier ikke havde nogen accepteret universel formalisering. Løsningen var typeklasserne , som er en mekanisme til eksplicit diskret opregning af de tilladte værdier af typevariabler til statisk afsendelse i typelaget. De samler de to varianter af polymorfi adskilt af Strachey, " gør ad hoc polymorfi mindre ad hoc " [5] ( spil på dualitet). Yderligere generalisering af typeklasser førte til konstruktionen af ​​en teori om kvalificerede typer , som ensartet formaliserer de mest eksotiske typesystemer, herunder udvidelige notationer og undertyper.

I modsætning til overbelastning og typestøbning er subtype polymorfisme ægte polymorfi: subtypeobjekter kan manipuleres ensartet, som om de tilhørte deres supertyper (men dette er ikke sandt for sprog, der implementerer "polymorfi ved nedarvning" via casting typer og funktionsoverbelastning , som i tilfældet med C++ ). Den reneste er parametrisk polymorfi : det samme objekt eller den samme funktion kan bruges ensartet i forskellige indtastningskontekster uden modifikationer, afstøbninger eller andre køretidstjek eller konverteringer. Dette kræver dog en vis ensartet repræsentation af data (for eksempel gennem pointere ) [4] .

Grundlæggende typer af polymorfi

Ad-hoc polymorfi

Ad-hoc polymorfi (oftest oversat i russisk litteratur som "særlig polymorfisme" eller "specialiseret polymorfi", selvom begge muligheder ikke altid er sande ) understøttes på mange sprog gennem funktions- og metodeoverbelastning og i svagt skrevet dem  også gennem typestøbning .

I det følgende eksempel ( Pascal language ) ser funktionerne Addud som om de implementerer den samme funktionalitet på forskellige typer, men compileren definerer dem som to helt forskellige funktioner.

program Adhoc ; funktion Tilføj ( x , y : Heltal ) : Heltal ; begynde Tilføj := x + y ende ; funktion Tilføj ( s , t : String ) : String ; begynde Tilføj := Konkat ( s , t ) ende ; start Writeln ( Tilføj ( 1 , 2 )) ; Writeln ( Tilføj ( 'Hej, ' , 'Verden!' )) ; ende .

I dynamisk indtastede sprog kan situationen være mere kompliceret, da valget af den påkrævede funktion at kalde kun kan foretages under kørsel.

Overbelastning  er en syntaktisk mekanisme, der gør det muligt at kalde forskellige funktioner med en enkelt identifikator [13] . Typecasting  er en semantisk mekanisme, der udføres for at konvertere den faktiske type af et argument til den forventede type af en funktion, uden hvilken der ville opstå en typefejl . Det vil sige, at når en funktion kaldes med et typecast, udføres forskellig kode for forskellige typer (forud for kaldet af selve funktionen) [13] .

Parametrisk polymorfi

Parametrisk polymorfi gør det muligt at definere en funktion eller datatype generisk, så værdier behandles identisk uanset deres type. En parametrisk polymorf funktion bruger adfærdsbaserede argumenter frem for værdibaserede, og har kun adgang til egenskaberne af de argumenter, den har brug for, hvilket gør den brugbar i enhver kontekst, hvor objekttypen opfylder de givne adfærdskrav.

Avancerede typesystemer (såsom Hindley-Milner-systemet ) giver mekanismer til at definere polymorfe typer , hvilket gør brugen af ​​polymorfe funktioner mere bekvemt og giver statisk type sikkerhed . Sådanne systemer er andenordens typesystemer, der til førsteordens typesystemer (brugt i de fleste proceduresprog ) tilføjer typeparametrisering (ved hjælp af en typevariabel ) og typeabstraktion (ved hjælp af eksistentiel kvantificering over dem). I andenordens typesystemer er der ikke umiddelbart behov for at understøtte primitive typer , da de kan udtrykkes gennem mere avancerede midler. [fjorten]

Det klassiske eksempel på en polymorf type er en liste over vilkårlige typeelementer, for hvilke mange Hindley-Milner- typesprog (mest statisk indtastede funktionelle programmeringssprog ) giver syntaktisk sukker . Følgende eksempel viser definitionen af ​​en ny algebraisk type "parametrisk polymorf liste " og to funktioner på den:

dataliste a = Nul | _ Ulemper a ( Liste a ) længde :: List a - > Heltalslængde Nul = 0 længde ( Cons x xs ) = 1 + længde xs map :: ( a -> b ) -> Liste a -> Liste b map f Nul = Ingen kort f ( Cons x xs ) = Cons ( f x ) ( map f xs )

Ved substituering af betontyper til en typevariabel og så videre, vil der blive bygget henholdsvis betontyper og så videre. Disse særlige typer kan igen erstattes med den type variabel igen , producere typer , og så videre. I dette tilfælde, for alle objekter af alle konstruerede typer, vil den samme fysiske implementering af funktionerne og blive brugt . aIntStringList IntList StringList List StringList (Int, List String)lengthmap

Begrænsede former for parametrisk polymorfi er også tilgængelige i nogle imperative (især objektorienterede ) programmeringssprog, hvor udtrykket " generisk programmering " almindeligvis bruges til at henvise til det. Især i C, er utypebestemt parametrisk polymorfi traditionelt tilvejebragt ved brug af en utypebestemt pointer void* , selvom en maskinskrevet form også er mulig. Brug af C++ skabeloner ligner overfladisk parametrisk polymorfi, men semantisk implementeret af en kombination af ad-hoc mekanismer; i C++- fællesskabet kaldes det "statisk polymorfi" (i modsætning til "dynamisk polymorfi" ).

Parametrisitet

Formaliseringen af ​​parametrisk polymorfi fører til begrebet parametricity , som består i evnen til at forudsige programmers adfærd ved kun at se på deres typer. For eksempel, hvis en funktion er af typen " forall a. a -> a", så uden nogen eksterne midler, der komplementerer sproget , kan det bevises , at det kun kan være identisk . Derfor er parametrisitet ofte ledsaget af sloganet "theorems for free" ( eng.  theorems for free ). [15] [16] [17]

En vigtig konsekvens af  dette er også repræsentationsuafhængighed , hvilket betyder, at funktioner over en abstrakt type er ufølsomme over for dens struktur, og forskellige implementeringer af denne type kan frit erstatte hinanden (selv inden for det samme program) uden at påvirke disse funktioners adfærd. [18] .

De mest avancerede parametrisk polymorfe systemer (højeste punkt i lambda-terningen ) tager ideen om parametri til det punkt, at de fuldt ud er i stand til at bevise rigtigheden af ​​programmer: de gør det muligt at skrive programmer, der er korrekte af design, så bestået et typekonsistenstjek garanterer i sig selv, at programmets opførsel er korrekt forventet [19] .

Registrering og variant polymorfi

Et separat problem er udvidelsen af ​​parametrisk polymorfi til aggregerede typer: diskriminerede produkter af typer (traditionelt kaldet poster ) og diskriminerede summer af typer (også kendt som varianttyper ). Forskellige " record calculus " ( engelsk  record calculi ) tjener som et formelt grundlag for objektorienteret og modulær programmering [20] .

val r = { a = 1 , b = sand , c = "hej" } val { a = n , ... = r1 } = r val r2 = { d = 3,14 , ... = r1 }

En ellipse betyder et vist antal indtastede felter, det vil sige en abstraktion af koden fra specifikke typer poster, der kunne behandles her (og "længden" af denne serie kan også variere). At kompilere polymorf adgang til felter, der kan placeres i en anden rækkefølge i forskellige poster, er et vanskeligt problem, både ud fra et synspunkt om at kontrollere sikkerheden ved operationer på sprogniveau og ud fra et synspunkt om ydeevne ved maskinkoden niveau. En naiv løsning kan være dynamisk at slå ordbogen op ved hvert opkald (og scriptsprog bruger den), men dette er naturligvis ekstremt ineffektivt. Dette problem er blevet aktivt undersøgt i flere årtier; Der er bygget mange teoretiske modeller og praktiske systemer baseret på dem, der adskiller sig i udtrykskraft og metateoretisk kompleksitet. De vigtigste præstationer på dette område er in-line polymorfi foreslået af Mitchell Wand og polymorf rekordregning bygget af Atsushi Ohori .  En mere almindelig model, men halter bagud i mange karakteristika, er subtypning på poster .  

Understøttelse af registreringspolymorfi i en eller anden form kan åbne op for muligheder i et polymorfisk sprog såsom meddelelser af højere orden (den mest kraftfulde form for objektorienteret programmering ) , den sømløse indlejring af operationer på databaseelementer ( SQL ) i sprogkode til generelle formål og andre, op til udvidelsesbar programmering (det vil sige programmering fri for udtryksproblemet ), der garanterer fraværet af ubehandlede undtagelser i programmer og visse former for metaprogrammering .

Undertype polymorfi

Inklusionspolymorfi eren generaliseret formalisering af subtypebestemmelse [ og arv [21] . Disse begreber bør ikke forveksles: undertyper definerer relationer på grænsefladeniveau, mens arv definerer relationer på implementeringsniveau [22] .

Subtyping ( subtyping ) , eller subtype polymorphism ( subtype polymorphism ), betyder, at adfærden af ​​en parametrisk polymorf funktion er begrænset til et sæt typer afgrænset i et supertype-subtype hierarki [23] [10] [24] . For eksempel, hvis der er typer , og , begrænset af relationer og , så vil en funktion defineret på type , også være i stand til at acceptere argumenter af typer eller , og dens adfærd vil være identisk. Den faktiske type af et objekt kan skjules som en "sort boks" og kun udleveres efter anmodning om objektidentifikation. Faktisk, hvis en type er abstrakt, så kan et konkret objekt af den type ikke engang eksistere (se abstrakt klasse , men må ikke forveksles med abstrakt datatype ). Dette typehierarki er kendt (især i sammenhæng med skemasproget ) som nummertårnet , og indeholder normalt flere typer. NumberRationalIntegerNumber :> RationalNumber :> IntegerNumberIntegerRationalNumber

Ideen med subtyping er motiveret ved at øge antallet af typer, der kan håndteres af allerede skrevne funktioner, og derved øge kodegenbrugsraten under stærk indtastning (dvs. at øge antallet af indtastede programmer). Dette er tilvejebragt af subsumtionsreglen : " hvis et udtryk tilhører en type i en skrivekontekst , og er sandt , så hører det også til typen " [25] [26] . et'Гt'<:tet

Subtypeforhold er mulige på en lang række typekategorier: primitive typer (som Integer <: Number), sumtyper , produkttyper , funktionelle typer osv. Desuden foreslog Luca Cardelli begrebet magtsortering ( “magt”-typer ) for at beskrive subtyping [27] : han navngav slægten af ​​alle dens undertyper som typens magttype [ 28 ] .

En særlig plads inden for datalogi er optaget af subtypning på poster .

Undertastning på poster

Record subtyping , også kendt som subsumption (  se Barbara Liskovs substitutionsprincip ) , er den mest almindelige teoretiske begrundelse for objektorienteret programmering (OOP) [29] [30] [24] [31] (men ikke den eneste - se # registrering og variant polymorfi ).

Martín Abadi og Luca Cardelli formaliserede subtypning på poster gennem begrænset kvantificering over parametrisk polymorfe typer [29] [30] ; mens typeparameteren er sat implicit [32] .

Ved subtyping på poster skelnes der mellem to varianter: i bredden og i dybden.

Breddeunderskrivning involverer tilføjelse af nye felter til en post . For eksempel:

type Objekt = { alder: Int } type Køretøj = { alder: Int; hastighed: Int} type Cykel = { alder: Int; hastighed: Int; gear: Int; } typeMachine = { age: Int; brændstof: String

På den ene side kan man skrive undertypningsrelationerne Vehicle <: Object, Bike <: Vehicle(og da undertypningen er transitiv , så og Bike <: Object) og Machine <: Object. På den anden side kan vi sige, at typer Vehicle, Bikeog Machine inkluderer (arver) alle egenskaber af type Object. (Her er typesystemets strukturelle semantik underforstået )

Fordi en type ofte intuitivt ses som et sæt værdier, kan en forøgelse af antallet af felter i en undertype være kontraintuitiv fra et sætteoretisk synspunkt . I virkeligheden er typer ikke sæt [33] , de er beregnet til at verificere programmers adfærd, og ideen med subtyping er, at en undertype i det mindste har egenskaberne af sin supertype og dermed er i stand til at efterligne den i det mindste hvor en genstand forventes supertype [25] . Eller med andre ord: en supertype definerer et minimumssæt af egenskaber for et sæt af objekter, og derefter en type, der har disse egenskaber og muligvis nogle andre, danner en delmængde af dette sæt, og derfor er dens undertype [30] .

Subtypeforhold med hensyn til sæt er mere intuitive i tilfælde af varianttyper [34] :

type Dag = man | tirs | bryllup | tor | fre | sad | sol type Arbejdsdag = man | tir | bryllup | tor | fre type WeekEnd = lør | sol

Her Workday <: Dayog WeekEnd <: Day.

Navngivning af felter giver dig mulighed for at abstrahere fra rækkefølgen af ​​deres forekomst i poster (i modsætning til tuples ), hvilket gør det muligt at bygge vilkårlige rettede acykliske nedarvningsgrafer, der formaliserer multipel nedarvning [34] :

type Bil = { alder: Int; hastighed: Int; brændstof: String

Nu Car <: Vehicleog på samme tid Car <: Machine. Det er også indlysende at Car <: Object(se diamantformet arv ).

Dybdeundertypning betyder, at typerne af bestemte postfelter kan erstattes af deres undertyper:

type Voyage = { veh: Vehicle; dato: Dag type Sport = { veh: Cykel; dato: Dag type Ferie = { veh: Bil; dato: Weekend }

Ud fra definitionerne ovenfor kan vi udlede , at Sports <: Voyageog Vacation <: Voyage.

Metoder i postundertyper

Fuld understøttelse af objektorienteret programmering indebærer, at der i antallet af postfelter også inkluderes funktioner , der behandler værdierne af de posttyper , de tilhører [29] [35] . Sådanne funktioner kaldes traditionelt " metoder ". En generaliseret model for binding af poster til metoder er afsendelsesmatrixen ; i praksis dekomponerer de fleste sprog det til vektorer i rækker eller kolonner - henholdsvis implementerer enten en klassebaseret organisation eller en metodebaseret organisation [36 ] . Samtidig bør man skelne mellem overordnede metoder i undertyper ( metodeoverstyring ) og undertypefunktioner ( funktionel undertypebestemmelse ). Tilsidesættelse af metoder binder dem ikke med undertypeforhold på funktioner, men giver dem mulighed for at ændre deres typesignaturer. I dette tilfælde er tre muligheder mulige: invariant, kovariant og kontravariant redefinition, og de sidste to bruger subtyping af deres parametre [37] (for flere detaljer, se kovarians og kontravarians ). Abadi-Cardelli-regningen [29] tager kun hensyn til invariante metoder, som er nødvendige for at bevise sikkerhed .

Mange objektorienterede sprog giver en indbygget mekanisme til at binde funktioner til metoder og implementerer dermed en klassebaseret organisering af programmer. Sprog, der behandler funktioner som førsteklasses objekter og skriver dem (se førsteklasses funktioner , funktionel type  - må ikke forveksles med en funktions returtype ) tillader vilkårlig metodebaseret organisation, som tillader objektorienteret design uden direkte støtte fra siderne af tungen [38] . Nogle sprog (såsom OCaml ) understøtter begge dele.

Sprog med typesystemer baseret på formel subtyping-teori ( OCaml , efterfølgeren ML -projektet ) behandler objektsystemer og klassesystemer uafhængigt [39] [40] . Det betyder, at objekttypen primært er knyttet til et objekt , og kun når det er udtrykkeligt angivet, er objekttypen knyttet til en bestemt klasse. I dette tilfælde udføres dynamisk afsendelse på objektniveau, hvilket betyder, at i sådanne sprog kan to objekter, der tilhører samme klasse, generelt have et andet sæt metoder. Sammen med den formelt definerede semantik af multipel nedarvning giver dette øjeblikkelig omfattende støtte til mixins .

CLOS implementerer hele afsendelsesmatrixen gennem multimetoder , det vil sige dynamisk afsendte metoder, der er polymorfe i flere argumenter på én gang [41] .

Nogle sprog bruger ejendommelige ad-hoc] løsninger. For eksempel sørger C++ sprogtypesystemet for automatisk typecasting (dvs. det er svagt ), ikke-polymorf , emulerer subtyping manifest nedarvning med invariante metodesignaturer og understøtter ikke typeabstraktion (ikke at forveksle med feltskjul ) . Nedarvning i C++ er implementeret af et sæt ad-hoc mekanismer, men dets brug kaldes "polymorfi" i sprogsamfundet (og feltskjul kaldes "abstraktion" [42] ). Det er muligt at styre arvegrafen: diamantformet arv i C++ kaldes " virtuel arv " og er specificeret af en eksplicit attribut ; som standard duplikeres nedarvede felter og tilgås med kvalificeret navn. Brugen af ​​et sådant sprog kan være usikkert  - man kan ikke garantere programmernes stabilitet [43] [37] (et sprog kaldes sikkert , hvis programmer i det, som kan accepteres af compileren som velformede, aldrig vil gå længere end den tilladte adfærd i dynamik [44] ). virtual

Højere-ordens subtyping

Systemet er en udvidelse af System F (ikke repræsenteret i lambda-terningen ), som formaliserer begrænset kvantificering over typeoperatorer , hvilket udvider undertyperelationer fra slægt til typer af højere slægt . Der er flere versioner af systemet , der adskiller sig i udtrykskraft og metateoretisk kompleksitet, men de fleste af hovedideerne blev fastlagt af Luca Cardelli [45] . *

En kombination af varianter af polymorfi

Indtast klasser

En typeklasse implementerer en enkelt uafhængig tabel over virtuelle metoder for mange ( universelt kvantificerede ) typer. På denne måde adskiller typeklasser sig fra klasser i objektorienteret programmering , hvor hvert objekt af enhver ( begrænset kvantificeret ) type er ledsaget af en pointer til en virtuel metodetabel [46] . Typeklasser er ikke typer, men kategorier af typer; deres forekomster er ikke værdier, men typer.

For eksempel [46] :

klasse Num a hvor ( + ), ( * ) :: a -> a -> a negate :: a -> a

Denne erklæring lyder således: " En type ahører til en klasse, Numhvis funktioner (+), (*)og negatemed de givne signaturer er defineret på den ."

instans Num Int hvor ( + ) = addInt ( * ) = mulInt negate = negInt instans Num Float hvor ( + ) = addFloat ( * ) = mulFloat negate = negFloat

Den første erklæring lyder: " Der er funktioner (+)og tilsvarende signaturer, (*)der negateer defineret over typenInt ." Den anden udtalelse lyder på samme måde.

Nu kan du indtaste følgende funktioner korrekt (og det er muligt at bestemme slutningen ):

kvadrat :: Tal a => a -> a kvadrat x = x * x kvadrater3 :: Tal a , tal b , tal c => ( a , b , c ) -> ( a , b , c ) kvadrater3 ( x , y , z ) = ( kvadrat x , kvadrat y , kvadrat z )

Da multiplikationsoperationen er implementeret fysisk anderledes for heltal og flydende kommatal , i mangel af typeklasser, ville to overbelastede funktioner squareog otte overbelastede funktioner allerede være påkrævet her squares3, og i rigtige programmer med komplekse datastrukturer er der meget mere duplikatkode . I objektorienteret programmering løses problemer af denne art gennem dynamisk forsendelse , med tilhørende overhead. Typeklassen udsendes statisk og bringer parametriske og ad-hoc polymorfismer i en enkelt model [5] . Med hensyn til parametrisk polymorfi har en typeklasse en parameter ( en typevariabel ), der spænder over et sæt typer. Fra ad-hoc polymorfis synspunkt er dette sæt ikke kun diskret, men også eksplicit specificeret ned til implementeringsniveauet. Kort sagt betyder signaturen , at funktionen er parametrisk polymorf , men rækken af ​​typer af dens parameter er kun begrænset til de typer, der tilhører typeklassen . På grund af dette er funktionen skrevet på en unik måde, på trods af opfordringen til den overbelastede funktion fra dens krop. square :: Num a => a -> aNum

Native support for typeklasser blev først implementeret i Haskell , men de kan også introduceres i ethvert parametrisk polymorft sprog ved simpel forbehandling [5] og også implementeret idiomatisk (se f.eks. ML-modulsproget#Implementing Alternative Models ). Direkte støtte kan dog lette automatisk ræsonnement om programmernes betydning.

Ligestillingstyper i Haskell er implementeret som forekomster af en typeklasse (Eq generaliserer ligestillingstypevariabler fra Standard ML ) :

( == ) :: Eq a => a -> a -> Bool

For at reducere besværet med at kode nogle af de ofte åbenlyst nødvendige egenskaber ved brugerdefinerede typer, leverer Haskell desuden syntaktisk sukker  , en konstruktion deriving, der er gyldig for et begrænset sæt standardtypeklasser (såsom Eq). (I det russisktalende samfund forveksles dets brug ofte med begrebet " arv " på grund af de særlige forhold ved oversættelsen af ​​ordet " aflede ".)

Generiske algebraiske datatyper

Polytypisme

Udtrykket "polytypisme" eller "datatypegeneralisering" bruges nogle gange. Grundlæggende refererer polytyping til sprogets indbyggede understøttelse af typekonstruktørpolymorfi , designet til at forene programmeringsgrænseflader og øge kodegenbrug . Et eksempel på polytypisme er den generaliserede mønstertilpasningsalgoritme [47] .

Per definition, i en polytype-funktion, " selv om der kan være et begrænset antal ad-hoc-grene for nogle typer, er der ingen ad-hoc-kombinator " [48] .

Polytyping kan implementeres ved brug af en generisk datatype eller højere rang polymorfi . PolyP [49] -udvidelsen af ​​Haskell er en syntakskonstruktion, der forenkler definitionen af ​​polytypefunktioner i Haskell .

En polytypefunktion er i en vis forstand mere generel end en polymorf funktion, men på den anden side kan en funktion være polytype og ikke polymorf, som det kan ses af følgende funktionstypesignaturer :

hoved :: [ a ] ​​-> a ( + ) :: Antal a => a -> a -> a længde :: Regulær d => d a -> Int sum :: Regulær d => d Int -> Int

Den første funktion ( head) er polymorf (parametrisk polymorf ), den anden (infix-operatoren “ ”) er overbelastet (ad-hoc-polymorf), den tredje og fjerde er polytype: typevariablen i deres definition varierer over type konstruktører . Samtidig er den tredje funktion ( ) polytype og polymorf (formentlig beregner den "længden" for nogle sæt af polymorfe aggregattyper - for eksempel antallet af elementer i lister og træer ), og den fjerde ( ) er polytype, men ikke polymorf (monomorf over aggregattyper, der tilhører typeklassen , for hvilken den formentlig beregner summen af ​​heltal, der danner et objekt af en bestemt aggregattype). + dlengthsum Regular

Diverse

Dynamisk indtastede sprog repræsenterer ensartet varianter af polymorfi, som danner en karakteristisk ideologi i dem og påvirker de anvendte opgavenedbrydningsmetoder. For eksempel i Smalltalk er enhver klasse i stand til at modtage beskeder af enhver type og enten behandle dem på egen hånd (inklusive gennem introspektion ) eller videresende den til en anden klasse - således er enhver metode formelt parametrisk polymorf, mens dens interne struktur kan forgrene sig i henhold til betingelsen for dynamisk argumenttype, implementere speciel polymorfi. I CLOS er multimetoder samtidig førsteklasses funktioner , hvilket giver os mulighed for at betragte dem både som begrænset kvantificerede og som generaliserede ( ægte polymorfe ).

Statisk polymorfisk typede sprog kan derimod implementere varianter af polymorfi ortogonalt (uafhængigt af hinanden), hvilket gør det muligt for dem at blive indviklet konstrueret på en typesikker måde. For eksempel understøtter OCaml parametriske klasser (svarende i egenskaber til C++ klasseskabeloner , men verificerbare uden behov for instansiering), deres bredde- og dybdearv (inklusive multiple ), idiomatisk implementering af typeklasser (gennem signaturer - se det tilsvarende eksempel på brug af ML-modulsproget ), inline polymorfi , parametrisk polymorfi af rangerer over 1 (ved hjælp af såkaldte lokalt abstrakte typer , der implementerer eksistentielle typer ) og generaliserede algebraiske datatyper .

Historie

Udtrykket "polymorfi" kommer fra græsk. πολύς ("meget") og μορφή ("form, udseende, enhed").

Udtrykkene "specialiseret polymorfisme" og "parametrisk polymorfisme" nævnes første gang i 1967 i Christopher Stracheys forelæsningsnotater med titlen " Fundamentals of Programming Languages [ " [1] . I 1985 formaliserede Peter Wegner og Luca Cardelli indeslutningspolymorfi til modellering af subtyper og arv [10] [27] , selvom implementeringer af undertyper og arv dukkede op meget tidligere, i Simula -sproget i 1967 . Inklusionspolymorfi er baseret på begrænset kvantificering .

Notationen af ​​parametrisk polymorfi som en udvikling af λ-regningen (kaldet F-systemet ) blev formelt beskrevet af logikeren Jean-Yves Girard [50] [51] ( 1971 ), uafhængigt af ham blev et lignende system beskrevet. af datalogen John S. Reynolds [52] ( 1974 ).

Det første sprog, der udelukkende var baseret på den polymorfe λ-regning, var ML ( 1973 ); uafhængigt af ham blev parametriske typer implementeret i Clu ( 1974 ) [27] . Mange moderne sprog ( C++ , Java , C# , D og andre) giver parametriske typer i en form, der er mere eller mindre tæt på deres implementering i Clu.

I 1987 formaliserede Mitchel Wand inline polymorfisme og typeinferens for det [53] ; dette arbejde havde en enorm indflydelse på den efterfølgende udvikling af typesystemer . Samme år foreslog Philip Wadler og Stephen Blott typeklasser [ ⇨ ] at formalisere ad-hoc polymorfi . 

Se også

Noter

  1. ↑ 1 2 3 4 Strachey, 1967 .
  2. ↑ Cardelli, 1991 , s. 3.
  3. ↑ Pierce, 2012 , 22.7. Polymorfisme gennem let, s. 354.
  4. ↑ 1 2 Cardelli, 1985 , s. 6.
  5. ↑ 1 2 3 4 5 Wadler, 1988 , s. 1-2.
  6. ↑ Bjarne Stroustrup . C++ Ordliste (19. februar 2007). Arkiveret fra originalen den 29. juni 2018.
  7. ↑ Andrew W. Appel. En kritik af Standard ML . - Princeton University, 1992.
  8. ↑ Harper, 2012 , 20.1 System F, s. 172.
  9. ↑ Pierce, 2012 , 23.2 Varieties of polymorphism, s. 365.
  10. ↑ 1 2 3 Cardelli, 1985 .
  11. ↑ Mitchell, 2002 , 6.4. Polymorfi og overbelastning, s. 145-151.
  12. ↑ Cardelli, 1985 , 1.3. Arts of Polymorphism, s. 6.
  13. ↑ 1 2 Cardelli, 1985 , s. 5-6.
  14. ↑ Cardelli, 1996 , 5 Second-order Type Systems, s. 25.
  15. ↑ Harper, 2012 , 20.3 Parametrisitetsoversigt, s. 177.
  16. ↑ Harper, 2012 , 49 Parametricity, s. 495-508.
  17. ↑ Pierce, 2012 , 23.9 Parametricity, s. 384-385.
  18. ↑ Harper, 2012 , 21.4 Representation Independence, s. 188.
  19. ↑ Pierce, 2012 , 30.5 Going Further: Dependent Types, s. 489-493.
  20. ↑ Reynolds, 1998 , 16. Undertyper og skæringstyper. Bibliografiske noter, s. 376.
  21. ↑ Cardelli, 1985 .
  22. ↑ Mitchell, 2002 , 10.2.6 Inheritance Is Not Subtyping, s. 287.
  23. ↑ Cardelli, 1991 .
  24. ↑ 1 2 Pierce, 2012 , 15 undertyper, s. 193.
  25. ↑ 1 2 Pierce, 2012 , 15. Undertyper, s. 193.
  26. ↑ Harper, 2012 , 23.1. Subsumtion, s. 208.
  27. ↑ 1 2 3 Pierce, 2012 , 1.4 Kort historie, s. 11-13.
  28. ↑ Cardelli, 1991 , 6. Power kinds, s. 32.
  29. ↑ 1 2 3 4 Abadi, Cardelli, 1994 .
  30. ↑ 1 2 3 Cardelli, 1985 , 6. Bounded Quantification, s. 28.
  31. ↑ Minsky oversat af DMK, 2014 , Subtyping, s. 259.
  32. ↑ Cardelli, 1985 , s. 9.
  33. ↑ Harper, 2012 , kapitel 16. Rekursive typer, s. 132.
  34. ↑ 1 2 Cardelli, 1991 , s. 35-37.
  35. ↑ Cardelli, 1985 , 2.3. Grundtyper, strukturerede typer og rekursion, s. 12-14.
  36. ↑ Harper, 2012 , kapitel 25. Dynamic Dispatch, s. 229.
  37. ↑ 1 2 Joyner, 1996 , 3.38 Signature Variance, s. 35.
  38. ↑ Objektorienteret programmering i Standard ML . Hentet 11. marts 2016. Arkiveret fra originalen 14. januar 2016.
  39. ↑ Minsky oversat af DMK, 2014 , kapitel 11. Objekter, s. 253.
  40. ↑ ML2000-arbejdsgruppen. Principper og et foreløbigt design for ML2000 . – 1999.
  41. ↑ Castagna, Ghelli, Longo. En beregning for overbelastede funktioner med subtyping  // Information and Computation. - Akademisk presse, 1995. - T. 117 , no. 1 . - S. 115-135 . - doi : 10.1006/inco.1995.1033 .
  42. ↑ Joyner, 1996 , 2.8 Encapsulation, s. otte.
  43. ↑ Mitchell, 2002 , 6.2.1 Type Safety, s. 132-133.
  44. ↑ Harper, 2012 , kapitel 4. Statik, s. 35.
  45. ↑ Pierce, 2012 , 31. Subtyper af højere orden, s. 495.
  46. ↑ 12 Wadler , 1988 , s. 3.
  47. ↑ Johan Jeuring. Polytypisk mønstertilpasning  // FPCA. - 1995. - doi : 10.1.1.36.5645 .
  48. ↑ Ralf Lammel og Joost Visser, "Typed Combinators for Generic Traversal", i Practical Aspects of Declarative Languages: 4th International Symposium (2002), s. 153.
  49. ↑ Patrik Jansson, Johan Jeuring. PolyP - En polytypisk programmeringssprogudvidelse . — Sigplan SPPL, 1997.
  50. ↑ Girard - Extension of Type Theory, 1971 .
  51. ↑ Girard - Higher-orders calculus, 1972 .
  52. ↑ Reynolds, 1974 .
  53. ↑ Wand, 1987 .

Litteratur

  • Christopher Strachey. Grundlæggende begreber i  programmeringssprog . - 1967. Arkiveret 12. august 2017.
    • Genudgivet: Christopher Strachey. Grundlæggende begreber i programmeringssprog  // Højere orden og symbolsk beregning  . - 2000. - Vol. 13 . - S. 11-49 . - doi : 10.1023/A:1010000313106 .
  • 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  (fransk)  // Proceedings of the Second Scandinavian Logic Symposium. - Amsterdam, 1971. - S. 63-92 . - doi : 10.1016/S0049-237X(08)70843-7 .
  • Jean-Yves Girard. Fortolkning fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur  (fransk) . — Université Paris 7, 1972.
  • John C. Reynolds. Towards a Theory of Type Structure // Lecture Notes in Computer Science . - Paris: Colloque sur la programmation, 1974. - Vol. 19 . - S. 408-425 . - doi : 10.1007/3-540-06859-7_148 .
  • Luca Cardelli , Peter Wegner. Om forståelse af typer, dataabstraktion og polymorfi //ACM Computing Surveys. - New York, USA:ACM, 1985. -17,nr. 4. -S. 471-523. —ISSN 0360-0300. -doi:10.1145/6041.6042.
  • Robert Harper . Introduktion til Standard ML. - Carnegie Mellon University, 1986. - ISBN PA 15213-3891.
  • Oversættelse til russisk: Robert Harper . Introduktion til Standard ML. - Carnegie Mellon University, 1986. - 97 s. — ISBN PA 15213-3891.
  • Mitchell Wand . Komplet typeslutning for simple objekter // In Proc. 2. IEEE-symposium om logik i datalogi. - 1987. -S. 37-44.
  • Philip Wadler, Stephen Blott. Hvordan man gør ad-hoc polymorfi mindre ad hoc  . - 1988.
  • Luca Cardelli . Typisk programmering // IFIP state-of-the-art rapporter. - New York: Springer-Verlag, 1991. -Iss. Formel beskrivelse af programmeringskoncepter. -S. 431-507.
  • Martin Abadi, Luca Cardelli . En semantik af objekttyper  . — LICS , 1994.
  • Luca Cardelli . Typesystemer (engelsk) // Handbook of Computer Science and Engineering. — CRC Press, 1996.
  • John C. Reynolds. Teorier om programmeringssprog . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (hardback), 978-0-521-10697-9 (paperback).
  • Benjamin Pierce. Typer og programmeringssprog  . - MIT Press , 2002. - ISBN 0-262-16209-1 .
    • Oversættelse til russisk: Benjamin Pierce. Typer i programmeringssprog . - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .
  • John C. Mitchell Begreber i programmeringssprog  . - Cambridge University Press, 2002. - 540 s. - ISBN 978-0-521-78098-8 .
  • Minsky, Madhavapeddy, Hickey. Real World OCaml: Funktionel programmering for  masserne . - O'Reilly Media, 2013. - 510 s. — ISBN 9781449324766 .
    • Oversættelse til russisk: Minsky, Madhavapeddy, Hickey. Programmering i Ocaml-sproget . - DMK, 2014. - 536 s. — (Funktionel programmering). - ISBN 978-5-97060-102-0 .