Fórum Root.cz
Hlavní témata => Vývoj => Téma založeno: BoneFlute 01. 05. 2018, 00:57:43
-
Zdravím.
Mějme takovouto funkci v blíže neurčeném jazyku podobném haskellu:
fn s : String 0 40 -> String 4 20 =
if (Str.len s) < 2 then
"default"
else
Str.sub s 20
Čtěte to prosím jako "funkce fn má jeden parametr typu String který je minimálně nula znaků dlouhý, a maximálně 40; a vrací String, který je minimálně čtyři znaky dlouhý a maximálně 20.
A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?
(Tak jasně, můžu na to pustit testy, ale já bych rád zůstal jen u typů a formální verifikace.)
Díky.
-
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
-
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
-
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.
-
A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?
Např. když si délkově omezený řetězec zadefinuji jako
data BString : Nat -> Nat -> Type where
MkBString : (a : Nat) -> (b : Nat) -> (s : String) -> (LTE a (length s)) -> (LTE (length s) b) -> BString a b
tak abych do něj zabalil "default", musím psát něco jako
d : BString 4 20
d = MkBString 4 20 "default" (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))
kde poslední dva termy typů (LTE 4 7) a (LTE 7 20) jsou důkazy, že 4 <= 7 a 7 <= 20. V tomto případě by stačilo místo nich dát podtržítko a kompilátor je vymyslí sám. Nicméně i ve vaší funkci by bylo třeba dát důkazy, že nerovnosti platí - bez toho by se program nepřeložil.
-
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.
Díky.
Uniká mi v tvé odpovědi, jak ten systém pozná, že Str.sub s 20 ve větvi else vrátí vždy korektní minimální čtyři znaky. (Tedy v mém případě pozná, že nevrátí, a tudíž nahlásí chybu.)
-
A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?
Např. když si délkově omezený řetězec zadefinuji jako
data BString : Nat -> Nat -> Type where
MkBString : (a : Nat) -> (b : Nat) -> (s : String) -> (LTE a (length s)) -> (LTE (length s) b) -> BString a b
tak abych do něj zabalil "default", musím psát něco jako
d : BString 4 20
d = MkBString 4 20 "default" (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))
kde poslední dva termy typů (LTE 4 7) a (LTE 7 20) jsou důkazy, že 4 <= 7 a 7 <= 20. V tomto případě by stačilo místo nich dát podtržítko a kompilátor je vymyslí sám. Nicméně i ve vaší funkci by bylo třeba dát důkazy, že nerovnosti platí - bez toho by se program nepřeložil.
Trochu jsem se v tom ztratil. Je to odpověď, na to, jak zjistí, že výstup není správně (to není tak zajímavé), nebo to, jak zjistí, že ta větev else, přestože může vrátit výsledek neodpovídající požadovanému výstupu, tak vždy vrátí (vrátila by) správný výsledek, protože proběhne jen v těch případech (to mě zajímá).
Díky.
-
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.
Díky.
Uniká mi v tvé odpovědi, jak ten systém pozná, že Str.sub s 20 ve větvi else vrátí vždy korektní minimální čtyři znaky. (Tedy v mém případě pozná, že nevrátí, a tudíž nahlásí chybu.)
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
-
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)
Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.
A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
-
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)
Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.
A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.
-
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)
Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.
A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.
Počkej, počkej, mám pocit, že jsme se tu někdo z nás ztratil.
Str.sub má návratový typ String 0 ∞. Takže může vrátit dvouznakový řetězec. Vstupní argumenty jsou 20, což je ok na výstup, takže tento argument změní návratový typ na String 0 20. A dále String, jehož minimální velikost je určena tou kontrolou v if. Což je tedy defakto taky správně, a ta funkce bude pracovat korektně. A já se tedy táži, jak typový systém pozná, že díky podmínce if se z hodnoty String 0 20 stane hodnota typu String 2 20 (respektive String 4 20).
Zdůrazňuji, že já se táži na typový systém, který řeší mou úlohu. Netáži se jak fungují závislostní typy (i když zrovna třeba ony mohou řešit mou úlohu, a pak mě zajímá jak to řeší).
-
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)
Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.
A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.
Počkej, počkej, mám pocit, že jsme se tu někdo z nás ztratil.
Str.sub má návratový typ String 0 ∞. Takže může vrátit dvouznakový řetězec. Vstupní argumenty jsou 20, což je ok na výstup, takže tento argument změní návratový typ na String 0 20. A dále String, jehož minimální velikost je určena tou kontrolou v if. Což je tedy defakto taky správně, a ta funkce bude pracovat korektně. A já se tedy táži, jak typový systém pozná, že díky podmínce if se z hodnoty String 0 20 stane hodnota typu String 2 20 (respektive String 4 20).
Zdůrazňuji, že já se táži na typový systém, který řeší mou úlohu. Netáži se jak fungují závislostní typy (i když zrovna třeba ony mohou řešit mou úlohu, a pak mě zajímá jak to řeší).
Jo, teď jsem se už definitivně ztratil já :( Co je myšleno tím "změnit návratový typ"?
-
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.
-
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).
Napsalo by se to takhle:
fn s : String 0 40 -> String 4 20 =
case s `hasMinimumLen` 4 of
Just sn -> Str.sub sn 20 -- sn ma tady typ (String 4 40)
Nothing -> "default"
Ono dnešní jazyky (Java..) by to uměly odvodit i z té podmínky - třeba "null" to schopné odvodit je, ale takhle je to hezčí a explicitně.
-
Napsalo by se to takhle:
fn s : String 0 40 -> String 4 20 =
case s `hasMinimumLen` 4 of
Just sn -> Str.sub sn 20 -- sn ma tady typ (String 4 40)
Nothing -> "default"
Ono dnešní jazyky (Java..) by to uměly odvodit i z té podmínky - třeba "null" to schopné odvodit je, ale takhle je to hezčí a explicitně.
Fikaný!
-
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.
Tak to je fikaný, teď je uvedeno:
if (Str.len s) < 4 then
zatímco původně bylo:
if (Str.len s) < 2 then
Jak to tedy má být?
-
Tak to je fikaný, teď je uvedeno:
if (Str.len s) < 4 then
zatímco původně bylo:
if (Str.len s) < 2 then
Jak to tedy má být?
To je fuk, ne? Otázka zněla, jak má typový systém ověřit správnost. V původním by nahlásil chybu, v tom druhém, že je to v pořádku. Podstatné je, zda je schopen.