Typový system versus unittesty

[BoneFlute]

Obecně asi platí, že když se program převede do churchovského λ-kalkulu (kde se nerozlišuje mezi dobou překladu a běhu), tak jakákoliv totální funkce, jejíž doména je konečná, se dá verifikovat typově (čili v době překladu v nějaké implementaci s dostatečně silným typovým systémem). Odhalování a charakteristika chyb tímto způsobem souvisí (na úrovni pusté teorie) s ι-operátorem.

Limit typů jsou časová náročnost. Limit testů zase neúplnost. Dokážete si někdo představit, že by se dal uělat nějaký kompromis, omezit ultimátnost typů, aby to otestování proběhlo v kontrolovaném čase. Nebo optimalizovat compiler, aby si dokázal domyslet některé věci a nepočítal to hrubou silou?
Samozřejmě si představuju spíš otázku konfigurace, kdy při vývoji budu mět méně striktní režim, a pak při buildu dám kompilovat třeba tejden.

[Reklama]

[Filip Jirsák]

tak zrovna to sčítání řeší

„To sčítání“ možná řeší. Ale to je nějaký váš problém, který tu neřešíme. My tu řešíme problém, že programátor měl použít sčítání a použil odčítání. Tohle neřeší žádný typový systém (tedy kromě takového, který odčítání vůbec nedovolí, což ale bude pro většinu programů nepoužitelné).

[JSH]

... (kde se nerozlišuje mezi dobou překladu a běhu) ...

Akorát že doba překladu a běhu jsou oddělené jak v čase, tak v prostoru. Spoustu informací typový systém prostě nemá a ani nemůže mít k dispozici.

Už jsem to tu jednou zmiňoval a v se zmohl akorát na "to se dá řešit".

[Gődel]

co si vlastně představujete pod pojmem "silný typový systém"?

Rozhodně něco s HKT (tím se vyloučí Java apod.), to by byl středně silný, nicméně jak tu už někdo zmiňoval, adjektivum "silný" by mělo implikovat alespoň běžné závislostní typy à la Agda/Coq/Idris.

Rád bych, když bychom se nedrželi jen toho, co se zatím někomou podařilo implementovat. Zajímá mě klidně i to, co by teoreticky šlo.

Co by šlo teoreticky se ví. Stačí vzít churchovský λ-kalkul a zamyslet se, jaké výpočty lze přenést na úroveň typů. Pokud požadujeme, aby překlad syntakticky správně utvořeného programu trval vždy jen konečnou dobu (to je poměrně rozumný předpoklad), lze přenést na tu vyšší ("typovou") úroveň funkce, které jsou totální (předpokladem je samozřejně dostatečně silný typový systém). Vše, co zbyde, se musí ponechat v tělech formulí. V implementaci by to pak zbylo na jednotkové testy. V podstatě stačí přečíst si původní článek o zmiňovaném λ-kalkulu a v příslušných kontextech si u typů představovat závislostní typy (jež korespondují s formální logikou s kvantifikátory). Tolik k tomu "co by teoreticky šlo", protože v praxi by byl přínos sporný až nesmyslný.

[v]

... (kde se nerozlišuje mezi dobou překladu a běhu) ...

Akorát že doba překladu a běhu jsou oddělené jak v čase, tak v prostoru. Spoustu informací typový systém prostě nemá a ani nemůže mít k dispozici.

Už jsem to tu jednou zmiňoval a v se zmohl akorát na "to se dá řešit".

taky jste se mohl zeptat na detaily, nechce se mi rozepisovat všechno, když píšu sem, tak nepíšu kód
http://augustss.blogspot.com/2009/06/more-llvm-recently-someone-asked-me-on.html
tohle je můj oblíbený příklad, ukazuje jak se od netypového syntaktického stromu dostat k silně typovanému, stejně to jde i s číslama

[Reklama]

[Filip Jirsák]

Limit typů jsou časová náročnost. Limit testů zase neúplnost. Dokážete si někdo představit, že by se dal uělat nějaký kompromis, omezit ultimátnost typů, aby to otestování proběhlo v kontrolovaném čase. Nebo optimalizovat compiler, aby si dokázal domyslet některé věci a nepočítal to hrubou silou?
Samozřejmě si představuju spíš otázku konfigurace, kdy při vývoji budu mět méně striktní režim, a pak při buildu dám kompilovat třeba tejden.

Problém je, že hodně zjednodušujete, a pak vyvozujete něco z nepřesností toho zjednodušení. Protože problém neúplnosti testů znamená, že mohou existovat vstupy, pro které dává testovaná jednotka chybný výsledek – přičemž taková kombinace není pokrytá testem. To je ale úplně jiná neúplnost, než „úplnost“ typů.

Formální dokazatelnost má smysl řešit u jednoduchých a kritických úloh typu zabezpečovací zařízení na železnici. U komplexních systémů typu ERP, bankovní systémy, webové prohlížeče apod. nemá vůbec smysl řešit rychlost případného kompilátoru, protože to je ten nejmenší problém – skutečný problém je v tom, že nikdo tak komplexní systém nedokáže správně formálně vyjádřit.

[Gődel]

... (kde se nerozlišuje mezi dobou překladu a běhu) ...

Akorát že doba překladu a běhu jsou oddělené jak v čase, tak v prostoru. Spoustu informací typový systém prostě nemá a ani nemůže mít k dispozici.

Už jsem to tu jednou zmiňoval a v se zmohl akorát na "to se dá řešit".

Jistě, ale když už se tu volá po teorii, je poměrně snadné namapovat si prakticky používaný jazyk na zmíněný λ-kalkul a uvědomit si, že těla formulí jsou "běh" a typové výrazy "překlad". Typový systém taky může počítat, jen o úroveň výš (v praxi něco na způsob TMP v C++, v teorii na úrovni typů složených z *). Jde jen o to, jaké operátory jsou na té které úrovni povoleny.

