Teoria tipurilor
Această intrare sau secțiune despre subiectul teoriilor informatice nu citează sursele necesare sau cei prezenți sunt insuficienți . |
Din punct de vedere mai general, teoria tipurilor este ramura matematicii și logicii care se ocupă cu clasificarea entităților generice, grupându-le în colecții numite tipuri . Din acest punct de vedere există puncte de contact cu noțiunea de tip metafizică . Formularea modernă a teoriei tipurilor a apărut, în parte, dintr-o încercare de a da un răspuns la așa-numitul Paradox al lui Russell și este tratată pe larg în Bertrand Russell și Principia Mathematica de Alfred North Whitehead .
Descriere
Odată cu răspândirea computerelor din ce în ce mai puternică și cu introducerea limbajelor de programare pentru dezvoltarea programelor , teoria tipurilor a găsit un domeniu semnificativ, în special în proiectarea unor astfel de limbaje de programare. În acest context, există mai multe definiții aplicabile unui sistem de tip, dar următoarele, datorită lui Benjamin C. Pierce, sunt probabil cele care adună cel mai mult consens:
- „Un sistem de tip este o metodă sintactică tratabilă care poate demonstra absența anumitor comportamente în programe prin clasificarea expresiilor pe baza naturii valorilor pe care le procesează.”
- ( Tipuri și limbaje de programare , presa MIT, 2002 )
Cu alte cuvinte, un sistem de tip împarte valorile manipulate de programe în seturi numite tipuri - prin efectuarea unei operații numite atribuire sau tastare de tip - și determină sau nu anumite comportamente ale programului în funcție de tipul valorilor. Implicat în aceste comportamente.
De exemplu, să presupunem că un sistem de tip clasifică valoarea ciao ca un șir și valoarea 5 ca un întreg și, pe baza acestor atribuții diferite, interzice programatorului să adauge ciao la 5 . În cadrul acestui sistem, ar fi „ilegal” programarea instrucțiunilor:
-
ciao+5
Avantajul acestei „interdicții” sau imposibilitatea de a face programul să efectueze această operațiune este că nu se va întâmpla niciodată să adăugați șiruri la numere, operație care ar produce rezultate fără sens.
Proiectarea și implementarea unui sistem de tip este un subiect vast și complex, aproape ca limbajul de programare în sine care îl folosește. Creatorii și cărturarii sistemelor de tip merg atât de departe încât să afirme că este însăși esența limbajului:
" Proiectați corect sistemul de tip și veți vedea că limba se va proiecta singură! [ fără sursă ] " |
Este important de reținut că discuția de până acum se referă la tipuri statice . Sistemele de tipuri și limbajele care utilizează tipurile dinamice nu pot verifica a priori că un program folosește corect valorile și, prin urmare, generează o eroare de fiecare dată când programul se comportă astfel încât să le facă o utilizare incorectă. Din acest motiv, conform unora [ este necesară citarea ] , definiția „tip dinamic” este inerent inadecvată. Cu toate acestea, în multe limbaje orientate pe obiecte care utilizează tipuri dinamice, un tip este mai mult decât o interfață și, atâta timp cât clasele partajează interfețe, nu este nevoie să vă faceți griji cu privire la care clasă aparține un anumit obiect.
Elemente conexe
- Paradoxul lui Russell
- Principia Mathematica
- Tip sistem
- Teoria limbajelor de programare
- Teoria tipului intuiționist
linkuri externe
- ( EN ) Tipuri de date abstracte , la nist.gov .
