ta funkce pak má typ Nat->y:Nat->Not (y=0)->Nat.
Můžeš mi prosím, v nějakém srozumitelnějším pseudo jazyku s hodně komentáři popsat, cože to vlastní říká? Jsem na to Nat už narazil mnohokrát. Vždycky tím začíná každá učebnice Idris a Agdy, a já to prostě neumím přečíst. (Předpokládám, že Nat je jako Natural - přirozené číslo?)
Jo, Nat jsou přirozená čísla. Když T je typ, tak Not T se definuje jako T->Void (kde Void je typ bez hodnot, odpovídající false v intuicionistické logice), typ třetího parametru je tedy (y=0)->Void. Možná si spíš představ něco jako typ NonZero n:Nat, kde bude konstruktor NonZero (Succ n). Popravdě tento příklad není úplně nejjednodušší, protože obsahuje rovnostní typ a negaci.
Takže Nat -> y : ... je typ pojmenovaný jako Nat, mající jeden argument. Něco podobného jako Maybe a = ... (eee deklarace typu, nebo deklarace uplatnění typu?)
Tak jinak:
Takže já mám funkci:
div a b = ...
Anotace moje:
div :: Numeric -> PositiveUnzeroNumeric -> Numeric
Anotace tvoje:
div Numeric y :: Numeric -> Not (y = 0) -> Numeric
nebo třeba:
div :: Numeric -> Numeric y, Not (y = 0) -> Numeric
A jak se potom ta funkce zavolá, explicitně, bez type inference. Jak tam bude figurovat ta typová proměnná y?
Ne ne, bylo by to
div : Numeric -> (y:Numeric) -> Not (y=0) -> Numeric . V těchto jazycích jakákoliv hodnota typu se bere jako důkaz platnosti formule odpovídající tomu typu (Curry-Howard). S tou rovností to je trik, že když předám příslušnou hodnotu ("důkaz"), můžu tu funkci zavolat a mám zaručenou nenulovost. Jinak kód vůbec nepřeložím. Fakt si místo
Not (y=0) vezmi
NonZero y. Tento typ má konstruktor
MkNonZero (S n). No a teď si zkus s tímto zavolat
div na nulu
Tady je vidět, že to není (u takto jednoduchých příkladů) žádná věda, zvlášť když ten důkaz musíš dodat sám. Síla záv. typů je jen a pouze v tom, co za tebe dosadí ("odvodí") překladač automaticky.
P.S. Kdybys měl to tvé
NonzeroNat a nevěděl vůbec nic o druhém parametru, musel bys použít např. funkci
Nat -> Maybe NonzeroNat, aby ošetřil nenulovost před voláním
div. V některých případech tě záv. typy jen donutí ke kontrole vstupu/ošetření chyby, žádná magie v tom není.