Увод у функционално програмирање (3. део)

Аутор: Стефан Ножинић

У претходном делу смо увели нотацију типова, а у овом ћемо се детаљније бавити системима типова. Тип је заправо унија тагованих производа неких других типова, на пример:

data Nat = 0 | 1 | 2 | ...

Дакле овде имамо унију тагова 0, 1, …. али скуп природних бројева можемо дефинисати и овако:

data Nat = 0 | Succ Nat

Дакле природни број може бити или нула или наредни елемент од неког природног броја. На пример:

1 = Succ 0 
2 = Succ 1 = Succ (Succ 0)
...

Скуп целих бројева онда можемо дефинисати као:

data Int = 0 | Succ Int | Pred Int

па је онда:

1 = Succ 0 
-1 = Pred 0 
...

Мотивација за увођење типова се јавља на следећем примеру. Уводимо let … in … израз на следећи начин:

let x = E1 in E2 <=> (λx. E2) E1

Дакле свако појављивање x у изразу Е2 замењујемо са Е1.

Узмимо сада следећи пример:

let f = λx. if x then 5 else 2 in f 5

Овде имамо ситуацију да се број 5 користи за Bool односно проверава се да ли је 5 тачно и ако јесте онда целокупан израз има вредност 5, а ако није онда целокупан израз има вредност 2. Овде наилазимо на проблем што не можемо да тврдимо да ли је 5 еквивалент TRUE или FALSE. На пример, у програмском језику Ц је сваки број осим 0 еквивалент TRUE а 0 је еквивалент FALSE. У другим језицима ово пак не мора да важи и долази до неконзистентности типова. Због овога уводимо систем типова и кажемо да x мора бити типа Bool односно да мора имати или вредност TRUE или FALSE:

data Bool = True | False 
let f :: Bool -> Int 
	f = λx. if x then 5 else 2 
	in f True

Ово можемо написати и без ламбда израза како бисмо лакше разумели нотацију:

let f :: Bool -> Int 
	f x = if x then 5 else 2 
	in f True

Овде смо дефинисали функцију f која пресликава Bool у Int, ово значи да је израз “f x” валидан ако је x типа Bool и да је тип овог израза Int.

Други пример где су типови кључни јесте следећи: да ли следећи израз може да се израчуна?

(λx. x x) (λx. x x)

Да ли бисмо, на било који начин могли да одредимо тип овог израза?

За језик кажемо да је статички типован ако је одређивање типова извршено током превођења. Ово не значи нужно да у коду морамо наводити тип објекта!

Полиморфизам је својство система типова да се дата операција може генерализовати на више различитих типова без потребе да се дата операција имплементира за сваки тип засебно.

За илустрацију овог својства узећемо листу. Листа може бити листа бројева, али исто тако може бити листа слова. Ово значи да тип листа има додатни параметар који одређује тип који садржи листа. Многи језици, на овај или онај начин, ово подржавају. На пример Ц++ има свој темплејтинг систем, а Јава има генеричке класе. За сврху овог чланка, и касније за сврху рада у Хаскелу, ми ћемо рећи да листа прима параметар који одређује тип објекта који листа садржи:

data List a = Empty | Cons a (List a)

Овде смо дефинисали листу као тип који прима параметар, а који одређује тип објекта који листа садржи. Листа је унија два могућа скупа података: празна листа (Empty) или уређеног пара објекта типа а (глава листе) и листе објеката типа а (тело листе, остатак листе).

За лакше објашњавање типова узмимо следећи пример:

twice f x = f (f x)

Сада поставимо услове:

x :: t0 
f :: t1 
f x :: t2 
f (f x) :: t3

Сада доносимо закључке:

twice :: t1 -> t0 -> t3
t1 = t0 -> t2 (zato što f x je tipa t2)
t1 = t2 -> t3 (zbog f (f x))
t0 -> t2 = t2 -> t3 
t0 = t2 = t3
t1 = t0 -> t0

Одавде следи да је тип функције twice: (t0 → t0) → t0 → t0

Други пример је следећи:

conditionalSum cond x y = if cond then x+y else 0

Прво поставимо систем:

0 :: Int 
cond :: t0 
x :: t1 
y :: t2 
+ :: Int -> Int -> Int
x+y :: t3
if ... then ... else ... :: Bool -> t5 -> t5 -> t5
if cond then x+y else 0 :: t4

Сада записујемо закључке:

conditionalSum :: t0 -> t1 -> t2 -> t4 
t1 = t2 = t3 = Int (zbog +)
t5 = Int (zbog else 0)
t5 = t3 (zbog x+y)
t0 = Bool
t4 = t5
conditionalSum :: Bool -> Int -> Int -> Int

Хајде сада да одредимо тип следеће функције и видимо како се на исти начин може доћи до контрадикције:

f x = x + "pera"
x :: t0 
"pera" :: String
+ :: Int -> Int -> Int
x + "pera" :: t1
f :: t0 -> t1

t1 = Int 
t0 = Int 
String = Int <- kontradikcija!

Међутим, ово се може поправити ако се оператор + дефинише као:

+ :: t2 -> t2 -> t2

Онда се добија:

t0 = String = t1 = t2 
f :: String -> String

Касније током овог серијала ћемо директно имплементирати систем типова у Хаскелу, а у наредном делу ћемо увести Хаскел као језик и објаснити његову синтаксу.

Претходни део