Polimorfismul parametric

Versiunea actuală a paginii nu a fost încă examinată de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 12 aprilie 2021; verificările necesită 5 modificări .

Polimorfismul parametric în limbaje de programare și teoria tipurilor este o proprietate a semanticii unui sistem de tipuri care vă permite să procesați valori de diferite tipuri într-un mod identic, adică să executați fizic același cod pentru date de diferite tipuri. [1] [2] .

Polimorfismul parametric este considerat forma „adevărată” a polimorfismului [3] , făcând limbajul mai expresiv și crescând foarte mult reutilizarea codului . În mod tradițional, se opune polimorfismului ad-hoc [1] , care oferă o singură interfață la cod potențial diferit pentru diferite tipuri permise într-un context dat, potențial incompatibil ( static sau dinamic ). Într-o serie de calcule, cum ar fi teoria tipurilor calificate , polimorfismul ad-hoc este tratat ca un caz special de polimorfism parametric.

Polimorfismul parametric stă la baza sistemelor de tip de limbaje din familia ML ; astfel de sisteme de tip se numesc polimorfe. În comunitățile de limbi cu sisteme de tip nepolimorfe (descendenții lui Algol și BCPL [4] ), funcțiile și tipurile polimorfe parametric sunt numite „ generalizate ”.

Polimorfism de tip

Termenul „ polimorfism parametric ” este folosit în mod tradițional pentru a se referi la polimorfismul parametric sigur de tip , deși există și forme netipizate ale acestuia (vezi polimorfismul parametric în C și C++ ) [4] . Conceptul cheie al polimorfismului parametric sigur de tip , pe lângă funcția polimorfă , este tipul polimorf .

Un tip polimorf ( ing. tip polimorf ) sau un politip ( ing. politip ) este un tip parametrizat de un alt tip. Un parametru din stratul de tip se numește variabilă de tip (sau variabilă de tip) .

Formal , polimorfismul de tip este studiat în calculul lambda tipizat polimorf , numit Sistem F.

De exemplu, o funcție care appendconcatenează două liste într-una poate fi construită indiferent de tipul elementelor listei. Lăsați variabila tip a să descrie tipul elementelor listei. Apoi funcția appendpoate fi tastată ca " forall a. [a] × [a] -> [a]" (aici construcția [a]înseamnă tipul " o listă, fiecare element având un tipa " - sintaxa adoptată în limbajul Haskell ). În acest caz, se spune că tipul este parametrizat de o variabilă apentru toate valorile a. În fiecare loc de aplicare appenda unor argumente specifice, valoarea aeste rezolvată, iar fiecare mențiune a acesteia în semnătura de tip este înlocuită cu o valoare corespunzătoare contextului de aplicare. Astfel, în acest caz, semnătura tipului funcției necesită ca tipurile de elemente ale ambelor liste și rezultatul să fie identice .

Setul de valori valide pentru o variabilă de tip este dat prin cuantificare . Cele mai simple cuantificatoare sunt universale (ca în exemplul cu append) și existențiale (vezi mai jos).

Un tip calificat este un tip polimorf, echipat suplimentar cu un set de predicate care reglementează intervalul de valori valide pentru un parametru de acest tip. Cu alte cuvinte, calificarea tipului vă permite să controlați cuantificarea într-un mod arbitrar. Teoria tipurilor calificate a fost construită de Mark P. Jones în 1992 [5] . Oferă o rațiune comună pentru cele mai exotice sisteme de tip, inclusiv clase de tip, notații extensibileși subtipuri și permite formularea precisă a constrângerilor specifice pentru anumite tipuri polimorfe, stabilind astfel relația dintre parametrii și ad-hoc. polimorfism ( supraîncărcare ) și între supraîncărcare explicită și implicită. Asocierea unui tip cu un predicat în această teorie senumește dovezi . O algebră similară calculului lambda este formulată pentru dovezi , inclusiv abstracția dovezilor, aplicarea dovezilor etc. Corelarea unui termen al acestei algebre cu o funcție supraîncărcată în mod explicitse numește traducerea dovezilor .

Exemple motivante pentru dezvoltarea unei teorii generalizate au fost clasele de tip Wadler-Blott și tiparea înregistrărilor extensibile prin predicate Harper-Pearce [5] [6] .

Clasificarea sistemelor polimorfe

Sistemele de tip parametric polimorfe se clasifică în mod fundamental în funcție de rang și de proprietatea predicativă . În plus, se disting polimorfismul explicit și implicit [7] și o serie de alte proprietăți. Polimorfismul implicit este furnizat prin inferența de tip , care îmbunătățește foarte mult utilizarea, dar are o expresivitate limitată. Multe limbaje practice polimorfe parametric separă fazele unui limbaj extern tipizat implicit și a unui limbaj intern tipizat explicit .

Cea mai generală formă de polimorfism este „ polimorfismul impredicativ de rang superior ”. Cele mai populare restricții ale acestei forme sunt polimorfismul de rang 1 numit " prenex " și polimorfismul predicativ . Împreună formează „ polimorfismul predicativ preex ” similar cu cel implementat în ML și versiunile anterioare ale lui Haskell .

Pe măsură ce sistemele de tip devin mai complexe, semnăturile de tip devin atât de complexe încât derivarea lor completă sau aproape completă este considerată de mulți cercetători drept o proprietate critică, a cărei absență va face limbajul nepotrivit pentru practică [8] [9] . De exemplu, pentru un combinator tradițional, mapsemnătura completă a tipului (ținând cont de cuantificarea generică ) sub urmărirea fluxului de excepții cu siguranță de tip are următoarea formă [10] [8] (ca mai sus , înseamnă o listă de elemente de tip ):[a]a
$val\;hartă\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 \ dreapta]{\xrightarrow {\gamma }}\left[\beta \right]\;)$

Clasament

Rangul polimorfismului aratăadâncimea de imbricare a cuantificatorilor de variabile de tip permise în cadrul sistemului . „ Polimorfismul rangului k ” (pentru k > 1 ) vă permite să specificați variabile de tip după tipuri polimorfe de rang nu mai mare decât ( k - 1) . „ Polimorfismul rangurilor superioare ” vă permite să puneți cuantificatori de variabile de tip la stânganumăr arbitrar de săgeți în tipuri de ordine superioare .

Joe Wells a demonstrat [ 11] că inferența de tip pentru un Sistem F tip Curry nu este decidabilă pentru rangurile de peste 2, așa că adnotarea de tip explicită trebuie utilizată atunci când se utilizează ranguri mai mari [12] .

Există sisteme de tip inferenţial parţial care necesită adnotare numai variabile de tip nederivabil [13] [14] [15] .

Polimorfism Prenex

Polimorfismul de rang 1 este adesea numit polimorfism prenex (de la cuvântul "prenex" - vezi forma normală prenex ). Într-un sistem polimorf preex , variabilele de tip nu pot fi instanțiate de tipuri polimorfe. Această limitare face distincția între tipurile monomorfe și polimorfe esențială, motiv pentru care în sistemul prenex tipurile polimorfe sunt adesea numite „ scheme de tipare ” ( scheme de tip engleză ) pentru a le distinge de tipurile (monotipuri) „obișnuite” (monomorfe). În consecință, toate tipurile pot fi scrise în forma când toți cuantificatorii de variabile de tip sunt plasați în poziția cea mai exterioară (prenex), care se numește forma normală prenex . Mai simplu spus, definițiile de funcții polimorfe sunt permise, dar funcțiile polimorfe nu pot fi transmise ca argumente altor funcții [16] [17] - funcțiile definite polimorfic trebuie să fie instanțiate monotip înainte de utilizare.

Un echivalent apropiat este așa-numitul „ Let-polimorfism ” sau „ ML - style polymorphism ” de Damas-Milner. Din punct de vedere tehnic, polimorfismul Let în ML are restricții sintactice suplimentare, cum ar fi „ restricția de valoare ” asociată cu probleme de siguranță tip atunci când se utilizează referințe (care nu apar în limbaje pure , cum ar fi Haskell și Clean ) [18] [19] .

Predicativitate

Polimorfism predicativ

Polimorfismul predicativ (condițional) necesită ca o variabilă de tip să fie instanțiată cu un monotip (nu un politip).

Sistemele predicative includ teoria tipurilor intuiționiste și Nuprl .

Polimorfism impredicativ

Polimorfismul impredicativ (necondiționat) vă permite să instanțiați o variabilă de tip cu un tip arbitrar - atât monomorf, cât și polimorf, inclusiv tipul care este definit. (Permiterea, în cadrul unui calcul, unui sistem să se includă recursiv în sine însuși se numește impredicativitate . Potențial, aceasta poate duce la paradoxuri precum Russell sau Cantor [20] , dar acest lucru nu se întâmplă în cazul unui sistem de tip elaborat). [21] .)

Polimorfismul impredicativ vă permite să treceți funcții polimorfe altor funcții ca parametri, să le returnați ca rezultat, să le stocați în structuri de date etc., motiv pentru care este numit și polimorfism de primă clasă . Aceasta este cea mai puternică formă de polimorfism, dar, pe de altă parte, prezintă o problemă serioasă de optimizare și face ca inferența de tip să nu fie rezolvată .

Un exemplu de sistem impredicativ este Sistemul F și extensiile sale (vezi cubul lambda ) [22] .

Suport recursiv

În mod tradițional, în descendenții lui ML , o funcție poate fi polimorfă numai atunci când este privită „din exterior” (adică poate fi aplicată la argumente de diferite tipuri), dar definiția ei poate conține doar recursiune monomorfă (adică rezoluția tipului este făcut înainte de apel). Extinderea reconstrucției de tip ML la tipuri recursive nu prezintă dificultăți serioase. Pe de altă parte, combinația reconstrucției de tip cu termeni definiți recursiv creează o problemă dificilă cunoscută sub numele de recursivitate polimorfă . Mycroft și Meertens au propus o regulă de tipare polimorfă care permite ca apelurile recursive către o funcție recursivă din propriul corp să fie instanțiate cu diferite tipuri. În acest calcul, cunoscut sub numele de calcul Milner-Mycroft, inferența de tip este indecidabilă . [23]

Polimorfism de tip structural

