DEV Community

Betelgeuse
Betelgeuse

Posted on

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
Enter fullscreen mode Exit fullscreen mode

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

isMonday : DayOfWeek -> Bool
isMonday Mon = True
isMonday _ = False
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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

aProof _ prf = rewrite prf in Refl
Enter fullscreen mode Exit fullscreen mode

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)
Enter fullscreen mode Exit fullscreen mode

Definice této funkce je

anotherProof _ prf = rewrite prf in falseNotTrue
Enter fullscreen mode Exit fullscreen mode

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

falseNotTrue : Not (False = True)
falseNotTrue _ impossible
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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

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

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ě.

Discussion (0)