- Za běhu funkce div nikoho nezajímá, nemá dva argumenty, není vůbec... Za běhu je na všechno pozdě a prostě děj se vůle boží.
To bych takhle neřekl, myslím, že jádro věci je, že za běhu nikoho nezajímá její třetí argument.
No, trochu si zatrucuju: já bych to tak řekl :-) Ale rád si to nechám vysvětlit.
Ale ta funkce div tam je, ne? A počítá za běhu.
Ta funkce
div tam je. Ale nemá žádné argumenty, o kterých by se dalo uvažovat. Nebo ještě jinak, za běhu s ní vůbec nijak nepracuješ. Tobě, jako programátorovi/matematikovi se ta funkce jeví tak, jak ji vidíš v kódu - tedy
div se
třemi argumenty.
Primitivní validační funkce ti stačí, ale jak jsi sám psal, bude se vyhodnocovat za běhu.
Počkej, počkej, takto mi to neštymuje.
Zkusme změnit syntax:
isNotZero x = x /= 0
divide :: Int -> a:Int -> Float & isNotZero a
divide a b = a `div` b
calculate x = divide 42 x
- Důkaz píšu jako jméno validační funkce za ampersand.
- Ta validační funkce je úplně nudná.
- Funkci
divide volám úplně obyčejně, není třeba ji tam explicitně uvádět.
- Při kompilaci mašina projde graf volání, a je schopna staticky, při kompilaci, ověřit, že při volání
divide a b,
b není nula.
- To ověření proběhne při kompilaci, nikoliv za běhu.
- Statické ověřování se týká konstantního kódu. Jakmile je tam nějaká dynamika, to znamená vnější svět, tak se opět vracíme k Maybe, protože to jinak nejde.
Vidím to příliš jednoduše, nebo je to opravdu v tom, že
tohle přišlo od akademiků, kterým evidentně nezáleží na hezké čitelné syntaxi a jasném oddělení argumentů pro běh a pro kontrolu typů (např. číselné argumenty pro dělení vs. důkazy).
?
Zobrazit příspěvky
