Typový system versus unittesty

BoneFlute

  • *****
  • 1 983
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #165 kdy: 19. 06. 2018, 15:23:54 »
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.


Re:Typový system versus unittesty
« Odpověď #166 kdy: 19. 06. 2018, 15:27:42 »
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

Re:Typový system versus unittesty
« Odpověď #167 kdy: 19. 06. 2018, 15:29:30 »
... (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

Re:Typový system versus unittesty
« Odpověď #168 kdy: 19. 06. 2018, 15:30:35 »
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

Re:Typový system versus unittesty
« Odpověď #169 kdy: 19. 06. 2018, 15:35:36 »
... (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 :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


Re:Typový system versus unittesty
« Odpověď #170 kdy: 19. 06. 2018, 15:36:36 »
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

Re:Typový system versus unittesty
« Odpověď #171 kdy: 19. 06. 2018, 15:36:54 »
... (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

Re:Typový system versus unittesty
« Odpověď #172 kdy: 19. 06. 2018, 15:43:59 »
... (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 :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

Re:Typový system versus unittesty
« Odpověď #173 kdy: 19. 06. 2018, 15:47:37 »
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

Re:Typový system versus unittesty
« Odpověď #174 kdy: 19. 06. 2018, 15:47:57 »
... (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 :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

Re:Typový system versus unittesty
« Odpověď #175 kdy: 19. 06. 2018, 15:50:21 »
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

  • *****
  • 1 983
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #176 kdy: 19. 06. 2018, 15:52:01 »
ž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?
« Poslední změna: 19. 06. 2018, 15:56:12 od BoneFlute »

Kit

Re:Typový system versus unittesty
« Odpověď #177 kdy: 19. 06. 2018, 15:56:34 »
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

Re:Typový system versus unittesty
« Odpověď #178 kdy: 19. 06. 2018, 16:01:54 »
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

Re:Typový system versus unittesty
« Odpověď #179 kdy: 19. 06. 2018, 16:04:06 »
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