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

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

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

Уређени пар је структура која садржи два елемента и пишемо то као (x,y) где су x и y неке вредности или функције. Уређени пар можемо дефинисати на следећи начин употребом ламбда алгебре:

PAR = λx y f. f x y

Дакле, овде је пар дефинисан као функција која прима два аргумента и функцију која се позива са аргументима пара. Ово нам омогућава следеће:

1. Пар можемо дефинисати као нпр: A = PAR 1 2 и онда је A функција која прима функцију којој ће проследити аргументе 1 и 2

2. Први елемент пара се може добити на следећи начин: PRVI = λp. p TRUE – ово је могуће јер је TRUE = λx y. x

3. Други елемент пара се може аналогно дефинисати као: DRUGI = λp. p FALSE

Листа се лако може дефинисати помоћу уређеног пара. Први елемент пара је глава листе, а други се дефинише као остатак листе.

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

На пример, листа са једним елементом се може дефинисати као:

PAR x PRAZNO

Листа са три елемента се може дефинисати као:

PAR x (PAR y z)

Као што знамо, у већини језика у којима смо програмирали, користили смо типове података. До сада у ламбда алгебри нисмо говорили о томе шта је ког типа, нити смо уводили нотацију типова. Када је реч о ламбда алгебри, постоји много система типова. Систем типова је скуп правила која важе за тај систем као аксиоми. За потребе овог серијала, ми ћемо увести сопствени систем типова који је јако сличан оном којег ћемо касније користити у пракси.

Када дефинишемо функцију или вредност, поред њене дефиниције морамо навести и тип и то на следећи начин:

x : τ

Ово значи да је x типа τ. Функцију која пресликава објекат типа τ1 у објекат типа τ2 записујемо овако:

f : τ1 -> τ2

Ово само значи да њен улаз МОРА бити наведеног типа, а да излаз МОРА исто бити наведеног типа. Када имамо функцију две променљиве које су типа τ1 и τ2, а која враћа резултат типа τ3, онда то записујемо као:

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

Такође, уводимо и следећу нотацију, ако је хипотеза H задовољена, онда је и закључак Z, и то пишемо као:

H => Z

На пример, за природне бројеве можемо рећи:

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

Сада можемо дефинисати неке типове:

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

Од ових примитивних типова можемо правити комплексније типове и то по следећим правилима:

1. τ1 + τ2: је тип који може имати вредност из првог скупа или из другог (унија, збир)

2. τ1 * τ2: је тип који има две вредности, једна је из првог скупа, а друга из другог. Ово је еквивалент уређеном пару и записујемо га као: x : τ1 ⇒ y : τ2 ⇒ (x,y) : τ1 * τ2 – односно, ако је x првог типа, а y другог типа, онда је уређени пар типа производа два наведена типа.

Поред овога, дефинишемо и следеће типове:

1. Σ – тип који има само једну вредност

2. Θ – тип који нема никакву вредност и за који не постоји објекат који је овог типа.

Уз помоћ примитивних типова и ове две операције са типовима, можемо дефинисати све остале сложеније типове.

У наредном делу ћемо се више бавити алгебром типова и видети како се лако описују рекурзивне структуре података уз помоћ исте.