Definice vlastních typů

• klíčové slovo data

data Nazev_typu = Hodnotove_konstruktory

• Hodnotové konstruktory oddělujeme |
• Nově definovaný typ i hodnotové konstruktory musí začínat velkým písmenem.

Hodnotový konstruktor jako n-ární funkce

• Jmeno Typ1 ... Typn
• data Barva = RBG Int Int Int
• Hodnoty typu Barva:
  • RGB 42 42 42
  • RGB 12 (-23) 45
• Uplatňuje se částečná aplikace hodnotového konstruktoru.

Typové konstruktory

• Nazev_typu je nulární typový konstruktor, typová konstanta.
• N-ární typové konstruktory = -> nebo [] nedefinují typ, pouze předpis jak nový typ vyrobit.

Tvorba typu

• Každá typová konstanta definuje typ.
• Typ získáme také úplnou aplikací n-árních typových konstruktorů na již definované typy.

(->) Dny Bool = Dny -> Bool
[] Dny = [Dny]

Definice polymorfních typových konstruktorů

• Seznam prvků typu a, strom hodnot typu a, … (Polymorfní typové konstruktory)
• data Nazev_typu a1 ... an = ...

Typový konstruktor Maybe

• Předdefinovaný unární polymorfní typový konstruktor.

data Maybe a = Nothing | Just a

• Zamýšlena použití pro funkce, jejichž hodnota může být nedefinována.

Typové aliasy

• type zavádí typový alias k již existujícím typům.
• Používá se pro lepší čitelnost kódu.

type String = [Char]

type Day = Int
type Month = Int
type Year = Int
type Date = (Day, Month, Year)

Rekurze

• Nesprávné použití může vést k nekonečnému vyhodnocování - výpočet cyklí.
• Důležité je si uvědomit, co určuje ,,vzdálenost od středu“ pomyslné spirály.
• 2 části definice: Co je středem spirály (konec rekurze) a jak se k tomuto středu bude výpočet blížit.
• Struktura, podle které se rekurze řídí, musí být dobře založená (well-founded), neexistuje v ní nekonečně dlouhá klesající posloupnost prvků.

Rekurzivní datové struktury

• Rekurzivní datová struktura má základní (bázovou) hodnotu.
• Základní hodnota je rozvíjena rekurzivním pravidlem.
• Mnoho problémů je přirozené řešit s využitím jiné rekurzivně definované struktury - binárního stromu. (Nelineární rekurzivní datová struktura.)

Binární strom

Rekurzivní definice binárního stromu

• Prázdný strom je binární strom.
• Hodnota a k asociovaný levý a pravý binární strom je binární strom.
• Kořen
• Vnitřní vrcholy
• Listy = oba podstromy jsou prázdné
• Podstrom

Definice datového typu

data BinTree a = Empty | Node a (BinTree a) (BinTree a)

-- Příklad hodnoty defiovaného typu
tc :: BinTree Char
tc = Node 'e'
	(Node 'i' Empty (Node 'c' Empty Empty))
	(Node 'j' (Node 'd' Empty Empty)
		(Node 'r' Empy Empty))

-- Práce s rekurzivními datovými strukturami
-- Pomocí rekurze
treeP1 :: Num a => BinTree a -> BinTree a
treeP1 Empty = Empty
treeP1 (Node x left right)
	= Node (x+1) (treeP1 left) (treeP1 right)

Dokazování správnosti programů

Důkaz korektnosti algoritmu

• Dokazujeme, že pokud výpočet algoritmu na platných vstupech skončí, tak algoritmus vrací korektní výsledek. o algoritmu, který má tuto vlastnost říkáme, že je částečně správný.
• Pokud je algoritmus částečně správný a dokážeme, že na platných vstupech svůj výpočet vždy skončí, pak říkáme, že algoritmus je úplně správný.