Algebarski tipovi podataka

Do sada smo videli kako možemo kreirati nove tipove koristeći newtype konstrukciju. U ovoj lekciji predstavićemo jedan opštiji način kreiranja novih tipova. Prva razlika u ovom načinu kreiranja tipova je ta što se umesto ključne reči newtype koristi data. Definicija tipa T sada će počinjati sa data T = …, a umesto jednog konstruktora od sada ćemo potencijalno imati više konstruktora.

Tipove ćemo kreirati od postojećih tipova koristeći dve operacije: proizvod i sumu. Tipovi koji se dobijaju uz ove dve operacije nazivaju se algebarski tipovi podataka.

Navedene operacije odgovaraju pojmovima Dekartovog proizvoda i unije u teoriji skupova. Kao što ćemo uvideti, sličnost se ne završava na tome: proizvod i suma tipova poštuju zakone poznate iz algebre skupova i algebre prirodnih brojeva¹.

Proizvod

Proizvod dva tipa A i B je tip čije vrednosti odgovaraju kombinacijama vrednosti tipova A i B. Proizvod tipova u Haskelu se jednostavno konstruiše na sledeći način:

data P = MkP A B

Svaka vrednost gore definisanog tipa P, je oblika MkP a b gde su a :: A i b :: B neke vrednosti. Podudaranje oblika dozvoljava da vrednosti tipa P "dekonstruišemo" na ovaj način.

data Vektor = Vektor Float Float deriving (Show)

ghci> v = Vektor 2 1

dužinaVektora :: Vektor -> Float
dužinaVektora (Vektor x y) = sqrt (x**2 + y**2)

ghci> dužinaVektora v
2.23606797749979

Nije nužno postaviti iste tipove u proizvod, niti ih mora biti dva.

data Osoba = Osoba String Int Bool deriving (Show)

imeOsobe :: Osoba -> String
imeOsobe (Osoba ime _ _) = ime

promeniIme :: String -> Osoba -> Osoba
promeniIme novoIme (Osoba _ godine drzavljanin) = Osoba novoIme godine drzavljanin

Zadatak 1. Napisati getere i setere za sva polja vrednosti tipa Vektor i Osoba.

Proizvod tipova može da sadrži i samo jedan tip. U tom slučaju proizvod je ekvivalentan newtype konstrukciji koju smo ranije upoznali.

Uređene \(n\)-torke kao proizvodi tipova

Pažljiv čitalac će uvideti da smo koncept proizvoda tipova već imali kod uređenih \(n\)-torki. I zaista tip Osoba iz prethodnog primera je u nekom smislu ekvivalentan tipu ([Char], Int, Bool). Svaku vrednost tipa Osoba možemo konvertovati u vrednost tipa ([Char], Int, Bool) i obrnuto.

Sličnost nije slučajna, jer uređene \(n\)-torke jesu proizvodi tipova. Na primer, uređen par je apstraktni tip definisan sa data (,) a b = (,) a b. Slično su definisane i druge uređene \(n\)-torke data (,,) a b c = (,,) a b c, data (,,,) a b c d = (,,,) a b c d i tako dalje. Primetimo da tipovi i konstruktori imaju isto ime!

Haskel kompajler dozvoljava da se ovaj konstruktor upotrebljava na malo drugačiji način, pa se može pisati (1, 'a') umesto (,) 1 'a'.

Koliko god ovo delovalo čudno, možemo se zaista uveriti da (,) jeste jedno ime koje dele konstruktor tipa i konstruktor vrednosti:

ghci> :t (,)
(,) :: a -> b -> (a, b)
ghci> :k (,)
(,) :: * -> * -> *

Zadatak 2. Koristeći proizvod tipova (bez korišćenja uređenih parova), definisati tip kompleksnih brojeva Kompleksan oslanjajući se na Double vrednosti. Instancirati Num Kompleksan i Fractional Kompleksan.

Jedinični tip

