Sistemul de inferente de tipuri stabileste singur tipul oricarei expresii ?
In conditiile lambda calculului cu tipuri si constante, daca mai adaugam si posibilitatea de a folosi functii polimorfice si ne propunem sa facem inferente de tipuri (deductii de tipuri automate) ajungem la o situatie in care problema verificarii tipurilor (type checking) devine nedecidabila algoritmic. Pentru mai multe detalii se pot consulta lucrari de specialitate (vedeti in bibliografia pdf-ului de mai jos.)
Partea buna este ca in 1969 Hindley si in 1987 Milner au propus independent (?) un sistem de tipuri polimorfice restrictionat (cu cateva ipoteze suplimentare care sunt de fapt restrictii) care pastreaza aproape toata expresivitatea lambda calculului tipizat si pentru care problema inferentelor de tipuri este decidabila. Acest lucru a facut posibila aparitia limbajelor functionale tipizate, in care sistemul de inferente de tipuri asista programatorul, stabilind unde a facut erori de tip. Este adevarat ca exista cativa termeni care nu pot fi tipizati corect in sistemul Hindley-Milner dar sunt niste raritati a caror folosire un programator o poate ocoli.
Vedeti si restrictia monomorfica (eng. monomorphism restriction).
Bibliografie
Cititi printre altele pagina 377 din lucrarea:
Hudak Paul, Conception, Evolution and, Application of Functional Programming Languages ACM Computing Surveys, vol 21, no 3 , Sept 1989 - ar trebui sa fie disponibila in format pdf aici.
Aceast articol poate fi dezvoltat.
Pagina indexata la indexul Categories:Ro
<= Inapoi la pagina principala Ro/Haskell.
<- Inapoi la inceputul paginii 'Intrebarile incepatorului Ro/Haskell'.