Theses
Theses
Lovro Rožić
Funkcijsko programiranje
Functional Programming
2014
Graduate
Jan Šnajder
Mladen Vuković
PMF-MO
FER2
63
HR
U ovom radu, demonstrirali smo dva osnovna koncepta formalne teorije funkcijskog programiranja: redukciju i tipiziranje. U prvom smo poglavlju, na primjeru netipiziranog λ-računa, proučili svojstva β-redukcije kao osnovnog načina transformacije λ-terma, te dokazali da je takav račun dovoljno moćan da izrazi bilo koju izračunljivu funkciju. U drugom poglavlju cilj je bio, uz definiciju tipova i tipiziranih termi, formalno predstaviti Hindley-Milnerov algoritam. Definirali smo što znači rješiti jednadžbu tipova, a kao korolar Hindley-Milnerovog algoritma demonstrirali smo da je odredivanje tipa nekog terma, u jednostavno tipiziranom λ-raˇcunu a la Curry, izračunljivo. U zadnjem smo poglavlju na manje formalan način pojasnili neke praktične varijante redukcije i tipova, kakve se implementiraju u programske jezike, koristeći pritom jezik Haskell kao primjer. Fokus je bio na polimorfnim tipovima i klasama tipova kao sustavu tipova te na lijenoj redukciji kao načinu reduciranja izraza.
In this work, we have demonstrated two basic concepts of the formal theory of functional languages: reduction and typing. In the first chapter, using the untyped calculus as a basis, we have studied properties of β-reduction as a basic method of transformation of λ-terms, and proved that the untyped λ-calculus is a theory powerful enough to express any computable function. In the second chapter, the goal was to present the Hindley-Milner algorithm in a formal manner, after defining types and typed terms. We defined what it means to solve type equations and, as a corollary of the Hindley-Milner algorithm, proved typing is computable in the case of the simply typed λ-calculus a la Curry. The final chapter was a less formal presentation of some more practical variants of reduction and typing used in programming languages, using the language Haskell as an example. The main focus was on polymorphic types and type-classes, and the call-by-need reduction, concerning type systems and reduction respectively.
28.2.2014