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ě.
Top comments (0)