Konstrukcija proizvoda tipova ima oblik K T₁ T₂ … Tₙ, gde su T₁, ... Tₙ neki tipovi, a K konstruktor. U specijalnom slučaju možemo napraviti proizvod čiji konstruktor ne uzima ni jedan dodatni tip:

data T = K

Konstruktor K je funkcija arnosti 0, odnosno konstanta tipa T. Drugim rečima, tip T sadrži samo jednu vrednost a to je K. Zbog toga za T takođe kažemo da je jedinični tip baš kao za (). Zapravo, tip () je takođe definisan kao prazan proizvod:

data () = ()

Suma

Suma dva tipa A i B je tip koji sadrži vrednosti koje odgovaraju svim vrednostima tipova A i B. Suma tipova može se shvati kao unija dva tipa. Suma tipova se vrši navođenjem više konstruktora razdvojenih vertikalnom crtom. Svaki od konstruktora predstavlja konstruktor proizvoda, i može imati proizvoljno mnogo argumenata.

data SlovoIliBroj = Slovo Char | Broj Int deriving (Show)

ghci> a1 = Slovo 'a'
ghci> a2 = Broj 2
ghci> :t a1
a1 :: SlovoIliBroj
ghci> :t a2
a2 :: SlovoIliBroj

daLiJeSlovo :: SlovoIliBroj -> Bool
daLiJeSlovo (Slovo x) = True
daLiJeSlovo (Broj x) = False

Moguće je "sabrati" više tipova istovremeno, odnosno navesti više od dva konstruktora.

data Dužina = Metar Float | Milja Float | SvetlosnaSekunda Float
                deriving (Show)

uMetre :: Dužina -> Dužina
uMetre (Milja x) = Metar (1609.344 * x)
uMetre (SvetlosnaSekunda x) = Metar (299792458 * x)
uMetre x = x

Napomenimo da poredak konstruktora u sumi nije od značaja. Tako na primer, definicija data SlovoIliBroj = Slovo Char | Broj Int definiše isti² tip kao i definicija data SlovoIliBroj = Broj Int | Slovo Char. Za razliku od toga, u proizvodima poredak tipova je bitan. Tako na primer, definicija data SlovoIBroj = SIB Int Char je sasvim različita od definicije³ data SlovoIBroj = SIB Char Int

Suma jediničnih tipova

Jedinični tipovi nisu mnogo korisni sami po sebi, ali su veoma korisni kada se koriste unutar sume. Na primer, sada lako (i logično) možemo da predstavimo tipove sa konačno mnogo članova (takozvane enumeracije):

data Pol = Muško | Žensko

data ZnakKarte = Herc | Karo | Tref | Pik

data Boje = Crna | Bela | Crvena | Plava | Zelena | Žuta

Do sada smo se susreli sa više tipova koji su suma jediničnih tipova (a da to nismo ni znali):

1. Logički tip Bool je definisan kao suma jediničnih tipova True i False.
2. Tip Ordering je definisan kao suma jediničnih tipova LT, EQ i GT. Podsećamo da se vrednosti ovog tipa koriste kao rezultati poređenja.

data Ruka = Papir | Kamen | Makaze

uporedi :: Ruka -> Ruka -> Ordering
uporedi Kamen  Kamen  = EQ
uporedi Papir  Papir  = EQ
uporedi Makaze Makaze = EQ
uporedi Makaze Papir  = GT
uporedi Kamen  Makaze = GT
uporedi Papir  Kamen  = GT
uporedi _      _      = LT

data Dan = Ponedeljak
    | Utorak
    | Sreda
    | Četvrtak
    | Petak
    | Subota
    | Nedelja 

Zadatak 5. U lekciji o rekurziji pokazan je zadatak sa Hanojskim kulama. U tom zadatku, iskoristili smo tip Char da bismo predstavili različite štapove (\(A\), \(B\) ili \(C\)). Definisati tip Štap koji sadrži tri vrednosti, i prepraviti rešenje pomenutog zadataka tako da se umesto tipa Char koristi novi tip.

Možda-tip

