Uvod u funkcionalno programiranje (2. deo)

Autor: Stefan Nožinić

U prethodnom tekstu smo dali uvod u lambda algebre, a u ovom nastavljamo sa kratkim dodatnim teorijskim principima lambda algebre kao i uvodom u algebru tipova.

Uređeni par je struktura koja sadrži dva elementa i pišemo to kao (x,y) gde su x i y neke vrednosti ili funkcije. Uređeni par možemo definisati na sledeći način upotrebom lambda algebre:

PAR = λx y f. f x y

Dakle, ovde je par definisan kao funkcija koja prima dva argumenta i funkciju koja se poziva sa argumentima para. Ovo nam omogućava sledeće:

1. Par možemo definisati kao npr: A = PAR 1 2 i onda je A funkcija koja prima funkciju kojoj će proslediti argumente 1 i 2

2. Prvi element para se može dobiti na sledeći način: PRVI = λp. p TRUE – ovo je moguće jer je TRUE = λx y. x

3. Drugi element para se može analogno definisati kao: DRUGI = λp. p FALSE

Lista se lako može definisati pomoću uređenog para. Prvi element para je glava liste, a drugi se definiše kao ostatak liste.

LISTA = λh t. PAR h t PRAZNO = λx. TRUE PROVERI_PRAZNO = λp. p (λx y. FALSE )

Na primer, lista sa jednim elementom se može definisati kao:

PAR x PRAZNO

Lista sa tri elementa se može definisati kao:

PAR x (PAR y z)

Kao što znamo, u većini jezika u kojima smo programirali, koristili smo tipove podataka. Do sada u lambda algebri nismo govorili o tome šta je kog tipa, niti smo uvodili notaciju tipova. Kada je reč o lambda algebri, postoji mnogo sistema tipova. Sistem tipova je skup pravila koja važe za taj sistem kao aksiomi. Za potrebe ovog serijala, mi ćemo uvesti sopstveni sistem tipova koji je jako sličan onom kojeg ćemo kasnije koristiti u praksi.

Kada definišemo funkciju ili vrednost, pored njene definicije moramo navesti i tip i to na sledeći način:

x : τ

Ovo znači da je x tipa τ. Funkciju koja preslikava objekat tipa τ1 u objekat tipa τ2 zapisujemo ovako:

f : τ1 -> τ2

Ovo samo znači da njen ulaz MORA biti navedenog tipa, a da izlaz MORA isto biti navedenog tipa. Kada imamo funkciju dve promenljive koje su tipa τ1 i τ2, a koja vraća rezultat tipa τ3, onda to zapisujemo kao:

f : τ1 -> τ2 -> τ3

Takođe, uvodimo i sledeću notaciju, ako je hipoteza H zadovoljena, onda je i zaključak Z, i to pišemo kao:

H => Z

Na primer, za prirodne brojeve možemo reći:

0 : N n : N => n+1 : N

Sada možemo definisati neke tipove:

TRUE : B FALSE : B 0 : N n : N => n+1 : N

Od ovih primitivnih tipova možemo praviti kompleksnije tipove i to po sledećim pravilima:

1. τ1 + τ2: je tip koji može imati vrednost iz prvog skupa ili iz drugog (unija, zbir)

2. τ1 * τ2: je tip koji ima dve vrednosti, jedna je iz prvog skupa, a druga iz drugog. Ovo je ekvivalent uređenom paru i zapisujemo ga kao: x : τ1 ⇒ y : τ2 ⇒ (x,y) : τ1 * τ2 – odnosno, ako je x prvog tipa, a y drugog tipa, onda je uređeni par tipa proizvoda dva navedena tipa.

Pored ovoga, definišemo i sledeće tipove:

1. Σ – tip koji ima samo jednu vrednost

2. Θ – tip koji nema nikakvu vrednost i za koji ne postoji objekat koji je ovog tipa.

Uz pomoć primitivnih tipova i ove dve operacije sa tipovima, možemo definisati sve ostale složenije tipove.

U narednom delu ćemo se više baviti algebrom tipova i videti kako se lako opisuju rekurzivne strukture podataka uz pomoć iste.