Haskell a funkcionální programování (5)

Samotný Haskell je čistě funkcionální programovací jazyk. Proto v něm platí, že výsledek funkce závisí pouze na jejích argumentech. Naproti tomu vstupně/výstupní operace tuto vlastnost nemají. Z tohoto důvodu jsou akce čtení a zápisu odděleny od zbytku programu. Celý vstupně/výstupní sytém Haskellu je založen na matematické teorii tzv. monád. Její pochopení ale (naštěstí) není pro praktické použití nutné. Jak poznamenávají autoři jednoho dokumentu, porozumění teorii monád není pro provádění vstupně/výstupních operací o nic víc důležitější, než znalost teorie grup k provádění základní aritmetiky. S tímto konstatováním tedy můžeme na monády zapomenout.

Jelikož i vstupně/výstupní akce (dále jen akce) jsou funkcemi, musí vracet nějaký výsledek. Aby se však daly odlišit od běžných funkcí, mají akce návratové hodnoty označeny navíc typem IO. Jako příklad může posloužit signatura typu funkce načítající znak

getChar :: IO Char

U některých (výstupních) akcí není výsledná hodnota většinou zajímavá nebo užitečná, a proto se typ výsledku označuje (). Příkladem je opak funkce předchozí – výpis znaku

putChar :: Char -> IO ()

Obvyklá posloupnost při práci z daty je načtení, zpracování a vypsání výsledku. Aby bylo možné takovéto sekvence provádět jednoduše, definuje Haskell syntaktickou konstrukci uvozenou klíčovým slovem do. Za ním následuje posloupnost příkazů, které se vykonávají v zadaném pořadí. Příkazem se rozumí akce, vzor propojený s akcí pomocí dvojice znaků ← , větvení (if a case) nebo lokální definice pomocí let. Opět následuje jednoduchý příklad

locase = do z <- getChar
        putChar '\n'
        putChar (toLower z)

Zajímavý je hlavně první řádek deklarace, který říká, že výsledek funkce getChar se má uložit do proměnné z. Za povšimnutí též stojí fakt, že tato proměnná je platná v celém bloku do. Víme už tedy, jak uložit do proměnné výsledek nějaké akce. Jak ale něco ze vstupně/výstupní sekvence vrátit? Řešením problému je funkce return :: a -> IO a, která je jakýmsi převodníkem z obyčejného typu na typ akce. Podívejme se na příklad jejího použití

readLine = do z <- getChar
          if z == '\n'
            then
             return ""
            else
             do r <- readLine
            return (z:r)

Uvedený kód demonstruje kromě funkce return i větvení pomocí if a vnořování bloků akcí. I když není možné míchat akce do deklarací obyčejných funkcí (platí to, co bylo řečeno na začátku – akce musí být od zbytku programu odděleny), jsou vstupně/výstupní operace právoplatnými hodnotami, které mohou být předávány jako parametry nebo mohou být uloženy do datových struktur. Můžeme tedy vytvářet např. seznamy akcí, jako je tento

pozdrav = [putChar 'a', putChar 'h', putChar 'o',
       do putChar 'j'
          getChar
          putChar '\b' >> putChar '!' >> putChar '\n']

Uvedený seznam má pouze čtyři prvky, ale obsahuje celkem osm akcí. Poslední prvek obsahuje operátor >>, který spojuje sekvenci akcí podobně jako blok do. Mimochodem tento operátor společně s >>= patří do typové třídy Monad a tvoří základ pro vstupně/výstupní operace. Jednotlivé akce jsou v seznamu pouze uloženy, ale pro jejich provedení ještě něco schází. Onou esencí je funkce obvykle pojmenovaná sequence s následující deklarací

sequence  :: Monad m => [m a] -> m ()
sequence  = foldr (>>) (return ())

Její použití je jednoduché – vyhodnocení výrazu sequence pozdrav způsobí provedení akcí ze seznamu. Naskýtá se několik dalších možností, jak funkci sequence využít. Až doteď jsme používali jen funkci putChar pro výpis znaků. Běžnější je ale výpis řetězců. Můžeme si proto k tomuto účelu deklarovat vlastní funkci

writeLine :: String -> IO ()
writeLine xs = sequence (map putChar xs)

Práce naší funkce spočívá v převedení řetězce znaků na seznam akcí vypisujících znak (map putChar xs) a následné provedení těchto akcí (sequence). Samozřejmě není nutné, aby si uživatel takovéto základní akce programoval sám. V modulu Prelude jsou deklarovány funkce putStr, putStrLn pro výpis na standardní výstup a getLine pro čtení řetězců ze standardního vstupu. Obecnější funkce pro práci se soubory se nacházejí v modulu IO. Ten se na rozdíl od Prelude nevkládá automaticky, a proto je zapotřebí ve zdrojovém kódu explicitně uvést klauzuli import IO. Jak při diskových operacích bývá zvykem, je nutné před použitím soubor nejprve otevřít. K tomu slouží funkce

