Parametrisk polymorfism

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 12 april 2021; kontroller kräver 5 redigeringar .

Parametrisk polymorfism i programmeringsspråk och typteori är en egenskap hos semantiken i ett typsystem som låter dig bearbeta värden av olika typer på ett identiskt sätt, det vill säga att fysiskt exekvera samma kod för data av olika typer [1] [2] .

Parametrisk polymorfism anses vara den "sanna" formen av polymorfism [3] , vilket gör språket mer uttrycksfullt och kraftigt ökande kodåteranvändning . Traditionellt är det motsats till ad-hoc-polymorfism [1] , som ger ett enda gränssnitt till potentiellt olika kod för olika typer som är tillåtna i ett givet sammanhang, potentiellt inkompatibla ( statiskt eller dynamiskt ). I ett antal kalkyler, såsom teorin om kvalificerade typer , behandlas ad-hoc polymorfism som ett specialfall av parametrisk polymorfism.

Parametrisk polymorfism ligger till grund för typsystemen av språk i ML- familjen ; sådana typsystem kallas polymorfa. I gemenskaper av språk med icke-polymorfa typsystem (ättlingar till Algol och BCPL [4] ), kallas parametriskt polymorfa funktioner och typer " generaliserade ".

Skriv polymorfism

Termen " parametrisk polymorfism " används traditionellt för att hänvisa till typsäker parametrisk polymorfism, även om otypade former av den också existerar (se parametrisk polymorfism i C och C++ ) [4] . Nyckelbegreppet för typsäker parametrisk polymorfism, förutom den polymorfa funktionen , är den polymorfa typen .

En polymorf typ ( eng. polymorphic type ), eller en polytype ( eng. polytype ) är en typ som parametriseras av en annan typ. En parameter i typlagret kallas en typvariabel (eller typvariabel) .

Formellt studeras typpolymorfism i den polymorfiskt typade lambda-kalkylen , kallad System F.

Till exempel kan en funktion som appendsammanfogar två listor till en byggas oberoende av typen av listelement. Låt typvariabeln a beskriva typen av listelement. Sedan kan funktionen appendskrivas som " forall a. [a] × [a] -> [a]" (här betyder konstruktionen [a]typen " en lista, vars element har en typa " - syntaxen som används i Haskell-språket ). I det här fallet sägs typen vara parametriserad av en variabel aför alla värden a. På varje plats för tillämpning av specifika argument löses appendvärdet och varje omnämnande av det i typsignaturen ersätts med ett värde som motsvarar tillämpningskontexten. I det här fallet kräver funktionstypsignaturen att elementtyperna för båda listorna och resultatet är identiska .a

Uppsättningen av giltiga värden för en typvariabel ges genom kvantifiering . De enklaste kvantifierarna är universella (som i exemplet med append) och existentiella (se nedan).

En kvalificerad typ är en polymorf typ, dessutom utrustad med en uppsättning predikat som reglerar intervallet av giltiga värden för en parameter av denna typ. Med andra ord låter typkvalificering dig kontrollera kvantifieringen på ett godtyckligt sätt. Teorin om kvalificerade typer byggdes av Mark P. Jones 1992 [ 5] . Den tillhandahåller en gemensam motivering för de mest exotiska typsystemen, inklusive typklasser , utvidgbara beteckningaroch subtyper , och tillåter att specifika begränsningar formuleras exakt för specifika polymorfa typer, vilket etablerar förhållandet mellan parametriska och ad-hoc polymorfism ( överbelastning ), och mellan explicit och implicit överbelastning. Föreningen av en typ med ett predikat idenna teori kallas bevis . En algebra som liknar lambdakalkylen formuleras för bevis , inklusive abstraktion av bevis, tillämpning av bevis, etc. Att korrelera en term av denna algebra med en explicit överbelastad funktion kallas bevisöversättning .

Motiverande exempel för utvecklingen av en generaliserad teori var Wadler-Blott-typklasserna och typningen av utvidgbara poster genom Harper-Pearce-predikat [5] [6] .

Klassificering av polymorfa system

Parametriskt polymorfa typsystem klassificeras i grunden enligt rang och predikativ egenskap . Dessutom urskiljs explicit och implicit polymorfism [7] och ett antal andra egenskaper. Implicit polymorfism tillhandahålls genom typinferens , vilket avsevärt förbättrar användbarheten men har begränsad uttrycksförmåga. Många praktiska parametriskt polymorfa språk separerar faserna av ett externt implicit typat språk och ett internt explicit typat språk .

Den mest allmänna formen av polymorfism är " impredikativ polymorfism av högre rang ". De mest populära restriktionerna för denna form är polymorfismen i rang 1 som kallas " prenex " och den predikativa polymorfismen . Tillsammans bildar de " predikativ prenexpolymorfism " liknande den som implementerats i ML och tidigare versioner av Haskell .

När typsystem blir mer komplexa blir typsignaturer så komplexa att deras fullständiga eller nästan fullständiga härledning betraktas av många forskare som en kritisk egenskap, vars frånvaro kommer att göra språket olämpligt för praktik [8] [9] . Till exempel, för en traditionell kombinator, har den mapfullständiga typsignaturen (med hänsyn till generisk kvantifiering) under typsäker undantagsflödesspårning följande form [10] [8] (som ovan betyder en lista med element av typ ):[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 }}\;(\;\left[\alpha \ höger]{\xrightarrow {\gamma }}\left[\beta \right]\;)$

Rank

Rangen av polymorfism visarhäckningsdjupet för kvantifierare av typvariabler tillåtna inom ramen för systemet . " Polymorfism av rang k " (för k > 1 ) låter dig specificera typvariabler efter polymorfa typer av rangordning som inte är högre än ( k - 1) . " Polymorfism av högre rang " låter dig sätta kvantifierare av typvariabler till vänster om ett godtyckligt antal pilar i typer av högre ordning .

Joe Wells bevisade [ 11] att typinferens för ett Currytypat System F inte kan avgöras för rang över 2, så explicit typanteckning måste användas när man använder högre rang [12] .

Det finns partiella inferentiella typsystem som kräver att endast icke-deriverbara typvariabler ska annoteras [13] [14] [15] .

Prenex polymorfism

Polymorfism av rang 1 kallas ofta prenex polymorfism (från ordet "prenex" - se prenex normalform ). I ett prenex polymorft system kan typvariabler inte instansieras av polymorfa typer. Denna begränsning gör distinktionen mellan monomorfa och polymorfa typer väsentlig, varför polymorfa typer i prenex-systemet ofta kallas för " typing schemes " ( engelska typschemas ) för att skilja dem från "vanliga" (monomorfa) typer (monotyper). Som en konsekvens kan alla typer skrivas i formen när alla typvariabelkvantifierare är placerade i den yttersta (prenex) positionen, vilket kallas prenex normalform . Enkelt uttryckt är polymorfa funktionsdefinitioner tillåtna, men polymorfa funktioner kan inte skickas som argument till andra funktioner [16] [17] - polymorfiskt definierade funktioner måste monotypinstansieras före användning.

En nära motsvarighet är den så kallade " Let-polymorphism " eller " ML - style polymorphism " av Damas-Milner. Tekniskt sett har Let-polymorphism i ML ytterligare syntaktiska begränsningar, såsom " värdebegränsningen " förknippad med typsäkerhetsproblem vid användning av referenser (som inte förekommer i rena språk som Haskell och Clean ) [18] [19] .

Predikativitet

Predikativ polymorfism

Predikativ (villkorlig) polymorfism kräver att en typvariabel instansieras med en monotyp (inte en polytyp).

Predikativa system inkluderar intuitionistisk typteori och Nuprl .

Impredikativ polymorfism

Impredikativ (ovillkorlig) polymorfism låter dig instansiera en typvariabel med en godtycklig typ - både monomorf och polymorf, inklusive typen som definieras. (Att tillåta, inom en kalkyl, ett system att rekursivt inkludera sig självt i sig självt kallas impredikativitet . Potentiellt kan detta leda till paradoxer som Russell eller Cantor [20] , men detta händer inte i fallet med ett utarbetat system . [21] .)

Impredikativ polymorfism låter dig överföra polymorfa funktioner till andra funktioner som parametrar, returnera dem som ett resultat, lagra dem i datastrukturer, etc., varför det också kallas förstklassig polymorfism . Detta är den mest kraftfulla formen av polymorfism, men utgör å andra sidan ett allvarligt problem för optimering och gör typinferens olöslig .

Ett exempel på ett impredikativt system är System F och dess förlängningar (se lambdakub ) [22] .

Rekursionsstöd

Traditionellt, i ättlingar till ML , kan en funktion endast vara polymorf när den ses "från utsidan" (det vill säga den kan appliceras på argument av olika typer), men dess definition kan bara innehålla monomorf rekursion (det vill säga typupplösning är gjort innan samtalet). Att utvidga rekonstruktion av ML-typ till rekursiva typer ger inga allvarliga svårigheter. Å andra sidan skapar kombinationen av typrekonstruktion med rekursivt definierade termer ett svårt problem som kallas polymorf rekursion . Mycroft och Meertens föreslog en polymorf typningsregel som tillåter att rekursiva anrop till en rekursiv funktion från sin egen kropp instansieras med olika typer. I den här kalkylen, känd som Milner-Mycroft-kalkylen, är typinferens oavgörlig . [23]

