DEV Community

Betelgeuse
Betelgeuse

Posted on • Updated on

Prolegomena k úvodu do základů závislostních typů

Funkce většinou pracují s hodnotami jako čísla, řetězce nebo záznamy, například 12 nebo Praha, jejichž typy jsou Nat a String. Matematické funkce mohou ale pracovat s libovolnými objekty, je proto smysluplné ptát se, jakého typu je ono Nat nebo String. Zadefinujme si jejich typ jako Type. To nám umožní definovat takovouto funkci:

getType : Bool -> Type
getType True = String
getType False = Nat
Enter fullscreen mode Exit fullscreen mode

Funkce getType je sama o sobě k ničemu, ale co kdybychom ji použili v definici jiné funkce? Zkusme například

getValue : (b : Bool) -> getType b
getValue True = "abcd"
getValue False = 1234
Enter fullscreen mode Exit fullscreen mode

Protože funkce getType vrací typ (hodnotu typu Type), můžeme ji použít pro výpočet typu návratové hodnoty funkce getValue, kterou můžeme použít takto:

putStrLn $ show $ getValue True
putStrLn $ show $ getValue False
Enter fullscreen mode Exit fullscreen mode

Pokud vám tato funkce připadá divná, máte pravdu, ve většině jazyků by zapsat nešla, ale v jazycích s takzvanými závislostními typy jsou takovéto funkce běžné.

Představme si, že chceme napsat funkci pro dělení přirozených čísel, která funguje korektně (bez pádů nebo výjimek) na všech vstupech. Předpokládáme, že máme funkci typu

divNat : Nat -> Nat -> Nat
Enter fullscreen mode Exit fullscreen mode

která ale při dělení nulou zkolabuje. Máme dvě možnosti: buď rozšíříme typ návratové hodnoty, abychom mohli při pokusu o dělení nulou sdělit, že výpočet nelze provést, nebo zúžíme definiční obor funkce pro dělení. V prvním případě dostaneme například:

safeDiv : Nat -> Nat -> Maybe Nat
Enter fullscreen mode Exit fullscreen mode

a pří dělení nulou vrátíme místo číselného výsledku Nothing. Ve druhém případě musíme přidat k funkci argument, který zaručí, že dělitel je nenulový:

safeDiv : Nat -> (n : Nat) -> {auto prf : IsNonZero n} -> Nat
safeDiv m n {prf} = divNat m n
Enter fullscreen mode Exit fullscreen mode

Všimněte si, že IsNonZero je generický typ, jehož parametrem je přirozené číslo. K definici tohoto typu využijeme úvahu, že přirozené číslo je nenulové, pokud má předchůdce (který je taktéž přirozeným číslem):

data IsNonZero : Nat -> Type where
    SucNonZero : (n : Nat) -> IsNonZero (S n)
Enter fullscreen mode Exit fullscreen mode

Důkaz nenulovosti druhého argumentu není vždy možné automaticky odvodit, pokud jej například čteme na vstupu, uživateli nic nebrání zadat nulu. Potřebujeme proto funkci, která nám příslušný důkaz dodá, pokud existuje:

isNonZero : (n : Nat) -> Maybe (IsNonZero n)
isNonZero 0 = Nothing
isNonZero (S n) = Just (SucNonZero n)
Enter fullscreen mode Exit fullscreen mode

Funkce isNonZero vrátí Nothing pro nulu a důkaz nenulovosti (dodá předchůdce čísla na vstupu) v ostatních případech. Pokud tedy v kódu není možné nenulovost dělitele odvodit automaticky (viz deklarace auto prf), použijeme funkci isNonZero, která příslušný důkaz umí dodat (jinak vrátí Nothing):

Just m <- readNat | Nothing => putStrLn "not a number"
Just n <- readNat | Nothing => putStrLn "not a number"
case isNonZero n of
    Just prf => putStrLn $ show $ safeDiv m n {prf=prf}
    _ => putStrLn "division by zero"
Enter fullscreen mode Exit fullscreen mode

Přidaný třetí argument se tak dá považovat za kontrakt. Podobný přístup se používá i v jiných jazycích navržených pro bezpečnostně kritické aplikace, například v jazyce SPARK.

V pokračování dojde na typy, které vyjadřují rovnost a negaci.

Discussion (1)

Collapse
greta profile image
Info Comment hidden by post author - thread only accessible via permalink
Greta

nóóóóó ato je jakoby kdo ten legoman pro kterýho si to jakože napsal 😯 😯 🤪 😜

Some comments have been hidden by the post's author - find out more