Jo, teď jsem se už definitivně ztratil já Co je myšleno tím "změnit návratový typ"?
:-D
Představme si, že jsem typový systém, a mám ověřit, zda tato funkce je v pořádku:
fn s : String 0 40 -> String 4 20 =
if (Str.len s) < 4 then
"default"
else
Str.sub s 20
Kouknu, a vidím, že na vstupu může přijít řetězec, minimálně 0, maximálně 40. Na výstupu je minimálně 4, max 20.
Takže 13 znaků cajk. 20 znaků cajk. 30 znaků cajk (hrubou silou oříznu). Ale 2 znaky už jsou problém, na vstupu přijít mohou, a na výstupu nesmí.
Funkce
Str.sub s 20 v daném kontextu znamená
Str.sub (String 0 40) 20 -> String 0 20 protože podle druhého argumentu si mohu odvodit, že tedy nedostanu delší string jak 20znaků, ale jako první argument stále mohu dostat prázdný string. A tedy nevím, jak bych měl
uvažovat (jako ten typový systém).
Tedy samozřejmě si takhle jen hraju. Nikdy jsem typový systém neimplementoval, a tak se zkouším
vcítit do jeho uvažování :-) A pravděpodobně někde mám i nějaké ty díry v úvaze.