Parametrisk polymorfi

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 12. april 2021; checks kræver 5 redigeringer .

Parametrisk polymorfi i programmeringssprog og typeteori er en egenskab ved semantikken i et typesystem, der giver dig mulighed for at behandle værdier af forskellige typer på en identisk måde, det vil sige fysisk at udføre den samme kode for data af forskellige typer [1] [2] .

Parametrisk polymorfi betragtes som den "sande" form for polymorfi [3] , hvilket gør sproget mere udtryksfuldt og i høj grad stigende kodegenbrug . Traditionelt er det i modsætning til ad-hoc-polymorfi [1] , som giver en enkelt grænseflade til potentielt forskellig kode for forskellige typer tilladt i en given kontekst, potentielt inkompatibel ( statisk eller dynamisk ). I en række beregninger, såsom teorien om kvalificerede typer , behandles ad-hoc polymorfi som et særligt tilfælde af parametrisk polymorfi.

Parametrisk polymorfi ligger til grund for typesystemerne af sprog i ML -familien ; sådanne typesystemer kaldes polymorfe. I sprogsamfund med ikke-polymorfe typesystemer (efterkommere af Algol og BCPL [4] ), kaldes parametrisk polymorfe funktioner og typer " generaliserede ".

Indtast polymorfi

Udtrykket " parametrisk polymorfi " bruges traditionelt til at henvise til typesikker parametrisk polymorfi, selvom der også findes utypede former for den (se parametrisk polymorfi i C og C++ ) [4] . Nøglekonceptet for typesikker parametrisk polymorfi, ud over den polymorfe funktion , er den polymorfe type .

En polymorf type ( eng. polymorphic type ), eller en polytype ( eng. polytype ) er en type parametriseret af en anden type. En parameter i typelaget kaldes en typevariabel (eller typevariabel) .

Formelt studeres type polymorfi i den polymorfisk type lambdaregning , kaldet System F.

For eksempel kan en funktion, der appendsammenkæder to lister til én, bygges uanset typen af listeelementer. Lad typevariablen a beskrive typen af listeelementerne. Derefter kan funktionen appendskrives som " forall a. [a] × [a] -> [a]" (her [a]betyder konstruktionen typen " en liste, hvor hvert element har en typea " - den syntaks, der er adopteret i Haskell-sproget ). I dette tilfælde siges typen at være parametriseret af en variabel afor alle værdier a. På hvert anvendelsessted til specifikke argumenter opløses appendværdien , og hver omtale af den i typesignaturen erstattes med en værdi, der svarer til anvendelseskonteksten. I dette tilfælde kræver funktionstypesignaturen , at elementtyperne for begge lister og resultatet er identiske .a

Sættet af gyldige værdier for en typevariabel er givet ved kvantificering . De enkleste kvantificerere er universelle (som i eksemplet med append) og eksistentielle (se nedenfor).

En kvalificeret type er en polymorf type, der desuden er udstyret med et sæt prædikater , der regulerer rækken af gyldige værdier for en parameter af denne type. Med andre ord giver typekvalificering dig mulighed for at kontrollere kvantificeringen på en vilkårlig måde. Teorien om kvalificerede typer blev bygget af Mark P. Jones i 1992 [5] . Det giver en fælles begrundelse for de mest eksotiske typesystemer, herunder typeklasser , udvidelige notationerog subtyper , og tillader specifikke begrænsninger at blive præcist formuleret for specifikke polymorfe typer, og dermed etablere forholdet mellem parametriske og ad-hoc polymorfi ( overbelastning ), og mellem eksplicit og implicit overbelastning. Sammenhængen af en type med et prædikat idenne teori kaldes bevis . En algebra svarende til lambda-regningen er formuleret til beviser , herunder abstraktion af beviser, anvendelse af beviser osv. At korrelere et led i denne algebra med en eksplicit overbelastet funktion kaldes bevisoversættelse .

Motiverende eksempler for udviklingen af en generaliseret teori var Wadler-Blott-typeklasserne og indtastningen af udvidelige optegnelser gennem Harper-Pearce-prædikater [5] [6] .

Klassificering af polymorfe systemer

Parametrisk polymorfe type systemer er grundlæggende klassificeret i henhold til rang og prædikative egenskab . Derudover skelnes der mellem eksplicit og implicit polymorfi [7] og en række andre egenskaber. Implicit polymorfi er tilvejebragt gennem typeinferens , som i høj grad forbedrer brugervenligheden, men har begrænset udtryksevne. Mange praktiske parametrisk polymorfe sprog adskiller faserne af et eksternt implicit skrevet sprog og et internt eksplicit skrevet sprog .

Den mest generelle form for polymorfisme er " højere rangerende impredikativ polymorfi ". De mest populære restriktioner for denne form er rang 1 polymorfi kaldet " prenex " og den prædikative polymorfi . Sammen danner de " prædikativ prenex polymorfisme " svarende til den implementeret i ML og tidligere versioner af Haskell .

Efterhånden som typesystemer bliver mere komplekse, bliver typesignaturer så komplekse, at deres fuldstændige eller næsten fuldstændige udledning af mange forskere betragtes som en kritisk egenskab, hvis fravær vil gøre sproget uegnet til praksis [8] [9] . For en traditionel kombinator har den fulde typesignatur map (under hensyntagen til generisk kvantificering) under typesikker undtagelsesflowsporing følgende form [10] [8] (som ovenfor betyder en liste over elementer af type ):[a]a
$val\;map\colon \forall \alpha \colon \star _{\cdot }\forall \beta \colon \star _{\cdot }\forall \gamma \colon \emptyset _{\cdot }\forall \delta \colon \emptyset _{\cdot }(\;\alpha {\xrightarrow {\gamma }}\beta \;)\;{\xrightarrow {\delta }}\;(\;\venstre[\alpha \ højre]{\xrightarrow {\gamma }}\left[\beta \right]\;)$

Ranger

Rangen af polymorfi viserindlejringsdybden af kvantifikatorer af typevariabler tilladt inden for systemets rammer . " Polymorfi af rang k " (for k > 1 ) giver dig mulighed for at specificere typevariable ved polymorfe typer med rang, der ikke er højere end ( k - 1) . " Polymorfisme af højere rækker " giver dig mulighed for at sætte kvantificerere af typevariabler til venstre for et vilkårligt antal pile i typer af højere orden .

Joe Wells beviste [ 11 ] at typeinferens for et Curry - typet System F ikke kan afgøres for rangeringer over 2, så eksplicit type annotation skal bruges ved brug af højere rangeringer [12] .

Der er partielle inferentielle typesystemer , der kun kræver, at ikke-afledbare typevariable skal annoteres [13] [14] [15] .

Prenex polymorfisme

Polymorfi af rang 1 kaldes ofte prenex polymorfi (fra ordet "prenex" - se prenex normalform ). I et prenex polymorfisk system kan typevariabler ikke instansieres af polymorfe typer. Denne begrænsning gør skelnen mellem monomorfe og polymorfe typer væsentlig, hvorfor polymorfe typer i prenex-systemet ofte kaldes "typeskemaer " ( engelsk typeskemaer ) for at skelne dem fra "almindelige" (monomorfe) typer (monotyper). Som en konsekvens kan alle typer skrives på formen, når alle typevariable kvantifikatorer er placeret i den yderste (prenex) position, hvilket kaldes prenex normalform . Enkelt sagt er polymorfe funktionsdefinitioner tilladt, men polymorfe funktioner kan ikke videregives som argumenter til andre funktioner [16] [17] - polymorfisk definerede funktioner skal monotype instansieres før brug.

En tæt ækvivalent er den såkaldte " Lad-polymorphism " eller " ML - style polymorphism " af Damas-Milner. Teknisk set har Let-polymorphism i ML yderligere syntaktiske begrænsninger, såsom " værdibegrænsningen " forbundet med typesikkerhedsproblemer ved brug af referencer (som ikke forekommer i rene sprog som Haskell og Clean ) [18] [19] .

Prædikativitet

Prædikativ polymorfi

Prædikativ (betinget) polymorfi kræver, at en typevariabel instansieres med en monotype (ikke en polytype).

Prædikative systemer omfatter intuitionistisk typeteori og Nuprl .

Impredikativ polymorfi

Impredikativ (ubetinget) polymorfi giver dig mulighed for at instansiere en typevariabel med en vilkårlig type - både monomorf og polymorf, inklusive den type, der defineres. (At tillade et system rekursivt at inkludere sig selv i sig selv i en calculus kaldes impredicativity . Potentielt kan dette føre til paradokser som Russell eller Cantor [20] , men dette sker ikke i tilfælde af et kompliceret typesystem [21] .)

Impredikativ polymorfi giver dig mulighed for at overføre polymorfe funktioner til andre funktioner som parametre, returnere dem som et resultat, gemme dem i datastrukturer osv., hvorfor det også kaldes førsteklasses polymorfi . Dette er den mest kraftfulde form for polymorfi, men udgør på den anden side et alvorligt problem for optimering og gør typeinferens uløselig .

Et eksempel på et impredikativt system er System F og dets udvidelser (se lambda-terning ) [22] .

Rekursionsstøtte

Traditionelt kan en funktion i efterkommere af ML kun være polymorf, når den ses "udefra" (det vil sige, den kan anvendes på argumenter af forskellige typer), men dens definition kan kun indeholde monomorf rekursion (det vil sige, typeopløsning er gjort før opkaldet). Udvidelse af ML type rekonstruktion til rekursive typer giver ingen alvorlige vanskeligheder. På den anden side skaber kombinationen af typerekonstruktion med rekursivt definerede termer et vanskeligt problem kendt som polymorf rekursion . Mycroft og Meertens foreslog en polymorf skriveregel, der tillader rekursive kald til en rekursiv funktion fra sin egen krop at blive instansieret med forskellige typer. I denne calculus, kendt som Milner-Mycroft calculus, er typeinferens uafgørlig . [23]

