Rovnostní typy a negace typů

Předchozí článek byl úvodem do závislostních typů a jejich použití v bezpečnostně kritických aplikacích. V tomto zavedeme rovnostní typy a vylepšíme původní kód.

Nejprve definice typu pro ilustrační příklad:

data DayOfWeek = Mon | Tue | Wed | Thu | Fri | Sat | Sun

Jednoduchá funkce ověří, že zadaný den je pondělí:

isMonday : DayOfWeek -> Bool
isMonday Mon = True
isMonday _ = False

V kontraktech se často používají porovnání hodnot. Každé porovnání a = b hodnot stejného typu je možné považovat za typ. Pokud rovnost platí, tento typ má hodnotu Refl, kterou je možné použít ve funkcích. Následující funkce je v podstatě náhradou příslušného jednotkového testu, korektnost se ale ověřuje již v době překladu v rámci typové kontroly, ne až za běhu.

aProof : (d : DayOfWeek) -> d = Mon -> isMonday d = True

Tato funkce dostane dva argumenty a ověří, že funkce isMonday vrátí správnou hodnotu. Její definice je

aProof _ prf = rewrite prf in Refl

Typ návratové hodnoty je rovnostní, proto se musí jednat o nějaké Refl. Tuto hodnotu získáme tak, že pomocí rewrite přepíšeme d na Mon v typu isMonday d, což se vyhodnotí jako True.

Podobně bychom mohli mít analogický test, ale nyní chceme dokázat, že něco neplatí. Zavedeme proto negaci typů, Not T, což je v zásadě funkce typu T -> Void, kde Void je typ bez hodnot. Tuto funkci proto není možné zavolat, neboť není možné vrátit žádnou hodnotu. Příkladem budiž následující analogie jednotkového testu:

anotherProof : (d : DayOfWeek) -> d = Tue -> Not (isMonday d = True)

Definice této funkce je

anotherProof _ prf = rewrite prf in falseNotTrue

Zbývá definovat funkci falseNotTrue typu Not (False = True):

falseNotTrue : Not (False = True)
falseNotTrue _ impossible

Obecně platí, že dvě hodnoty stejného typu můžou být shodné ve smyslu výrokové rovnosti, pokud výslovně neřekneme, že se rovnat nemůžou.

Vraťme se nyní ke staré známé funkci safeDiv. Změníme typ kontraktu, že nelze dělit nulou:

safeDiv : Nat -> (n : Nat) -> {auto prf : Not (n = 0)} -> Nat

Budeme potřebovat pomocnou funkci říkající, že nula není následníkem žádného přirozeného čísla:

sucNonZero : (n : Nat) -> Not ((S n) = 0)
sucNonZero _ _ impossible

Původní funkce isNonZero nyní vypadá takto:

isNonZero : (n : Nat) -> Maybe (Not (n = 0))
isNonZero 0 = Nothing
isNonZero (S n) = Just (sucNonZero n)

Je potěšitelné, že na samotné funkci safeDiv se nic nemění.

Funkce isNonZero je ale stále poněkud problematická, protože sice někdy vrací důkaz nenulovosti, ale pokud je výsledkem Nothing, nevíme, jestli je argument funkce nulový nebo ne. Místo Nothing bychom chtěli důkaz n = 0. K tomu slouží typový operátor Dec, kterému se budeme věnovat příště.