Prolegomena k úvodu do základů závislostních typů
Tags: agda, coq, idris
Published: 2022-02-21 22:29:08

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í](https://dev.to/betelgeuse/rovnostni-typy-a-negace-typu-18c2) dojde na typy, které vyjadřují rovnost a negaci.