Sada ćemo kreirati tip MoždaBroj kojim možemo da predstavimo ili jedan Float broj ili izostanak bilo kakve smislene vrednosti⁴. Ovaj tip ćemo konstruisati kao sumu tipa Float i jediničnog tipa Ništa:

data MoždaBroj = SamoBroj Float | Ništa 

Tip MoždaBroj je koristan kad god hoćemo da radimo u programu sa nekim vrednostima koje možda nisu ni zadate.

Sa MoždaBroj vrednostima nije lako raditi kao sa Float vrednostima, ali nije ni preteško napisati funkcije koje su nam potrebne:

apsolutnaRazlika :: MoždaBroj -> MoždaBroj -> MoždaBroj
apsolutnaRazlika (SamoBroj x) (SamoBroj y) = SamoBroj $ abs $ x - y
apsolutnaRazlika _ _ = Ništa

podeli :: MoždaBroj -> MoždaBroj -> MoždaBroj
podeli (SamoBroj x) (SamoBroj y) = 
    if y == 0
        then Ništa
        else SamoBroj $ x / y
podeli _ _ = Ništa

Slično tipu MoždaBroj možemo konstruisati⁵ tip MoždaNiska:

data MoždaNiska = SamoNiska String | Ništa

Konstrukcija tipa je MozdaNiska je u potpunosti analogna konstrukciji tipa MoždaBroj. Jasno je da je ovakva konstrukcija korisna za bilo koji tip, stoga možemo definisati naredni apstraktni tip

data Možda t = Samo t | Ništa

Upravo ovako je definisan apstraktni tip Maybe koji je dostupan u Prelidu: data Maybe t = Just t | Nothing. Od sada, svaki tip oblika Maybe a nazivaćemo možda-tip.

Totalne funkcije sa možda tipovima

Možda-tipovi se često koriste da bi se parcijalnim funkcijama pridružile odgovarajuće totalne funkcije. Ideja je da se za one vrednosti domena za koje je funkcija nedefinisana, prosto vrati Nothing vrednost.

maybeHead :: [a] -> Maybe a
maybeHead []  = Nothing
maybeHead x:_ = Just x

Zadatak 8. Definisati totalne varijante funkcija tail, init, last koristeći možda tipove.

Zapisi

Koliko god proizvod tipova delovao korisno, u nekim situacijama pristupanje elementima proizvoda može dovesti do glomaznog i nečitljivog koda.

data Osoba = MkOsoba String String String String Int

punoIme :: Osoba -> String
punoIme (MkOsoba ime prezime _ _ _)
    = ime ++ " " ++ prezime

punaAdresa :: Osoba -> String
punaAdresa (MkOsoba _ _ mesto adresa _)
    = adresa ++ ", " ++ ime

punoletna :: Int -> Osoba -> MyBool
punoletna trenutnaGodina (MkOsoba _ _ _ _ godinaRođenja)
    = trenutnaGodina - godinaRođenja >= 18

Da bi se sprečili problemi opisani u primeru, i olakšao programerima posao, Haskel dozvoljava nešto drugačiju definiciju proizvoda koju nazivamo zapis⁶. U definiciji zapisa svakoj od koordinata se dodeljuje ime - labela, koje se može kasnije iskoristiti za pristupanje toj koordinati. Niz imena koordinata se navodi u vitičastim zagradama.

Nastavljajući priču iz prošlog primera, možemo definisati tip Osoba kao zapis:

data Osoba = MkOsoba {
    ime :: String,
    prezime :: String,
    godinaRođenja :: Int,
    mestoStanovanja :: String,
    adresaStanovanja :: String,
}

Vrednosti tipa Osoba je i dalje moguće konstruisati navođenjem vrednosti nakon konstruktora, ali je moguće i iskorititi sintaksu za zapise:

osoba1 = MkOsoba "Petar" "Petrović" 2000 "Beograd" "Njegoševa"

osoba2 = MkOsoba {
    ime = "Jovana",
    prezime = "Jovanović",
    godinaRođenja = 1990,
    mestoStanovanja = "Novi Sad",
    adresaStanovanja = "Zmaj Jovina",
}

