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.

Practic: Iata si un term pe care Hugs nu-l poate tipiza corect desi matematic i se poate atribui un tip:

(\ x -> x x) (\ y -> y)

O simpla beta reducere ne-ar arata ca termul este convertibil in

(\y -> y) (\y -> y)

... ceea ce ne duce la: (\y -> y) care are evident tipul a -> a

Iata si ce ar face interpretorul de Haskell (aici Hugs, dar puteti incerca si GHCi pentru a obtine ceva oarecum asemanator):

Prelude> :t (\x -> x x) (\y -> y)
ERROR - Type error in application
*** Expression     : x x
*** Term           : x
*** Type           : a -> b
*** Does not match : a
*** Because        : unification would give infinite type

Prelude> :t (\y -> y) (\y -> y)
(\y -> y) (\y -> y) :: a -> a

Concluzie practica: Uneori nu strica sa faceti o beta reducere unei formule, cu creionul si hartia, inainte de a o introduce intr-un program Haskell. Si la urma urmei ce este nou aici ? Si intr-un limbaj imperativ ati fost invatati - despre anumite compilatoare - ca genereaza cod mai scurt si mai eficient daca scrieti x+y+8 in loc de 3+x+y+5 deci este preferabil sa aduceti expresiiile la o forma mai simpla

Cititi si despre restrictia monomorfica (eng. monomorphism restriction). In esenta ea spune ca nu puteti instantia in aceeasi expresie aceeasi functie polimorfica in doua moduri diferite (adica avand doua tipuri) distincte.

Exemplu preluat din lucrarea de mai jos, a ceea ce nu se poate face:

unusual one_map f g where 
                      g:: Char -> Char
                      f:: Int  -> Int
                      one_map :: (a->b) -> [a] -> [b]
                      unusual m f g = (m f [1,2,4,7] , m g ['A','C','M'] )

In acest caz problema provine din faptul ca in cursul calculului expresiei unusual m f g nu se poate infera un (cel mai mic) tip al lui m deoarece m este folosit odata ca

m :: (Int  -> Int ) -> [Int ] -> [Int]  -- iar a doua oara ca
m :: (Char -> Char) -> [Char] -> [Char]

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'.