Tipurile de produse (cunoscute și ca „ înregistrări ”) servesc drept bază formală pentru programarea orientată pe obiecte și modulară . Perechea lor duală este alcătuită din tipuri de sume (cunoscute și ca „ variante ”) [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

Împreună, ele reprezintă un mijloc de exprimare a oricăror structuri complexe de date și a unor aspecte ale comportamentului programelor .

Record calculi este o denumire generalizată pentru problema și o serie de soluții ale acesteia privind flexibilitatea tipurilor de produse în limbaje de programare în condiția siguranței tipului [26] [27] [28] . Termenul se extinde adesea la tipurile de sumă, iar limitele conceptului de „ tip de înregistrare ” pot varia de la calcul la calcul (precum și conceptul de „ tip ” însuși). Termenii „ polimorfism de înregistrare ” (care, din nou, include adesea polimorfismul variante ) [27] , „ calcul de modul ” [9] și „ polimorfism structural ” sunt de asemenea utilizați.

Informații generale

Produsele de tip și sumele ( înregistrări și variante [ en ] oferă flexibilitate în construirea structurilor de date complexe, dar limitările multor sisteme de tip real împiedică adesea utilizarea lor să fie cu adevărat flexibilă. Aceste limitări apar de obicei din cauza problemelor de eficiență, deducere a tipului sau pur și simplu de utilizare. [29]

Exemplul clasic este Standard ML , al cărui sistem de tip a fost limitat în mod deliberat doar suficient pentru a combina ușurința de implementare cu expresivitate și siguranța tip demonstrată matematic .

Exemplu de definiție a înregistrării :

> val r = { name = "Foo" , used = true }; (* val r : {nume : șir, folosit : bool} = {nume = „Foo”, folosit = adevărat} *)

Accesul la valoarea câmpului după numele său se realizează printr-o construcție de prefix de forma #field record:

> val r1 = #nume r ; (* val r1 : șir = „Foo” *)

Următoarea definiție a funcției peste înregistrare este corectă:

> fun name1 ( x : { nume : șir , vârstă : int }) = #nume x

Și următoarele generează o eroare de compilator că tipul nu este complet rezolvat :

> fun name2 x = #nume x (* tip nerezolvat în declarație: {name : '1, ...} *)

Monomorfismul înregistrărilor le face inflexibile, dar eficiente [30] : deoarece locația reală de memorie a fiecărui câmp de înregistrare este cunoscută dinainte (la momentul compilării), referirea la acesta prin nume se compilează în indexare directă, care este de obicei calculată într-o singură mașină. instrucție. Cu toate acestea, atunci când dezvoltați sisteme scalabile complexe, este de dorit să puteți abstrage câmpuri din înregistrări specifice - de exemplu, pentru a defini un selector de câmp universal:

fun select r l = #l r

Dar compilarea accesului polimorf la câmpuri care pot fi în ordine diferită în diferite înregistrări este o problemă dificilă, atât din punct de vedere al controlului securității operațiunilor la nivel de limbaj, cât și din punct de vedere al performanței la nivel de cod mașină. O soluție naivă ar putea fi să căutați în mod dinamic dicționarul la fiecare apel (și limbajele de scripting îl folosesc), dar acest lucru este evident extrem de ineficient. [31]

Sumele de tip formează baza expresiei de ramificație și, datorită strictității sistemului de tip, compilatorul asigură controlul asupra completității parsării. De exemplu, pentru următorul tip de sumă :

tipul de date 'a foo = A din 'a | B din ( 'a * 'a ) | C

orice funcție de peste el va arăta ca

bara de distracție ( p : 'a foo ) = cazul p de A x => ... | B ( x , y ) => ... | c => ...

iar când oricare dintre clauze este eliminată, compilatorul va emite un avertisment de analiza incompletă (" match nonexhaustive"). Pentru cazurile în care doar câteva dintre multele opțiuni necesită analiză într-un context dat, este posibil să se organizeze default-ramificarea folosind așa-numita. „Joker” - un eșantion universal, cu care toate valorile valide (în funcție de tastare) sunt comparabile. Este scris cu un caracter de subliniere (" _"). De exemplu:

bara de distracție ( p : 'a foo ) = cazul p de C => ... | _ => ...

În unele limbi (în Standard ML , în Haskell ) chiar și construcția „mai simplă” if-then-elseeste doar zahăr sintactic peste un caz special de ramificare , adică expresia

dacă A atunci B altfel C

deja în stadiul analizei gramaticale este prezentat sub formă

cazul A de adevărat => B | fals => C

cazul A de adevărat => B | _ => C

Zahar sintactic

În Standard ML , înregistrările și variantele sunt monomorfe, totuși, este acceptat zahărul sintactic pentru tratarea înregistrărilor cu mai multe câmpuri, numit „ model universal ” [32] :

> val r = { name = "Foo" , used = true }; (* val r : {nume : șir, folosit : bool} = {nume = „Foo”, folosit = adevărat} *) > val { folosit = u , ...} = r ; (* val u : bool = adevărat *)

O elipsă de {used, ...}tipul „ ” înseamnă că în această înregistrare există și alte câmpuri, în plus față de cele menționate. Cu toate acestea, nu există un polimorfism de înregistrare ca atare (nici măcar preexul ): este necesară rezoluția statică completă a informațiilor de tip de înregistrare monomorfă (prin inferență sau adnotare explicită ).

Extinderea și actualizarea funcțională a înregistrărilor

Termenul de înregistrări extensibile este folosit pentru o desemnare generalizată a unor astfel de operațiuni ca extindere (construirea unei noi înregistrări pe baza uneia existente cu adăugarea de noi câmpuri), tăierea (preluarea unei părți specificate dintr-o înregistrare existentă) etc. În special, implică posibilitatea așa-numitei „ actualizări funcționale a înregistrării ” ( functional record update ) - operațiunea de construire a unei noi valori de înregistrare pe baza celei existente prin copierea denumirilor și tipurilor câmpurilor acesteia, în care unul sau mai multe câmpuri din noua înregistrare primește noi valori care diferă de cele originale (și, eventual, au un alt tip). [33] [34] [19] [35] [36] [37]

Prin ele însele, operațiunile de actualizare și extindere funcționale sunt ortogonale la înregistrarea polimorfismului, dar utilizarea lor polimorfă este de un interes deosebit. Chiar și pentru înregistrările monomorfe, devine important să se poată omite mențiunea explicită a câmpurilor care sunt copiate neschimbate, iar acest lucru reprezintă de fapt polimorfismul înregistrărilor în forma pur sintactică . Pe de altă parte, dacă considerăm toate înregistrările din sistem ca extensibile, atunci acest lucru permite ca funcțiile din înregistrări să fie tipizate ca polimorfe.

Un exemplu de variantă de proiectare cea mai simplă este implementat în Alice ML (conform convențiilor actuale ML succesoare ) [36] . Modelul universal (elipse ) are capacități extinse: poate fi folosit pentru a „captura un rând” pentru a lucra cu partea „rămasă” a înregistrării ca valoare:

> val r = { a = 1 , b = adevărat , c = "bună ziua" } (* r = {a = 1, b = adevărat, c = "bună ziua"} *) > val { a = n , ... = r1 } = r (* r1 = {b=adevărat, c="bună ziua"} *) > val r2 = { d = 3,14 , ... = r1 } (* r2 = {b=adevărat, c="bună ziua ", d=3,14} *)

Actualizarea funcțională este implementată ca o derivată a captării unui rând cu un cuvânt de serviciu where. De exemplu, următorul cod:

> fie val r = { a = 1 , c = 3.0 , d = "nu este o listă" , f = [ 1 ], p = [ "nu este un șir" ], z = NIMIC } în { r unde d = zero , p = „bună ziua” } sfârşit

va fi rescris automat sub forma:

> fie val r = { a = 1 , c = 3.0 , d = "nu este o listă" , f = [ 1 ], p = [ "nu este un șir" ], z = NIMIC } val { d = _, p = _, ... = tmp } = r in { ... = tmp , d = nil , p = "bună ziua" } sfârșit

Înregistrează concatenarea

Una dintre primele (sfârșitul anilor 1980 - începutul anilor 1990 ) a propus diverse opțiuni pentru formalizarea înregistrărilor extensibile prin operații de concatenare pe înregistrări nepolimorfe (Harper-Pearce [38] , Wand [39] , Salzmann [40] ). Cardelli a folosit chiar și operațiuni de înregistrare în loc de polimorfism în limba chihlimbar. Nu există o modalitate cunoscută de a compila eficient aceste calcule; în plus, aceste calcule sunt foarte complexe din punct de vedere al analizei teoretice de tip . [27] [41] [42] [43]

De exemplu [33] :

val mașină = { nume = "Toyota" ; vârstă = „vechi” ; id = 6678 } val truck = { nume = "Toyota" ; id = 19823235 } ... val repaired_truck = { mașină și camion }

polimorfism de rând ) a arătat că moștenirea multiplă poate fi modelată prin concatenarea înregistrărilor [39] [33] .

Subtipări structurale de Cardelli

Luca Cardelli a explorat posibilitatea oficializării „ polimorfismului înregistrărilor ” prin subtiparea relațiilor pe înregistrări: pentru a face acest lucru, o înregistrare este tratată ca un „subtip universal”, adică valoarea sa i se permite să se refere la întregul set de supertipuri. Această abordare acceptă, de asemenea, moștenirea metodei și servește ca fundație teoretică a tipurilor pentru cele mai comune forme de programare orientată pe obiecte . [27] [44] [45]

Cardelli a prezentat o variație a metodei de compilare a polimorfismului înregistrărilor în subtipurile lor prin predefinirea offset-ului tuturor etichetelor posibile într-o structură potențial uriașă cu multe sloturi goale [31] .

Metoda are dezavantaje semnificative. Suportul pentru subtipări în sistemul de tipare complică foarte mult mecanismul de verificare a consistenței tipului [46] . În plus, în prezența sa, tipul static al expresiei încetează să ofere informații complete despre structura dinamică a valorii intrării . De exemplu, când se utilizează numai subtipuri, următorul termen:

> dacă adevărat , atunci { A = 1 , B = adevărat } else { B = fals , C = "Pisică" } (* val it : {B : bool} *)

are tipul {B : bool}, dar valoarea sa dinamică este egală cu {A = 1, B = true}, adică se pierd informații despre tipul înregistrării extinse [43] , ceea ce reprezintă o problemă serioasă pentru verificarea operațiunilor care necesită informații complete despre structura valorii pentru executarea lor (cum ar fi comparaţie pentru egalitate ) [19] . În sfârșit, în prezența subtipurilor, alegerea între reprezentarea ordonată și neordonată a înregistrărilor afectează grav performanța [47] .

Popularitatea subtipării se datorează faptului că oferă soluții simple și vizuale la multe probleme. De exemplu, obiectele de diferite tipuri pot fi plasate într-o singură listă dacă au un supertip comun [48] .

Polimorfismul rândurilor Wanda

Mitchell Wand a propus în 1987 ideea de a capta informații despre partea „rămasă” (nespecificată în mod explicit) a înregistrării prin ceea ce el a numit o variabilă de tip rând ( variabilă de tip rând ) [49] .

O variabilă de rând este o variabilă de tip care rulează printr-un set de seturi finite (rânduri) de câmpuri tipizate (perechi de " (значение : тип)"). Rezultatul este capacitatea de a implementa moștenirea pe lățimea directă peste polimorfismul parametric care stă la baza ML , fără a complica sistemul de tip cu reguli de subtipizare Tipul de polimorfism rezultat se numește polimorfism de rând . Polimorfismul inline se extinde atât la produsele de tipuri , cât și la sumele de tipuri .

Vand a împrumutat termenul din engleză. rând (rând, lanț, linie) din Algol-68 , unde însemna un set de vederi. În literatura în limba rusă, acest termen în contextul lui Algol a fost tradus în mod tradițional ca „multispecie”. Există, de asemenea, o traducere a „variabilelor de rând” ca „variabile de șir” [41] , care poate provoca confuzie cu literele mici din tipurile de șir .

Exemplu ( limbajul OCaml ; sintaxă postfix, record#field) [50] :

# let send_m a = a # m ;; (* valoare send_m : < m : a; .. > -> a = <distractiv> *)

Aici, punctele de suspensie (din două puncte) sunt sintaxa acceptată de OCaml pentru o variabilă de tip inline fără nume . Datorită unei astfel de tastări, funcția send_mpoate fi aplicată unui obiect de orice tip de obiect ( necunoscut anterior ), care include o metodă a msemnăturii corespunzătoare.

Deducerea tipului pentru calculul Wanda în versiunea originală a fost incompletă: din cauza lipsei de restricții privind extinderea seriei, adăugarea unui câmp dacă numele se potrivește va înlocui pe cel existent - ca urmare, nu toate programele au un tip principal [6] [43] . Cu toate acestea, acest sistem a fost prima propunere concretă de extindere a ML cu înregistrări care susțin moștenirea [51] . În anii următori, au fost propuse o serie de îmbunătățiri diferite, inclusiv cele care îl fac complet [51] [27] .

Cea mai notabilă urmă a fost lăsată de Didier Remy ( franceză: Didier Rémy ). El a construit un sistem de tip practic cu înregistrări extensibile, inclusiv un algoritm de reconstrucție a tipului complet și eficient [52] [53] . Remy stratifică limbajul tipurilor în sortare , formulând o algebră sortată de tipuri ( ing. algebră sortată de tipuri, limbaj sortat de tipuri ). Se face o distincție între tipul de tipuri propriu-zis (inclusiv tipurile de câmpuri) și felul de câmpuri ; se introduc mapări între ele şi pe baza lor se formulează regulile de tastare a înregistrărilor extinse ca o simplă extensie a regulilor clasice ML . Informația de prezență a unui câmp este definită ca o mapare de la o sortare de tip la o sortare de câmp . Variabilele de tip rând sunt reformulate ca variabile aparținând sortării câmpului și egale cu constanta de absență , care este un element al sortării câmpului care nu are o potrivire în sortarea tipului . O operație de evaluare a tipului pentru o înregistrare de n câmpuri este definită ca maparea unui câmp n-ary la un tip (unde fiecare câmp din tuplu este fie calculat de funcția de prezență , fie dat de constanta de absență ).

Într-un mod simplificat, ideea de calcul poate fi interpretată ca o extensie a tipului oricărui câmp al înregistrării cu un steag de prezență/absență și reprezentarea înregistrării ca un tuplu cu un slot pentru fiecare câmp posibil [6] . În prototipul de implementare, sintaxa limbajului de tip a fost făcută mai aproape de formularea teoretică a tipurilor , de exemplu [52] :

# let car = { name = "Toyota" ; vârstă = „vechi” ; id = 7866 } ;; (* mașină : ∏ (nume : pre (șir); id : pre (num); vârstă : pre (șir); abs) *) # let truck = { name = "Blazer" ; id = 6587867567 } ;; (* camion : ∏ (nume : pre (șir); id : pre (num); abs) *) # let person = { name = "Tim" ; vârsta = 31 ; id = 5656787 } ;; (* persoană: ∏ (nume: pre (șir); id: pre (num); vârstă: pre (num); abs) *)

(simbolul ∏în Remy înseamnă operația de calcul a tipului)

Adăugarea unui câmp nou se scrie folosind construcția with:

# let driver = { persoana cu vehicul = masina } ;; (* șofer : ∏ (vehicul : pre (∏ (nume : pre (șir); id : pre (num); vârsta : pre (șir); abs)); nume : pre (șir); id : pre (num) ; varsta: pre (numar); abs) *)

Actualizarea funcțională este scrisă identic, cu diferența că menționarea unui câmp deja existent îl înlocuiește:

# let truck_driver = { șofer cu vehicul = camion };; (* șofer camion : ∏ (vehicul : pre (∏ (nume : pre (șir); id : pre (num); abs)); nume : pre (șir); id : pre (num); vârstă : pre (num) ); abs) *)

Această schemă formalizează constrângerea necesară pentru verificarea operațiunilor pe înregistrări și deducerea tipului principal, dar nu conduce la o implementare evidentă și eficientă [6] [43] . Remy folosește hashing, care este destul de eficient în medie, dar crește timpul de rulare chiar și pentru programele monomorfe native și este prost potrivit pentru înregistrări cu multe câmpuri [31] .

Rémy a continuat să exploreze utilizarea polimorfismului inline în combinație cu subtiparea datelor , subliniind că acestea sunt concepte ortogonale și arătând că înregistrările devin cele mai expresive atunci când sunt utilizate împreună [54] . Pe această bază, împreună cu Jérôme Vouillon , a propus o extensie ușoară orientată pe obiecte a ML [55] . Această extensie a fost implementată în limbajul „Caml Special Light” al lui Xavier Leroy , transformându-l în OCaml [56] . Modelul obiect OCaml este strâns împletit cu utilizarea subtipării structurale și a polimorfismului inline [48] , motiv pentru care sunt uneori identificate greșit. Polimorfismul produsului în linie în OCaml este în centrul inferenței de tip ; relațiile de subtipizare nu sunt necesare într-un limbaj acceptat, dar cresc și mai mult flexibilitatea în practică [55] [50] [48] . OCaml are o sintaxă mai simplă și mai descriptivă pentru informațiile de tip.

Jacques Garrigue ( fr. Jacques Garrigue ) a implementat [25] un sistem practic de sume polimorfe . El a combinat munca teoretică a lui Remi și Ohori , construind un sistem care rulează la mijloc: informațiile despre prezența etichetelor într-o înregistrare sunt reprezentate folosind genuri , iar informațiile despre tipurile lor folosesc variabile inline. Pentru ca compilatorul să facă distincția între sumele polimorfe și monomorfe, Garriga folosește o sintaxă specială (backtick, prefix tag). Acest lucru elimină necesitatea unei declarații de tip - puteți scrie imediat funcții pe ea, iar compilatorul va scoate o listă minimă de etichete pe măsură ce aceste funcții sunt compuse. Acest sistem a devenit parte a OCaml în jurul anului 2000 , dar nu în locul lui , ci pe lângă sumele monomorfe , deoarece acestea sunt oarecum mai puțin eficiente și, din cauza incapacității de a controla completitatea analizei , fac dificilă găsirea erorilor (spre deosebire de Bloom soluție ). [25] [57]

Dezavantajele polimorfismului inline al lui Wand sunt neevidența implementării (nu există o singură modalitate sistematică de compilare, fiecare sistem de tip specific bazat pe variabile inline are propria sa implementare) și relația ambiguă cu teoria (nu există o uniformitate). formularea pentru verificarea tipului și inferența , suportul pentru inferență a fost rezolvat separat și a necesitat experimente cu impunerea diverselor restricții) [27] .

Sume translucide Harper-Lilybridge

Cel mai complex tip de înregistrări sunt înregistrările dependente . Astfel de înregistrări pot include tipuri, precum și valori „obișnuite” (tipuri materializate, reificate [9] ), iar termenii și tipurile următoare în ordine în corpul înregistrării pot fi determinate pe baza celor care le preced . Asemenea notații corespund „ sumelor slabe ” ale teoriei tipurilor dependente , cunoscute și sub denumirea de „ existențiale ”, și servesc drept rațiunea cea mai generală pentru sistemele de module din limbaje de programare [58] [59] . Cardelli a considerat [60] tipuri similare în proprietăți ca fiind unul dintre tipurile principale în programarea de tip complet (dar le-a numit „ tupluri ”).

Robert Harper și Mark Lillibridge au construit [61 ] [59] calculul sumelor translucide pentrua justifica formal un limbaj de modul de ordin superior de primă clasă , cel mai avansat sistem de module cunoscut. Acest calcul, printre altele, este folosit în semantica Harper-Stone , care reprezintăjustificarea teoretică a tipului pentru Standard ML .

Sumele translucide generalizează sumele slabe prin etichete și un set de egalități care descriu constructorii de tip . Termenul translucid înseamnă că un tip de înregistrare poate conține atât tipuri cu o structură exportată în mod explicit, cât și cele complet abstracte . Stratul de genuri în calcul are o compoziție clasică simplă: se disting genul de toate tipurile și genurile funcționale ale felului , constructori de tip tastând ( ML nu acceptă polimorfismul în genurile superioare , toate variabilele de tip aparțin genului , iar abstractizarea constructorilor de tip este posibilă numai prin functori [62 ] ). Calculul distinge între regulile de subtipizare pentru înregistrări ca tipuri de bază și pentru câmpurile de înregistrări ca constituenți, respectiv, luând în considerare „subtipurile” și „subcâmpurile”, în timp ce obturarea (abstracția) semnăturilor de câmp este un concept separat de subtipare. Subtiparea aici formalizează maparea modulelor la interfețe . [61] [9] $\star$ ${\displaystyle k_{1}=>k_{2))$ $\star$

Calculul Harper-Lilybridge este indecidibil chiar și în ceea ce privește verificarea coerenței tipului ( dialectele limbajului modulului implementate în Standard ML și OCaml folosesc subseturi limitate ale acestui calcul). Mai târziu, însă, Andreas Rossberg , pe baza ideilor lor, a construit limbajul „ 1ML ”, în care înregistrările tradiționale la nivel de bază ale limbajului și structurile la nivel de modul sunt aceeași construcție de primă clasă [9] (semnificativ mai expresivă decât Cardelli - vezi critica limbajului modulului ML ). Prin încorporarea ideii lui Harper și Mitchell [63] despre subdivizarea tuturor tipurilor în universuri de tipuri „mici” și „mari” (simplificat, aceasta este similară cu diviziunea fundamentală a tipurilor în tipuri simple și agregate, cu reguli de tipare inegale), Rossberg a oferit solubilitate nu numai verificări de consistență , ci și inferență de tip aproape completă . Mai mult, 1ML permite polimorfismul impredicativ [64] . În același timp, limbajul intern în 1ML se bazează pe Sistemul plat F ω și nu necesită utilizarea tipurilor dependente ca metateorie. Începând cu 2015, Rossberg a lăsat deschisă posibilitatea de a adăuga polimorfism inline la 1ML , menționând doar că acest lucru ar trebui să ofere o inferență de tip mai completă [9] . Un an mai târziu, a adăugat [65] polimorfismul efectelor la 1ML .

Calcul polimorf al înregistrărilor Ohori

Atsushi Ohori , împreună cu supervizorul său Peter Buneman , au propus în 1988 ideea de a limita gama de valori posibile ale variabilelor de tip obișnuit în tiparea polimorfă a înregistrărilor în sine . Mai târziu, Ohori a formalizat această idee prin genurile de notație , după ce a construit până în 1995 un calcul cu drepturi depline și o metodă pentru compilarea sa eficientă [19] [30] . Prototipul de implementare a fost creat în 1992 ca o extensie a compilatorului SML/NJ [66] , apoi Ohori a condus dezvoltarea propriului compilator SML# , care implementează dialectul Standard ML cu același nume . În SML# , polimorfismul înregistrărilor servește ca bază pentru încorporarea perfectă a constructelor SQL în programele SML . SML# este folosit de marile companii japoneze pentru a rezolva problemele de afaceri asociate cu bazele de date cu încărcare mare [67] . Un exemplu de astfel de sesiune ( REPL ) [68] :

distracție bogată { Salariul = s , ... } = s > 100000 ; (* val bogat = fn : 'a#{ Salariul:int, ... } -> bool *) distractiv tânăr x = #Vârsta x < 24 ; (* val young = fn : 'a#{ Age:int, ... } -> bool *) distractiv youngAndWealthy x = bogat x și, de asemenea, tânăr x ; (* val youngAndWealthy = fn : 'a#{ Age:int, Salary:int, ... } -> bool *) fun select display l pred = fold ( fn ( x , y ) => if pred x then ( display x ) ::y else y ) l nil ; (* val select = fn : ('a -> 'b) -> 'a list -> ('a -> bool) -> 'b list *) distracție youngAndWealthyEmployees l = selectează #Nume l youngAndWealthy ; (* val youngAndWealthyEmployees = fn : 'b#{ Age:int, Name:'a, Salary:int, ... } list -> 'a list *)

Ohori și-a numit calculul „ polimorfism de înregistrare ” ( polimorfism de înregistrare în engleză ) sau „ calcul de înregistrare polimorf ” ( calcul de înregistrare polimorf în engleză ), subliniind în același timp că el, ca și Wand, consideră polimorfismul nu numai al tipurilor de produse , ci și al tipurilor- sume [27] .

Calculul Ohori se distinge prin utilizarea cea mai intensă a stratului genurilor [6] . În intrare (tip de referință la gen ), simbolul înseamnă fie genul tuturor tipurilor ; sau genul de înregistrări , care are forma , care denotă setul tuturor înregistrărilor care conțin cel puțin câmpurile specificate; sau un gen de variante având forma care denotă ansamblul tuturor tipurilor de variante care conţin cel puţin constructorii specificaţi . În sintaxa plată a limbajului, o constrângere de tip pentru un fel de notație este scrisă ca (vezi exemplele de mai sus). Soluția este oarecum similară cu cuantificarea restrânsă 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#{...}

Singura operație polimorfă oferită de acest calcul este operația de extracție în câmp [69] . Cu toate acestea, Ohori a fost primul care a introdus o schemă de compilare simplă și eficientă pentru polimorfismul de înregistrare [43] . El l-a numit „calcul realizărilor” ( calcul de implementare ). O înregistrare este reprezentată printr-un vector ordonat lexicografic după numele câmpurilor înregistrării originale; adresarea unui câmp după nume se traduce într-un apel la o funcție intermediară care returnează numărul câmpului dat în vectorul dat prin numele solicitat și indexarea ulterioară a vectorului după numărul de poziție calculat. Funcția este apelată numai la instanțierea termenilor polimorfi, ceea ce impune o supraîncărcare minimă la timpul de execuție atunci când se folosește polimorfismul și nu impune nicio supraîncărcare atunci când se lucrează cu tipuri monomorfe. Metoda funcționează la fel de bine cu intrări și variante arbitrar de mari. Calculul oferă inferență de tip și găsește o corespondență puternică cu teoria ( cuantificarea generică este direct legată de indexarea vectorială obișnuită ), fiind o extensie directă a calculului lambda de ordinul doi Girard-Reynolds , care permite diverse proprietăți binecunoscute ale polimorfei. tastarea pentru a fi transferată la înregistrarea polimorfismului [31] .

În practică, suportul pentru variantele polimorfe în SML# nu a fost implementat din cauza incompatibilității sale cu mecanismul de definire a tipului de sumă al Standard ML (necesită separarea sintactică a sumelor și a tipurilor recursive) [70] .

Dezavantajul calculului Ohori este lipsa suportului pentru operațiunile de extindere sau trunchiere a înregistrărilor [27] [71] [43] .

Note Guster-Jones de primă clasă

În teoria tipurilor calificate, înregistrările extensibile sunt descrise prin absența unui câmp ( predicat „lipsește” ) și prezența unui câmp ( predicat „are” ) predicate. Benedict Gaster ( Benedict R. Gaster ) împreună cu autorul teoriei Mark Jones ( Mark P. Jones ) au finalizat-o sub aspectul înregistrărilor extensibile la un sistem tip practic de limbaje implicit tipizate, inclusiv definirea metodei de compilare [6] . Ei inventează termenul de etichete de primă clasă pentru a sublinia capacitatea de a abstrage operațiunile de teren din etichetele cunoscute static. Mai târziu, Gaster și-a susținut disertația [72] despre sistemul construit .

Calculul Gaster-Jones nu oferă o inferență completă de tip . În plus, din cauza problemelor de decidebilitate, a fost impusă o restricție artificială: interdicția seriei goale [73] . Sulzmann a încercat să reformuleze calculul [40] , dar sistemul pe care l-a construit nu poate fi extins pentru a sprijini extinderea înregistrărilor polimorfe și nu are o metodă de compilare universală eficientă [43] .

Daan Leijen a adăugat un predicat de egalitate de rând (sau predicat de egalitate de rând ) la calculul Gaster-Jones și a mutat limbajul seriei în limbajul predicatelor - acest lucru a asigurat inferența completă a tipului și a ridicat interdicția serielor goale [74] . Când sunt compilate, înregistrările sunt convertite într-un tuplu ordonat lexicografic și traducerea dovezilor este aplicată conform schemei Gaster-Jones. Sistemul lui Layen permite exprimarea unor idiomuri precum mesaje de ordin superior (cea mai puternică formă de programare orientată pe obiecte ) și ramuri de primă clasă .

Pe baza acestor lucrări au fost implementate extensii la limbajul Haskell [75] .

Rezultatele lui Gaster-Jones sunt foarte apropiate de cele ale lui Ohori , în ciuda diferențelor semnificative de justificare teoretică de tip , iar principalul avantaj este suportul pentru operațiuni de extindere și trunchiere a înregistrărilor [6] . Dezavantajul calculului este că se bazează pe proprietăți ale sistemului de tip care nu se găsesc în majoritatea limbajelor de programare. În plus, deducerea tipului pentru aceasta este o problemă serioasă, motiv pentru care autorii au impus restricții suplimentare. Și deși Layen a eliminat multe dintre deficiențe, utilizarea ramurii - nu este posibilă. [71]default

Polimorfismul constructului de control

Odată cu dezvoltarea sistemelor software, numărul de opțiuni din tipul sumă poate crește , iar adăugarea fiecărei opțiuni necesită adăugarea unei ramuri corespunzătoare fiecărei funcții peste acest tip, chiar dacă aceste ramuri sunt identice în diferite funcții. Astfel, complexitatea creșterii funcționalității în majoritatea limbajelor de programare depinde neliniar de modificările declarative ale termenilor de referință. Acest model este cunoscut ca problema expresiei . O altă problemă binecunoscută este gestionarea excepțiilor : de-a lungul deceniilor de cercetare asupra sistemelor de tip , toate limbile clasificate ca tip sigur ar putea ieși în continuare prin lansarea unei excepții neprinse - deoarece, în ciuda tastării excepțiilor în sine, mecanismul de ridicare iar manipularea lor nu a fost dactilografiată. În timp ce instrumentele pentru analizarea fluxului de excepții au fost construite, aceste instrumente au fost întotdeauna externe limbajului.

Matthias Blume , un coleg al lui Andrew Appel care lucrează la succesorul proiectului ML [76] ), studentul său absolvent Wonseok Chae și colegul Umut Acar au rezolvat ambele probleme bazate pe produse și sume de dualitate matematică . Întruchiparea ideilor lor a fost limbajul MLPolyR [71] [34] [77] , bazat pe cel mai simplu subset al Standardului ML și completându-l cu mai multe niveluri de siguranță de tip [78] . Wonseok Chai și-a susținut ulterior disertația despre aceste realizări [78] .

Soluția este următoarea. Conform principiului dualității, forma de introducere pentru un concept corespunde formei de eliminare a dualului său [71] . Astfel, forma de eliminare a sumelor (analiza ramurilor) corespunde formei introductive a înregistrărilor. Acest lucru încurajează ramificarea să aibă aceleași proprietăți care sunt deja disponibile pentru intrări - faceți-le obiecte de primă clasă și permiteți extinderea acestora.

De exemplu, cel mai simplu interpret de limbaj de expresie:

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

odată cu introducerea construcției de primă clasă casespoate fi rescrisă ca:

fun eval e = potriviți e cu cazuri `Const i => i | `Plus (e1,e2) => eval e1 + eval e2

după care casespoate fi redat blocul:

fun eval_c eval = cazuri `Const i => i | `Plus (e1,e2) => eval e1 + eval e2 fun eval e = potriviți e cu (eval_c eval)

Această soluție permite default-ramificarea (spre deosebire de calculul Gaster-Jones ), ceea ce este important pentru alcătuirea ramurilor de primă clasă [34] . Completarea compoziției rândului se realizează cu ajutorul cuvântului . nocases

fun const_c d = cazuri `Const i => i implicit : d fun plus_c eval d = cazuri `Plus (e1,e2) => eval e1 + eval e2 implicit : d fun eval e = potriviți e cu const_c (plus_c eval nocases ) fun bind env v1 x v2 = if v1 = v2 then x else env v2 fun var_c env d = cazuri `Var v => env v implicit : d fun let_c eval env d = cazuri `Let (v,e,b) => eval (bind env v (eval env e)) b implicit : d fun eval_var env e = potriviți e cu const_c (plus_c (eval_var env) (var_c env (let_c eval_var env nocases )))

După cum puteți vedea, noul cod, care trebuie adăugat cu complicația calitativă a sistemului, nu necesită schimbarea codului deja scris (funcțiile const_cși plus_c„nu știu nimic” despre adăugarea ulterioară a suportului pentru variabile și letblocuri la interpretul de limbă). Astfel, cazurile extensibile de primă clasă sunt o soluție fundamentală la problema expresiei , permițând să vorbim despre o paradigmă de programare extensibilă [71] [78] . polimorfismul inline , care este deja suportat în sistemul de tip, iar în acest sens, avantajul unei astfel de soluții tehnice este simplitatea sa conceptuală [ 34] .

Cu toate acestea, extinderea sistemelor software necesită și control asupra gestionării excepțiilor care pot fi aruncate la adâncimi arbitrare de imbricare a apelurilor. Și aici Bloom și colegii proclamă un nou slogan de siguranță de tip în dezvoltarea sloganului lui Milner : „ Programele care trec verificarea tipului nu aruncă excepții necontrolate ”. Problema este că, dacă semnătura tipului funcției include informații despre tipurile de excepții pe care această funcție le poate arunca, iar aceste informații din semnătura funcției transmise trebuie să fie strict în concordanță cu informațiile despre parametrul funcției de ordin superior (inclusiv dacă acesta este un set gol) - tastarea mecanismului de gestionare a excepțiilor necesită imediat polimorfismul tipurilor de excepții în sine - în caz contrar, funcțiile de ordin superior nu mai sunt polimorfe. În același timp, într-un limbaj sigur, excepțiile sunt o sumă extensibilă [79] [80] [81] , adică un tip de variantă ai cărui constructori se adaugă pe măsură ce programul progresează. În consecință, siguranța tipului de flux excepțional înseamnă necesitatea de a accepta tipuri de sume care sunt atât extensibile, cât și polimorfe. Din nou, soluția este polimorfismul inline .

Ca și calculul Garriga , MLPolyR folosește o sintaxă specială pentru sumele polimorfe (backtick, etichetă de început) și nu este nevoie de o declarație prealabilă a tipului sum (adică codul de mai sus este întregul program, nu un fragment). Avantajul este că nu există nicio problemă cu analizarea controlului completității: semantica MLPolyR este definită prin conversia într - un limbaj intern de fiabilitate dovedită care nu acceptă nici polimorfism de sumă, nici excepții (ca să nu mai vorbim de excepții neprinse), deci necesitatea acestora. ștergerea în timp de compilare este ea însăși o dovadă a fiabilității. [34]

MLPolyR folosește o combinație non-trivială de mai mulți calculi și translație în două etape. Folosește calculul Remy pentru deducerea tipului și potrivirea tipului , în timp ce utilizează simultan principiul dualității pentru a reprezenta sume ca produse, apoi traduce limba într-un limbaj intermediar tatat explicit cu înregistrări polimorfe și apoi utilizând metoda eficientă de compilare a lui Ohori. . Cu alte cuvinte, modelul de compilare al lui Ohori a fost generalizat pentru a sprijini calculul Remy [69] . La nivel teoretic de tip , Bloom introduce mai multe notații sintactice noi simultan, permițându-ne să scrieți reguli pentru excepții de tastare și ramuri de primă clasă. Sistemul de tip MLPolyR oferă inferență de tip complet , astfel încât autorii au abandonat dezvoltarea unei sintaxe plate pentru scrierea explicită a tipurilor și suport pentru semnături în limbajul modulului .

Sistemul de tip Leyen introduce, de asemenea, o variantă a polimorfismului de ramuri: un construct poate fi reprezentat ca o funcție de ordin superior care primește o intrare de la funcții, fiecare dintre acestea corespunde unei anumite ramuri de calcul ( sintaxa lui Haskell este potrivită pentru această modificare și nu necesită revizuire). De exemplu: case

dataList a = nil :: { } | contra :: { hd :: a , tl :: List a } snoc xs r = caz ( xs invers ) r ultimul xs = snoc xs { nil = \ r -> _ | _ , contra = \ r -> r . hd }

Deoarece înregistrările din sistemul lui Layen sunt extensibile, analiza ramurilor este flexibilă la nivelul deciziilor dinamice (cum ar fi înlănțuirea verificărilor sau utilizarea unui tablou asociativ ), dar oferă o implementare mult mai eficientă (eticheta de variantă corespunde unui offset în înregistrare). Cu toate acestea, suportul implicit de ramificare ( default) trebuie renunțat în acest caz, deoarece un singur defaultmodel s-ar potrivi cu mai multe câmpuri (și, prin urmare, mai multe offset-uri). Leyen numește această construcție „ modele de primă clasă ” ( modele de primă clasă ).

Polimorfismul la genurile superioare

Polimorfismul de tip superior înseamnă abstractizare peste constructori de tip de ordin, adică operatori de tip de formă

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

Suportul pentru această caracteristică duce polimorfismul la un nivel superior, oferind abstracție atât asupra tipurilor, cât și asupra constructorilor de tip , la fel cum funcțiile de ordin superior oferă abstracție atât asupra valorilor, cât și asupra altor funcții. Polimorfismul la genurile superioare este o componentă naturală a multor idiomuri funcționale de programare , inclusiv monade , pliuri și limbaje încorporabile . [62] [82]

De exemplu [62] dacă definiți următoarea funcție ( limba Haskell ):

când b m = dacă b atunci m altfel returnează ()

atunci se va deduce următorul tip funcțional pentru acesta :

când :: forall ( m :: * -> * ) . Monada m => Bool -> m () -> m ()

Semnătura m :: * -> *spune că variabila de tip m este o variabilă de tip aparținând unui tip superior ( variabilă de tip în limba engleză de tip superior ). Aceasta înseamnă că abstractizează constructorii de tip (în acest caz, unary , cum ar fi Maybesau []), care pot fi aplicați unor tipuri concrete, cum ar fi Intsau (), pentru a construi noi tipuri.

În limbile care acceptă abstractizarea tipului complet ( Standard ML , OCaml ), toate variabilele de tip trebuie să fie de gen * , altfel sistemul de tip ar fi nesigur . Polimorfismul în genurile superioare este astfel furnizat de mecanismul de abstractizare în sine, combinat cu adnotarea explicită la instanțiere, ceea ce este oarecum incomod. Cu toate acestea, este posibilă o implementare idiomatică a polimorfismului în genurile superioare, fără a necesita adnotare explicită - pentru aceasta, la nivel de tip este utilizată o tehnică similară defuncționalizării . [62]

Polimorfism generic

Sistemele amabile asigură siguranța sistemelor de tip în sine permițândcontrolul asupra semnificației expresiilor de tip .

De exemplu, să fie necesar să se implementeze în locul tipului obișnuit „ vector ” (matrice liniară) familia de tipuri „ vector de lungimen ”, cu alte cuvinte, să se definească tipul „ vector indexat după lungime ”. Implementarea clasică Haskell arată astfel [83] :

date Zero data Succ n data Vec :: * -> * -> * unde Nil :: Vec a Zero Cons :: a -> Vec a n -> Vec a ( Succ n )

Aici se definesc mai întâi tipurile fantomă [84] , adică tipurile care nu au o reprezentare dinamică. Constructorii Zero și Succservesc ca „valori ale stratului de tip”, iar variabila nimpune inegalitatea diferitelor tipuri de beton construite de constructor Succ. Tipul Veceste definit ca un tip de date algebrice generalizate (GADT).

Soluția presupune în mod condiționat că tipul fantomă nva fi folosit pentru a modela parametrul întreg al vectorului pe baza axiomelor Peano - adică vor fi construite numai expresii precum Succ Zero, Succ Succ Zero, Succ Succ Succ Zeroetc.. Cu toate acestea, deși definițiile sunt scrise în limbaj de tip , ele înșiși sunt formulate în mod netipificat . Acest lucru se vede din semnătura Vec :: * -> * -> *, ceea ce înseamnă că tipurile de beton trecute ca parametri aparțin genului * , ceea ce înseamnă că pot fi orice tip de beton. Cu alte cuvinte, expresiile de tip fără sens ca Succ Boolsau nu sunt interzise aici Vec Zero Int. [83]

Un calcul mai avansat ar permite specificarea mai precisă a intervalului parametrului tip:

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

Dar, de obicei, numai sistemele foarte specializate cu tipuri dependente [85] implementate în limbi precum Agda , Coq și altele au o astfel de expresivitate. De exemplu, din punctul de vedere al limbii Agda , intrarea Vec :: * -> Nat -> *ar însemna că genul unui tip Vec depinde de tip Nat(adică un element de un fel depinde de un element de altul, sortare inferioară ).

În 2012, a fost construită o extensie a limbajului Haskell [83] , care implementează un sistem mai avansat de genuri și face codul de mai sus corect codul Haskell. Soluția este că toate tipurile (sub anumite restricții) sunt automat „ promovate ” ( ing. promovare ) la un nivel superior, formând genuri cu același nume care pot fi utilizate în mod explicit. Din acest punct de vedere, intrarea nu este dependentă - înseamnă doar că al doilea parametru al vectorului trebuie să aparțină genului numit , iar în acest caz singurul element al acestui gen este tipul cu același nume. Vec :: * -> Nat -> *Nat

Soluția este destul de simplă, atât din punct de vedere al implementării în compilator, cât și din punct de vedere al accesibilității practice. Și, deoarece polimorfismul tipului este în mod inerent un element natural al semanticii lui Haskell , promovarea tipului duce la polimorfismul tipului , care mărește reutilizarea codului și oferă un nivel mai ridicat de siguranță a tipului . De exemplu, următorul GADT este utilizat pentru a verifica egalitatea tipului:

date EqReﬂ a b unde Reﬂ :: EqReﬂ a a

are un gen în Haskell clasic * -> * -> *, ceea ce îl împiedică să fie folosit pentru a testa egalitatea de constructori de tip, cum ar fi Maybe. Un sistem de gen bazat pe promovarea tipului deduce un gen polimorfforall X. X -> X -> * , făcând tipul EqReﬂmai generic. Aceasta poate fi scrisă explicit:

date EqReﬂ ( a :: X ) ( b :: X ) unde Reﬂ :: forall X . forall ( a :: X ) . EqReﬂ a a

Polimorfism de efect

Sistemele de efecte au fost propuse de Gifford și Lucassen în a doua jumătate a anilor 1980 [86] [87] [88] cu scopul de a izola efectele secundare pentru un control mai fin asupra siguranței și eficienței în programarea competitivă .

În acest caz , polimorfismul de efect înseamnă cuantificarea purității unei anumite funcții, adică includerea unui steag în tipul funcțional care caracterizează funcția ca pură sau impură. Această extensie de tastare face posibilă abstracția purității funcțiilor de ordin superior din puritatea funcțiilor transmise acestora ca argumente.

Acest lucru este de o importanță deosebită atunci când se trece la funcții peste module ( înregistrări care includ tipuri abstracte ) - functori - deoarece în condițiile de puritate au dreptul să fie aplicative, dar în prezența efectelor secundare trebuie să fie generatoare pentru a asigura siguranța tipului . (pentru mai multe despre aceasta, consultați echivalența tipurilor în limbajul modulului ML ). Astfel, în limbajul modulelor de ordin superior de primă clasă, polimorfismul efectului se dovedește a fi o bază necesară pentru susținerea polimorfismului generativ : trecerea unui steag de puritate unui functor oferă o alegere între semantica aplicativă și generativă într-un singur sistem. [65]

Suport în limbaje de programare

Polimorfismul parametric sigur de tip este disponibil în limbile Hindley-Milner - tipizate - în dialectele ML ( Standard ML , OCaml , Alice , F# ) și descendenții lor ( Haskell , Clean , Idris , Mercury , Agda ) - de asemenea ca și în cele moștenite de la ele limbi hibride ( Scala , Nemerle ).

Tipurile de date generice (generice) diferă de sistemele polimorfe parametric prin faptul că folosesc o cuantificare restricționată și, prin urmare, nu pot avea un rang mai mare de 1 . Sunt disponibile în Ada , Eiffel , Java , C# , D , Rust ; și, de asemenea, în Delphi din versiunea 2009. Au apărut pentru prima dată în CLU .

Polimorfism intensional

Polimorfismul intensional este o tehnică de optimizare a compilării polimorfismului parametric bazată pe analiză complexă teoretică a tipurilor , care constă în calcule pe tipuri în timpul execuției. Polimorfismul intențional permite colectarea gunoiului fără etichetă , transmiterea necutiea argumentelor către funcții și structuri de date plate în casete (optimizate pentru memorie). [89] [90] [91]

Monomorfizare

Monomorfizarea este o tehnică de optimizare a compilării polimorfismului parametric, care constă în generarea unei instanțe monomorfe pentru fiecare caz de utilizare a unei funcții sau tip polimorf. Cu alte cuvinte, polimorfismul parametric la nivelul codului sursă se traduce prin polimorfism ad-hoc la nivelul platformei țintă. Monomorfizarea îmbunătățește performanța (mai precis, face polimorfismul „liber”), dar, în același timp, poate crește dimensiunea codului mașinii de ieșire . [92]

Hindley - Milner

În versiunea clasică , sistemul de tip Hindley-Milner (de asemenea pur și simplu „Hindley-Milner” sau „X-M”, engleză HM ) [93] [94] care stă la baza limbajului ML este un subset al Sistemului F , limitat de predicativ prenex polimorfism pentru a permite inferența automată de tip , pentru care Hindley-Milner a inclus în mod tradițional și așa-numitul „ Algoritm W ” , dezvoltat de Robin Milner .

Multe implementări ale X-M sunt o versiune îmbunătățită a sistemului, reprezentând o „ schemă principală de tastare ” [93] [2] care, într-o singură trecere cu complexitate aproape liniară , deduce simultan cele mai generale tipuri polimorfe pentru fiecare expresie și le verifică strict . acord .

De la începuturile sale , sistemul de tip Hindley-Milner a fost extins în mai multe moduri [95] . Una dintre cele mai cunoscute extensii este suportul pentru polimorfismul ad-hoc prin clase de tip , care sunt generalizate în continuare în tipuri calificate .

Inferența de tip automat a fost considerată o necesitate în dezvoltarea inițială a ML ca sistem interactiv de demonstrare a teoremei „ Logica pentru funcții calculabile ”, motiv pentru care au fost impuse restricțiile corespunzătoare. Ulterior, pe baza ML , au fost dezvoltate o serie de limbaje de uz general compilate eficient , orientate spre programare la scară largă , iar în acest caz, nevoia de a suporta inferența de tip este redusă drastic, deoarece interfețele modulelor în practica industrială trebuie în orice caz să fie adnotate explicit cu tipuri [81 ] . Prin urmare, au fost propuse multe extensii Hindley-Milner care evita inferența de tip în favoarea împuternicirii, până la și inclusiv suport pentru un Sistem F complet cu polimorfism impredicativ , cum ar fi limbajul modular de ordin superior , care sa bazat inițial pe adnotare explicită de tip modul și are multe extensii și dialecte, precum și extensii de limbaj Haskell ( , și ). Rank2TypesRankNTypesImpredicativeTypes

Compilatorul MLton al lui Standard ML monomorfizează , dar datorită altor optimizări aplicabile Standardului ML , creșterea rezultată a codului de ieșire nu depășește 30% [92] .

C și C++

În C, funcțiile nu sunt obiecte de primă clasă , dar este posibil să definiți pointeri de funcție , ceea ce vă permite să construiți funcții de ordine superioară [96] . Polimorfismul parametric nesigur este disponibil și prin trecerea explicită a proprietăților necesare unui tip printr-un subset netipizat al limbajului reprezentat de un pointer netipizat ).comunitateaîn”generic pointer(numit „97][ polimorfismul ad-hoc , deoarece nu modifică reprezentarea pointerului, totuși, este scris explicit pentru a ocoli sistemul de tip al compilatorului [96] . void* void*

De exemplu, funcția standard qsorteste capabilă să manipuleze tablouri de elemente de orice tip pentru care este definită o funcție de comparație [96] .

struct segment { int start ; int end ; }; int seg_cmpr ( struct segment * a , struct segment * b ) { return abs ( a -> sfârşitul - a -> începutul ) - abs ( b -> sfârşitul - b -> începutul ); } int str_cmpr ( char ** a , char ** b ) { return strcmp ( * a , * b ); } struct segment segs [] = { { 2 , 5 }, { 4 , 3 }, { 9 , 3 }, { 6 , 8 } }; char * strs [] = { „trei” , „unu” , „două” , „cinci” , „patru” }; principal () { 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 ); ... }

Totuși, în C este posibil să se reproducă idiomatic polimorfismul parametric tipat fără a utiliza void*[98] .

Limbajul C++ oferă un subsistem șablon care arată ca un polimorfism parametric, dar este implementat semantic printr-o combinație de mecanisme ad-hoc :

șablon < nume tip T > T max ( T x , T y ) { dacă ( x < y ) returnează y ; altfel întoarce x ; } int main () { int a = max ( 10 , 15 ); dublu f = max ( 123,11 , 123,12 ); ... }

Monomorfizarea la compilarea șabloanelor C++ este inevitabilă , deoarece sistemul de tip al limbajului nu are suport pentru polimorfism - limbajul polimorf este aici un add-on static la nucleul limbajului monomorf [99] . Acest lucru duce la o creștere multiplă a cantității de cod de mașină primit , care este cunoscut sub numele de „ cod bloat ” [100] .

Istorie

Notarea polimorfismului parametric ca dezvoltare a calculului lambda (numit calcul lambda polimorf sau Sistem F ) a fost descrisă formal de către logicianul Jean-Yves Girard [101] [102] ( 1971 ), independent de el un similar sistem a fost descris de informaticianul John S. Reynolds [103] ( 1974 ) [104] .

Polimorfismul parametric a fost introdus pentru prima dată în ML în 1973 [41] [105] . Independent de el, tipurile parametrice au fost implementate sub conducerea Barbara Liskov la CLU ( 1974 ) [41] .

Vezi și

Constructor de tip
Gen (teoria tipurilor)
recursivitate polimorfă

Note

↑ 1 2 Strachey, „Concepte fundamentale”, 1967 .
↑ 1 2 Pierce, 2002 .
↑ Cardelli, Wegner, „On Understanding Types”, 1985 , 1.3. Tipuri de polimorfism, p. 6.
↑ 1 2 Appel, „Critica SML”, 1992 .
↑ 1 2 Jones, „Teoria tipurilor calificate”, 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 (Teză de doctorat), 2009 , p. 91-92.
↑ 1 2 3 4 5 6 Rossberg, „1ML - Core and Modules United (F-ing First-class Modules)”, 2015 .
↑ Blume, „Exception Handlers”, 2008 , p. unsprezece.
↑ Wells, 1994 .
↑ Pierce, 2002 , 22 Reconstrucție de tipuri, p. 361.
^ Pierce, 2002 , 23.6 Erasure, typability , and type reconstruction, p. 378-381.
↑ Remy, „ML with abstract and record types”, 1994 .
^ Garrigue, Remy, „Semi-Explicit First-Class Polymorphism for ML”, 1997 .
↑ Reynolds, „Teoriile limbajelor de programare”, 1998 , 17. Polimorfism. Note bibliografice, p. 393.
↑ Polimorfism de primă clasă pe MLton . Consultat la 28 iulie 2016. Arhivat din original la 28 noiembrie 2015. (nedefinit)
↑ Pierce, 2002 , 22.7 Polimorfism via let, p. 354-359.
↑ 1 2 3 4 5 Ohori, „Polymorphic Record Calculus and Its Compilation”, 1995 .
↑ Dușkin, „Monomorfism, polimorfism și tipuri existențiale”, 2010 .
↑ Cardelli, „Programare tip”, 1991 , p. douăzeci.
↑ Pierce, 2002 , 23.10 Impredicativitate, p. 385.
↑ Pierce, 2002 , capitolul 22. Reconstrucție tip. Secțiunea 22.8. Observații suplimentare, p. 361-362.
↑ Wonseok Chae (Teză de doctorat), 2009 , p. paisprezece.
↑ 1 2 3 Garrigue, „Variante polimorfe”, 1998 .
↑ Blume, „Programare extensibilă cu cazuri de primă clasă”, 2006 , p. zece.
↑ 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, p. 3-6.
↑ Leijen, „Etichete de primă clasă”, 2004 , p. unu.
↑ Gaster, Jones, „Polymorphic Extensible Records and Variants”, 1996 , Rezumat, p. unu.
↑ 1 2 Paulson, „ML for the Working Programmer”, 1996 , 2.9 Records, p. 35.
↑ 1 2 3 4 Ohori, „Polymorphic Record Calculus and Its Compilation”, 1995 , 1.2 Compilation Method for Record Polymorphism, p. 6-8.
↑ Harper, „Intro to SML”, 1986 .
↑ 1 2 3 Remy, „Type Inference for Records”, 1991 , p. 2.
↑ 1 2 3 4 5 Blume, „Row polymorphism at work”, 2007 .
↑ Actualizare înregistrări funcționale . Consultat la 30 iunie 2016. Arhivat din original pe 2 iunie 2016. (nedefinit)
↑ 1 2 Îmbunătățiri sintactice Alice ML . Consultat la 30 iunie 2016. Arhivat din original la 27 noiembrie 2016. (nedefinit)
↑ Extensie de înregistrare funcțională și captură de rând . Preluat la 30 iunie 2016. Arhivat din original la 13 august 2016. (nedefinit)
^ Harper, Pierce, „Înregistrarea calculului bazat pe concatenarea simetrică”, 1991 .
↑ 1 2 Wand, „Type inference for record concatenation and multiple heritance”, 1991 .
↑ 12 Sulzmann , 1997 .
↑ 1 2 3 4 Pierce, 2002 , 1.4 Scurtă istorie, p. 11-13.
↑ Remy, „Type Inference for Records”, 1991 , p. 2-3.
↑ 1 2 3 4 5 6 7 Leijen, „Etichete de primă clasă”, 2004 , p. 13-14.
↑ Cardelli, „Semantica moștenirii multiple”, 1988 .
↑ Cardelli, Wegner, „On Understanding Types”, 1985 .
↑ Pierce, 2002 , 16. Subtip metatheory, p. 225.
↑ Pierce, 2002 , 11.8 Înregistrări, p. 135.
↑ 1 2 3 Minsky tradus de DMK, 2014 , Subtyping and inline polymorphism, p. 267-268.
^ Wand, „Type Inference for objects”, 1987 .
↑ 1 2 Minsky tradus de DMK, 2014 , Object Polymorphism, p. 255-257.
↑ 1 2 Remy, „Type Inference for Records”, 1991 , Lucrări conexe, p. 3.
↑ 1 2 Remy, „Type Inference for Records”, 1991 .
↑ Blume, „Programare extensibilă cu cazuri de primă clasă”, 2006 , p. unsprezece.
↑ Remy, „Subtypes and Row polymorphism”, 1995 .
↑ 1 2 Remy, Vouillon, „Obiectiv ML”, 1998 .
↑ Pierce, 2002 , 15.8 Observații suplimentare, p. 223.
↑ Minsky tradus de DMK, 2014 , Variante polimorfe, p. 149-158.
↑ Pierce, 2002 , 24 de tipuri existențiale, p. 404.
↑ 1 2 Reynolds, „Teoriile limbajelor de programare”, 1998 , 18. Module Specification, p. 401-410.
↑ Cardelli, „Programare tip”, 1991 , 4.4. Tipuri de tuplu, p. 20-23.
↑ 1 2 Harper, Lillibridge, „Abordarea teoretică de tip a modulelor de ordin superior cu partajare”, 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, p. 6.
↑ 1 2 Rossberg, „1ML with Special Effects (F-ing Generativity Polymorphism)”, 2016 .
↑ Ohori, „Metoda de compilare pentru calculele de înregistrare polimorfică”, 1992 .
↑ Ohori - SML# (prezentare) (downlink) . Preluat la 30 iunie 2016. Arhivat din original la 27 august 2016. (nedefinit)
↑ Ohori, „Polymorphic Record Calculus and Its Compilation”, 1995 , p. 38.
↑ 1 2 Blume, „Programare extensibilă cu cazuri de primă clasă”, 2006 , p. 9.
↑ Ohori, „Polymorphic Record Calculus and Its Compilation”, 1995 , 5 Implementaion, p. 37.
↑ 1 2 3 4 5 Blume, „Programare extensibilă cu cazuri de primă clasă”, 2006 .
↑ Gaster (Teză de doctorat), 1998 .
↑ Leijen, „Etichete de primă clasă”, 2004 , p. 7.
↑ Leijen, „Etichete de primă clasă”, 2004 .
↑ Înregistrări extensibile pe Haskell-Wiki (link în jos)
↑ Pagina personală Blume . Preluat la 30 iunie 2016. Arhivat din original la 19 mai 2016. (nedefinit)
↑ Blume, „Exception Handlers”, 2008 .
↑ 1 2 3 Wonseok Chae (Teză de doctorat), 2009 .
↑ Paulson, „ML for the Working Programmer”, 1996 , 4.6 Declararea excepțiilor, p. 135.
↑ Harper, „Practical Foundations for Programming Languages”, 2012 , 28.3 Exception Type, p. 258-260.
↑ 1 2 ML2000 Preliminary Design, 1999 .
↑ Harper, „Practical Foundations for Programming Languages”, 2012 , capitolul 22. Constructori și tipuri, p. 193.
↑ 1 2 3 Weirich et al, „Giving Haskell a promotion”, 2012 .
↑ Fluet, Pucella, „Tipuri fantomă și subtipări”, 2006 .
↑ Pierce, 2002 , 30.5 Going Further: Dependent Types, p. 489-490.
^ Gifford, Lucassen, „Sisteme de efecte”, 1986 .
^ Lucassen , Gifford, „Sisteme cu efect polimorf”, 1988 .
↑ Talpin, Jouvelot, 1992 .
^ Harper, Morrisett, „ Intensional Type Analysis”, 1995 .
^ Crary, Weirich, Morrisett, „ Intensional polymorphism”, 1998 .
↑ Pierce, 2002 , 23.2 Varieties of polymorphism, p. 364-365.
↑ 1 2 Weeks, „Compilarea întregului program în MLton”, 2006 .
↑ 1 2 Hindley, „Principal Type Scheme”, 1969 .
↑ Milner, „Teoria polimorfismului de tip”, 1978 .
^ Jones, „FP cu supraîncărcare și polimorfism HO”, 1995 .
↑ 1 2 3 Kernighan B. , Ritchie D. Limbajul de programare C = Limbajul de programare C. - Ed. a II-a. - Williams , 2007. - S. 304. - ISBN 0-13-110362-8 . , Capitolul 5.11. Indicatori de funcție
↑ Appel, „Critica SML”, 1992 , p. 5.
↑ Oleg Kiselyov. Liste cu adevărat polimorfe în C . okmij.org. Consultat la 22 noiembrie 2016. Arhivat din original la 30 ianuarie 2017. (nedefinit)
↑ Mitchell, „Concepte în limbaje de programare”, 2004 , 6.4. Polimorfism și supraîncărcare, p. 145-151.
↑ Scott Meyers . Cod Bloat din cauza șabloanelor . comp.lang.c++.moderat . Usenet (16 mai 2002). Preluat: 19 ianuarie 2010. (nedefinit)
↑ Girard, „Extension of Type Theory”, 1971 .
↑ Girard, „Higher-order calculus”, 1972 .
↑ Reynolds, „Theory of Type Structure”, 1974 .
↑ Pierce, 2002 , 23.3 System F, p. 365-366.
^ Milner și colab., „LCF”, 1975 .

Literatură

Christopher Strachey. Concepte fundamentale în limbaje de programare . - 1967. Arhivat la 12 august 2017.
- Republicat: Christopher Strachey. Concepte fundamentale în limbaje de programare // Calcul de ordin superior și simbolic . - 2000. - T. 13 . - S. 11-49 . - doi : 10.1023/A:1010000313106 .

J Roger Hindley. Schema principală de tip a unui obiect în logica combinatorie // Tranzacții ale Societății Americane de Matematică . - Societatea Americană de Matematică, 1969. - Vol. 146 . - P. 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 (franceză) // Proceedings of the Second Scandinavian Logic Symposium. - Amsterdam, 1971. - P. 63-92 . - doi : 10.1016/S0049-237X(08)70843-7 .

Jean-Yves Girard. Interprétation fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur (franceză) . - Universitatea Paris 7, 1972.

John C. Reynolds. Către o teorie a structurii tipului // Note de curs în informatică . - 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. Conferința privind demonstrarea și îmbunătățirea programelor, 1975.

Robin Milner . O teorie a polimorfismului de tip în programare. - 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. Operații pe înregistrări // Structuri matematice în informatică. - 1991. -1,numărul. 1.

Luca Cardelli , Peter Wegner. Despre înțelegerea tipurilor, abstracției datelor și polimorfismului //ACM Computing Surveys. - New York, SUA:ACM, 1985. -17,nr. 4. -S. 471-523. —ISSN 0360-0300. -doi:10.1145/6041.6042.

Robert Harper . Introducere în Standard ML. - Universitatea Carnegie Mellon, 1986. - 97 p. — ISBN PA 15213-3891. (Rusă)

John M. Lucassen, David K. Gifford. Integrarea programării funcționale și imperative . — 1986.

Luca Cardelli . Verificare de tip polimorfă de bază. — 1987.

Mitchell Wand . Inferență de tip completă pentru obiecte simple // În Proc. Al 2-lea simpozion IEEE privind logica în informatică. - 1987. -P. 37-44.

Martín Abadi, Luca Cardelli , Pierre-Louis Curien. Polimorfismul Parametric Formal . — POPL, 1993.

Luca Cardelli . O semantică a moștenirii multiple // Inf. Calculator. 76. - 1988. -P. 138-164.

John M. Lucassen, David K. Gifford. Sisteme cu efect polimorf . - POPL , 1988.

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

Luca Cardelli . Programare tipul // IFIP de ultimă generație. - New York: Springer-Verlag, 1991. -Iss. Descrierea formală a conceptelor de programare. -P. 431-507.

Robert Harper , Benjamin Pierce. Înregistrați calculul pe baza concatenării simetrice // CMU-CS-90-157R. — Universitatea Carnegie Mellon, susținută și monitorizată de Naval Research, 1991.

Mitchell Wand . Inferență de tip pentru concatenarea înregistrărilor și moștenirea multiplă // Selecții din 1989 IEEE Symposium on Logic in Computer Science. - Informare și calcul, 1991. -T. 93,nr. 1. -doi:10.1016/0890-5401(91)90050-C.

Andrew W. Appel. O critică a ML standard . - Universitatea Princeton, 1992.

Mark P. Jones. O teorie a tipurilor calificate . — 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 simpozion on Principles of programming languages,. - Universitatea din Kyoto, ACM , 1992. - S. 154-165 . - doi : 10.1.1.105.7655 .

J.P. Talpin, P. Jouvelot. Tip polimorf, regiune și inferență de efect // 2(3):245271. — JFP , 1992.

Robert Harper , John C. Mitchell. Despre structura de tip a standardului ML. -ACMTOPLAS, 1993. -S. 211-252.

Robert Harper , Mark Lillibridge. Abordare teoretică tip a modulelorcu partajare . -ACMPress,POPL, 1993. - ISBN CMU-CS-93-197. -doi:10.1.1.14.3595.

Didier Remy. Programarea obiectelor cu ML-ART: O extensie a ML cu tipuri de abstract și de înregistrare . - Simpozionul Internațional privind aspectele teoretice ale software-ului de calculator, Springer-Verlag, 1994. - P. 321-346 .

JB Wells. Tipabilitate și verificarea tipului în calculul lambda de ordinul al doilea sunt echivalente și indecidabile // Proceedings of the 9th Annual IEEE . - Simpozion de logică în informatică (LIS), 1994. - P. 176-185 .

Robert Harper , . Compilarea polimorfismului folosind analiza de tip intensional. — 1995.

Atsushi Ohori. Un calcul de înregistrare polimorfă și compilarea acestuia . - Universitatea din Kyoto, ACM , 1995. - S. 844-895 .

Mark P. Jones. Programare funcțională cu supraîncărcare și polimorfism de ordin superior . - Springer-Verlag Lecture Notes, 1995. - doi : 10.1.1.26.9460 .

Didier Remy. Subtipuri și variabile de rând mai bune pentru tipurile de înregistrări // Prezentat la workshop-ul privind Progresele în tipuri pentru informatică de la Institutul Newton. — Cambridge, Marea Britanie, 1995.

Lawrence C. Paulson . ML pentru programatorul de lucru. — al 2-lea. - Cambridge, Marea Britanie: Cambridge University Press, 1996. - 492 p. -ISBN 0-521-57050-6(copertă cartonată), 0-521-56543-X (copertă cartonată).

Benedict R. Gaster, Mark P. Jones. Un sistem de tip polimorf pentru înregistrări și variante extensibile // Raport tehnic NOTTCS-TR-96-3. - Universitatea din Nottingham, 1996.

Jacques Garrigue, Didier Remy. Polimorfism semi-explicit de primă clasă pentru ML // Academic Press. — Informație și calcul, 1997.

M. Sulzmann. Proiectarea sistemelor de înregistrare // Raport tehnic YALEU/DCS/RR-1128. - Universitatea Yale, 1997. - doi : 10.1.1.17.6563 .

Karl Crary, Stephanie Weirich, J. Gregory Morrisett. Polimorfismul intensional în semantica ștergerii de tip . — ICFP , 1998.

Benedict R. Gaster. Înregistrări, variante și tipuri calificate // Raport tehnic NOTTCS-TR-98-3. — Ph.D. teză, 1998.

Jacques Garrigue. Programare cu variante polimorfe . — Universitatea din Kyoto, 1998.

Didier Rémy, Jérome Vouillon. Objective ML: O extensie eficientă orientată pe obiecte a ML . - Teoria și practica sistemelor de obiecte, ACM , 1998. - V. 4 (1) . - S. 27-50 .

John C. Reynolds. Teorii ale limbajelor de programare . - Cambridge University Press, 1998. - ISBN 978-0-521-59414-1 (copertă cartonată), 978-0-521-10697-9 (copertă).

Grupul de lucru ML2000. Principii și un proiect preliminar pentru ML2000 . — 1999.

Benjamin Pierce. Tipuri și limbaje de programare . - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Traducere în rusă: Benjamin Pierce. Tipuri în limbaje de programare. - Dobrosvet , 2012. - 680 p. — ISBN 978-5-7913-0082-9 .

John C. Mitchell Concepte în limbaje de programare. - Cambridge University Press, 2004. - ISBN 0-511-04091-1 (eBook în netLibrary); 0-521-78098-5 (copertă cartonată).

Jens Palsberg, Tian Zhao. Tastați Inferență pentru concatenarea înregistrărilor și subtipărirea . - 2004. Arhivat la 16 septembrie 2016.

Daan Leijen. Etichete de primă clasă pentru rânduri extensibile // TechReport UU-CS-2004-51. — Universiteit Utrecht, 2004.

Matthias Blume, Umut A. Acar, Wonseok Chae. Programare extensibilă cu cazuri de primă clasă . — ICFP , 2006.

Matthew Fluet, Riccardo Pucella. Tipuri fantomă și subtipări . — JFP , 2006.

Stephen Weeks. Compilarea întregului program în MLton . - 2006. Arhivat la 29 iunie 2007.

Matthias Blume. Înregistrări, sume, cazuri și excepții: polimorfismul rândurilor la locul de muncă : video vorbire. — Microsoft, 2007.

Matthias Blume, Umut A. Acar, Wonseok Chae. Manipulatorii de excepții ca cazuri extensibile . - Institutul Tehnologic Toyota din Chicago, APLAS, 2008.

Wonseok Chae. Tip Safe Extensible Programming // Ph.D. teza. — Institutul tehnologic Toyota din Chicago, 2009.

Roman Dușkin. Monomorfism, polimorfism și tipuri existențiale . — 2010.

Jeremy Yallop, Leo White. Polimorfism ușor de tip superior . — Simpozion internațional de programare funcțională și logică, 2014.

Robert Harper . Baze practice pentru limbaje de programare. - versiunea 1.37 (revizuită la 11.01.2014). - licențiat conform Creative Commons Atribuire-Necomercial-Fără lucrări derivate 3.0 Statele Unite ale Americii Licență., 2012. - 544 p. Arhivatpe 24 octombrie 2015 laWayback Machine

Stephanie Weirich, Brent A. Yorgey, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis și Jose P. Magalhães. Promovarea lui Haskell // În lucrările celui de-al 8-lea Atelier ACM SIGPLAN privind tipurile în proiectarea și implementarea limbajului. - NY, SUA: TLDI , 2012. - S. 53-66 .

Minsky, Madhavapeddy, Hickey. Lumea reală OCaml: Programare funcțională pentru mase . - O'Reilly Media, 2013. - 510 p. — ISBN 9781449324766 .
- Traducere în rusă:
  Minsky, Madhavapeddy, Hickey. Programare în limbajul OCaml . - DMK, 2014. - 536 p. - ISBN 978-5-97060-102-0 . (Rusă)

Andreas Rossberg. 1ML - Core and Modules United (Module de primă clasă F-ing) . — ICFP , 2015.

Andreas Rossberg. 1ML cu efecte speciale (polimorfismul generativității F-ing) . — WadlerFest, Google, 2016.

Haskell-Wiki: tipuri existențiale . (nedefinit)

Haskell-Wiki: tipuri de rang N . (nedefinit)

Haskell-Wiki: Tipuri impredicative . (nedefinit)

Jacques Garrigue. Manual OCaml: Variante polimorfe . (nedefinit)

Tipuri de date
Ininterpretabil	Pic Ciuguli octet qubit Trata Trăsătură Cuvânt
Numeric	Întreg punct fix punctul de plutire Raţional Complex Lung interval
Text	Simbolic Şir
Referinţă	Abordare Legătură Indicator Înveliș
Compozit	Tip de date algebrice ( generic ) Clasă Tip produs ( Scrie Tuplu structura ) Un obiect Consolidare ( etichetat ) Pereche comandată
abstract	matrice Listă Întoarce-te Grămadă Matrice asociativă (afișare, hartă ) Multe multiset Tip Grafic
Alte	Logic Inferior Superior Polimorfă Funcţional enumerabil Colectie Excepție Gen ( Metaclasă ) Monadă Semafor curgere gol
subiecte asemănătoare	Tip de date abstracte tip primitiv Structură de date Generic variabilă de tip Interfață Constructor (OOP) Constructor (FP) Constructor de tip Tip turnare Prototip Tip sistem