Definisanjem tipa Osoba sintaksom za zapise, zapravo je kreirano šest funkcija ime :: Osoba -> String, prezime :: Osoba -> String, godinaRođenja :: Osoba -> Int, mestoStanovanja :: Osoba -> String, adresaStanovanja :: Osoba -> String. Ove funkcije se nazivaju projekcije, i vraćaju vraćaju odgovarajuće koordinate:

ghci> :t ime
ime :: Osoba -> String
ghci> ime osoba1
"Petar"
ghci> ime osoba2
"Jovana"

Prema tome, labele zapisa se koriste poput getera u objektno orijentisanim jezicima⁷. Što se tiče promene vrednosti koordinate (odnosno setera), to se može izvršiti navođenjem labele sa novom vrednošću koordinate:

ghci> ime osoba1
"Petar"
ghci> osoba3 = osoba1{ime = "Miloš"}
ghci> ime osoba3
"Miloš"

Pri podudaranju oblika, moguće je "uhvatiti" samo labele koje su nam potrebne. Tako bi se funkcije od malopre mogla ovako napisati:

punoIme :: Osoba -> String
punoIme (MkOsoba {ime = ime, prezime = prezime})
    = ime ++ " " ++ prezime

punaAdresa :: Osoba -> String
punaAdresa (MkOsoba {mestoStanovanja = mesto, adresaStanovanja = adresa})
    = mesto ++ ", " ++ adresa

punoletna :: Int -> Osoba -> MyBool
punoletna trenutnaGodina (MkOsoba {godinaRođenja = godinaRođenja})
    = trenutnaGodina - godinaRođenja >= 18

Algebra tipova

U matematici, alegbra⁸ označava disciplinu koja proučava zakonitosti koje važe u formalnim sistemima, pri čemu se te zakonitosti proučavaju i iskazuju kroz algebarske izraze. Na primer, činjenica da je \[(5+2)(5-2) = 25 - 4\] spada u domen aritmetike, dok iskaz \[(m+n)(m-n) = m^2 - n^2\] spada u domen algebre prirodnih brojeva. Ovaj iskaz je tačan za sve prirodne brojeve \(m\) i \(n\), i prethodno navedena činjenica je samo jedna instanca ovog algebarskog zakona. Međutim, algebra je mnogo šira od algebre brojeva. Algebra proučava i apstraktne zakonitosti koje važe sa operacijama nad vektorima, skupovima, funkcijama...

Na primer, algebarski izraz \[(a \circledast b) \circledast c = (c \circledast b) \circledast a\] važi za sve prirodne brojeve \(a\), \(b\) i \(c\) ako operator \(\circledast\) predstavlja sabiranje. Takođe važi i za sve dvodimenzionalne vektore \(a\), \(b\) i \(c\) ako operator \(\circledast\) predstavlja sabiranje vektora. Međutim, važi i za sve rotacije \(a\), \(b\) i \(c\) oko neke ose \(p\) u prostoru, ako \(\circledast\) predstavlja nadovezivanje (odnosno kompoziciju) rotacija. Slično i za skupove i za operaciju unije skupova... U svim navedenim slučajevima, ovaj algebarski zakon ima gotovo isti dokaz i zasniva se na osobinama komutativnosti i asocijativnosti odgovarajuće operacije.

Jednakost tipova

Algebarski zakoni se gotovo uvek navode u obliku jednakosti. Pošto želimo da proučimo algebru tipova, neophodno je prvo razumeti jednakost između tipova.

Sistem tipova u nekom programskim jeziku često spada u kategoriju strukturalnih ili nominativnih tipskih sistema. U strukturalnom tipskom sistemu, dva tipa su jednaka ako je njihova struktura ista (šta god to značilo za taj tipski sistem). Nasuprot tome, u nominativnom (nominalnom) tipskom sistemu dva tipa su jednaka ako su definisana istom definicijom, tj. ako su istog imena. Da bismo shvatili šta ove definicije znače, pogledaćemo zašto sistem tipova u Haskelu zapravo nije ni strukturalan niti nominativan.