Strukturel type polymorfi

Produkttyper (også kendt som " poster ") tjener som det formelle grundlag for objektorienteret og modulær programmering. Deres dobbelte par består af sumtyper (også kendt som " varianter ") [24] [25] [19] :

\neg \lbrace a\land b\rbrace =\langle \neg a\lor \neg b\rangle

\neg \langle a\lor b\rangle =\lbrace \neg a\land \neg b\rbrace

Sammen er de et middel til at udtrykke alle komplekse datastrukturer og nogle aspekter af programmers adfærd .

Record calculi er et generaliseret navn for problemet og en række af dets løsninger vedrørende fleksibiliteten af produkttyper i programmeringssprog under betingelse af typesikkerhed [26] [27] [28] . Udtrykket strækker sig ofte til sumtyper, og grænserne for begrebet " optegnelsestype " kan variere fra beregning til beregning (såvel som selve begrebet " type "). Udtrykkene " registrer polymorfi " (som igen ofte inkluderer variant polymorfi ) [27] , " modulus calculus " [9] og " strukturel polymorfi " bruges også.

Generel information

Typeprodukter og summer ( poster og varianter [ da ] giver fleksibilitet til at konstruere komplekse datastrukturer, men begrænsningerne i mange systemer af den virkelige type forhindrer ofte deres brug i at være virkelig fleksibel. Disse begrænsninger opstår normalt på grund af problemer med effektivitet, typeslutning eller blot brugervenlighed. [29]

Det klassiske eksempel er Standard ML , hvis typesystem var bevidst begrænset nok til at kombinere let implementering med udtryksfuldhed og matematisk bevisbar typesikkerhed .

Eksempel på postdefinition :

> val r = { navn = "Foo" , brugt = sand }; (* val r: {navn: streng, brugt: bool} = {navn = "Foo", brugt = sand} *)

Adgang til feltværdien ved dens navn udføres af en præfikskonstruktion af formen #field record:

> val r1 = #navn r ; (* val r1 : string = "Foo" *)

Følgende funktionsdefinition over posten er korrekt:

> sjovt navn1 ( x : { navn : streng , alder : int }) = #navn x

Og følgende genererer en compiler fejl, at typen ikke er fuldt løst :

> sjovt navn2 x = #navn x (* uafklaret type i erklæringen: {navn : '1, ...} *)

Optegnelsernes monomorfi gør dem ufleksible, men effektive [30] : da den faktiske hukommelsesplacering af hvert postfelt er kendt på forhånd (på kompileringstidspunktet), kompileres ved at henvise til det ved navn til direkte indeksering, som normalt beregnes i én maskine instruktion. Men når man udvikler komplekse skalerbare systemer, er det ønskeligt at kunne abstrahere felter fra specifikke poster - for eksempel at definere en universel feltvælger:

sjovt vælg r l = #l r

Men at kompilere polymorf adgang til felter, der kan være i forskellig rækkefølge i forskellige poster, er et vanskeligt problem, både ud fra et synspunkt om sikkerhedskontrol af operationer på sprogniveau og ud fra et synspunkt om ydeevne på maskinkodeniveau. 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. [31]

Typesummer danner grundlaget for grenudtrykket , og på grund af typesystemets strenghed giver compileren kontrol over fuldstændigheden af parsingen. For eksempel for følgende sumtype :

datatype 'a foo = A af 'a | B af ( 'a * 'a ) | C

enhver funktion over det vil se ud

fun bar ( p : 'a foo ) = kasus p af A x => ... | B ( x , y ) => ... | c => ...

og når nogen af klausulerne fjernes, vil compileren udstede en advarsel om ufuldstændig parse (" match nonexhaustive"). For de tilfælde, hvor kun få af de mange muligheder kræver analyse i en given sammenhæng, er det muligt at tilrettelægge default-forgrening ved hjælp af den såkaldte. "Joker" - en universel prøve, som alle gyldige (i henhold til indtastning) værdier er sammenlignelige. Det er skrevet med en understregning (" _"). For eksempel:

sjov bar ( p : 'a foo ) = kasus p af C => ... | _ => ...

På nogle sprog (i Standard ML , i Haskell ) er selv den "simpelere" konstruktion if-then-elseblot syntaktisk sukker over et særligt tilfælde af forgrening , dvs. udtrykket

hvis A så B ellers C

allerede på stadiet af grammatisk analyse præsenteres i skemaet

tilfælde A af sand => B | falsk => C

eller

tilfælde A af sand => B | _ => C

Syntaktisk sukker

I Standard ML er poster og varianter monomorfe, dog understøttes syntaktisk sukker til håndtering af poster med flere felter, kaldet det " universelle mønster " [32] :

> val r = { navn = "Foo" , brugt = sand }; (* val r : {navn : streng, brugt : bool} = {navn = "Foo", brugt = sand} *) > val { brugt = u , ...} = r ; (* val u : bool = sand *)

En ellipse af {used, ...}typen " " betyder, at der findes andre felter i denne post, ud over de nævnte. Der er dog ingen postpolymorfi som sådan (ikke engang prænexet ): fuld statisk opløsning af den monomorfe posttypeinformation (via inferens eller eksplicit annotation ) er påkrævet.

Udvidelse og funktionel opdatering af poster

Udtrykket udvidelige optegnelser bruges til en generaliseret betegnelse af sådanne operationer som udvidelse (opbygning af en ny post baseret på en eksisterende med tilføjelse af nye felter), skæring (tager en specificeret del fra en eksisterende post) osv. Især, det indebærer muligheden for den såkaldte " funktionel postopdatering " ( funktionel postopdatering ) - operationen med at konstruere en ny postværdi baseret på den eksisterende ved at kopiere navnene og typerne af dens felter, hvor et eller flere felter i den nye rekord modtager nye værdier, der adskiller sig fra de originale (og muligvis har en anden type). [33] [34] [19] [35] [36] [37]

I sig selv er funktionelle opdaterings- og udvidelsesoperationer ortogonale til at registrere polymorfi, men deres polymorfe anvendelse er af særlig interesse. Selv for monomorfe poster bliver det vigtigt at kunne undlade eksplicit omtale af felter, der kopieres uændret, og dette repræsenterer faktisk postpolymorfi i den rent syntaktiske form . På den anden side, hvis vi betragter alle poster i systemet som udvidelige, så tillader dette funktioner på poster at blive skrevet som polymorfe.

Et eksempel på den enkleste designvariant er implementeret i Alice ML (i henhold til de nuværende efterfølgere ML -konventioner ) [36] . Det universelle mønster (ellipsis ) har udvidede muligheder: det kan bruges til at "fange en række" for at arbejde med den "resterende" del af posten som en værdi:

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

Den funktionelle opdatering er implementeret som en afledning af at fange en række med et serviceord where. For eksempel følgende kode:

> lad val r = { a = 1 , c = 3,0 , d = "ikke en liste" , f = [ 1 ], p = [ "ikke en streng" ], z = INGEN } i { r hvor d = nul , p = "hej" } ende

vil automatisk blive omskrevet i formen:

> lad val r = { a = 1 , c = 3,0 , d = "ikke en liste" , f = [ 1 ], p = [ "ikke en streng" ], z = INGEN } val { d = _, p = _, ... = tmp } = r i { ... = tmp , d = nul , p = "hej" } ende

Optag sammenkædning

En af de første (slutningen af 1980'erne - begyndelsen af 1990'erne ) foreslog forskellige muligheder for formalisering af udvidelige optegnelser gennem sammenkædningsoperationer på ikke-polymorfe optegnelser (Harper-Pearce [38] , Wand [39] , Salzmann [40] ). Cardelli brugte endda pladeoperationer i stedet for polymorfi på det ravnære sprog. Der er ingen kendt måde at kompilere disse beregninger effektivt; derudover er disse beregninger meget komplekse set ud fra en typeteoretisk analyse. [27] [41] [42] [43]

For eksempel [33] :

val bil = { navn = "Toyota" ; alder = "gammel" ; id = 6678 } val lastbil = { navn = "Toyota" ; id = 19823235 } ... val repaired_truck = { bil og lastbil }

rækkepolymorfismen ) viste, at multipel nedarvning kan modelleres gennem rekordsammenkædning [39] [33] .

Strukturel undertypebestemmelse af Cardelli

Luca Cardelli undersøgte muligheden for at formalisere " optegnelsespolymorfi " gennem subtypeforhold på poster: For at gøre dette behandles en post som en "universel undertype", det vil sige, at dens værdi får lov til at henvise til hele sættet af dens supertyper. Denne tilgang understøtter også metodearv og fungerer som et typeteoretisk fundament for de mest almindelige former for objektorienteret programmering . [27] [44] [45]

Cardelli præsenterede en variation af metoden til at kompilere rekordpolymorfi på tværs af deres undertyper ved at foruddefinere offset af alle mulige etiketter i en potentielt enorm struktur med mange tomme slots [31] .

Metoden har betydelige ulemper. Understøttelse af undertypebestemmelse i typesystemet komplicerer i høj grad mekanismen til kontrol af typekonsistens [46] . Derudover ophører den statiske type af udtrykket i sin tilstedeværelse med at give fuldstændig information om den dynamiske struktur af værdien af posten . For eksempel, når du kun bruger undertyper, er følgende udtryk:

> hvis sandt, så er { A = 1 , B = sand } ellers { B = falsk , C = "Kat" } (* val det : {B : bool} *)

har type {B : bool}, men dens dynamiske værdi er lig med {A = 1, B = true}, dvs. information om typen af den udvidede post går tabt [43] , hvilket er et alvorligt problem for kontrol af operationer, der kræver fuldstændig information om værdistrukturen for deres udførelse (som f.eks. sammenligning for ligestilling ) [19] . Endelig, i tilstedeværelsen af undertyper, påvirker valget mellem ordnet og uordnet repræsentation af poster alvorligt ydeevnen [47] .

Populariteten af subtyping skyldes, at det giver enkle og visuelle løsninger på mange problemer. For eksempel kan objekter af forskellige typer placeres på en enkelt liste, hvis de har en fælles supertype [48] .

Wanda række polymorfi

Mitchell Wand foreslog i 1987 ideen om(ikke eksplicit specificeret) del af posten gennem det, han kaldte en rækketypevariabel ( rækketypevariabel ) [49] .

En rækkevariabel er en variabel af typen , der løber gennem et sæt af endelige sæt (rækker) af indtastede felter (par af " (значение : тип)"). Resultatet er evnen til at implementere bredde-wide arv direkte oven på den parametriske polymorfi, der understøtter ML uden at komplicere typesystemet med undertyperegler Den resulterende form for polymorfi kaldes rækkepolymorfi . Inline polymorfi strækker sig til både produkter af typer og summer af typer .

Vand lånte udtrykket fra englænderne. række (række, kæde, linje) fra Algol-68 , hvor det betød et sæt visninger. I russisksproget litteratur er dette udtryk i forbindelse med Algol traditionelt blevet oversat som "multispecies". Der er også en oversættelse af "rækkevariabler" som "strengvariabler" [41] , hvilket kan forårsage forvirring med små bogstaver i strengtyper .

Eksempel ( OCaml -sprog ; postfix-syntaks, record#field) [50] :

# lad send_m a = a # m ;; (* værdi send_m : < m : a; .. > -> a = <sjov> *)

Her er ellipsen (af to prikker) OCamls accepterede syntaks for en unavngiven inline type variabel . På grund af sådan indtastning kan funktionen send_manvendes på et objekt af enhver (ikke tidligere kendt ) objekttype, som inkluderer en metode til den mtilsvarende signatur.

Typefradrag for Wanda-regningen i den originale version var ufuldstændig: på grund af manglen på restriktioner for udvidelsen af serien, vil tilføjelse af et felt, hvis navnet matcher, erstatte det eksisterende - som et resultat, har ikke alle programmer en hovedtype [6] [43] . Dette system var imidlertid det første konkrete forslag om at udvide ML med poster, der understøtter arv [51] . I de efterfølgende år blev der foreslået en række forskellige forbedringer, herunder dem, der gør det komplet [51] [27] .

Det mest bemærkelsesværdige spor blev efterladt af Didier Remy ( fransk: Didier Rémy ). Han byggede et praktisk typesystem med udvidelige optegnelser, inklusive en komplet og effektiv typerekonstruktionsalgoritme [52] [53] . Remy stratificerer typersproget i sorter , og formulerer en sorteret algebra af typer ( eng. sorteret algebra af typer, sorteret sprog af typer ). Der skelnes mellem den egentlige type typer (herunder felttyper) og typen af felter ; kortlægninger mellem dem indføres og på grundlag heraf formuleres reglerne for indtastning af udvidede poster som en simpel udvidelse af de klassiske ML- regler . Tilstedeværelsesoplysningerne for et felt er defineret som en tilknytning fra en typesortering til en feltsortering . Rækketypevariable omformuleres som variabler tilhørende feltsorteringen og lig med fraværskonstanten , som er et element i feltsorteringen , der ikke har et match i typesorteringen . En typeevalueringsoperation for en post med n felter er defineret som at kortlægge et n-ært felt til en type (hvor hvert felt i tuplen enten beregnes af tilstedeværelsesfunktionen eller givet af fraværskonstanten ).

På en forenklet måde kan ideen om kalkulation fortolkes som en udvidelse af typen af ethvert felt i posten med et tilstedeværelse / fravær flag og repræsentation af posten som en tuple med en plads for hvert muligt felt [6] . I implementeringsprototypen blev typesprogets syntaks gjort tættere på den typeteoretiske formulering, for eksempel [52] :

# lad bil = { navn = "Toyota" ; alder = "gammel" ; id = 7866 } ;; (* bil : ∏ (navn : pre (streng); id : pre (num); alder : pre (streng); abs) *) # lad lastbil = { name = "Blazer" ; id = 6587867567 } ;; (* lastbil : ∏ (navn : pre (streng); id : pre (num); abs) *) # lad person = { navn = "Tim" ; alder = 31 ; id = 5656787 } ;; (* person : ∏ (navn : pre (streng); id : pre (num); alder : pre (num); abs) *)

(symbolet ∏i Remy betyder typeberegningsoperationen)

Tilføjelse af et nyt felt skrives ved hjælp af konstruktionen with:

# lad chauffør = { person med køretøj = bil } ;; (* fører : ∏ (køretøj : pre (∏ (navn : pre (streng); id : pre (num); alder : pre (streng); abs)); navn : pre (streng); id : pre (num) ; alder: pre (antal); abs) *)

Funktionel opdatering er skrevet identisk, med den forskel, at omtale af et allerede eksisterende felt tilsidesætter det:

# lad truck_driver = { chauffør med køretøj = lastbil };; (* lastbilchauffør : ∏ (køretøj : pre (∏ (navn : pre (streng); id : pre (num); abs)); navn : pre (streng); id : pre (num); alder : pre (antal) ); abs) *)

Denne ordning formaliserer den nødvendige begrænsning for at kontrollere operationer på poster og udlede hovedtypen, men fører ikke til en åbenlys og effektiv implementering [6] [43] . Remy bruger hashing, hvilket er ret effektivt i gennemsnit, men øger runtime overhead selv for oprindeligt monomorfe programmer, og er dårligt egnet til poster med mange felter [31] .

Rémy fortsatte med at udforske brugen af inline polymorfi i forbindelse med data subtyping , og understregede, at disse er ortogonale begreber og viste, at optegnelser bliver mest udtryksfulde, når de bruges sammen [54] . På dette grundlag foreslog han sammen med Jérôme Vouillon en letvægts objektorienteret udvidelse til ML [55] . Denne udvidelse blev implementeret i Xavier Leroys sprog "Caml Special Light" , hvilket gjorde det til OCaml [56] . OCaml objektmodellen er tæt sammenflettet med brugen af strukturel subtyping og inline polymorfi [48] , hvorfor de nogle gange fejlagtigt identificeres. Inline produktpolymorfi i OCaml er kernen i typeslutningen ; subtyperelationer er ikke nødvendige i et understøttet sprog, men øger fleksibiliteten yderligere i praksis [55] [50] [48] . OKaml har en enklere og mere beskrivende syntaks for typeinformation.

Jacques Garrigue ( fr. Jacques Garrigue ) implementerede [25] et praktisk system af polymorfe summer . Han kombinerede Remi og Ohori's teoretiske arbejde og byggede et system, der kører i midten: information om tilstedeværelsen af tags i en post er repræsenteret ved hjælp af køn , og information om deres typer bruger inline-variabler. For at compileren kan skelne mellem polymorfe og monomorfe summer, bruger Garriga en speciel syntaks (backtick, præfikstag). Dette eliminerer behovet for en typedeklaration - du kan straks skrive funktioner på den, og compileren vil udsende en minimal liste af tags, efterhånden som disse funktioner er sammensat. Dette system blev en del af OCaml omkring 2000 , men ikke i stedet for , men ud over monomorfe summer , da de er noget mindre effektive, og på grund af manglende evne til at kontrollere fuldstændigheden af parsingen , gør det vanskeligt at finde fejl (i modsætning til Blooms løsning ). [25] [57]

Ulemperne ved Wands inline-polymorfi er implementeringens uindlysendehed (der er ingen enkelt systematisk måde at kompilere den på, hvert specifikt typesystem baseret på inline-variable har sin egen implementering) og det tvetydige forhold til teorien (der er ingen ensartet formulering til typekontrol og slutning , støtte til slutning blev løst separat og krævede eksperimenter med at pålægge forskellige restriktioner) [27] .

Gennemskinnelige Harper-Lilybridge summer

Den mest komplekse type poster er afhængige poster. Sådanne poster kan omfatte typer såvel som "almindelige" værdier (materialiserede typer, reified [9] ), og termerne og typerne i rækkefølgen i kroppen af posten kan bestemmes baseret på dem, der går forud for dem . Sådanne notationer svarer til de " svage summer " af afhængig typeteori , også kendt som " eksistentialer ", og tjener som den mest generelle begrundelse for systemer af moduler i programmeringssprog [58] [59] . Cardelli betragtede [60] typer lignende i egenskaber som en af hovedtyperne i fuld-type programmering (men kaldte dem " tuples ").

Robert Harper og Mark Lillibridge konstruerede [61 ] [59] den gennemskinnelige sumkalkulus forformelt at retfærdiggøre et højere-ordens førsteklasses modulsprog , det mest avancerede system af moduler kendt. Denne calculus er blandt andet brugt i Harper-Stone semantikken , som repræsenterer den typeteoretiske begrundelse for Standard ML .

Gennemsigtige summer generaliserer svage summer gennem etiketter og et sæt ligheder, der beskriver typekonstruktører . Udtrykket translucent betyder , at en posttype kan indeholde både typer med en eksplicit eksporteret struktur, såvel som helt abstrakte . Laget af slægter i calculus har en simpel klassisk sammensætning: kønnet af alle typer og de funktionelle slægter af arten skelnes , typetypekonstruktører ( ML understøtter ikke polymorfi i højere slægter , alle typevariable hører til slægten , og abstraktionen af typekonstruktører er kun mulig gennem funktorer [62] ). Regnestykket skelner mellem undertypningsregler for henholdsvis poster som grundlæggende typer og for felter af poster som deres bestanddele, idet man tager "undertyper" og "underfelter" i betragtning, mens sløring af (abstraherende) feltsignaturer er et separat begreb fra subtypning. Subtyping her formaliserer kortlægningen af moduler til grænseflader . [61] [9] $\star$ ${\displaystyle k_{1}=>k_{2))$ $\star$

Harper-Lilybridge-regningen kan ikke afgøres , selv med hensyn til kontrol af typekonsistens ( modulsprogsdialekter implementeret i Standard ML og OCaml bruger begrænsede delmængder af denne beregning). Senere byggede Andreas Rossberg , baseret på deres ideer, imidlertid " 1ML "-sproget, hvori de traditionelle kerneniveauregistreringer af sprog- og modulniveaustrukturerne er den samme førsteklasses konstruktion [9] (betydeligt mere udtryksfuld end Cardelli's - se kritik af ML-modulsproget ). Ved at inkorporere ideen fra Harper og Mitchell [63] om at opdele alle typer i universer af "små" og "store" typer (forenklet svarer dette til den grundlæggende opdeling af typer i simple og aggregerede typer, med ulige typningsregler), sørgede Rossberg for løselighed , ikke kun konsistenstjek , men næsten fuldstændig typeslutning . Desuden tillader 1ML impredikativ polymorfi [64] . Samtidig er det interne sprog i 1ML baseret på det flade System F ω og kræver ikke brug af afhængige typer som metateori. Fra 2015 lod Rossberg muligheden for at tilføje inline polymorfi til 1ML stå åben , idet han kun bemærkede, at dette skulle give mere fuldstændig typeslutning [9] . Et år senere tilføjede han [65] effekterne polymorfisme til 1ML .

Polymorf beregning af Ohori-poster

Atsushi Ohori foreslog sammen med sin vejleder Peter Buneman i 1988 ideen om at begrænse rækken af mulige værdier for almindelige typevariabler i selve den polymorfe typning af poster . Senere formaliserede Ohori denne idé gennem notationsslægterne , efter at have bygget i 1995 en fuldgyldig kalkulus og en metode til dens effektive kompilering [19] [30] . Implementeringsprototypen blev skabt i 1992 som en udvidelse af SML/NJ [66] compileren, derefter ledede Ohori udviklingen af sin egen SML# compiler, som implementerer Standard ML dialekten af samme navn . I SML# tjener rekordpolymorfi som grundlaget for problemfri indlejring af SQL - konstruktioner i SML - programmer . SML# bruges af store japanske virksomheder til at løse forretningsproblemer forbundet med højbelastede databaser [67] . Et eksempel på en sådan session ( REPL ) [68] :

sjovt velhavende { Løn = s , ... } = s > 100000 ; (* val velhavende = fn : 'a#{ Løn:int, ... } -> bool *) sjov ung x = #Alder x < 24 ; (* val young = fn : 'a#{ Alder:int, ... } -> bool *) sjov youngAndWealthy x = velhavende x og også ung x ; (* val youngAndWealthy = fn : 'a#{ Alder:int, Løn:int, ... } -> bool *) sjovt vælg display l pred = fold ( fn ( x , y ) => if pred x then ( display x ) :: y else y ) l nul ; (* val select = fn : ('a -> 'b) -> 'en liste -> ('a -> bool) -> 'b liste *) sjov youngAndWealthyEmployees l = vælg #Navn l youngAndWealthy ; (* val youngAndWealthyEmployees = fn : 'b#{ Alder:int, Navn:'a, Løn:int, ... } liste -> 'en liste *)

Ohori kaldte sin calculus for " rekordpolymorfisme " ( engelsk rekordpolymorfisme ) eller " polymorphic record calculus " ( engelsk polymorphic record calculus ), og understregede samtidig, at han ligesom Wand betragter polymorfi ikke kun af produkttyper , men også af typer- summer [27] .

Ohori-regningen er kendetegnet ved den mest intensive brug af slægtslaget [6] . I indgangen (referencetype til slægt ), betyder symbolet enten slægten af alle typer ; eller postslægten , som har formen , der angiver sættet af alle poster, der mindst indeholder de specificerede felter; eller en variantslægt med den form, der angiver sættet af alle varianttyper , der mindst indeholder de specificerede konstruktører . I sprogets flade syntaks er en typebegrænsning til en form for notation skrevet som (se eksempler ovenfor). Løsningen ligner lidt den begrænsede kvantificering Cardelli-Wegner [27] . $t\colon \colon k$ $t$ $k$ $k$ $U$ ${\displaystyle \left\{\left\{l_{1}\colon t_{1},\dots ,l_{n}\colon t_{n}\right\}\right\))$ $\left\langle \left\langle l_{1}:t_{1},\dots ,l_{n}\colon t_{n}\right\rangle \right\rangle$ t#{...}

Den eneste polymorfe operation, som denne beregning giver, er feltekstraktionsoperationen [69] . Men Ohori var den første til at introducere et simpelt og effektivt kompileringsskema for rekordpolymorfi [43] . Han kaldte det "realisationsberegningen" ( implementeringskalkulus ). En post er repræsenteret af en vektor ordnet leksikografisk efter feltnavnene på den originale post; adressering af et felt ved navn oversættes til et kald til en mellemfunktion, der returnerer nummeret på det givne felt i den givne vektor med det anmodede navn, og efterfølgende indeksering af vektoren med det beregnede positionsnummer. Funktionen kaldes kun ved instansiering af polymorfe termer, hvilket pålægger en minimal overhead på kørselstid ved brug af polymorfi og ikke pålægger nogen overhead, når der arbejdes med monomorfe typer. Metoden fungerer lige så godt med vilkårligt store indtastninger og varianter. Kalkulussen giver typeslutning og finder en stærk overensstemmelse med teorien ( generisk kvantificering er direkte relateret til den sædvanlige vektorindeksering ), idet den er en direkte forlængelse af Girard-Reynolds andenordens lambdaregning , som tillader forskellige velkendte egenskaber ved polymorfe typning, der skal overføres til registreringspolymorfi [31] .

I praksis er understøttelse af polymorfe varianter i SML# ikke blevet implementeret på grund af dets inkompatibilitet med Standard ML 's sumtypedefinitionsmekanisme (kræver syntaktisk adskillelse af summer og rekursive typer) [70] .

Ulempen ved Ohori-regningen er manglen på støtte til rekordudvidelse eller trunkeringsoperationer [27] [71] [43] .

Førsteklasses Guster-Jones-mærker

I teorien om kvalificerede typer beskrives udvidelige poster ved fraværet af et felt ( "mangler" prædikat ) og tilstedeværelsen af et felt ( "har" prædikat ) prædikater. Benedict Gaster ( Benedict R. Gaster ) sammen med forfatteren af teorien Mark Jones ( Mark P. Jones ) færdiggjorde den i form af udvidelige optegnelser til et praktisk typesystem af implicit maskinskrevne sprog, herunder definition af kompileringsmetoden [6] . De opfinder udtrykket førsteklasses etiketter for at understrege evnen til at abstrahere feltoperationer fra statisk kendte etiketter. Senere forsvarede Gaster sin afhandling [72] om det konstruerede system .

Gaster-Jones-regningen giver ikke fuld type-inferens . Derudover blev der på grund af afgørelighedsproblemer indført en kunstig begrænsning: et forbud mod tomme serier [73] . Sulzmann forsøgte at omformulere beregningen [40] , men det system, han byggede, kan ikke udvides til at understøtte polymorf rekordudvidelse og har ikke en universel effektiv kompileringsmetode [43] .

Daan Leijen tilføjede et rækkelighedsprædikat (eller rækkelighedsprædikat ) til Gaster-Jones-regningen og flyttede seriesproget til prædikatsproget - dette sikrede fuldstændig typeslutning og ophævede forbuddet mod tomme serier [74] . Når de er kompileret, konverteres optegnelserne til en leksikografisk ordnet tuple , og bevisoversættelse anvendes efter Gaster-Jones-skemaet. Layens system tillader udtryk for idiomer såsom meddelelser af højere orden (den mest kraftfulde form for objektorienteret programmering ) og førsteklasses grene .

Baseret på disse værker er udvidelser til Haskell-sproget [75] blevet implementeret .

Resultaterne af Gaster-Jones er meget tæt på Ohoris resultater , på trods af betydelige forskelle i typeteoretisk begrundelse, og den største fordel er støtten til rekordudvidelse og trunkeringsoperationer [6] . Ulempen ved calculus er, at den er afhængig af egenskaber af typesystemet, som ikke findes i de fleste programmeringssprog. Derudover er typeslutning for det et alvorligt problem, hvorfor forfatterne har pålagt yderligere begrænsninger. Og selvom Layen har elimineret mange af manglerne, er det ikke muligt at bruge -grenen [71]default

Kontrolkonstruktionspolymorfi

Med udviklingen af softwaresystemer kan antallet af optioner i sumtypen øges , og tilføjelse af hver option kræver, at der tilføjes en tilsvarende gren til hver funktion over denne type, selvom disse grene er identiske i forskellige funktioner. Kompleksiteten af at øge funktionaliteten i de fleste programmeringssprog afhænger således ikke-lineært af deklarative ændringer i kommissoriet. Dette mønster er kendt som udtryksproblemet . Et andet velkendt problem er håndtering af undtagelser : gennem årtiers forskning i typesystemer kunne alle sprog, der er klassificeret som typesikre , stadig forlades ved at kaste en ufanget undtagelse - for på trods af selve indtastningen af undtagelserne er mekanismen til at hæve og håndteringen af dem var ikke maskinskrevet. Mens værktøjer til at analysere strømmen af undtagelser er blevet bygget, har disse værktøjer altid været eksterne i forhold til sproget.

Matthias Blume , en kollega af Andrew Appel der arbejder på projektets efterfølger ML [76] ), hans kandidatstuderende Wonseok Chae og kollega Umut Acar løste begge problemer baseret på matematisk dualitet produkter og summer . Legemliggørelsen af deres ideer var sproget MLPolyR [71] [34] [77] , baseret på den enkleste delmængde af Standard ML og suppleret med flere niveauer af typesikkerhed [78] . Wonseok Chai forsvarede senere sin afhandling om disse præstationer [78] .

Løsningen er som følger. Ifølge dualitetsprincippet svarer introduktionsformen for et begreb til eliminationsformen for dets duale [71] . Således svarer elimineringsformen for summer (analyse af filialer) til den indledende form for poster. Dette tilskynder forgrening til at have de samme egenskaber, som allerede er tilgængelige for indtastninger - gør dem til førsteklasses objekter og tillad dem at blive udvidet.

For eksempel det enkleste udtryk sprogfortolker:

sjov eval e = tilfælde e af `Const i => i | `Plus (e1,e2) => eval e1 + eval e2

med introduktionen af førsteklasses byggeri caseskan omskrives som:

sjov eval e = match e med tilfælde `Const i => i | `Plus (e1,e2) => eval e1 + eval e2

hvorefter cases-blokken kan gengives:

fun eval_c eval = cases `Const i => i | `Plus (e1,e2) => eval e1 + eval e2 sjov eval e = match e med (eval_c eval)

Denne løsning tillader default-forgrening (i modsætning til Gaster-Jones calculus ), som er vigtig for sammensætningen af førsteklasses grene [34] . Færdiggørelse af sammensætningen af rækken udføres ved hjælp af ordet . nocases

fun const_c d = cases `Const i => i standard : d sjov plus_c eval d = tilfælde `Plus (e1,e2) => eval e1 + eval e2 standard : d sjov eval e = match e med const_c (plus_c eval nocases ) fun bind env v1 x v2 = hvis v1 = v2 så x else env v2 fun var_c env d = cases `Var v => env v default : d fun let_c eval env d = tilfælde `Lad (v,e,b) => eval (bind env v (eval env e)) b default : d fun eval_var env e = match e med const_c (plus_c (eval_var env) (var_c env (let_c eval_var env nocases )))

Som du kan se, kræver den nye kode, som skal tilføjes med den kvalitative komplikation af systemet, ikke at ændre den allerede skrevne kode (funktionerne const_cog plus_c"ved ingenting" om den efterfølgende tilføjelse af understøttelse af variabler og let-blokke til sprogtolken). Således er førsteklasses udvidelige tilfælde en grundlæggende løsning på -udtryksproblemet , hvilket giver mulighed for at tale om et udvideligt programmeringsparadigme [71] [78] . inline polymorphism , som allerede er understøttet i typesystemet, og i denne forstand er fordelen ved en sådan teknisk løsning dens konceptuelle enkelhed [ 34] .

Udvidelse af softwaresystemer kræver dog også kontrol over håndteringen af undtagelser , der kan kastes på vilkårlige indlejringsdybder. Og her proklamerer Bloom og kolleger et nyt type sikkerhedsslogan i udviklingen af Milners slogan : " Programmer, der består typekontrol , kaster ikke ubehandlede undtagelser ." Problemet er, at hvis funktionstypesignaturen indeholder information om de typer undtagelser, som denne funktion potentielt kan give, og denne information i signaturen for den beståede funktion skal være strengt konsistent med informationen om funktionsparameteren af højere orden (inklusive hvis dette er et tomt sæt ) - indtastning af undtagelseshåndteringsmekanismen kræver øjeblikkeligt polymorfi af typerne af undtagelserne selv - ellers ophører højere-ordens funktioner med at være polymorfe. Samtidig er undtagelser i et sikkert sprog en udvidelig sum [79] [80] [81] , det vil sige en varianttype, hvis konstruktører tilføjes efterhånden som programmet skrider frem. I overensstemmelse hermed betyder sikkerhed for undtagelsesstrømstype behovet for at understøtte sumtyper, der er både udvidelige og polymorfe. Her er løsningen igen inline polymorfi .

Ligesom Garriga -regningen , bruger MLPolyR en speciel syntaks for polymorfe summer (backtick, førende tag), og der er ikke behov for en præ-deklaration af sum-typen (det vil sige, at ovenstående kode er hele programmet, ikke et fragment). Fordelen er, at der ikke er noget problem med at analysere fuldstændighedskontrol: semantikken i MLPolyR defineres ved at konvertere til et bevist pålidelighed internt sprog , der hverken understøtter sumpolymorfi eller undtagelser (for ikke at nævne ufangede undtagelser), så behovet for dem sletning ved kompilering er i sig selv et bevis på pålidelighed. [34]

MLPolyR bruger en ikke-triviel kombination af flere calculi og to-trins oversættelse. Den bruger Remy -regningen til typededuktion og typematching , mens den samtidig bruger princippet om dualitet til at repræsentere summer som produkter, derefter oversætter sproget til et mellemliggende, eksplicit skrevet sprog med polymorfe optegnelser og derefter bruger Ohoris effektive kompileringsmetode . Med andre ord er Ohoris kompileringsmodel blevet generaliseret til at understøtte Remy-regningen [69] . På det typeteoretiske niveau introducerer Bloom flere nye syntaktiske notationer på én gang, så man kan nedskrive regler for indtastning af undtagelser og førsteklasses grene. MLPolyR type systemet giver fuld type inferens , så forfatterne opgav udviklingen af en flad syntaks til eksplicit at skrive typer og understøttelse af signaturer i modulsproget .

Leyen typesystemet introducerer også en variant af grenpolymorfi: en konstruktion kan repræsenteres som en højere ordens funktion , der modtager en indgang fra funktioner, som hver svarer til en bestemt gren af beregningen ( Haskells syntaks er egnet for denne ændring og kræver ikke revision). For eksempel: case

dataList a = nul :: { } | ulemper :: { hd :: a , tl :: List a } snoc xs r = case ( omvendt xs ) r sidste xs = snoc xs { nul = \ r -> _ | _ , ulemper = \ r -> r . hd }

Fordi poster i Layens system kan udvides, er brancheparsing fleksibel på niveauet af dynamiske beslutninger (såsom kædechecks eller brug af et associativt array ), men giver en meget mere effektiv implementering (variantetiketten svarer til en offset i posten). Standardforgreningsstøtten ( default) skal dog droppes i dette tilfælde, da et enkelt default-mønster ville matche flere felter (og dermed flere forskydninger). Leyen kalder denne konstruktion " førsteklasses mønstre " ( førsteklasses mønstre ).

Polymorfi hos højere køn

Højere -type polymorfi betyder abstraktion overorden type konstruktører , det vil sige type operatorer af formen

* -> * -> ... -> *

Understøttelse af denne funktion tager polymorfi til et højere niveau, hvilket giver abstraktion over både typer og typekonstruktører , ligesom funktioner af højere orden giver abstraktion over både værdier og andre funktioner. Polymorfi hos højere køn er en naturlig komponent i mange funktionelle programmeringssprog , herunder monader , folder og indlejrede sprog . [62] [82]

For eksempel [62] hvis du definerer følgende funktion ( Haskell language ):

når b m = hvis b , så returnerer m ellers ()

så vil følgende funktionelle type blive udledt for det :

når :: forall ( m :: * -> * ) . Monade m => Bool -> m () -> m ()

Signaturen m :: * -> *siger, at typevariablen m er en typevariabel, der tilhører en højere type ( engelsk højere-kind typevariabel ). Det betyder, at den abstraherer over typekonstruktører (i dette tilfælde unære , såsom Maybeeller []), som kan anvendes på konkrete typer, såsom Inteller (), for at konstruere nye typer.

På sprog, der understøtter fuldtypeabstraktion ( Standard ML , OCaml ), skal alle typevariabler være af en slægt * , ellers ville typesystemet være usikkert . Polymorfi i højere slægter er således tilvejebragt af selve abstraktionsmekanismen, kombineret med eksplicit annotering ved instansiering, hvilket er noget ubelejligt. En idiomatisk implementering af polymorfi i højere slægter er dog mulig uden at kræve eksplicit annotering - til dette bruges en teknik svarende til defunktionalisering på typeniveau . [62]

Generisk polymorfi

Kindsystemer sikrer selve typesystemernes sikkerhed ved attillade kontrol over betydningen af typeudtryk .

Lad det for eksempel være påkrævet at implementere i stedet for den sædvanlige type " vektor " (lineær array) familien af typer " længdevektorn ", med andre ord at definere typen " vektor indekseret efter længde ". Den klassiske Haskell- implementering ser sådan ud [83] :

data Nul data Succ n data Vec :: * -> * -> * hvor Nil :: Vec a Zero Cons :: a -> Vec a n -> Vec a ( Succ n )

Her defineres fantomtyper [84] først , det vil sige typer, der ikke har en dynamisk repræsentation. Konstruktørerne Zero og Succtjener som "typelagsværdier", og variablen nfremtvinger uligheden mellem de forskellige betontyper konstrueret af konstruktøren Succ. Typen Vecer defineret som en generaliseret algebraisk datatype (GADT).

Løsningen forudsætter betinget, at fantomtypen vil blive brugt til at modellere vektorens nheltalsparameter baseret på Peano-aksiomerne - det vil sige, at der kun bygges udtryk som , , osv. Men selvom definitionerne er skrevet i typesprog , de selv er formuleret utyperet måde. Dette kan ses af signaturen , hvilket betyder, at de betontyper, der er sendt som parametre, tilhører slægten , hvilket betyder, at de kan være en hvilken som helst betontype. Med andre ord er meningsløse typeudtryk som eller ikke forbudt her . [83]Succ ZeroSucc Succ ZeroSucc Succ Succ ZeroVec :: * -> * -> * *Succ BoolVec Zero Int

En mere avanceret beregning ville gøre det muligt at specificere området for typeparameteren mere præcist:

data Nat = Nul | Succ Nat data Vec :: * -> Nat -> * hvor VNil :: Vec a Zero VCons :: a -> Vec a n -> Vec a ( Succ n )

Men normalt er det kun højt specialiserede systemer med afhængige typer [85] implementeret i sprog som Agda , Coq og andre, der har en sådan udtryksevne. For eksempel, set fra Agda -sprogets synspunkt, ville indgangen Vec :: * -> Nat -> *betyde, at en types køn Vec afhænger af typen Nat(det vil sige, at et element af en art afhænger af et element af en anden, lavere slags ).

I 2012 blev der bygget en udvidelse til Haskell -sproget [83] , som implementerer et mere avanceret system af køn og gør ovenstående kode til korrekt Haskell-kode. Løsningen er, at alle typer (under visse begrænsninger) automatisk " promoveres " ( eng. promote ) til et højere niveau, og danner slægter af samme navn, som kan bruges eksplicit. Fra dette synspunkt er indgangen ikke afhængig - det betyder kun, at vektorens anden parameter skal tilhøre den navngivne slægt , og i dette tilfælde er det eneste element i denne slægt typen med samme navn. Vec :: * -> Nat -> *Nat

Løsningen er ret enkel, både hvad angår implementering i compileren og i forhold til praktisk tilgængelighed. Og da typepolymorfi i sagens natur er et naturligt element i Haskells semantik, fører typefremme til venlig polymorfi , som både øger kodegenbrug og giver et højere niveau af typesikkerhed . For eksempel bruges følgende GADT til at verificere typelighed:

data EqReﬂ a b hvor Reﬂ :: EqReﬂ a a

har et køn i klassisk Haskell * -> * -> *, hvilket forhindrer det i at blive brugt til at teste for lighed af typekonstruktører som f.eks Maybe. Et typefremstødsbaseret slægtssystem udleder en polymorf slægt forall X. X -> X -> *, hvilket gør typen EqReﬂmere generisk. Dette kan skrives eksplicit:

data EqReﬂ ( a :: X ) ( b :: X ) hvor Reﬂ :: for alt X . forall ( a :: X ) . EqReﬂ a a

Effekt polymorfi

Effektsystemer blev foreslået af Gifford og Lucassen i anden halvdel af 1980'erne [86] [87] [88] med det formål at isolere bivirkninger for bedre kontrol over sikkerhed og effektivitet i konkurrencepræget programmering .

I dette tilfælde betyder effektpolymorfi kvantificering over renheden af en specifik funktion, det vil sige inkluderingen af et flag i den funktionelle type , der karakteriserer funktionen som ren eller uren. Denne indtastningsudvidelse gør det muligt at abstrahere renheden af højere-ordens funktioner fra renheden af funktioner, der sendes til dem som argumenter.

Dette er af særlig betydning, når man flytter til funktioner over moduler ( registreringer , der inkluderer abstrakte typer ) - funktorer - fordi de under renhedsbetingelser har ret til at være anvendelige, men i nærvær af bivirkninger skal de generere for at sikre typesikkerhed (for mere om dette, se ækvivalens af typer i ML-modulsproget ). På sproget af højere-ordens førsteklasses moduler viser effektpolymorfi sig således at være et nødvendigt grundlag for at understøtte generativitetspolymorfi : at videregive et renhedsflag til en funktor giver et valg mellem applikativ og generativ semantik i et enkelt system. [65]

Support i programmeringssprog

Typesikker parametrisk polymorfi er tilgængelig på Hindley-Milner -typesprog - i ML - dialekter ( Standard ML , OCaml , Alice , F# ) og deres efterkommere ( Haskell , Clean , Idris , Mercury , Agda ) - også som i dem, der er arvet fra dem hybridsprog ( Scala , Nemerle ).

Generiske datatyper (generiske) adskiller sig fra parametrisk polymorfe systemer ved, at de bruger en begrænset kvantificering , og derfor ikke kan have en højere rang end 1 . De fås i Ada , Eiffel , Java , C# , D , Rust ; og også i Delphi siden 2009-versionen. De dukkede først op i CLU .

Intentionel polymorfi

Intentionel polymorfi er en teknik til at optimere kompilering af parametrisk polymorfi baseret på kompleks typeteoretisk analyse, som består i beregninger på typer under kørsel. Intentionel polymorfi giver mulighed for tagfri affaldsindsamling , unboxedoverførsel af argumenter til funktioner og boxed (hukommelsesoptimerede) flade datastrukturer. [89] [90] [91]

Monomorfisering

Monomorfisering er en teknik til at optimere kompilering af parametrisk polymorfi, som består i at generere en monomorf instans for hvert brugstilfælde af en polymorf funktion eller type. Med andre ord oversættes parametrisk polymorfi på kildekodeniveau til ad hoc polymorfi på målplatformsniveau. Monomorfisering forbedrer ydeevnen (mere præcist gør polymorfi "fri"), men på samme tid kan den øge størrelsen af outputmaskinkoden . [92]

Hindley - Milner

I den klassiske version er Hindley-Milner-systemet (også ganske enkelt "Hindley-Milner" eller "X-M", engelsk HM ) [93] [94] der ligger til grund for ML -sproget en delmængde af System F , begrænset af prædikativet prenex polymorfi for at muliggøre automatisk typeslutning , for hvilken Hindley-Milner traditionelt også inkluderede den såkaldte " Algorithm W " , udviklet af Robin Milner .

Mange implementeringer af X-M er en forbedret version af systemet, der repræsenterer et " principal typing scheme " [93] [2] , der i en enkelt passage med næsten lineær kompleksitet samtidigt udleder de mest generelle polymorfe typer for hvert udtryk og nøje kontrollerer deres aftale .

Siden starten er Hindley-Milner-systemet blevet udvidet på flere måder [95] . En af de mest kendte udvidelser er understøttelse af ad-hoc polymorfi gennem typeklasser , som er yderligere generaliseret til kvalificerede typer .

Automatisk typeslutning blev betragtet som en nødvendighed i den oprindelige udvikling af ML som et interaktivt teorembevissystem " Logic for Computable Functions ", hvorfor de tilsvarende begrænsninger blev pålagt. Efterfølgende blev der på basis af ML udviklet en række effektivt kompilerede almenformålssprog orienteret til programmering i stor skala , og i dette tilfælde er behovet for at understøtte typeinferens reduceret kraftigt, da modulgrænseflader i industriel praksis skal under alle omstændigheder udtrykkeligt annoteres med typer [81] . Derfor er der blevet foreslået mange Hindley-Milner-udvidelser, som undgår typeslutning til fordel for empowerment, op til og med understøttelse af et komplet System F med impredikativ polymorfi, såsom højere-ordens modulsprog , som oprindeligt var baseret på eksplicit modultype annotation og har mange udvidelser og dialekter, såvel som Haskell sprogudvidelser ( , og ). Rank2TypesRankNTypesImpredicativeTypes

Standard ML 's MLton- kompiler monomorfiserer , men på grund af andre optimeringer gældende for Standard ML , overstiger den resulterende stigning i outputkode ikke 30 % [92] .

C og C++

I C er funktioner ikke førsteklasses objekter , men det er muligt at definere funktionspointere , som giver dig mulighed for at bygge funktioner af højere orden [96] . Usikker parametrisk polymorfi er også tilgængelig ved eksplicit at sende de påkrævede egenskaber af en type gennem en ikke- typebestemt delmængde af sproget repræsenteret af en ikke-typebestemt pointer ).sprogfællesskabeti"pointer generisk(kaldet en "97][ ad-hoc polymorfi , da den ikke ændrer repræsentationen af pointeren, er den dog skrevet eksplicit for at omgå compilerens typesystem [96] . void* void*

For eksempel er standardfunktionen qsorti stand til at håndtere arrays af elementer af enhver type, for hvilke der er defineret en sammenligningsfunktion [96] .

struct segment { int start ; int ende ; }; int seg_cmpr ( struct segment * a , struct segment * b ) { return abs ( a -> end - a -> start ) - abs ( b -> end - b -> start ); } int str_cmpr ( char ** a , char ** b ) { return strcmp ( * a , * b ); } struct segment segs [] = { { 2 , 5 }, { 4 , 3 }, { 9 , 3 }, { 6 , 8 } }; char * strs [] = { "tre" , "én" , "to" , "fem" , "fire" }; vigtigste () { qsort ( strs , sizeof ( strs ) / sizeof ( char * ), sizeof ( char * ), ( int ( * )( void * , void * )) str_cmpr ); qsort ( segs , sizeof ( segs ) / sizeof ( struct segment ), sizeof ( struct segment ), ( int ( * )( void * , void * )) seg_cmpr ); ... }

Men i C er det muligt at idiomatisk reproducere typet parametrisk polymorfi uden at bruge void*[98] .

C++-sproget giver et skabelonundersystem , der ligner parametrisk polymorfi, men er semantisk implementeret af en kombination af ad hoc- mekanismer:

skabelon < typenavn T > T max ( T x , T y ) { hvis ( x < y ) returnere y ; andet returnere x ; } int main () { int a = max ( 10 , 15 ); dobbelt f = max ( 123,11 , 123,12 ); ... }

Monomorfisering af ved kompilering af C++ skabeloner er uundgåelig , fordi sprogets typesystem mangler understøttelse af polymorfi - det polymorfe sprog her er en statisk tilføjelse til den monomorfe sprogkerne [99] . Dette fører til en multipel stigning i mængden af modtaget maskinkode , som er kendt som " code bloat " [100] .

Historie

Notationen af parametrisk polymorfi som en udvikling af lambdaregningen (kaldet den polymorfe lambdaregning eller System F ) blev formelt beskrevet af logikeren Jean-Yves Girard [101] [102] ( 1971 ), uafhængigt af ham en lignende system blev beskrevet af datalogen John S. Reynolds [103] ( 1974 ) [104] .

Parametrisk polymorfi blev først introduceret i ML i 1973 [41] [105] . Uafhængigt af ham blev parametriske typer implementeret under ledelse af Barbara Liskov ved CLU ( 1974 ) [41] .

Se også

Noter

↑ 1 2 Strachey, "Fundamental Concepts", 1967 .
↑ 1 2 Pierce, 2002 .
↑ Cardelli, Wegner, "On Understanding Types", 1985 , 1.3. Arts of Polymorphism, s. 6.
↑ 1 2 Appel, "Kritik af SML", 1992 .
↑ 1 2 Jones, "Theory of Qualified Types", 1992 .
↑ 1 2 3 4 5 6 7 Gaster, Jones, "Polymorphic Extensible Records and Variants", 1996 .
↑ Cardelli, "Basic Polymorphic Typechecking", 1987 .
↑ 1 2 Wonseok Chae (Ph.D.-afhandling), 2009 , s. 91-92.
↑ 1 2 3 4 5 6 Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 .
↑ Blume, "Exception Handlers", 2008 , s. elleve.
↑ Wells, 1994 .
↑ Pierce, 2002 , 22 Rekonstruktion af typer, s. 361.
↑ Pierce, 2002 , 23.6 Erasure, typability, and type reconstruction, s. 378-381.
↑ Remy, "ML med abstrakte og rekordtyper", 1994 .
↑ Garrigue, Remy, "Semi-Explicit First-Class Polymorphism for ML", 1997 .
↑ Reynolds, "Theories of programming languages", 1998 , 17. Polymorphism. Bibliografiske noter, s. 393.
↑ Førsteklasses polymorfi på MLton . Hentet 28. juli 2016. Arkiveret fra originalen 28. november 2015. (ubestemt)
↑ Pierce, 2002 , 22.7 Polymorphism via let, s. 354-359.
↑ 1 2 3 4 5 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 .
↑ Dushkin, "Monomorfisme, polymorfi og eksistentielle typer", 2010 .
↑ Cardelli, "Typeful programmering", 1991 , s. tyve.
↑ Pierce, 2002 , 23.10 Impredicativity, s. 385.
↑ Pierce, 2002 , kapitel 22. Typerekonstruktion. Afsnit 22.8. Yderligere bemærkninger, s. 361-362.
↑ Wonseok Chae (Ph.D.-afhandling), 2009 , s. fjorten.
↑ 1 2 3 Garrigue, "Polymorphic Variants", 1998 .
↑ Blume, "Extensible Programming with First-Class Cases", 2006 , s. ti.
↑ 1 2 3 4 5 6 7 8 9 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 1.1 Static Type System for Record Polymorphism, s. 3-6.
↑ Leijen, "First-class Labels", 2004 , s. en.
↑ Gaster, Jones, "Polymorphic Extensible Records and Variants", 1996 , Abstract, s. en.
↑ 1 2 Paulson, "ML for the Working Programmer", 1996 , 2.9 Records, s. 35.
↑ 1 2 3 4 Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 1.2 Compilation Method for Record Polymorphism, s. 6-8.
↑ Harper, "Intro til SML", 1986 .
↑ 1 2 3 Remy, "Type Inference for Records", 1991 , s. 2.
↑ 1 2 3 4 5 Blume, "Row polymorphism at work", 2007 .
↑ Funktionel postopdatering . Hentet 30. juni 2016. Arkiveret fra originalen 2. juni 2016. (ubestemt)
↑ 1 2 Alice ML syntaktiske forbedringer . Hentet 30. juni 2016. Arkiveret fra originalen 27. november 2016. (ubestemt)
↑ Funktionel postudvidelse og rækkefangst . Hentet 30. juni 2016. Arkiveret fra originalen 13. august 2016. (ubestemt)
↑ Harper, Pierce, "Record calculus based on symmetrisk concatenation", 1991 .
↑ 1 2 Wand, "Type inference for record concatenation and multiple inheritance", 1991 .
↑ 12 Sulzmann , 1997 .
↑ 1 2 3 4 Pierce, 2002 , 1.4 Kort historie, s. 11-13.
↑ Remy, "Type Inference for Records", 1991 , s. 2-3.
↑ 1 2 3 4 5 6 7 Leijen, "First-class Labels", 2004 , s. 13-14.
↑ Cardelli, "Semantics of Multiple Inheritance", 1988 .
↑ Cardelli, Wegner, "On Understanding Types", 1985 .
↑ Pierce, 2002 , 16. Subtype metatheory, s. 225.
↑ Pierce, 2002 , 11.8 Optagelser, s. 135.
↑ 1 2 3 Minsky oversat af DMK, 2014 , Subtyping and inline polymorphism, s. 267-268.
↑ Wand, "Type inference for objects", 1987 .
↑ 1 2 Minsky oversat af DMK, 2014 , Object Polymorphism, s. 255-257.
↑ 1 2 Remy, "Type Inference for Records", 1991 , Relateret arbejde, s. 3.
↑ 1 2 Remy, "Type Inference for Records", 1991 .
↑ Blume, "Extensible Programming with First-Class Cases", 2006 , s. elleve.
↑ Remy, "Subtypes and Row polymorphism", 1995 .
↑ 1 2 Remy, Vouillon, "Objective ML", 1998 .
↑ Pierce, 2002 , 15.8 Yderligere bemærkninger, s. 223.
↑ Minsky oversat af DMK, 2014 , Polymorphic variants, s. 149-158.
↑ Pierce, 2002 , 24 Existential Types, s. 404.
↑ 1 2 Reynolds, "Theories of programming languages", 1998 , 18. Modul Specification, s. 401-410.
↑ Cardelli, "Typeful programmering", 1991 , 4.4. Tupletyper, s. 20-23.
↑ 1 2 Harper, Lillibridge, "Type-Theoretic Approach to Higher-Order Modules with Sharing", 1993 .
↑ 1 2 3 4 Yallop, White, "Lightweight higher-kinded polymorphism", 2014 .
↑ Harper, Mitchell, "Type Structure of SML", 1993 .
↑ Rossberg, "1ML - Core and Modules United (F-ing First-class Modules)", 2015 , Impredicativity Reloaded, s. 6.
↑ 1 2 Rossberg, "1ML med specielle effekter (F-ing Generativity Polymorphism)", 2016 .
↑ Ohori, "Compilation Method for Polymorphic Record Calculi", 1992 .
↑ Ohori - SML# (præsentation) (downlink) . Hentet 30. juni 2016. Arkiveret fra originalen 27. august 2016. (ubestemt)
↑ Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , s. 38.
↑ 1 2 Blume, "Extensible Programming with First-Class Cases", 2006 , s. 9.
↑ Ohori, "Polymorphic Record Calculus and Its Compilation", 1995 , 5 Implementaion, s. 37.
↑ 1 2 3 4 5 Blume, "Extensible Programming with First-Class Cases", 2006 .
↑ Gaster (Ph.D.-afhandling), 1998 .
↑ Leijen, "First-class Labels", 2004 , s. 7.
↑ Leijen, "First-class Labels", 2004 .
↑ Udvidelige poster på Haskell-Wiki (downlink)
↑ Blumes personlige side . Hentet 30. juni 2016. Arkiveret fra originalen 19. maj 2016. (ubestemt)
↑ Blume, "Exception Handlers", 2008 .
↑ 1 2 3 Wonseok Chae (Ph.D.-afhandling), 2009 .
↑ Paulson, "ML for the Working Programmer", 1996 , 4.6 Declaring exceptions, s. 135.
↑ Harper, "Praktisk grundlag for programmeringssprog", 2012 , 28.3 Exception Type, s. 258-260.
↑ 1 2 ML2000 Preliminary Design, 1999 .
↑ Harper, "Praktisk grundlag for programmeringssprog", 2012 , kapitel 22. Konstruktører og slags, s. 193.
↑ 1 2 3 Weirich et al, "Giving Haskell a promotion", 2012 .
↑ Fluet, Pucella, "Phantom Types and Subtyping", 2006 .
↑ Pierce, 2002 , 30.5 Going Further: Dependent Types, s. 489-490.
↑ Gifford, Lucassen, "Effect systems", 1986 .
↑ Lucassen, Gifford, "Polymorphic Effect Systems", 1988 .
↑ Talpin, Jouvelot, 1992 .
↑ Harper, Morrisett, "Intensional Type Analysis", 1995 .
↑ Crary, Weirich, Morrisett, "Intensional polymorphism", 1998 .
↑ Pierce, 2002 , 23.2 Varieties of polymorphism, s. 364-365.
↑ 1 2 uger, "Whole-Program Compilation in MLton", 2006 .
↑ 1 2 Hindley, "Principal Type Scheme", 1969 .
↑ Milner, "Theory of Type Polymorphism", 1978 .
↑ Jones, "FP with Overloading and HO Polymorphism", 1995 .
↑ 1 2 3 Kernighan B. , Ritchie D. C-programmeringssproget = C-programmeringssproget. - 2. udg. - Williams , 2007. - S. 304. - ISBN 0-13-110362-8 . , kapitel 5.11. Funktionsmarkører
↑ Appel, "Critique of SML", 1992 , s. 5.
↑ Oleg Kiselyov. Virkelig polymorfe lister i C. okmij.org. Hentet 22. november 2016. Arkiveret fra originalen 30. januar 2017. (ubestemt)
↑ Mitchell, "Concepts in Programming Languages", 2004 , 6.4. Polymorfi og overbelastning, s. 145-151.
↑ Scott Meyers . Code Bloat på grund af skabeloner . comp.lang.c++.modereret . Usenet (16. maj 2002). Hentet: 19. januar 2010. (ubestemt)
↑ Girard, "Extension of Type Theory", 1971 .
↑ Girard, "Højere-ordens calculus", 1972 .
↑ Reynolds, "Theory of Type Structure", 1974 .
↑ Pierce, 2002 , 23.3 System F, s. 365-366.
↑ Milner et al, "LCF", 1975 .

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. - T. 13 . - S. 11-49 . - doi : 10.1023/A:1010000313106 .

J Roger Hindley. Hovedtypeskemaet for et objekt i kombinatorisk logik // Transactions of the American Mathematical Society . - American Mathematical Society, 1969. - Vol. 146 . - S. 29-60 . - doi : 10.2307/1995158 .

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 .

Milner R. , Morris L., Newey M. A Logic for Computable Functions with refleksive og polymorfe typer // Arc-et-Senans. — Proc. Konference om at bevise og forbedre programmer, 1975.

Robin Milner . En teori om typepolymorfi i programmering. - Journal of Computer and System Sciences , 1978. - V. 17 , no. 3 . - S. 348-375 . - doi : 10.1016/0022-0000(78)90014-4 .

Luca Cardelli , John C. Mitchell. Operations on Records // Matematiske strukturer i datalogi. - 1991. -1,udgave. 1.

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. - 97 s. — ISBN PA 15213-3891. (Russisk)

John M. Lucassen, David K. Gifford. Integration af funktionel og imperativ programmering . – 1986.

Luca Cardelli . Grundlæggende polymorfisk typekontrol. - 1987.

Mitchell Wand . Komplet typeslutning for simple objekter // In Proc. 2. IEEE-symposium om logik i datalogi. - 1987. -S. 37-44.

Martín Abadi, Luca Cardelli , Pierre-Louis Curien. Formel parametrisk polymorfi . — POPL, 1993.

Luca Cardelli . En semantik af multipel arv // Inf. Comput. 76. - 1988. -S. 138-164.

John M. Lucassen, David K. Gifford. Polymorfe effektsystemer . — POPL , 1988.

Didier Remy. Type Inference for Records in a natural Extension of ML // Research Report 1431. - Institut National de Recherche en Informatique et Automatisme, 1991.

Luca Cardelli . Typisk programmering // IFIP state-of-the-art rapporter. - New York: Springer-Verlag, 1991. -Iss. Formel beskrivelse af programmeringskoncepter. -S. 431-507.

Robert Harper , Benjamin Pierce. Registrer beregning baseret på symmetrisk sammenkædning // CMU-CS-90-157R. — Carnegie Mellon University, støttet og overvåget af Naval Research, 1991.

Mitchell Wand . Skriv inferens for rekordsammenkædning og multipel nedarvning // Udvalg fra 1989 IEEE Symposium on Logic in Computer Science. - Information and Computation, 1991. -T. 93,no. 1. -doi:10.1016/0890-5401(91)90050-C.

Andrew W. Appel. En kritik af Standard ML . - Princeton University, 1992.

Mark P. Jones. En teori om kvalificerede typer . — ESOP , Springer-Verlag Lecture Notes in Computer Science, 1992.

Atsushi Ohori. A Compilation Method for ML-Style Polymorphic Record Calculi // POPL: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programmeing languages,. - Kyoto Universitet, ACM , 1992. - S. 154-165 . - doi : 10.1.1.105.7655 .

J.P. Talpin, P. Jouvelot. Polymorf type, region og effektinferens // 2(3):245271. — JFP , 1992.

Robert Harper , John C. Mitchell. Om typestrukturen af standard ML. -ACMTOPLAS, 1993. -S. 211-252.

Robert Harper , Mark Lillibridge. Typeteoretisk tilgang til modulermed deling . -ACMPress,POPL, 1993. - ISBN CMU-CS-93-197. -doi:10.1.1.14.3595.

Didier Remy. Programmering af objekter med ML-ART: En udvidelse til ML med abstrakte og posttyper . - Internationalt symposium om teoretiske aspekter af computersoftware, Springer-Verlag, 1994. - S. 321-346 .

JB Wells. Typabilitet og typekontrol i andenordens lambda-kalkulus er ækvivalente og uafklarelige // Proceedings of the 9th Annual IEEE . - Symposium on Logic in Computer Science (LIS), 1994. - S. 176-185 .

Robert Harper , . Kompilering af polymorfi ved hjælp af intentionel typeanalyse. - 1995.

Atsushi Ohori. En polymorf optegnelsesregning og dens kompilering . - Kyoto Universitet, ACM , 1995. - S. 844-895 .

Mark P. Jones. Funktionel programmering med overbelastning og højere ordens polymorfi . - Springer-Verlag Lecture Notes, 1995. - doi : 10.1.1.26.9460 .

Didier Remy. Bedre undertyper og rækkevariabler for posttyper // Præsenteret på workshoppen om fremskridt inden for typer til datalogi på Newton Institute. - Cambridge, Storbritannien, 1995.

Lawrence C. Paulson . ML for den arbejdende programmør. — 2. - Cambridge, Storbritannien: Cambridge University Press, 1996. - 492 s. -ISBN 0-521-57050-6(hardback), 0-521-56543-X (paperback).

Benedict R. Gaster, Mark P. Jones. Et polymorfisk typesystem til udvidelige poster og varianter // Teknisk rapport NOTTCS-TR-96-3. - University of Nottingham, 1996.

Jacques Garrigue, Didier Remy. Semi-eksplicit førsteklasses polymorfisme for ML // Academic Press. — Information og beregning, 1997.

M. Sulzmann. Design af registreringssystemer // Teknisk rapport YALEU/DCS/RR-1128. - Yale University, 1997. - doi : 10.1.1.17.6563 .

Karl Crary, Stephanie Weirich, J. Gregory Morrisett. Intentionel polymorfi i typesletningssemantik . — ICFP , 1998.

Benedikt R. Gaster. Optegnelser, varianter og kvalificerede typer // Teknisk rapport NOTTCS-TR-98-3. - Ph.D. Speciale, 1998.

Jacques Garrigue. Programmering med polymorfe varianter . - Kyoto Universitet, 1998.

Didier Rémy, Jérome Vouillon. Objective ML: En effektiv objektorienteret udvidelse til ML . - Theory And Practice of Object Systems, ACM , 1998. - V. 4 (1) . - S. 27-50 .

John C. Reynolds. Teorier om programmeringssprog . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (hardback), 978-0-521-10697-9 (paperback).

ML2000 arbejdsgruppen. Principper og et foreløbigt design for ML2000 . – 1999.

Benjamin Pierce. Typer og programmeringssprog . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Oversættelse til russisk: Benjamin Pierce. Skriver i programmeringssprog. - Dobrosvet , 2012. - 680 s. — ISBN 978-5-7913-0082-9 .

John C. Mitchell Begreber i programmeringssprog. - Cambridge University Press, 2004. - ISBN 0-511-04091-1 (e-bog i netLibrary); 0-521-78098-5 (hardback).

Jens Palsberg, Tian Zhao. Typeinferens for postsammenkædning og subtypning . - 2004. Arkiveret 16. september 2016.

Daan Leijen. Førsteklasses etiketter til udvidelige rækker // TechReport UU-CS-2004-51. — Universiteit Utrecht, 2004.

Matthias Blume, Umut A. Acar, Wonseok Chae. Udvidelig programmering med førsteklasses sager . — ICFP , 2006.

Matthew Fluet, Riccardo Pucella. Fantomtyper og undertypning . — JFP , 2006.

Stephen Weeks. Kompilering af hele programmet i MLton . - 2006. Arkiveret den 29. juni 2007.

Matthias Blume. Optegnelser, summer, tilfælde og undtagelser: Rækkepolymorfi på arbejde : talevideo. - Microsoft, 2007.

Matthias Blume, Umut A. Acar, Wonseok Chae. Undtagelsesbehandlere som udvidelige sager . - Toyota Technological Institute i Chicago, APLAS, 2008.

Wonseok Chae. Type Sikker Udvidelig Programmering // Ph.D. afhandling. — Toyota Technological Institute i Chicago, 2009.

Roman Dushkin. Monomorfisme, polymorfi og eksistentielle typer . – 2010.

Jeremy Yallop, Leo White. Letvægts polymorfi af højere art . — Internationalt symposium om funktionel og logisk programmering, 2014.

Robert Harper . Praktiske grundlag for programmeringssprog. - version 1.37 (revideret 11/01/2014). - licenseret under Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License., 2012. - 544 s. Arkiveret24. oktober 2015 påWayback Machine

Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis og Jose P. Magalhães. Giver Haskell en forfremmelse // I forløbet af den 8. ACM SIGPLAN Workshop om typer i sprogdesign og -implementering. - NY, USA: TLDI , 2012. - S. 53-66 .

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. - ISBN 978-5-97060-102-0 . (Russisk)

Andreas Rossberg. 1ML - Core and Modules United (F-ing First-class Modules) . — ICFP , 2015.

Andreas Rossberg. 1ML med specielle effekter (F-ing Generativity Polymorphism) . — WadlerFest, Google, 2016.

Haskell-Wiki: Eksistentielle typer . (ubestemt)

Haskell-Wiki: Rang-N-typer . (ubestemt)

Haskell-Wiki: Impredikative typer . (ubestemt)

Jacques Garrigue. OKaml manual: Polymorfe varianter . (ubestemt)

Datatyper
Ufortolkelig	Bit Nappe Byte qubit Behandle Egenskab Ord
Numerisk	Hel fast punkt flydende komma Rationel Kompleks Lang interval
Tekst	Symbolsk Snor
Reference	Adresse Link Pointer Indpakning
Sammensatte	Algebraisk datatype ( generisk ) klasse Type-produkt ( Skriv Tuple struktur ) Et objekt Konsolidering ( tagget ) Bestilt par
abstrakt	array Liste Tur Stak Associativ array (visning, kort ) Masser af multisæt Type Kurve
Andet	Logisk Nederste Højere Polymorf Funktionel talløse Kollektion Undtagelse Slægt ( metaklasse ) Monade Semafor Flyde ugyldig
relaterede emner	Abstrakt datatype primitiv type Datastruktur Generisk type variabel Interface Konstruktør (OOP) Konstruktør (FP) Type konstruktør Type støbning Prototype Type system