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

#agda #coq #idris

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

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

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

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

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

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

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)

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)

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"

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.