Neka su definisani tipovi data A = A Int i data B = B Int. Za ove tipove bismo rekli da imaju potpuno istu strukturu, vrednosti oba tipa su "sačinjena" od jedne celobrojne vrednosti. Ako bi sistem tipova Haskela bio strukturalan, tada ova dva tipa mogla slobodno da se "mešaju", pa bi tako na primer funkcija tipa A -> Bool mogla biti primenjena na vrednost tipa B. Međutim, lako se možemo uveriti da će takva primena dovesti do tipske greške. Prema tome, sistem tipova Haskela nije strukturalan.

Sistem tipova Haskela nije ni nominativan, jer tipski sinonimi definisani sa type A = B, dozvoljavaju da se tipovi A i B mešaju. Na primer, na svakom mestu gde se može koristiti vrednost tipa [Char], može se iskoristiti vrednost tipa String. Prema tome, tipovi različitog imena mogu biti jednaki.

Tačnu definiciju jednakosti tipova ovde ne možemo dati, ali smo kroz prethode redove oslikali neke osobine jednakosti. Sam sistem bismo mogli da okarakterišemo kao nominalan modulo tipski sinonimi. Mi kao korisnici kompajlera i interpretera, možemo smatrati dva tipa u Haskelu jednakim ako ih možemo proizvoljno mešati (koristiti jedan umesto drugog ne uvodeći tipsku greške u kompilaciju). Kako sam kompajler proverava jednakost, ostavljamo za neka kasnija razmatranja.

Izomorfizam skupova

Jednakost tipova koju smo analizirali gora je previše stroga: videli smo da (ako ignorišemo tipske sinonime), tipovi su jednaki samo samim sebi⁹. Zbog toga želimo da uvedemo slabiji pojam jednakosti, takozvani izomorfizam, koji će nam omogućiti da lakše rezonujemo o nekim odnosima između tipova. Definiciju nove relacije uzećemo iz teorije skupova.

Ideja je da skupove sa istim brojem elemenata poistovetimo. Ova ideja bi bila sasvim dobra, ako bismo radili samo sa konačnim skupovima. U matematici mnogi skupovi nisu konačni (kao u ostalom i mnogi tipovi u Haskelu), te je stoga potrebno osmisliti definiciju koja se ne oslanja na pojam broja.

Primetimo da dva konačna skupova imaju isti broj elemenata ako se ti elementi mogu "povezati" tako da je svaki element iz jednog skupa povezan sa tačno jednim elementom iz drugog skupa. Ako ovakvo povezivanje formalizujemo kroz pojam funkcije, tada ćemo taj formalizam moći da koristimo i sa beskonačnim skupovima. Navedena razmišljanja su formalizovana kroz narednu definiciju.

Za skupove \(A\) i \(B\) kažemo da su izomorfni, i pišemo \(A \cong B\) ako postoji bijekcija¹⁰ između ova dva tipa, odnosno ako postoji funkcija \(f\colon A \to B\) sa sledećim osobinama:

1. za svaki element \(b\in B\) postoji element \(a\in A\) takav da je \(f(a) = b\) (osobina surjektivnosti)
2. ako je \(f(a_1) = f (a_2)\) za \(a_1, a_2 \in A\), tada mora važiti \(a_1 = a_2\) (osobina injektivnosti)

Ako bi ove uslove preneli na grafičko prezentovanje funkcija koje smo do sada videli, gde vrednosti tipa predstavljamo kao tačke, a funkciju kao skup strelica između tih tački, tada nam uslov surjektivnosti funkcije \(f\colon A \to B\) govori da je svaka tačka iz \(B\) povezana sa nekom tačkom iz \(A\). Uslov injektivnosti nam govori da ne postoje dve tačke iz \(A\) koje su povezane sa istom tačkom iz \(B\).