openFile :: FilePath -> IOMode -> IO Handle

Výsledkem je deskriptor souboru, se kterým pak pracují ostatní funkce. Typ FilePath uvedený jako první parametr je aliasem pro String a IOMode je výčtový typ definovaný následovně

data IOMode = ReadMode | WriteMode | AppendMode | ReadWriteMode

Po ukončení práce se souborem jej uzavřeme pomocí funkce

hClose :: Handle -> IO ()

Deklarovány jsou samozřejmě funkce pro čtení a zápis znaků a řetězců

hGetChar :: Handle -> IO Char
hGetLine :: Handle -> IO String
hPutChar :: Handle -> Char -> IO ()
hPutStr :: Handle -> String -> IO ()

Zajímavou možností je získat obsah celého souboru jako jeden řetězec pomocí funkce

hGetContents :: Handle -> IO String

Tato funkce může pracovat hlavně díky línému vyhodnocování. Nenačítá se tedy celý soubor najednou, ale pouze ta část, která je právě zapotřebí. Kromě souborů mohou uvedené funkce pracovat i s tzv. kanály. Předdefinovány jsou stdin (standardní vstup), stdout (výstup) a sterr (chybový výstup).

Při práci se soubory je ale nutné počítat i s chybami, lépe řečeno s výjimečnými situacemi (např. požadavek na otevření souboru nelze splnit). Proto v Haskellu existuje speciální datový typ IOError, který reprezentuje všechny možné výjimečné stavy vstupně/výstupního systému. Aby mohl uživatel na určitou chybu reagovat, musí pomocí funkce catch „nainstalovat“ vlastní obsluhu výjimek. Další, poněkud komplexnější příklad demonstruje, jak lze chybové stavy zpracovat

-- signatura typu funkce catch
-- catch :: IO a -> (IOError -> IO a) -> IO a

import IO

-- hlavni funkce
vypis :: IO ()
vypis = do putStr "Zadejte jmeno souboru : "
       jmeno <- getLine
       obsah <- (catch (nacti jmeno) obsluhaChyby)
       putStr obsah

-- obsluha výjimek
obsluhaChyby _ = return "Chyba pri nacitani souboru"

-- pomocná funkce
nacti :: String -> IO String
nacti jmeno = do handle <- openFile jmeno ReadMode
         hGetContents handle

Jak je (resp. mělo by být) vidět ze signatury typu a z použití, vrací catch buď výsledek funkce nacti, nebo při chybě výsledek funkce obsluhaChyby. Obsluze výjimek je vždy předáván jeden parametr typu IOError (v našem případě byl ignorován), který upřesňuje chybový stav. V modulu IO je několik funkcí typu IOError -> Bool (isEOFError, isPermissionError, …) jimiž se lze dotazovat na konkrétní chybu. Výjimku také můžeme pomocí funkce fail :: IOError -> IO a předat obsluze na vyšší úrovni. Pokud uživatel nezadá vlastní obsluhu výjimek, použije se standardní – vypsání chybové hlášky a ukončení programu.

Někdy v minulých dílech padla zmínka o tom, že u funkcionálních programů lze dokazovat jejich správnost. Základními principy, které se přitom využívají, jsou referenční transparence a strukturální indukce. Vlastnost nazvanou referenční transparence lze popsat slovy „stejné lze nahradit stejným“. Znamená to, že pokud mají dva výrazy po vyhodnocení stejnou hodnotu, lze je navzájem bez následků vyměnit. Strukturální indukcí pro seznamy nazýváme následující postup

1. Dokážeme platnost tvrzení pro prázdný seznam []
2. Předpokládáme, že tvrzení platí pro seznam xs a dokazujeme platnost pro (x:xs)

Nyní nastal čas přejít od teorie k „praxi“. Mějme dány tyto čtyři rovnice

1.1   [] ++ xs     = xs
1.2   (x:xs) ++ ys = x:(xs++ys)

2.1   length []     = 0
2.2   length (x:xs) = 1 + length xs

Tvrzení, které chceme dokázat, zní : Pro všechny konečné seznamy xs a ys platí

length (xs ++ ys) == length xs + length ys

K dokazování použijeme strukturální indukci přes proměnnou xs.

1) důkaz pro xs = []
levá strana  : length ([] ++ ys) == length ys      {podle 1.1}
pravá strana : length [] + length ys == length ys  {podle 2.1}
2) předpokládáme platnost tvrzení
   length (xs ++ ys) == length xs + length ys
a chceme dokázat, že platí
   length ((x:xs) ++ ys) == length (x:xs) + length ys

levá strana  : length ((x:xs) ++ ys) == {podle 1.2}
length (x:(xs ++ ys)) == {podle 2.2}
1 + length (xs ++ ys) == {podle indukčního předpokladu}
1 + length xs + length ys

   pravá strana : length (x:xs) + length ys == {podle 2.2}
1 + length xs + length ys

K důkazu (a vlastně i k článku) už zbývá dodat pouze   

Q.E.D.