[JSH]

... (kde se nerozlišuje mezi dobou překladu a běhu) ...

Akorát že doba překladu a běhu jsou oddělené jak v čase, tak v prostoru. Spoustu informací typový systém prostě nemá a ani nemůže mít k dispozici.

Už jsem to tu jednou zmiňoval a v se zmohl akorát na "to se dá řešit".

taky jste se mohl zeptat na detaily, nechce se mi rozepisovat všechno, když píšu sem, tak nepíšu kód
http://augustss.blogspot.com/2009/06/more-llvm-recently-someone-asked-me-on.html
tohle je můj oblíbený příklad, ukazuje jak se od netypového syntaktického stromu dostat k silně typovanému, stejně to jde i s číslama

Cože??? To jako že až se na uživatelově stroji načtou vstupy, tak si pro ty vstupy teprve zkompiluju něco spustitelného???

Já doufám, že jsem to vůbec nepochopil. Opravdu v to upřímně doufám.

[Kit]

Klidně zrovna ten v Haskellu. Problémy, které tu zazněly, totiž neřeší. Jeden každý váš odkaz řešil jiný a podstatně jednodušší problém.

tak zrovna to sčítání řeší

Jaké je tedy správné řešení s použitím typů, které odhalí, že ve sčítací funkci programátor chybně napsal znaménko "-"? Zatím jsem se dozvěděl jen to, že to jde, s odkazem na článek. Jak by tedy vypadal zápis této triviality, např. v Haskellu?

[v]

... (kde se nerozlišuje mezi dobou překladu a běhu) ...

Akorát že doba překladu a běhu jsou oddělené jak v čase, tak v prostoru. Spoustu informací typový systém prostě nemá a ani nemůže mít k dispozici.

Už jsem to tu jednou zmiňoval a v se zmohl akorát na "to se dá řešit".

taky jste se mohl zeptat na detaily, nechce se mi rozepisovat všechno, když píšu sem, tak nepíšu kód
http://augustss.blogspot.com/2009/06/more-llvm-recently-someone-asked-me-on.html
tohle je můj oblíbený příklad, ukazuje jak se od netypového syntaktického stromu dostat k silně typovanému, stejně to jde i s číslama

Cože??? To jako že až se na uživatelově stroji načtou vstupy, tak si pro ty vstupy teprve zkompiluju něco spustitelného???

Já doufám, že jsem to vůbec nepochopil. Opravdu v to upřímně doufám.

nepochopil a jestli máte podobný background jako já (v mém případě C, C++, C#, python), tak se ani nedivím, docela mi trvalo než jsem to vstřebal (s pauzama možná rok), vlastně to není nic tak komplikovaného, ale je to hodně odlišné od programátorského mainstreamu

[v]

Klidně zrovna ten v Haskellu. Problémy, které tu zazněly, totiž neřeší. Jeden každý váš odkaz řešil jiný a podstatně jednodušší problém.

tak zrovna to sčítání řeší

Jaké je tedy správné řešení s použitím typů, které odhalí, že ve sčítací funkci programátor chybně napsal znaménko "-"? Zatím jsem se dozvěděl jen to, že to jde, s odkazem na článek. Jak by tedy vypadal zápis této triviality, např. v Haskellu?

viz článek hned pod větou "For example, singleton function for natural addition :+ can be implemented as follows:"

[BoneFlute]

že těla formulí jsou "běh" a typové výrazy "překlad".

Možná ti jen nerozumím, ale:
mám množiny
Bool = True | False
RGB = Red | Green | Blue
pak mám funkci
isRed :: RGB -> Bool
která se dá zapsat takto:
isRed :: RGB -> Bool = (Red -> True) | (Green -> False) | (Blue -> False)
Té množině isRed ale obvykle říkáme funkce, a něco počítá, ale je to stejně jen množina, respektive pohled na průnik dvou množin. (Nebudu se pokoušet trefit se do přesného pojmosloví.)

Bavíme se cca o tom samém?

[Kit]

Jaké je tedy správné řešení s použitím typů, které odhalí, že ve sčítací funkci programátor chybně napsal znaménko "-"? Zatím jsem se dozvěděl jen to, že to jde, s odkazem na článek. Jak by tedy vypadal zápis této triviality, např. v Haskellu?

viz článek hned pod větou "For example, singleton function for natural addition :+ can be implemented as follows:"

Celý článek? V testech je to na několika řádcích a definice typu je na celý článek?

[SB]

Proč @v dokázal pochopit, že se táži na limity toho typového systému vůči unittestům, zatímco jiní se mě pokouší přesvědčit že jsem idiot a ani nejsou schopni uvést zajímavé argumenty?

Omezené možnosti kontroly správnosti programu typovým systémem jsem vám přímočaře a bleskově (a vypadá to, že nejen já, nečetl jsem vše) předvedl na příkladu, víceméně důkazu sporem. Takže odpověď na váš původní dotaz už máte. Je třeba ještě něco řešit?

[v]

Jaké je tedy správné řešení s použitím typů, které odhalí, že ve sčítací funkci programátor chybně napsal znaménko "-"? Zatím jsem se dozvěděl jen to, že to jde, s odkazem na článek. Jak by tedy vypadal zápis této triviality, např. v Haskellu?

viz článek hned pod větou "For example, singleton function for natural addition :+ can be implemented as follows:"

Celý článek? V testech je to na několika řádcích a definice typu je na celý článek?

typy můžou být definovány v knihovnách a mezi testem a tím v článku je přece jenom trochu rozdíl, ty záruky (pro všechny dvojice přirozených čísel) prostě testama nelze nahradit