Personal tools

Sistemul de inferente de tipuri stabileste singur tipul oricarei expresii ?

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
 
Line 7: Line 7:
 
Vedeti si restrictia monomorfica (eng. [[monomorphism restriction]]).
 
Vedeti si restrictia monomorfica (eng. [[monomorphism restriction]]).
   
  +
----
  +
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):
  +
  +
<haskell>
  +
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
  +
</haskell>
  +
  +
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 e nou aici ? Si intr-un limbaj imperativ ati fost invatati ca
  +
anumite compilatoare genereaza cod mai scurt si mai eficient daca scrieti x+y+8 in loc de 3+x+y+5.
  +
  +
----
 
'''Bibliografie'''
 
'''Bibliografie'''
   

Revision as of 19:09, 10 February 2008


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


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 e nou aici ? Si intr-un limbaj imperativ ati fost invatati ca anumite compilatoare genereaza cod mai scurt si mai eficient daca scrieti x+y+8 in loc de 3+x+y+5.


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