Asi nejjednodušší příklad je dokazování, že nějaké číslo není nula (aby například nedošlo k dělení nulou). Takový predikát se dá jednoduše vyjádřit záv. typem:
data NonZero : Nat -> Type
Dá se to brát jako běžná uzavřená formule v logice, jež je unární a říká něco o přirozených číslech.
NonZero určuje tu nenulovost, ok. Nat určuje přirozené číslo - "pro každé přirozené číslo". A to Type tam hraje jakou roli?
NonZero je prachobyčejná funkce, takže
Nat->Type je funkce z přirozených čísel do typů. Tohle je v praxi trochu trik, protože
Type v překladači reprezentuje nekonečnou množinu (meta)typů různých úrovní (něco na způsob Cantorova paradoxu). To ale není pro základní pochopení záv. typů podstatné.
Type je prostě "typ typů".
Aby to bylo k něčemu v praxi, musí se k tomu ale navíc napsat funkce, která pro každý typově správný vstup řekne, zda je predikát splněn:
isNonZero : (n:Nat) -> Dec (NonZero n)
Generický typ Dec má dva konstruktory, Yes a No, kde Yes má jako parametr důkaz platnosti predikátu pro daný vstup a No důkaz kontradikce (tj. důkaz Pred->Void, protože jsme v intuicionistické logice). Existence takovéto funkce vlastně říká, že daný predikát je úplný (pro každý vstup existuje důkaz buď jeho platnosti, nebo neplatnosti).
Dobře. A tak já si tu funkci takto (humpolácky naimplementuju):
isNonZero 0 = No (NonZero 0)
isNonZero x = Yes (NonZero x)
Chytám se?
Problém je, že
NonZero n je typ, ale
Yes musí mít jako parametr nějakou jeho hodnotu. Takže třeba si všimnu, že když
n je přirozené číslo, tak jeho následovník je nenulový. Takže můžu mít konstruktor
SuccNZ, který mi potřebný důkaz poskytne:
isNonZero : (n:Nat) -> Dec (NonZero n)
isNonZero Z = No absurd
isNonZero (S n) = Yes (SuccNZ n)
U
No je to trochu složitější, protože musím prokázat, že
NonZero 0 neplatí (implikuje
Void). K tomu má překladač magickou pomůcku:
absurd.
Potom můžu mít funkci pro dělení:
div : Nat -> (y:Nat) -> NonZero y -> Nat
Tato funkce je totální, protože pro nulu ve druhém parametru není definovaná (nejde zavolat, protože nejde vytvořit instance (důkaz) predikátu NonZero Z). Takový program je zřejmě bezpečnější, protože za běhu nemůže dojít k chybě při volání div.
Všemu rozumím, až na počet těch argumentů.
let a = 5
let b = 0
let x = div a b .... ?
Proč není ta signatura takto?
div : Nat -> NonZero -> Nat
Potřebuješ dva číselné parametry, první je dělenec a to
y je dělitel. Třetí argument typu
NonZero y zajistí, že dělitel není nula, viz
SuccNZ výše. Ten třetí "dokazovací" argument může překladač za určitých okolností uhádnout sám, ale o to teď nejde.