Inferență de tip

Inferență de tip ( eng. inferență de tip ) - în programare , capacitatea compilatorului de a deduce logic tipul valorii expresiei în sine . Mecanismul de inferență de tip a fost introdus pentru prima dată în limbajul ML , unde compilatorul deduce întotdeauna cel mai general tip polimorf pentru orice expresie. Acest lucru nu numai că reduce dimensiunea codului sursă și crește concizia acestuia, dar de multe ori crește reutilizarea codului [1] .

Inferența de tip este caracteristică limbajelor de programare funcționale , deși de-a lungul timpului a fost parțial implementată în limbaje orientate pe obiecte ( C# , D , Visual Basic .NET , Nim , C++11 , Vala , Java [a] ), unde se limitează la capacitatea de a omite tipul unui identificator într-o definiție cu inițializare (vezi zahăr sintactic ). De exemplu:

var s = "Bună, lume!" ; // Tipul variabilei s (din șir) este derivat din inițializator

Algoritmi

Algoritmul Hindley-Milner

Algoritmul Hindley-Milner este un mecanism de inferență de tip expresie implementat în limbaje de programare bazate pe sistemul de tip Hindley-Milner , cum ar fi ML (primul limbaj al acestei familii), Standard ML , OCaml , Haskell , F# , Fortress și Boo . Limbajul Nemerle folosește acest algoritm cu o serie de modificări necesare [2] .

Mecanismul de inferență de tip se bazează pe capacitatea de a deduce automat, integral sau parțial, tipul unei expresii obținute prin evaluarea unei expresii. Deoarece acest proces este efectuat sistematic în timpul traducerii programului, compilatorul poate deseori deduce tipul unei variabile sau funcție fără a specifica în mod explicit tipurile acelor obiecte. În multe cazuri, declarațiile de tip explicite pot fi omise - acest lucru se poate face pentru obiecte destul de simple sau pentru limbaje cu sintaxă simplă. De exemplu, limbajul Haskell are un mecanism de inferență de tip destul de puternic, deci nu este necesar să se specifice tipurile de funcții în acest limbaj de programare. Programatorul poate specifica tipul unei funcții în mod explicit pentru a restricționa utilizarea acesteia la anumite tipuri de date sau pentru formatarea codului sursă mai structurat.

Pentru a obține informații pentru deducerea corectă a tipului unei expresii în absența unei declarații explicite a tipului acestei expresii, traducătorul fie colectează astfel de informații din declarațiile explicite ale tipurilor de subexpresii (variabile, funcții) incluse. în expresia studiată, sau folosește informații implicite despre tipurile de valori atomice. Un astfel de algoritm nu ajută întotdeauna la determinarea tipului unei expresii, mai ales în cazurile de utilizare a funcțiilor de ordin superior și a polimorfismului parametric de natură destul de complexă. Prin urmare, în cazuri complexe, când este nevoie de evitarea ambiguităților, se recomandă specificarea explicită a tipului de expresii.

Modelul de tipare în sine se bazează pe algoritmul de inferență a tipului de expresie, care are ca sursă mecanismul de derivare a tipului de expresie utilizat în λ-calcul tipizat , care a fost propus în 1958 de H. Curry și R. Face. Mai mult, Roger Hindley în 1969 a extins algoritmul în sine și a demonstrat că derivă cel mai general tip de expresie. În 1978 , Robin Milner , independent de R. Hindley, a demonstrat proprietățile unui algoritm echivalent. Și în sfârșit, în 1985 , Louis Damas a arătat în sfârșit că algoritmul lui Milner este complet și poate fi folosit pentru tipurile polimorfe. În acest sens, algoritmul Hindley-Milner este uneori numit și algoritmul Damas-Milner .

Sistemul de tip este definit în modelul Hindley-Milner după cum urmează:

Tipurile primitive sunt tipuri de expresie. $v$
Variabilele de tip parametric α sunt tipuri de expresie.
Dacă și sunt tipuri de expresie, atunci tipul este tipul de expresie. $\sigma _{{1}}$ $\sigma _{{2}}$ $\sigma _{{1}}\rightarrow \sigma _{{2}}$
Un simbol este un tip de expresii. $\bot$

Expresiile ale căror tipuri sunt evaluate sunt definite într-un mod destul de standard:

Constantele sunt expresii.
Variabilele sunt expresii.
Dacă și sunt expresii, atunci ( ) este o expresie. $e_{{1}}$ $e_{{2}}$ $e_{{1}}e_{{2}}$
Dacă este o variabilă și este o expresie, atunci este o expresie. $v$ $e$ $\lambda ve$

Se spune că un tip este o instanță de tip atunci când există o conversie astfel încât: $\sigma _{{1}}$ $\sigma _{{2}}$ $\rho$

$\sigma _{{1}}=\rho (\sigma _{{2}})$

În acest caz, de obicei se presupune că conversiile de tip sunt supuse unor restricții, care sunt următoarele: $\rho$

$\rho (\sigma _{{1}}\rightarrow \sigma _{{2}})=\rho (\sigma _{{1}})\rightarrow \rho (\sigma _{{2}})$
$\rho (v)=v$

Algoritmul de inferență de tip în sine constă din doi pași - generarea unui sistem de ecuații și soluția ulterioară a acestor ecuații.

Construcția unui sistem de ecuații

Construcția unui sistem de ecuații se bazează pe următoarele reguli:

$\Gamma v=\tau$ - dacă legarea este în . $v:\tau$ $\Gamma$
$\Gamma (ge)=\tau$ — dacă , unde și . $\tau _{{1}}=\tau _{{2}}\rightarrow \tau$ $\tau _{1}=\Gamma g$ $\tau _{2}=\Gamma e$
$\Gamma (\lambda ve)=\tau \rightarrow \tau _{e)$ - în cazul în care , unde este cu obligatoriu adăugat . $\tau _{e}=\Gamma 'e$ $\gamma '$ $\Gamma$ $v:\tau$

În aceste reguli, un simbol este un set de asocieri între variabile și tipurile acestora: $\Gamma$

$\Gamma =v_{{1}}:A_{{1}},v_{{2}}:A_{{2}},\ldots ,v_{{n}}:A_{{n}}$

Rezolvarea unui sistem de ecuații

Rezolvarea sistemului construit de ecuații se bazează pe algoritmul de unificare . Acesta este un algoritm destul de simplu. Există o funcție care ia o ecuație de tipuri ca intrare și returnează o substituție care face ca părțile din stânga și din dreapta ale ecuației să fie aceleași („le unifică”). Substituția este pur și simplu o proiecție a tipurilor variabile pe tipurile în sine. Astfel de substituții pot fi calculate în diferite moduri, care depind de implementarea specifică a algoritmului Hindley-Milner. $u$

Vezi și

Note

Comentarii

↑ suport adăugat în Java SE 10

Surse

↑ Andrew W. Appel. O critică a ML standard. — Universitatea Princeton, versiunea revizuită a CS-TR-364-92, 1992.
↑ Michal Moskal. Tip Inferență cu amânare . — 2005.

Link -uri

Implementarea algoritmului Hindley-Milner în Perl
Mesaj de e-mail arhivat de Roger Hindley, explică istoria inferenței tipului
Inferența de tip polimorf de Michael Schwartzbach, oferă o privire de ansamblu asupra inferenței de tip polimorf.
Scheme principale de tip pentru programele funcționale. O copie reformulată a lucrării Damas și Milner care a descris dovezile de soliditate și completitudine.
Tutorial și implementare completă în Standard ML Tutorialul include o parte din istoricul logic al sistemelor de tip, precum și o descriere detaliată a algoritmului așa cum a fost implementat. Unele erori tipografice din lucrarea originală Damas Milner sunt corectate.
Lucrarea de bază de verificare a tipului de Luca Cardelli, descrie algoritmul, include implementarea în Modula-2
Implementarea inferenței de tip Hindley-Milner în Scala , de Andrew Forrest (preluat la 30 iulie 2009)
Implementarea Hindley-Milner în Perl 5, de Nikita Borisov (link indisponibil) . Data accesului: 12 martie 2009. Arhivat din original la 18 februarie 2007. (nedefinit)
Ce este Hindley-Milner? (și de ce este cool?) Explică Hindley-Milner, exemple în Scala
http://fprog.ru/2010/issue5/roman-dushkin-hindley-milner/ Modelul de tastare Hindley-Milner și un exemplu de implementare a acestuia în Haskell