Proč potřebuju ten dokazovací argument? Proč prostě nemohu napsat div : Nat -> NonZero -> Nat
, tím přeci vyjadřuju, že dělenec je nenulový. A mašina si na pozadí odvodí, že nemohu zapsat
let a = 5
let b = 0
let x = div a b
, protože nesedí typ, b je Nat, zatímco očekvám NonZero (ten jsem si definoval výše).
Tohle by bylo alternativní řešení (v podstatě bez záv. typů). Mohl bych mít:
div : Nat -> PosNat -> Nat
Jenže to vyžaduje funkce pro převod mezi oběma typy:
data PosNat = One | S' PosNat
posNatFromNat : Nat -> PosNat
posNatFromNat (S Z) = One
posNatFromNat (S n) = S' (posNatFromNat n)
natFromPosNat : PosNat -> Nat
natFromPosNat One = S Z
natFromPosNat (S' n) = S (natFromPosNat n)
Bohužel
posNatFromNat není totální, takže aby to bylo "čisté" řešení, musela by ta převodní funkce vracet
Maybe PosNat. Ale je to validní alternativa.
Předpokládám, že to bude podobná zábava jako u těch forall. Tedy, že bych sice mohl napsat [Show], ale ExistentialQuantification jsou obecnější, a tak se na to zneužijí. Mýlím se?
Show je generický typ, takže
[Show] by byl seznam funktorů a
[Show a] s typovým parametrem akorát zafixuje ten parametr. Ale obecně ano, je to hodně silný nástroj aplikovaný na poměrně jednoduchý problém. Neříkal bych tomu zneužití, je to prostě jako kopání základů na dům bagrem, i když by to šlo ručně lopatou.
BTW všimni si, jak se mění signatura. Při použití záv. typů se nemění typy vstupních parametrů ani výstupu, jen se přidá dodatečný parametr, se kterým se pracuje jen v době překladu. Bez použití záv. typů musím buď změnit typ(y) vstupu (
PosNat), nebo výstupu (
div : Nat -> Nat -> Maybe Nat). Většinou se dělá to druhé, z čehož vyplývá, že musím nějak ověřit nebo rozbalit výstupní hodnotu (jestli tam není
Nothing). U záv. typů naopak ověřuju ("dokazuju") správnost vstupu, se špatným nejde funkce vůbec zavolat (resp. vyhodnotit). Dělám tak z nějaké problematické funkce funkci totální omezením jejího def. oboru (domény). Jakmile tohle člověk pochopí, je to hezký praktický příklad omílaného "the analytical and problem solving skills acquired by studying mathematics", sice to není moc praktické (mainstreamové jazyky záv. typy téměř nemají), ale přinejmenším to rozšiřuje obzory, člověk pak ví, že vrcholem typového systému nejsou generické typy ani HKT.