Ako je \(f \colon A \to B\) bijekcija, tada za svaki element \(b\in B\) postoji element \(a\in A\) takav da je \(f(a) = b\) (zbog surjektivnosti). Štaviše takav, element mora biti jedinstven zbog injektivnosti. Stoga, možemo definisati funkciju tipa \(B \to A\) koja svakom elementu \(b\in B\) dodeljuje element \(a\in A\) takav da važi \(b= f(a)\). Ovakvu funkciju nazivamo inverzna funkcija funkcije \(f\) i obeležavamo sa \(f^{-1}\). Dakle, ako je \(f(a) = b\) tada je \(f^{-1}(b) = a\). Kombinujući ove dve jednakosti dobijamo da je \(f\left(f^{-1}(b)\right) = b\) i \(f^{-1}\left(f(a)\right)=a\) za sve elemente \(b\in B\) i sve \(a\in A\). Ove jednakosti se mogu zapisati i kao \[f^{-1}\circ f = \operatorname{id}_A \quad {\rm i} \quad f \circ f^{-1} = \operatorname{id}_B,\] gde su \(\operatorname{id}_A\) i \(\operatorname{id}_B\) identičke funkcije na skupovima \(A\) i \(B\) respektivno.

Važi i obrnuto: ako postoje funkcije \(f \colon A \to B\) i \(g \colon B \to A\) takve da je \(g\circ f = \operatorname{id}_A\) i \(f \circ g = \operatorname{id}_B\), onda su ove funkcije bijekcije i jedna drugoj inverzne. Funkcija \(f\) je surjektivna funkcija, jer za proizvoljno \(b\in B\), važi da \(f(g(b)) = \operatorname{id}_B (b) = b\), što znači da \(f\) slika \(g(b)\) u \(b\). Funkcija \(f\) je injektivna, jer ako je \(f(a_1) = f(a_2)\) tada je i \(g(f(a_1)) = g(f(a_2))\) pa je i \(a_1 = a_2\) zbog \(g\circ f = \operatorname{id}_A\). Analogno se dokazuje i da je \(g\) bijekcija.

Navedenim razmatranjem smo dokazali da postoji bijekcija između \(A\) i \(B\) ako i samo ako postoje funkcije \(f \colon A \to B\) i \(g \colon B \to A\) takve da je \(f \circ g = \operatorname{id}_B\) i \(g \circ f = \operatorname{id}_A\). Uslov izomorfizma skupova smo mogli da definišemo koristeći i ovu karakterizaciju, ali smo ovako (dužim putem) videli smisao jednakosti.

Koristeći prethodnu karakterizaciju izomorfnih skupova, možemo lako da dokažemo još neke osobine relacije izomorfnosti. Ako je \(A \cong B\) to znači da postoje funkcije \(f \colon A \to B\) i \(g \colon B \to A\) takve da je \(f \circ g = \operatorname{id}_B\) i \(g \circ f = \operatorname{id}_A\), a samim tim to znači da je \(B \cong A\). Takođe, ako je \(A \cong B\) i \(B \cong C\), sledi da postoje funkcije \(f_1 \colon A \to B\) i \(g_1 \colon B \circ A\) takve da je \(f_1 \circ g_1 = \operatorname{id}_B\) i \(g_1 \circ f_1 = \operatorname{id}_A\) i funkcije \(f_2 \colon B \to C\) i \(g_2 \colon C \to B\) takve da je \(f_2 \circ g_2 = \operatorname{id}_C\) i \(g_2 \circ f_2 = \operatorname{id}_B\). Dalje, važi da je¹¹ \[(g_1 \circ g_2) \circ (f_2 \circ f_1) = g_1 \circ \operatorname{id}_B \circ f_1 = \operatorname{id}_A\] i \[(f_2 \circ f_1) \circ (g_1 \circ g_2) = f_2 \circ \operatorname{id}_A \circ g_2 = \operatorname{id}_B,\] pa je \(A \cong C\), jer funkcije \(f_2 \circ f_1 \colon A \to C\) i \(g_1 \circ g_2 \colon C \to A\) imaju neophodne osobine.