Strukturell typ polymorfism

Produkttyper (även kända som " poster ") fungerar som den formella grunden för objektorienterad och modulär programmering. Deras dubbla par består av summatyper (även känd 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

Tillsammans är de ett sätt att uttrycka alla komplexa datastrukturer och vissa aspekter av beteendet hos program .

Record calculi är ett generaliserat namn för problemet och ett antal av dess lösningar angående flexibiliteten hos produkttyper i programmeringsspråk under villkoret typsäkerhet [26] [27] [28] . Termen sträcker sig ofta till summatyper, och gränserna för begreppet " posttyp " kan variera från kalkyl till kalkyl (liksom själva begreppet " typ "). Termerna " registrera polymorfism " (som, återigen, ofta inkluderar variant polymorfism ) [27] , " modulus calculus " [9] och " strukturell polymorfism " används också.

Allmän information

Typprodukter och summor ( poster och varianter [ en ] ger flexibilitet när det gäller att konstruera komplexa datastrukturer, men begränsningarna hos många system av verklig typ hindrar ofta att deras användning är riktigt flexibel. Dessa begränsningar uppstår vanligtvis på grund av problem med effektivitet, typinferens eller helt enkelt användbarhet. [29]

Det klassiska exemplet är Standard ML , vars typsystem medvetet begränsades precis tillräckligt för att kombinera enkel implementering med uttrycksfullhet och matematiskt bevisbar typsäkerhet .

Exempel på postdefinition :

> val r = { namn = "Foo" , använd = sant }; (* val r: {namn: sträng, använd: bool} = {namn = "Foo", använd = sant} *)

Åtkomst till fältvärdet med dess namn utförs av en prefixkonstruktion av formen #field record:

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

Följande funktionsdefinition över posten är korrekt:

> roligt namn1 ( x : { namn : sträng , ålder : int }) = # namn x

Och följande genererar ett kompilatorfel att typen inte är helt löst :

> roligt namn2 x = #namn x (* olöst typ i deklarationen: {namn : '1, ...} *)

Monomorfismen hos poster gör dem oflexibla, men effektiva [30] : eftersom den faktiska minnesplatsen för varje postfält är känd i förväg (vid kompilering), kompileras med namn till den till direkt indexering, som vanligtvis beräknas i en maskin instruktion. Men när man utvecklar komplexa skalbara system är det önskvärt att kunna abstrahera fält från specifika poster - till exempel för att definiera en universell fältväljare:

kul välj r l = #l r

Men att sammanställa polymorf åtkomst till fält som kan vara i olika ordning i olika register är ett svårt problem, både ur säkerhetskontroll av operationer på språknivå och ur prestandasynpunkt på maskinkodsnivå. En naiv lösning kan vara att dynamiskt slå upp ordboken vid varje samtal (och skriptspråk använder den), men detta är uppenbarligen extremt ineffektivt. [31]

Typsummor utgör grunden för grenuttrycket , och på grund av typsystemets stränghet ger kompilatorn kontroll över analysens fullständighet. Till exempel för följande summatyp :

datatyp 'a foo = A för 'a | B av ( 'a * 'a ) | C

vilken funktion som helst över det kommer att se ut

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

och när någon av satserna tas bort, kommer kompilatorn att utfärda en varning för att analysera ofullständig (" match nonexhaustive"). För fall där endast ett fåtal av de många alternativen kräver analys i ett givet sammanhang, är det möjligt att organisera default-förgrening med hjälp av den sk. "Joker" - ett universellt prov, med vilket alla giltiga (enligt skrivning) värden är jämförbara. Det är skrivet med ett understreck (" _"). Till exempel:

fun bar ( p : 'a foo ) = fallet p av C => ... | _ => ...

I vissa språk (i Standard ML , i Haskell ) är till och med den "enklare" konstruktionen if-then-elsebara syntaktisk socker framför ett specialfall av förgrening , dvs uttrycket

om A så B annars C

redan på stadium av grammatisk analys presenteras i formuläret

fallet A av sant => B | falskt => C

eller

fallet A av sant => B | _ => C

Syntaktisk socker

I Standard ML är poster och varianter monomorfa, men syntaktisk socker för att hantera poster med flera fält stöds, kallat det " universella mönstret " [32] :

> val r = { namn = "Foo" , använd = sant }; (* val r : {name : string, used : bool} = {name = "Foo", used = true} *) > val { used = u , ...} = r ; (* val u : bool = sant *)

En ellips av {used, ...}typen " " betyder att det finns andra fält i denna post, utöver de som nämns. Det finns dock ingen postpolymorfism som sådan (inte ens prenexet ): full statisk upplösning av informationen om monomorfa posttyp (via slutledning eller explicit anteckning ) krävs.

Utökning och funktionell uppdatering av poster

Termen utvidgbara poster används för en generaliserad beteckning av sådana operationer som expansion (bygga en ny post baserad på en befintlig med tillägg av nya fält), skärning (ta en specificerad del från en befintlig post), etc. I synnerhet, det innebär möjligheten för den så kallade " funktionella postuppdateringen " ( funktionell postuppdatering ) - operationen att konstruera ett nytt postvärde baserat på det befintliga genom att kopiera namnen och typerna av dess fält, i vilka ett eller flera fält i det nya rekordet får nya värden som skiljer sig från de ursprungliga (och möjligen har en annan typ). [33] [34] [19] [35] [36] [37]

Funktionella uppdaterings- och förlängningsoperationer är i sig själva ortogonala för att registrera polymorfism, men deras polymorfa användning är av särskilt intresse. Även för monomorfa poster blir det viktigt att kunna utelämna explicit omnämnande av fält som kopieras oförändrade, och detta representerar faktiskt postpolymorfism i den rent syntaktiska formen . Å andra sidan, om vi betraktar alla poster i systemet som utökningsbara, så gör detta att funktioner på poster kan skrivas som polymorfa.

Ett exempel på den enklaste designvarianten är implementerad i Alice ML (enligt de nuvarande efterföljande ML- konventionerna ) [36] . Det universella mönstret (ellipsis ) har utökade möjligheter: det kan användas för att "fånga en rad" för att arbeta med den "återstående" delen av posten som ett värde:

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

Funktionsuppdateringen implementeras som en derivata av att fånga en rad med ett serviceord where. Till exempel följande kod:

> låt val r = { a = 1 , c = 3,0 , d = "inte en lista" , f = [ 1 ], p = [ "inte en sträng" ], z = INGEN } i { r där d = noll , p = "hej" } slut

kommer automatiskt att skrivas om i formen:

> låt val r = { a = 1 , c = 3,0 , d = "inte en lista" , f = [ 1 ], p = [ "inte en sträng" ], z = INGEN } val { d = _, p = _, ... = tmp } = r in { ... = tmp , d = noll , p = "hej" } slut

Postsammansättning

En av de första (slutet av 1980 -talet - början av 1990 -talet ) föreslog olika alternativ för att formalisera expanderbara poster genom sammanlänkningsoperationer på icke-polymorfa poster (Harper-Pearce [38] , Wand [39] , Salzmann [40] ). Cardelli använde till och med skivoperationer istället för polymorfism på bärnstensspråket. Det finns inget känt sätt att sammanställa dessa kalkyler effektivt; dessutom är dessa beräkningar mycket komplexa ur typteoretisk analyssynpunkt. [27] [41] [42] [43]

Till exempel [33] :

val bil = { namn = "Toyota" ; ålder = "gammal" ; id = 6678 } val lastbil = { namn = "Toyota" ; id = 19823235 } ... val repaired_truck = { bil och lastbil }

radpolymorfismen ) visade att multipelt arv kan modelleras genom rekordsammansättning [39] [33] .

Strukturell undertypning av Cardelli

Luca Cardelli undersökte möjligheten att formalisera " postpolymorfism " genom att subtypa relationer på poster: för att göra detta behandlas en post som en "universell subtyp", det vill säga dess värde tillåts referera till hela uppsättningen av dess supertyper. Detta tillvägagångssätt stöder också metodarv och fungerar som en typteoretisk grund för de vanligaste formerna av objektorienterad programmering . [27] [44] [45]

Cardelli presenterade en variant på metoden att sammanställa rekordpolymorfism över deras undertyper genom att fördefiniera offseten av alla möjliga etiketter i en potentiellt enorm struktur med många tomma platser [31] .

Metoden har betydande nackdelar. Stöd för subtypning i typsystemet komplicerar i hög grad mekanismen för kontroll av typkonsistens [46] . Dessutom, i dess närvaro, upphör den statiska typen av uttrycket att ge fullständig information om den dynamiska strukturen för värdet på posten . Till exempel, när du endast använder undertyper, följande term:

> om sant så är { A = 1 , B = sant } annars { B = falskt , C = "Cat" } (* val it : {B : bool} *)

har typ {B : bool}, men dess dynamiska värde är lika med {A = 1, B = true}, det vill säga information om typen av den utökade posten går förlorad [43] , vilket är ett allvarligt problem för att kontrollera operationer som kräver fullständig information om värdestrukturen för att de ska kunna köras (t.ex. jämförelse för jämställdhet ) [19] . Slutligen, i närvaro av undertyper, påverkar valet mellan ordnad och oordnad representation av poster allvarligt prestandan [47] .

Populariteten för subtyping beror på att det ger enkla och visuella lösningar på många problem. Till exempel kan objekt av olika typer placeras i en enda lista om de har en gemensam supertyp [48] .

Wanda row polymorfism

Mitchell Wand föreslog 1987 idén att(inte uttryckligen specificerad) delen av posten genom vad han kallade en radtypsvariabel ( radtypsvariabel ) [49] .

En radvariabel är en variabel av typen som går genom en uppsättning ändliga uppsättningar (rader) av typade fält (par av " (значение : тип)"). Resultatet är förmågan att implementera breddövergripande arv direkt ovanpå den parametriska polymorfismen som ligger till grund för ML utan att komplicera typsystemet med undertypningsregler Den resulterande typen av polymorfism kallas radpolymorfism . Inline polymorfism sträcker sig till både produkter av typer och summor av typer .

Vand lånade termen från engelsmännen. rad (rad, kedja, linje) från Algol-68 , där det betydde en uppsättning vyer. I ryskspråkig litteratur har denna term i samband med Algol traditionellt översatts som "flerarter". Det finns också en översättning av "radvariabler" som "strängvariabler" [41] , vilket kan orsaka förvirring med små bokstäver i strängtyper .

Exempel ( OCaml- språk ; postfix-syntax, record#field) [50] :

# låt skicka_m a = a # m ;; (* värde send_m : < m : a; .. > -> a = <roligt> *)

Här är ellipsen (av två punkter) OCamls accepterade syntax för en icke namngiven inline-typvariabel . På grund av sådan typning kan funktionen send_mappliceras på ett objekt av vilken som helst (ej tidigare känd ) objekttyp, vilket inkluderar en metod för mmotsvarande signatur.

Typavdraget för Wanda-kalkylen i originalversionen var ofullständigt: på grund av bristen på begränsningar för utvidgningen av serien kommer att lägga till ett fält om namnet matchar det befintliga - som ett resultat har inte alla program en huvudtyp [6] [43] . Detta system var dock det första konkreta förslaget att utöka ML med register som stöder arv [51] . Under de följande åren föreslogs ett antal olika förbättringar, inklusive de som gör det komplett [51] [27] .

Det mest anmärkningsvärda spåret lämnades av Didier Remy ( franska: Didier Rémy ). Han byggde ett praktiskt typsystem med utbyggbara register, inklusive en komplett och effektiv typrekonstruktionsalgoritm [52] [53] . Remy stratifierar språket av typer i sorter , formulerar en sorterad algebra av typer ( eng. sorterad algebra av typer, sorterad språk av typer ). En skillnad görs mellan den egentliga typen av typer (inklusive fälttyper) och typen av fält ; mappningar mellan dem införs och på grundval av dem formuleras reglerna för att skriva utökade poster som en enkel förlängning av de klassiska ML- reglerna . Närvaroinformationen för ett fält definieras som en mappning från en typsortering till en fältsortering . Variabler av radtyp omformuleras till variabler som hör till fältsorteringen och är lika med frånvarokonstanten , som är ett element i fältsorteringen som inte har en matchning i typsorteringen . En typutvärderingsoperation för en post med n fält definieras som att mappa ett n-ärt fält till en typ (där varje fält i tupeln antingen beräknas av närvarofunktionen eller ges av frånvarokonstanten ).

På ett förenklat sätt kan idén med kalkyl tolkas som en förlängning av typen av vilket fält som helst i posten med en närvaro/frånvaro-flagga och representation av posten som en tuppel med en lucka för varje möjligt fält [6] . I implementeringsprototypen gjordes syntaxen för typspråket närmare den typteoretiska formuleringen, till exempel [52] :

# låt bilen = { namn = "Toyota" ; ålder = "gammal" ; id = 7866 } ;; (* bil : ∏ (namn : pre (sträng); id : pre (num); ålder : pre (sträng); abs) *) # let truck = { name = "Blazer" ; id = 6587867567 } ;; (* lastbil : ∏ (namn : pre (sträng); id : pre (num); abs) *) # låt person = { namn = "Tim" ; ålder = 31 ; id = 5656787 } ;; (* person : ∏ (namn : pre (sträng); id : pre (num); ålder : pre (num); abs) *)

(symbolen ∏i Remy betyder typberäkningsoperationen)

Att lägga till ett nytt fält skrivs med hjälp av konstruktionen with:

# låt förare = { person med fordon = bil } ;; (* förare : ∏ (fordon : pre (∏ (namn : pre (sträng); id : pre (num); ålder : pre (sträng); abs)); namn : pre (sträng); id : pre (num) ; ålder: pre (num); abs) *)

Funktionell uppdatering är skriven identiskt, med skillnaden att omnämnandet av ett redan existerande fält åsidosätter det:

# let truck_driver = { chaufför med fordon = lastbil };; (* lastbilschaufför : ∏ (fordon : pre (∏ (namn : pre (sträng); id : pre (num); abs)); namn : pre (sträng); id : pre (num); ålder : pre (num ); magmuskler) *)

Detta schema formaliserar den begränsning som behövs för att kontrollera operationer på poster och sluta sig till huvudtypen, men leder inte till en uppenbar och effektiv implementering [6] [43] . Remy använder hash, vilket är ganska effektivt i genomsnitt, men ökar runtime overhead även för inbyggt monomorfa program, och är dåligt lämpad för poster med många fält [31] .

Rémy fortsatte med att utforska användningen av inline polymorfism i samband med datasubtyping , och betonade att dessa är ortogonala begrepp och visar att poster blir mest uttrycksfulla när de används tillsammans [54] . På grundval av detta, tillsammans med Jérôme Vouillon , föreslog han en lättviktig objektorienterad förlängning till ML [55] . Denna förlängning implementerades i Xavier Leroys språk "Caml Special Light" , vilket gjorde det till OCaml [56] . OCaml- objektmodellen är nära sammanflätad med användningen av strukturell subtypning och inline polymorfism [48] , vilket är anledningen till att de ibland felaktigt identifieras. Inline produktpolymorfism i OCaml är kärnan i typinferensen ; subtypningsrelationer är inte nödvändiga i ett språk som stöds, men ökar flexibiliteten ytterligare i praktiken [55] [50] [48] . OKaml har en enklare och mer beskrivande syntax för typinformation.

Jacques Garrigue ( fr. Jacques Garrigue ) implementerade [25] ett praktiskt system av polymorfa summor . Han kombinerade Remi och Ohoris teoretiska arbete och byggde ett system som körs i mitten: information om förekomsten av taggar i en post representeras med hjälp av kön och information om deras typer använder inline-variabler. För att kompilatorn ska kunna skilja mellan polymorfa och monomorfa summor använder Garriga en speciell syntax (backtick, prefixtagg). Detta eliminerar behovet av en typdeklaration - du kan omedelbart skriva funktioner på den, och kompilatorn kommer att mata ut en minimal lista med taggar när dessa funktioner är sammansatta. Detta system blev en del av OCaml runt 2000 , men inte istället för , utan förutom monomorfa summor , eftersom de är något mindre effektiva, och på grund av oförmågan att kontrollera fullständigheten av analysen , gör det svårt att hitta fel (till skillnad från Blooms lösning ). [25] [57]

Nackdelarna med Wands inline-polymorfism är att implementeringen inte är självklar (det finns inget enda systematiskt sätt att kompilera den, varje specifik typsystem baserat på inline-variabler har sin egen implementering) och det tvetydiga förhållandet med teorin (det finns ingen enhetlig formulering för typkontroll och slutledning , stöd för slutledning löstes separat och krävde experiment med att införa olika restriktioner) [27] .

Genomskinliga Harper-Lilybridge summor

Den mest komplexa typen av poster är beroende poster. Sådana poster kan inkludera typer såväl som "vanliga" värden (materialiserade typer, reified [9] ), och termerna och typerna i nästa ordning i postens brödtext kan bestämmas baserat på de som föregår dem . Sådana beteckningar motsvarar de " svaga summorna " av beroendetypsteorin , även känd som " existentialer ", och fungerar som den mest allmänna motiveringen för modulsystem i programmeringsspråk [58] [59] . Cardelli ansåg [60] typer liknande egenskaper som en av huvudtyperna i fulltypsprogrammering (men kallade dem " tupler ").

Robert Harper och Mark Lillibridge konstruerade [61 ] [59] den genomskinliga summakalkylen för attformellt rättfärdiga ett förstklassigt modulspråk av högre ordning , det mest avancerade modulsystemet som är känt. Denna kalkyl används bland annat i Harper-Stone semantiken , som representerar den typteoretiska motiveringen för Standard ML .

Genomskinliga summor generaliserar svaga summor genom etiketter och en uppsättning likheter som beskriver typkonstruktörer . Termen genomskinlig betyder att en posttyp kan innehålla både typer med en explicit exporterad struktur, såväl som helt abstrakta . Lagret av släkten i kalkyl har en enkel klassisk sammansättning: kön av alla typer och funktionella släkten av slaget urskiljs , typtypkonstruktörer ( ML stöder inte polymorfism i högre släkten , alla typvariabler tillhör släktet , och abstraktionen av typkonstruktorer är endast möjlig genom funktorer [62] ). Kalkylen skiljer mellan subtypningsregler för poster som bastyper och för postfält som deras beståndsdelar, med hänsyn till "subtyper" och "subfields", medan döljande (abstraherande) fältsignaturer är ett separat koncept från subtyping. Subtyping här formaliserar kartläggningen av moduler till gränssnitt . [61] [9] $\star$ $k_{1}=>k_{2}$ $\star$

Harper-Lilybridge-kalkylen är obestämbar även när det gäller typkonsistenskontroll ( modulspråksdialekter implementerade i Standard ML och OCaml använder begränsade delmängder av denna kalkyl). Senare byggde dock Andreas Rossberg , baserat på deras idéer, språket " 1ML ", där de traditionella kärnnivåposterna för språk- och modulnivåstrukturerna är samma förstklassiga konstruktion [9] (betydligt mer uttrycksfulla än Cardelli's - se kritik av ML-modulens språk ). Genom att införliva idén från Harper och Mitchell [63] om att dela in alla typer i universum av "små" och "stora" typer (förenklat liknar detta den grundläggande uppdelningen av typer i enkla och aggregerade typer, med ojämlika typningsregler), tillhandahöll Rossberg lösbarhet inte bara konsistenskontroller , utan nästan fullständig typslutning . Dessutom tillåter 1ML impredikativ polymorfism [64] . Samtidigt är det interna språket i 1ML baserat på det platta System F ω och kräver inte användning av beroende typer som metateori. Från och med 2015 lämnade Rossberg möjligheten att lägga till inline polymorfism öppen till 1ML , och noterade bara att detta borde ge mer fullständig typslutning [9] . Ett år senare lade han [65] effekterna polymorfism till 1ML .

Polymorf kalkyl av Ohori-poster

Atsushi Ohori , tillsammans med sin handledare Peter Buneman , föreslog 1988 idén att begränsa utbudet av möjliga värden för vanliga typvariabler i den polymorfa typningen av själva poster . Senare formaliserade Ohori denna idé genom notationssläktena , efter att 1995 ha byggt en fullfjädrad kalkyl och en metod för dess effektiva sammanställning [19] [30] . Implementeringsprototypen skapades 1992 som en förlängning av SML/NJ [66] kompilatorn, sedan ledde Ohori utvecklingen av sin egen SML# kompilator, som implementerar Standard ML dialekten med samma namn . I SML# fungerar postpolymorfism som grunden för att sömlöst bädda in SQL- konstruktioner i SML- program . SML# används av stora japanska företag för att lösa affärsproblem i samband med högbelastade databaser [67] . Ett exempel på en sådan session ( REPL ) [68] :

rolig rik { Lön = s , ... } = s > 100000 ; (* val rik = fn : 'a#{ Lön:int, ... } -> bool *) kul ung x = #Ålder x < 24 ; (* val young = fn : 'a#{ Age:int, ... } -> bool *) fun youngAndWealthy x = rik x och även ung x ; (* val youngAndWealthy = fn : 'a#{ Age:int, Lön:int, ... } -> bool *) roligt välj display l pred = fold ( fn ( x , y ) => if pred x then ( visa x ) ::y else y ) l noll ; (* val select = fn : ('a -> 'b) -> 'en lista -> ('a -> bool) -> 'b lista *) fun youngAndWealthyEmployees l = välj #Name l youngAndWealthy ; (* val youngAndWealthyEmployees = fn : 'b#{ Ålder:int, Namn:'a, Lön:int, ... } lista -> 'en lista *)

Ohori kallade sin kalkyl för " record polymorphism " ( engelsk rekordpolymorfism ) eller " polymorphic record calculus " ( engelsk polymorphic record calculus ), samtidigt som han betonade att han, liksom Wand, betraktar polymorfism inte bara av produkttyper , utan också av typer- summor [27] .

Ohori-kalkylen kännetecknas av den mest intensiva användningen av släktskiktet [6] . I posten (referenstyp till genus ), betyder symbolen antingen släktet av alla typer ; eller postsläktet , som har formen , som betecknar uppsättningen av alla poster som innehåller åtminstone de angivna fälten; eller ett variantsläkte med formen som anger uppsättningen av alla varianttyper som innehåller åtminstone de specificerade konstruktörerna . I språkets platta syntax skrivs en typbegränsning till någon sorts notation som (se exempel ovan). Lösningen liknar något som den begränsade kvantifieringen 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 enda polymorfa operationen som tillhandahålls av denna kalkyl är fältextraktionsoperationen [69] . Men Ohori var den första som introducerade ett enkelt och effektivt kompileringsschema för rekordpolymorfism [43] . Han kallade det "realisationskalkylen" ( implementeringskalkyl ). En post representeras av en vektor ordnad lexikografiskt efter fältnamnen på den ursprungliga posten; adressering av ett fält med namn översätts till ett anrop till en mellanfunktion som returnerar numret på det givna fältet i den givna vektorn med det begärda namnet, och efterföljande indexering av vektorn med det beräknade positionsnumret. Funktionen anropas endast när man instansierar polymorfa termer, vilket medför en minimal overhead på körtid när man använder polymorfism och inte lägger någon overhead när man arbetar med monomorfa typer. Metoden fungerar lika bra med godtyckligt stora poster och varianter. Kalkylen ger typinferens och finner en stark överensstämmelse med teorin ( generisk kvantifiering är direkt relaterad till den vanliga vektorindexeringen ), som är en direkt förlängning av Girard-Reynolds andra ordningens lambdakalkyl , som tillåter olika välkända egenskaper hos polymorfa typning som ska överföras till rekordpolymorfism [31] .

I praktiken har stöd för polymorfa varianter i SML# inte implementerats på grund av dess inkompatibilitet med Standard ML :s definitionsmekanism för summatyp (kräver syntaktisk separation av summor och rekursiva typer) [70] .

Nackdelen med Ohori-kalkylen är bristen på stöd för rekordexpansion eller trunkeringsoperationer [27] [71] [43] .

Första klass Guster-Jones markerar

I teorin om kvalificerade typer beskrivs expanderbara poster av frånvaron av ett fält ( "saknar" predikat ) och närvaron av ett fält ( "har" predikat ) predikat. Benedict Gaster ( Benedict R. Gaster ) tillsammans med författaren till teorin Mark Jones ( Mark P. Jones ) slutförde den i termer av utvidgbara poster till ett praktiskt typsystem av implicit maskinskrivna språk, inklusive definition av kompileringsmetoden [6] . De myntar termen förstklassiga etiketter för att betona förmågan att abstrahera fältoperationer från statiskt kända etiketter. Senare försvarade Gaster sin avhandling [72] om det konstruerade systemet .

Gaster-Jones-kalkylen ger inte full typ av slutledning . På grund av beslutbarhetsproblem infördes dessutom en konstgjord begränsning: ett förbud mot tomma serier [73] . Sulzmann försökte omformulera kalkylen [40] , men systemet han byggde kan inte utökas för att stödja polymorf rekordexpansion och har inte en universell effektiv kompileringsmetod [43] .

Daan Leijen lade till ett radlikhetspredikat (eller radlikhetspredikat ) till Gaster-Jones-kalkylen och flyttade seriespråket till predikatspråket - detta säkerställde fullständig typslutning och upphävde förbudet mot tomma serier [74] . Vid sammanställning omvandlas protokollen till en lexikografiskt ordnad tupel och bevisöversättning tillämpas enligt Gaster-Jones-schemat. Layens system tillåter uttryck av idiom som meddelanden av högre ordning (den mest kraftfulla formen av objektorienterad programmering ) och förstklassiga grenar .

Baserat på dessa arbeten har tillägg till Haskell-språket [75] implementerats .

Resultaten av Gaster-Jones är mycket nära Ohoris , trots betydande skillnader i typteoretisk motivering, och den största fördelen är stödet för rekordexpansion och trunkeringsoperationer [6] . Nackdelen med kalkyl är att den förlitar sig på egenskaper hos typsystemet som inte finns i de flesta programmeringsspråk. Dessutom är typinferens för det ett allvarligt problem, varför författarna har infört ytterligare begränsningar. Och även om Layen har eliminerat många av bristerna, är det inte möjligt att använda -grenen [71]default

Kontrollkonstruktionspolymorfism

Med utvecklingen av mjukvarusystem kan antalet alternativ i summatypen öka och att lägga till varje alternativ kräver att man lägger till en motsvarande gren till varje funktion över denna typ, även om dessa grenar är identiska i olika funktioner. Således beror komplexiteten i att öka funktionaliteten i de flesta programmeringsspråk icke-linjärt på deklarativa ändringar i referensvillkoren. Detta mönster är känt som uttrycksproblemet . Ett annat välkänt problem är undantagshantering : under decennier av forskning om typsystem kunde alla språk som klassificerats som typsäkra fortfarande lämnas genom att kasta ett oupptäckt undantag - eftersom, trots att själva undantagen skrivits, mekanismen för att höja och hanteringen av dem var inte maskinskriven. Även om verktyg för att analysera flödet av undantag har byggts, har dessa verktyg alltid varit externa i förhållande till språket.

Matthias Blume , en kollega till Andrew Appel som arbetar med projektets efterföljare ML [76] , hans doktorand Wonseok Chae och kollega Umut Acar löste både problem baserade på matematisk dualitet produkter och summor . Förkroppsligandet av deras idéer var språket MLPolyR [71] [34] [77] , baserat på den enklaste delmängden av Standard ML och kompletterande den med flera nivåer av typsäkerhet [78] . Wonseok Chai försvarade senare sin avhandling om dessa prestationer [78] .

Lösningen är följande. Enligt principen om dualitet motsvarar introduktionsformen för ett begrepp elimineringsformen för dess dual [ 71] . Således motsvarar elimineringsformen för summor (analys av grenar) den inledande formen för poster. Detta uppmuntrar förgrening att ha samma egenskaper som redan är tillgängliga för poster – gör dem till förstklassiga objekt och låt dem utökas.

Till exempel, det enklaste uttrycket språktolk:

fun eval e = fall e av `Const i => i | `Plus (e1,e2) => eval e1 + eval e2

med införandet av förstklassig konstruktion caseskan skrivas om som:

fun eval e = matcha e med fall `Const i => i | `Plus (e1,e2) => eval e1 + eval e2

varefter cases-blocket kan renderas:

fun eval_c eval = fall `Const i => i | `Plus (e1,e2) => eval e1 + eval e2 fun eval e = matcha e med (eval_c eval)

Denna lösning möjliggör default-förgrening (till skillnad från Gaster-Jones kalkylen ), vilket är viktigt för sammansättningen av förstklassiga grenar [34] . Komplettering av radens sammansättning utförs med hjälp av ordet . nocases

fun const_c d = fall `Const i => i standard : d fun plus_c eval d = fall `Plus (e1,e2) => eval e1 + eval e2 default : d fun eval e = matcha e med const_c (plus_c eval nocases ) fun bind env v1 x v2 = om v1 = v2 så x else env v2 fun var_c env d = fall `Var v => env v default : d fun let_c eval env d = fall `Let (v,e,b) => eval (bind env v (eval env e)) b default : d fun eval_var env e = matcha 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 nya koden, som måste läggas till med den kvalitativa komplikationen av systemet, inte ändra den redan skrivna koden (funktionerna const_coch plus_c"vet ingenting" om det efterföljande tillägget av stöd för variabler och let-block till språktolken). Således är förstklassiga utvidgbara fall en grundläggande lösning på uttrycksproblemet , vilket gör att man kan tala om ett utvidgbart programmeringsparadigm [71] [78] . inline polymorphism , som redan stöds i typsystemet, och i denna mening är fördelen med en sådan teknisk lösning dess konceptuella enkelhet [ 34] .

Utvidgning av mjukvarusystem kräver dock också kontroll över hanteringen av undantag som kan kastas på godtyckliga anropskapslingsdjup. Och här proklamerar Bloom och kollegor en ny typsäkerhetsslogan i utvecklingen av Milners slogan : " Program som klarar typkontroll kastar inte obehandlade undantag ." Problemet är att om funktionstypens signatur innehåller information om de typer av undantag som denna funktion potentiellt kan ge, och denna information i signaturen för den godkända funktionen måste vara strikt överensstämmande med informationen om funktionsparametern av högre ordning (inklusive om detta är en tom uppsättning ) - att skriva undantagshanteringsmekanismen kräver omedelbart polymorfismen hos själva undantagstyperna - annars upphör funktioner av högre ordning att vara polymorfa. Samtidigt, i ett säkert språk, är undantagen en utvidgbar summa [79] [80] [81] , det vill säga en varianttyp vars konstruktorer läggs till allt eftersom programmet fortskrider. Följaktligen innebär säkerhet av undantagsflödestyp behovet av att stödja summatyper som är både töjbara och polymorfa. Även här är lösningen inline polymorfism .

Liksom Garriga-kalkylen , använder MLPolyR en speciell syntax för polymorfa summor (backtick, ledande tagg), och det finns inget behov av en fördeklaration av summatypen (det vill säga ovanstående kod är hela programmet, inte ett fragment). Fördelen är att det inte finns några problem med att analysera fullständighetskontroll: semantiken för MLPolyR definieras genom att konvertera till ett bevisat tillförlitlighet internt språk som varken stöder summapolymorfism eller undantag (för att inte tala om oförfångade undantag), så behovet av dem radering vid kompilering är i sig ett bevis på tillförlitlighet. [34]

MLPolyR använder en icke-trivial kombination av flera kalkyler och tvåstegsöversättning. Den använder Remy-kalkylen för typavdrag och typmatchning , samtidigt som den använder principen om dualitet för att representera summor som produkter, sedan översätter språket till ett mellanliggande uttryckligt maskinskrivet språk med polymorfa poster, och använder sedan Ohoris effektiva kompileringsmetod . Med andra ord, Ohoris kompileringsmodell har generaliserats för att stödja Remy-kalkylen [69] . På typteoretisk nivå introducerar Bloom flera nya syntaktiska notationer samtidigt, vilket gör att man kan skriva ner regler för att skriva undantag och förstklassiga grenar. Typsystemet MLPolyR ger full typslutledning , så att författarna övergav utvecklingen av en platt syntax för att explicit skriva typer och stöd för signaturer på modulspråket .

Systemet av Leyen -typ introducerar också en variant av grenpolymorfism: en konstruktion kan representeras som en funktion av högre ordning som tar emot en post från funktioner, som var och en motsvarar en viss beräkningsgren ( Haskells syntax är lämplig för denna ändring och kräver ingen revidering). Till exempel: case

dataList a = noll :: { } | nackdelar :: { hd :: a , tl :: Lista a } snoc xs r = case ( omvänd xs ) r sista xs = snoc xs { noll = \ r -> _ | _ , nackdelar = \ r -> r . hd }

Eftersom poster i Layens system är utökningsbara är grenparsning flexibel på nivån av dynamiska beslut (som kedja av kontroller eller användning av en associativ array ), men ger en mycket effektivare implementering (variantetiketten motsvarar en offset i posten). Dock måste standardförgreningsstödet ( default) tas bort i detta fall, eftersom ett enda default-mönster skulle matcha flera fält (och därmed flera förskjutningar). Leyen kallar denna konstruktion " förstklassiga mönster " ( förstklassiga mönster ).

Polymorfism hos högre kön

Högre sorts polymorfism betyder abstraktion överordningens typkonstruktorer , det vill säga typoperatorer av formen

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

Stöd för denna funktion tar polymorfism till en högre nivå, vilket ger abstraktion över både typer och typkonstruktorer , precis som funktioner av högre ordning ger abstraktion över både värden och andra funktioner. Polymorfism i högre kön är en naturlig komponent i många funktionella programmeringsspråk , inklusive monader , veck och inbäddningsbara språk . [62] [82]

Till exempel [62] om du definierar följande funktion ( Haskell language ):

när b m = om b så returnerar m annars ()

då kommer följande funktionella typ att härledas för det :

när :: forall ( m :: * -> * ) . Monad m => Bool -> m () -> m ()

Signaturen m :: * -> *säger att typvariabeln m är en typvariabel som tillhör en högre sort ( engelska högre-kinded typevariabel ). Det betyder att den abstraherar över typkonstruktörer (i detta fall unary , såsom Maybeeller []), som kan appliceras på konkreta typer, såsom Inteller (), för att konstruera nya typer.

På språk som stöder full typabstraktion ( Standard ML , OCaml ) måste alla typvariabler vara av ett släkte * , annars skulle typsystemet vara osäkert . Polymorfism i högre släkten tillhandahålls alltså av själva abstraktionsmekanismen, i kombination med explicit annotering vid instansiering, vilket är något obekvämt. En idiomatisk implementering av polymorfism i högre släkten är dock möjlig, utan att kräva explicit anteckning - för detta används en teknik som liknar defunktionalisering på typnivå . [62]

Generisk polymorfism

Snälla system säkerställer själva typsystemens säkerhet genomatttillåta kontroll över betydelsen av typuttryck .

Låt det till exempel krävas att istället för den vanliga typen " vektor " (linjär array) implementera familjen av typer " längdvektorn ", med andra ord för att definiera typen " vektor indexerad efter längd ". Den klassiska Haskell- implementeringen ser ut så här [83] :

data Noll data Succ n data Vec :: * -> * -> * där Noll :: Vec a Zero Cons :: a -> Vec a n -> Vec a ( Succ n )

Här definieras fantomtyper [84] först , det vill säga typer som inte har en dynamisk representation. Konstruktörerna Zero och Succfungerar som "typlagervärden", och variabeln nframtvingar olikheten mellan de olika betongtyperna som konstruerats av konstruktören Succ. Typen Vecdefinieras som en generaliserad algebraisk datatyp (GADT).

Lösningen förutsätter villkorligt att fantomtypen nkommer att användas för att modellera vektorns heltalsparameter baserat på Peano-axiomen - det vill säga att endast uttryck som Succ Zero, Succ Succ Zero, Succ Succ Succ Zeroetc. kommer att byggas. Men även om definitionerna är skrivna i typspråk , de själva är formulerade på ett opartat sätt. Detta framgår av signaturen Vec :: * -> * -> *, vilket betyder att de betongtyper som skickas som parametrar tillhör släktet * , vilket betyder att de kan vara vilken betongtyp som helst. Med andra ord, meningslösa typuttryck som Succ Booleller är inte förbjudna här Vec Zero Int. [83]

En mer avancerad kalkyl skulle göra det möjligt att specificera intervallet för typparametern mer exakt:

data Nat = Noll | Succ Nat data Vec :: * -> Nat -> * där VNil :: Vec a Zero VCons :: a -> Vec a n -> Vec a ( Succ n )

Men vanligtvis har bara högspecialiserade system med beroende typer [85] implementerade i språk som Agda , Coq och andra en sådan uttrycksförmåga. Till exempel, från Agda- språkets synvinkel, skulle posten Vec :: * -> Nat -> *innebära att könet för en typ Vec beror på typen Nat(det vill säga ett element av ett slag beror på ett element av en annan, lägre sort ).

2012 byggdes en tillägg till Haskell- språket [83] , som implementerar ett mer avancerat system av kön och gör ovanstående kod korrekt Haskell-kod. Lösningen är att alla typer (under vissa restriktioner) automatiskt “ promoteras ” ( eng. promote ) till en högre nivå, och bildar släkten med samma namn som kan användas explicit. Ur denna synvinkel är posten inte beroende - det betyder bara att den andra parametern i vektorn måste tillhöra det namngivna släktet , och i det här fallet är det enda elementet i detta släkte typen med samma namn. Vec :: * -> Nat -> *Nat

Lösningen är ganska enkel, både vad gäller implementering i kompilatorn och vad gäller praktisk tillgänglighet. Och eftersom typpolymorfism i sig är en naturlig del av Haskells semantik, leder typpromotion till typpolymorfism , vilket både ökar kodåteranvändningen och ger en högre nivå av typsäkerhet . Till exempel används följande GADT för att verifiera typlikhet:

data EqReﬂ a b där Reﬂ :: EqReﬂ a a

har ett kön i klassisk Haskell , * -> * -> *vilket hindrar den från att användas för att testa för likhet av typkonstruktörer som t.ex. MaybeEtt typfrämjande släktsystem härleder ett polymorft släkte forall X. X -> X -> *, vilket gör typen EqReﬂmer generisk. Detta kan uttryckligen skrivas:

data EqReﬂ ( a :: X ) ( b :: X ) där Reﬂ :: forall X . forall ( a :: X ) . EqReﬂ a a

Effektpolymorfism

Effektsystem föreslogs av Gifford och Lucassen under andra hälften av 1980 -talet [86] [87] [88] med syftet att isolera bieffekter för bättre kontroll över säkerhet och effektivitet i konkurrenskraftig programmering .

I det här fallet betyder effektpolymorfism kvantifiering över renheten av en specifik funktion, det vill säga införandet av en flagga i den funktionella typen som karakteriserar funktionen som ren eller oren. Denna typtillägg gör det möjligt att abstrahera renheten hos funktioner av högre ordning från renheten hos funktioner som skickas till dem som argument.

Detta är särskilt viktigt när man flyttar till funktioner över moduler ( poster som inkluderar abstrakta typer ) - funktionorer - eftersom de under renhetsförhållanden har rätt att vara applicerande, men i närvaro av biverkningar måste de generera för att säkerställa typsäkerhet (för mer om detta, se motsvarighet av typer i ML-modulspråket ). Sålunda, på språket för högre ordningens förstklassiga moduler, visar sig effektpolymorfism vara en nödvändig bas för att stödja generativitetspolymorfism : att skicka en renhetsflagga till en funktor ger ett val mellan applikativ och generativ semantik i ett enda system. [65]

Stöd i programmeringsspråk

Typsäker parametrisk polymorfism är tillgänglig på Hindley-Milner -skrivna språk — på ML - dialekter ( Standard ML , OCaml , Alice , F# ) och deras ättlingar ( Haskell , Clean , Idris , Mercury , Agda ) — likaså som i de som ärvts från dem hybridspråk ( Scala , Nemerle ).

Generiska datatyper (generika) skiljer sig från parametriskt polymorfa system genom att de använder en begränsad kvantifiering , och därför inte kan ha en högre rang än 1 . De finns i Ada , Eiffel , Java , C# , D , Rust ; och även i Delphi sedan 2009 version. De dök först upp i CLU .

Intentionell polymorfism

Intensionell polymorfism är en teknik för att optimera kompileringen av parametrisk polymorfism baserad på komplex typteoretisk analys, som består av beräkningar på typer under körning. Intentionell polymorfism möjliggör taggfri sophämtning , oboxadöverföring av argument till funktioner och inramade (minnesoptimerade) platta datastrukturer. [89] [90] [91]

Monomorfisering

Monomorfisering är en teknik för att optimera kompileringen av parametrisk polymorfism, som består i att generera en monomorf instans för varje användningsfall av en polymorf funktion eller typ. Med andra ord, parametrisk polymorfism på källkodsnivå översätts till ad hoc- polymorfism på målplattformsnivå. Monomorfisering förbättrar prestandan (mer exakt, gör polymorfism "fri"), men samtidigt kan det öka storleken på utdatamaskinkoden . [92]

Hindley - Milner

I den klassiska versionen är Hindley-Milner-systemet (även helt enkelt "Hindley-Milner" eller "X-M", engelska HM ) [93] [94] som ligger bakom ML -språket en delmängd av System F , begränsat av predikativen prenex polymorfism för att möjliggöra automatisk typinferens , för vilken Hindley-Milner traditionellt också inkluderade den så kallade " Algorithm W " , utvecklad av Robin Milner .

Många implementeringar av X-M är en förbättrad version av systemet, som representerar ett " principiellt typningsschema " [93] [2] som, i ett enda pass med nästan linjär komplexitet, samtidigt härleder de mest allmänna polymorfa typerna för varje uttryck och strikt kontrollerar deras överenskommelse .

Sedan starten har Hindley-Milner-systemet utökats på flera sätt [95] . En av de mest välkända tilläggen är stöd för ad-hoc polymorfism genom typklasser , som ytterligare generaliseras till kvalificerade typer .

Automatisk typinferens ansågs vara en nödvändighet i den ursprungliga utvecklingen av ML som ett interaktivt teorembevisande system " Logic for Computable Functions ", vilket är anledningen till att motsvarande begränsningar infördes. Därefter, på basis av ML , utvecklades ett antal effektivt sammanställda allmänspråk, orienterade mot storskalig programmering , och i detta fall minskar behovet av att stödja typinferens kraftigt, eftersom modulgränssnitt i industriell praxis måste i alla fall uttryckligen annoteras med typer [81] . Därför har många Hindley-Milner-tillägg föreslagits som undviker typinferens till förmån för bemyndigande, upp till och inklusive stöd för ett komplett System F med impredikativ polymorfism, såsom modulspråket av högre ordning , som ursprungligen var baserat på explicit modultypsanteckning och har många tillägg och dialekter, samt Haskell -språktillägg ( , och ). Rank2TypesRankNTypesImpredicativeTypes

Standard ML :s MLton- kompilator monomorfiserar , men på grund av andra optimeringar som är tillämpliga på Standard ML överstiger den resulterande ökningen av utdatakod inte 30 % [92] .

C och C++

I C är funktioner inte förstklassiga objekt , men det är möjligt att definiera funktionspekare , vilket låter dig bygga funktioner av högre ordning [96] . Osäker parametrisk polymorfism är också tillgänglig genom att uttryckligen skicka de nödvändiga egenskaperna för en typ genom en otypad delmängd av språket som representeras av en otypad pekare ).språkgemenskapeni"pekare generisk(kallas en "97][ ad-hoc polymorfism , eftersom den inte ändrar representationen av pekaren, men den är skriven explicit för att kringgå kompilatorns typsystem [96] . void* void*

Till exempel kan standardfunktionen qsorthantera arrayer av element av vilken typ som helst för vilka en jämförelsefunktion [96] är definierad .

struct segment { int start ; int end ; }; 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" , "en" , "två" , "fem" , "fyra" }; huvud () { 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 är det möjligt att idiomatiskt reproducera typad parametrisk polymorfism utan att använda void*[98] .

C++-språket tillhandahåller ett mallundersystem som ser ut som parametrisk polymorfism, men är semantiskt implementerat av en kombination av ad hoc- mekanismer:

mall < typnamn T > T max ( T x , T y ) { om ( x < y ) returnera y ; annan returnera x ; } int main () { int a = max ( 10 , 15 ); dubbel f = max ( 123,11 , 123,12 ); ... }

Monomorfisering av vid kompilering av C++-mallar är oundviklig eftersom språkets typsystem saknar stöd för polymorfism - det polymorfa språket här är ett statiskt tillägg till den monomorfa språkkärnan [99] . Detta leder till en multipel ökning av mängden mottagen maskinkod , vilket är känt som " code bloat " [100] .

Historik

Notationen av parametrisk polymorfism som en utveckling av lambda-kalkylen (kallad polymorphic lambda-kalkylen eller System F ) beskrevs formellt av logikern Jean-Yves Girard [101] [102] ( 1971 ), oberoende av honom en liknande systemet beskrevs av datavetaren John S. Reynolds [103] ( 1974 ) [104] .

Parametrisk polymorfism introducerades först i ML 1973 [41] [105] . Oberoende av honom implementerades parametriska typer under ledning av Barbara Liskov vid CLU ( 1974 ) [41] .

Se även

Typ konstruktör
Genus (typteori)
Polymorf rekursion

Anteckningar

↑ 1 2 Strachey, "Fundamental Concepts", 1967 .
↑ 1 2 Pierce, 2002 .
↑ Cardelli, Wegner, "On Understanding Types", 1985 , 1.3. Typer of Polymorphism, sid. 6.
↑ 1 2 Appel, "Kritik av 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. Thesis), 2009 , sid. 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. elva.
↑ Wells, 1994 .
↑ Pierce, 2002 , 22 Rekonstruktion av typer, sid. 361.
↑ Pierce, 2002 , 23.6 Radering, typbarhet och typrekonstruktion, sid. 378-381.
↑ Remy, "ML med abstrakta och rekordtyper", 1994 .
↑ Garrigue, Remy, "Semi-Explicit First-Class Polymorphism for ML", 1997 .
↑ Reynolds, "Teorier om programmeringsspråk", 1998 , 17. Polymorphism. Bibliografiska anteckningar, sid. 393.
↑ Förstklassig polymorfism på MLton . Hämtad 28 juli 2016. Arkiverad från originalet 28 november 2015. (obestämd)
↑ Pierce, 2002 , 22.7 Polymorphism via let, sid. 354-359.
↑ 1 2 3 4 5 Ohori, "Polymorphic Record Calculus and its Compilation", 1995 .
↑ Dushkin, "Monomorfism, polymorfism och existentiella typer", 2010 .
↑ Cardelli, "typisk programmering", 1991 , sid. tjugo.
↑ Pierce, 2002 , 23.10 Impredicativity, sid. 385.
↑ Pierce, 2002 , kapitel 22. Typrekonstruktion. Avsnitt 22.8. Ytterligare anmärkningar, sid. 361-362.
↑ Wonseok Chae (Ph.D. Thesis), 2009 , sid. fjorton.
↑ 1 2 3 Garrigue, "Polymorphic Variants", 1998 .
^ Blume, "Utökningsbar programmering med förstklassiga fall", 2006 , s. tio.
↑ 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, sid. 3-6.
↑ Leijen, "Förstaklassetiketter", 2004 , sid. ett.
↑ Gaster, Jones, "Polymorphic Extensible Records and Variants", 1996 , Sammanfattning, sid. ett.
↑ 1 2 Paulson, "ML för den arbetande programmeraren", 1996 , 2.9 Records, sid. 35.
↑ 1 2 3 4 Ohori, "Polymorphic Record Calculus and its Compilation", 1995 , 1.2 Compilation Method for Record Polymorphism, sid. 6-8.
↑ Harper, "Intro till SML", 1986 .
↑ 1 2 3 Remy, "Typ slutledning för rekord", 1991 , sid. 2.
↑ 1 2 3 4 5 Blume, "Row polymorphism at work", 2007 .
↑ Funktionell postuppdatering . Hämtad 30 juni 2016. Arkiverad från originalet 2 juni 2016. (obestämd)
↑ 1 2 Alice ML syntaktiska förbättringar . Hämtad 30 juni 2016. Arkiverad från originalet 27 november 2016. (obestämd)
↑ Funktionell postförlängning och radfångst . Hämtad 30 juni 2016. Arkiverad från originalet 13 augusti 2016. (obestämd)
↑ Harper, Pierce, "Record calculus based on symmetric concatenation", 1991 .
↑ 1 2 Wand, "Typ inferens för rekordsammansättning och multipelt arv", 1991 .
↑ 12 Sulzmann , 1997 .
↑ 1 2 3 4 Pierce, 2002 , 1.4 Kort historia, sid. 11-13.
↑ Remy, "Typ slutledning för rekord", 1991 , s. 2-3.
↑ 1 2 3 4 5 6 7 Leijen, "Förstaklassetiketter", 2004 , sid. 13-14.
↑ Cardelli, "Semantics of Multiple Inheritance", 1988 .
↑ Cardelli, Wegner, "Om att förstå typer", 1985 .
↑ Pierce, 2002 , 16. Subtype metatheory, sid. 225.
↑ Pierce, 2002 , 11.8 Recordings, sid. 135.
↑ 1 2 3 Minsky översatt av DMK, 2014 , Subtyping and inline polymorphism, sid. 267-268.
↑ Wand, "Typ inferens för objekt", 1987 .
↑ 1 2 Minsky översatt av DMK, 2014 , Object Polymorphism, sid. 255-257.
↑ 1 2 Remy, "Typ slutledning för rekord", 1991 , Relaterat arbete, sid. 3.
↑ 1 2 Remy, "Typ inferens för rekord", 1991 .
^ Blume, "Utökningsbar programmering med förstklassiga fall", 2006 , s. elva.
^ Remy, "Subtypes and Row polymorphism", 1995 .
↑ 1 2 Remy, Vouillon, "Objective ML", 1998 .
↑ Pierce, 2002 , 15.8 Ytterligare anmärkningar, sid. 223.
↑ Minsky översatt av DMK, 2014 , Polymorphic variants, sid. 149-158.
↑ Pierce, 2002 , 24 Existential Types, sid. 404.
↑ 1 2 Reynolds, "Teorier om programmeringsspråk", 1998 , 18. Modulspecifikation, sid. 401-410.
↑ Cardelli, "Typeful programmering", 1991 , 4.4. Tuppeltyper, sid. 20-23.
↑ 1 2 Harper, Lillibridge, "Typteoretisk inställning till högre ordningsmoduler med delning", 1993 .
↑ 1 2 3 4 Yallop, White, "Lättvikts högre-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 specialeffekter (F-ing Generativity Polymorphism)", 2016 .
↑ Ohori, "Kompileringsmetod för polymorphic Record Calculi", 1992 .
↑ Ohori - SML# (presentation) (nedlänk) . Hämtad 30 juni 2016. Arkiverad från originalet 27 augusti 2016. (obestämd)
↑ Ohori, "Polymorphic Record Calculus och dess sammanställning", 1995 , s. 38.
↑ 1 2 Blume, "Utökningsbar programmering med förstklassiga fall", 2006 , s. 9.
↑ Ohori, "Polymorphic Record Calculus och dess sammanställning", 1995 , 5 Implementaion, sid. 37.
↑ 1 2 3 4 5 Blume, "Extensible Programming with First-Class Cases", 2006 .
↑ Gaster (Ph.D.-avhandling), 1998 .
↑ Leijen, "Förstaklassetiketter", 2004 , sid. 7.
↑ Leijen, "Förstklassiga etiketter", 2004 .
↑ Utökningsbara poster på Haskell-Wiki (nedlänk)
↑ Blumes personliga sida . Hämtad 30 juni 2016. Arkiverad från originalet 19 maj 2016. (obestämd)
↑ Blume, "Exception Handlers", 2008 .
↑ 1 2 3 Wonseok Chae (Ph.D. Thesis), 2009 .
↑ Paulson, "ML för den arbetande programmeraren", 1996 , 4.6 Deklarera undantag, sid. 135.
↑ Harper, "Praktiska grunder för programmeringsspråk", 2012 , 28.3 Exception Type, s. 258-260.
↑ 1 2 ML2000 Preliminär design, 1999 .
↑ Harper, "Praktiska grunder för programmeringsspråk", 2012 , kapitel 22. Konstruktörer och sorter, 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, sid. 489-490.
↑ Gifford, Lucassen, "Effect systems", 1986 .
↑ Lucassen, Gifford, "Polymorphic Effect Systems", 1988 .
↑ Talpin, Jouvelot, 1992 .
↑ Harper, Morrisett, "Intensionell typanalys", 1995 .
↑ Crary, Weirich, Morrisett, "Intensionell polymorphism", 1998 .
↑ Pierce, 2002 , 23.2 Varieties of polymorphism, sid. 364-365.
↑ 1 2 veckor, "Whole-Program Compilation in MLton", 2006 .
↑ 1 2 Hindley, "Principal Type Scheme", 1969 .
↑ Milner, "Teorin om typpolymorfism", 1978 .
↑ Jones, "FP med överbelastning och HO-polymorfism", 1995 .
↑ 1 2 3 Kernighan B. , Ritchie D. C-programmeringsspråket = C-programmeringsspråket. - 2:a uppl. - Williams , 2007. - S. 304. - ISBN 0-13-110362-8 . , kapitel 5.11. Funktionspekare
↑ Appel, "Kritik av SML", 1992 , sid. 5.
↑ Oleg Kiselyov. Verkligen polymorfa listor i C . okmij.org. Hämtad 22 november 2016. Arkiverad från originalet 30 januari 2017. (obestämd)
↑ Mitchell, "Concepts in Programming Languages", 2004 , 6.4. Polymorfism och överbelastning, sid. 145-151.
↑ Scott Meyers . Code Bloat på grund av mallar . comp.lang.c++.modererad . Usenet (16 maj 2002). Hämtad: 19 januari 2010. (obestämd)
↑ Girard, "Extension of Type Theory", 1971 .
↑ Girard, "Kalkyl av högre ordning", 1972 .
↑ Reynolds, "Theory of Type Structure", 1974 .
↑ Pierce, 2002 , 23.3 System F, sid. 365-366.
↑ Milner et al, "LCF", 1975 .

Litteratur

Christopher Strachey. Grundläggande begrepp i programmeringsspråk . - 1967. Arkiverad 12 augusti 2017.
- Återpublicerad: Christopher Strachey. Grundläggande begrepp i programmeringsspråk // Högre ordning och symbolisk beräkning . - 2000. - T. 13 . - S. 11-49 . - doi : 10.1023/A:1010000313106 .

J Roger Hindley. Det huvudsakliga typschemat för ett 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 (franska) // Proceedings of the Second Scandinavian Logic Symposium. - Amsterdam, 1971. - S. 63-92 . - doi : 10.1016/S0049-237X(08)70843-7 .

Jean-Yves Girard. Tolkning fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur (franska) . — Université Paris 7, 1972.

John C. Reynolds. Mot en teori om typstruktur // 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 reflexive and polymorphic types // Arc-et-Senans. — Proc. Konferens om att bevisa och förbättra program, 1975.

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

Luca Cardelli , John C. Mitchell. Operations on Records // Mathematical Structures in Computer Science. - 1991. -1,nummer. 1.

Luca Cardelli , Peter Wegner. Om att förstå typer, dataabstraktion och polymorfism //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 till Standard ML. - Carnegie Mellon University, 1986. - 97 sid. — ISBN PA 15213-3891. (ryska)

John M. Lucassen, David K. Gifford. Integrering av funktionell och imperativ programmering . — 1986.

Luca Cardelli . Grundläggande polymorfisk typkontroll. — 1987.

Mitchell Wand . Komplett typslutning för enkla objekt // In Proc. Andra IEEE-symposiet om logik i datavetenskap. - 1987. -S. 37-44.

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

Luca Cardelli . A Semantics of Multiple Inheritance // Inf. Comput. 76. - 1988. -P. 138-164.

John M. Lucassen, David K. Gifford. Polymorfa effektsystem . — POPL , 1988.

Didier Remy. Typ 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. Formell beskrivning av programmeringskoncept. -s. 431-507.

Robert Harper , Benjamin Pierce. Registrera kalkyl baserat på symmetrisk konkatenering // CMU-CS-90-157R. — Carnegie Mellon University, stödd och övervakad av Naval Research, 1991.

Mitchell Wand . Typ inferens för postsammansättning och multipelt arv // Urval från 1989 IEEE Symposium on Logic in Computer Science. - Information and Computation, 1991. -T. 93,nr. 1. -doi:10.1016/0890-5401(91)90050-C.

Andrew W. Appel. En kritik av Standard ML . — Princeton University, 1992.

Mark P. Jones. En teori om kvalificerade 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 University, ACM , 1992. - S. 154-165 . - doi : 10.1.1.105.7655 .

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

Robert Harper , John C. Mitchell. Om typstrukturen för standard ML. -ACMTOPLAS, 1993. -S. 211-252.

Robert Harper , Mark Lillibridge. Typteoretisk inställning till högre ordningsmodulermed delning . -ACMPress,POPL, 1993. - ISBN CMU-CS-93-197. -doi:10.1.1.14.3595.

Didier Remy. Programmering av objekt med ML-ART: En tillägg till ML med abstrakta och posttyper . - Internationellt symposium om teoretiska aspekter av datorprogramvara, Springer-Verlag, 1994. - P. 321-346 .

JB Wells. Typbarhet och typkontroll i andra ordningens Lambda-kalkyl är likvärdiga och obestämbara // Proceedings of the 9th Annual IEEE . - Symposium on Logic in Computer Science (LIS), 1994. - S. 176-185 .

Robert Harper , . Sammanställning av polymorfism med hjälp av intentionell typanalys. — 1995.

Atsushi Ohori. En Polymorphic Record Calculus och dess sammanställning . - Kyoto University, ACM , 1995. - S. 844-895 .

Mark P. Jones. Funktionell programmering med överbelastning och högre ordningspolymorfism . - Springer-Verlag Lecture Notes, 1995. - doi : 10.1.1.26.9460 .

Didier Remy. Bättre undertyper och radvariabler för posttyper // Presenteras vid workshopen om framsteg inom typer för datavetenskap vid Newton Institute. — Cambridge, Storbritannien, 1995.

Lawrence C. Paulson . ML för den arbetande programmeraren. — 2:a. - Cambridge, Storbritannien: Cambridge University Press, 1996. - 492 s. -ISBN 0-521-57050-6(inbunden), 0-521-56543-X (pocket).

Benedict R. Gaster, Mark P. Jones. Ett polymorfiskt system för utökningsbara poster och varianter // Teknisk rapport NOTTCS-TR-96-3. — University of Nottingham, 1996.

Jacques Garrigue, Didier Remy. Semi-Explicit förstklassig polymorfism för ML // Academic Press. — Information och beräkning, 1997.

M. Sulzmann. Designing Record Systems // Teknisk rapport YALEU/DCS/RR-1128. - Yale University, 1997. - doi : 10.1.1.17.6563 .

Karl Crary, Stephanie Weirich, J. Gregory Morrisett. Intentionell polymorfism i typraderingssemantik . — ICFP , 1998.

Benedict R. Gaster. Poster, varianter och kvalificerade typer // Teknisk rapport NOTTCS-TR-98-3. – Ph.D. Avhandling, 1998.

Jacques Garrigue. Programmering med polymorfa varianter . — Kyoto universitet, 1998.

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

John C. Reynolds. Teorier om programmeringsspråk . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (inbunden), 978-0-521-10697-9 (pocket).

ML2000-arbetsgruppen. Principer och en preliminär design för ML2000 . — 1999.

Benjamin Pierce. Typer och programmeringsspråk . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Översättning till ryska: Benjamin Pierce. Skriver i programmeringsspråk. - Dobrosvet , 2012. - 680 sid. — ISBN 978-5-7913-0082-9 .

John C. Mitchell Begrepp i programmeringsspråk. - Cambridge University Press, 2004. - ISBN 0-511-04091-1 (e-bok i netLibrary); 0-521-78098-5 (inbunden).

Jens Palsberg, Tian Zhao. Typ slutledning för postsammankoppling och subtyping . - 2004. Arkiverad 16 september 2016.

Daan Leijen. Förstklassiga etiketter för utdragbara rader // TechReport UU-CS-2004-51. — Universiteit Utrecht, 2004.

Matthias Blume, Umut A. Acar, Wonseok Chae. Utökningsbar programmering med förstklassiga fodral . — ICFP , 2006.

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

Stephen Weeks. Helprogramskompilering i MLton . - 2006. Arkiverad den 29 juni 2007.

Matthias Blume. Rekord, summor, fall och undantag: Radpolymorfism på jobbet : talvideo. – Microsoft, 2007.

Matthias Blume, Umut A. Acar, Wonseok Chae. Undantagshanterare som utdragbara fall . - Toyota Technological Institute i Chicago, APLAS, 2008.

Wonseok Chae. Typ Safe Extensible Programming // Ph.D. avhandling. — Toyota Technological Institute i Chicago, 2009.

Roman Dusjkin. Monomorfism, polymorfism och existentiella typer . — 2010.

Jeremy Yallop, Leo White. Lättvikts polymorfism av högre slag . — Internationellt symposium om funktionell och logisk programmering, 2014.

Robert Harper . Praktiska grunder för programmeringsspråk. - version 1.37 (reviderad 2014-11-01). - licensierad under Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License., 2012. - 544 sid. Arkiverad24 oktober 2015 påWayback Machine

Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis och Jose P. Magalhães. Ge Haskell en befordran // I förfaranden för den 8:e ACM SIGPLAN-workshopen om typer av språkdesign och -implementering. - NY, USA: TLDI , 2012. - S. 53-66 .

Minsky, Madhavapeddy, Hickey. Real World OKaml: Funktionell programmering för massorna . - O'Reilly Media, 2013. - 510 sid. — ISBN 9781449324766 .
- Översättning till ryska:
  Minsky, Madhavapeddy, Hickey. Programmering i Ocaml-språket . - DMK, 2014. - 536 sid. - ISBN 978-5-97060-102-0 . (ryska)

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

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

Haskell-Wiki: Existentiella typer . (obestämd)

Haskell-Wiki: Rank-N-typer . (obestämd)

Haskell-Wiki: Impredikativa typer . (obestämd)

Jacques Garrigue. OKaml manual: Polymorfa varianter . (obestämd)

Datatyper
Otolkbart	Bit Knapra Byte qubit Behandla Drag Ord
Numerisk	Hela fixpunkt flytpunkt Rationell Komplex Lång intervall
Text	Symbolisk Sträng
Referens	Adress Länk Pekare Omslag
Sammansatt	Algebraisk datatyp ( generisk ) Klass Typ-produkt ( Skriv Tuple struktur ) Ett objekt Konsolidering ( taggat ) Beställt par
abstrakt	array Lista Sväng Stack Associativ array (visning, karta ) Mycket av multiset Typ Graf
Övrig	Logisk Lägre Högre Polymorf Funktionell uppräknad Samling Undantag Genus ( metaklass ) Monad Semafor Flöde tomhet
Relaterade ämnen	Abstrakt datatyp primitiv typ Datastruktur Generisk typ variabel Gränssnitt Konstruktör (OOP) Konstruktör (FP) Typ konstruktör Typ gjutning Prototyp Typ system