Dakle relacija \(\cong\) poseduje svojstva kakva očekujemo od jednakosti. Svaki skup je izomorfan samom sebi. Ako je \(A\) izomorfan sa \(B\), tada je i \(B\) izomorfan sa \(A\). I, ako je \(A\) izomorfan sa \(B\) i \(B\) izomorfan sa \(C\), tada je i \(A\) izomorfan sa \(C\). Naravno, ovo je sasvim očekivano, jer smo relaciju \(\cong\) definisali tako da za konačne skupove važi \(A \cong B\) ako \(A\) i \(B\) imaju isti broj elementa.

Motivisani skupovima, uvodimo pojam izomorfizma Haskel tipova. Za tipove A i B kažemo da su izomorfni, ako postoje funkcije f :: A -> B i g :: B -> A takve da važi g . f = id i f . g = id. Ako su tipovi A i B izomorfni, to označavamo sa A ≅ B.

Kao i slučaju konačnih skupova, dva tipa sa konačno mnogo vrednosti su izomorfna ako imaju isti broj elementa.

Algebarski zakoni

U narednim redovima ćemo izneti neke zakone algebre prirodnih brojeva, videti koji je pandan tim zakonima u algebri tipova, a zatim i dokazati iznete zakone. Da bi skratili naredne redove, i napravili razliku između algebre brojeva i algebre tipova, uvešćemo skraćeni zapis za sumu i proizvod tipova. Sa A ⊕ B ćemo označiti sumu tipova A i B, a sa A ⊗ B proizvod tipova.

Za sabiranje prirodnih brojeva važi zakon komutativnosti: \(m + n = n + m\) za sve prirodne brojeve \(m\) i \(n\). Ako ovaj zakon "mehanički" prevedemo na algebru tipova dobijamo A ⊕ B ≅ B ⊕ A. Ovaj metaizraz¹² nam govori da je tip definisan sa kodom S1 A | S2 B izomorfan sa tipom definisanim sa S1 B | S2 A¹³. Da bi dokazali ovaj izomorfizam, definišimo narednu funkciju (jedna će biti dovoljna):

data S t1 t2 = S1 t1 | S2 t2

f :: S A B -> S B A
f (S1 a) = S2 a
f (S2 b) = S1 b

g :: S B A -> S A B
g (S1 b) = S2 b
g (S2 a) = S1 a  

Dokažimo da važi g . f = id :: S A B Svaka vrednost x :: S A B je oblika S1 a ili S2 b, gde a :: A i b :: B. Ako je x = S1 a, tada je f x = S2 a, pa je g (f x) = g (S2 a) = S1 a = x. Ako je x = S2 b tada je g (f x) = g (S1 b) = S2 b = x. Dakle, važi g (f x) = x za svako x: S A B, tj. g . f = id :: S A B -> S A B. Na potpuno isti način¹⁴ se dokazuje i jednakost f . g = id :: S B A -> S B A odakle zaključujemo da je S A B ≅ S B A.

Sličnim rezonovanjem se dokazuje i zakon komutativnosti proizvoda A ⊗ B ≅ B ⊗ A.

Određeni brojevi imaju posebna svojstva pri aritmetičkim operacijama. Na primer, broj \(0\) ima osobinu da važi \[0+n = n \quad {\rm i}\quad 0\times n = 0\] za svaki prirodan broj \(n\). Intuitivno deluje da je pandan broju \(0\) tip koji ne sadrži vrednosti, odnosno Void. Direktnim prevođenjem ovih jednakosti, dobijamo izomorfizme Void ⊕ A ≅ A i Void ⊗ A ≅ Void koje je potrebno dokazati.

Sledeći par funkcija dokazuju da je Void ⊕ A ≅ A:

data S t1 t2 = S1 t1 | S2 t2

f :: S Void A -> A
f (S2 a) = a

g :: A -> S Void A
g a = S2 a

Povera izomorfizma je jednostavna: svako x :: S Void A je oblika S2 a za a :: A. Sledi da je g (f x) = g (f (S2 a)) = a = S2 a = x i f (g a) = f (S2 a) = a.

Za dokazivanje Void ⊗ A ≅ Void iskoristićemo naredne funckije:

data P t1 t2 = P t1 t2

f :: P Void A -> Void
f (P v _) = v 

g :: Void -> P Void A
g v = g v

U ovom slučaju dokaz je jednstavan¹⁵: ne postoji vrednost x :: Void te jednakost važi f (g x) = x za sve x :: Void. Isto, postoji vrendost tipa P Void A pa i jednakost g (f x) = x važi uvek za x :: P Void A.

Dakle tip Void se ponaša u algebri tipova onako kako se ponaša broj \(0\) u algebri prirodnih brojeva. Broj \(1\) ima osobinu da je \(1\times n = n\) za sve prirodne brojeve \(n\). Pandan ovom zakonu je () ⊗ A ≅ A, što se dokazuje korišćenjem funkcija:

data P t1 t2 = P t1 t2

f :: P () A -> A
f (P _ a) = a 

g :: A -> P () A
g a = ((), a)

Dokaz za f . g = id i g . f = id nećemo navoditi, jer nije ništa komplikovaniji od prethodnih. Istaknimo da smo ovde umsesto () mogli da iskoristimo bilo koji tip kokji ima jednu vrednost. Štaviše, možemo dokazati nešto opštije tvrđenje: ako je A₁ ≅ A₂ i B₁ ≅ B₂, tada je i A₁ ⊕ B₁ ≅ A₂ ⊕ B₂ i A₁ ⊗ B₁ ≅ A₂ ⊗ B₂.

Zadaci

Zadatak 9. Kreirati algebarski tip podataka Vektor koji predstavlja vektor u trodimenzionalnom prostoru (Koristiti Float tip za koordinate). Kreirati funkcije za sabiranje vektora, množenje vektora skalarem, skalarnog množenja vektora, vektorskog množenja vektora i računanja dužine vektora.

Zadatak 10. Kreirati algebarski tip Valuta koji može da predstavi neke valute (npr, RSD, EUR, USD) i funkcije koje vrše konverziju između ovih valuta. Kreirati algebarski tip Svota koji sadrži jednu vrednost tipa Float i vrednost tipa Valuta. Kreirati algebarski tip Banka koji predstavlja nekoliko domaćih banaka. Kreirati tip Račun koji sadrži vrednost tipa Int (broj računa) i vrednost tipa Banka (predstavlja banku u kojoj je otvoren račun). Tip Račun se koristi samo za identifikaciju, i nema u sebi podatke o promeni računa. Kreirati algebarski tip Transakcija koji sadrži vrednost tipa Svota, a zatim dve vrednosti tipa Račun koje predstavljaju račun sa kog se šalje odnosno na koji se šalje novac. Kreirati jednu proizvoljnu listu Transakcija od 5 članova ili više. Kreirati funkciju promenaNaRačunu:: Račun -> Transakcija -> Svota koja računa promenu stanja računa nakon svih izvršenih transakcija. Pretpostaviti da račun može da prime svote novca u bilo kojoj valuti. Krajnju promenu iskazati u evrima.

Zadatak 11. Kreirati tip Tačka koji predstavlja tačku u dvodimenzionalnoj ravni. Kreirati tip Figura koji može da predstavi pravougaonik, krug, trougao, i proizvoljni pravilni mnogougao u ravni. Kreirati funkcije površina :: Figura -> Float i obim :: Figura -> Obim koje redom računaju površinu i obim figura. Kreirati funkciju transliraj :: (Float, Float) -> Figura -> Figura koja translira (pomera) figuru. Kreirati funkciju skaliraj :: Float -> Figura -> Figura koja skalira figuru za uneti faktor.

Zadatak 12. Kreirati tip KompleksanBroj. Implementirati funkcije koje sabiraju, oduzimaju, množe i dele kompleksne brojeve.

Zadatak 13. Kreirati tip Matrica koji predstavlja matricu dimenzija \(3\times 3\). Kreirati funkcije koje sabiraju matrice, skaliraju matricu, i računaju determinantu matrice. Kreirati tip Vektor koji predstavlja vektor trodimenzionalno prostora. Kreirati funkciju koja množi matricu i vektor.