Typový system versus unittesty

[Filip Jirsák]

já jsem ale o opakování implementace nic nepsal, pokud špatně pochopíte problém, můžete napsat test, který od funkce chce pro zadané vstupy jiné výstupy, než ty správné (z hlediska řešeného problému)

To je možné, ale je to spíše výjimečné. Daleko častější je případ, kdy ví správně, jaký výstup má být pro daný vstup, ale špatně to implementuje. Jednotkové testy řeší tenhle případ, a to silným typovým systémem nejde nahradit.

[Reklama]

[BoneFlute]

nejdřív bych zdůraznil svůj postoj: neargumentuju proti testům, testy jsou dobrá věc
původní dotaz se zabývá tím (moje interpretace), jestli se testy dají teoreticky nahradit typovým systémem a já si vzhledem k tomu co jsem o tématu četl, myslím, že ano, dále mě zajímají praktické limity tohoto přístupu, protože z vlastní praxe ho považuju za extrémně užitečný

Chápeš to zcela přesně jak jsem to myslel.

[BoneFlute]

Mimochodem v TDD je pravidlem, že se píší vybrakované metody, které se teprve na stížnost hotových testů vyplňují, případně (a teď pozor, soudruzi javaři nečtěte dále, aby vám z toho nehráblo) se tyto metody teprve vytvářejí! :O :O :O (No nekecej!)

Tohle není odpověď pro JSH, ale autora dotazu Boneflute.

Obnošená vesta.

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?

[BoneFlute]

tak když někdo špatně pochopí problém, tak mu taky nic nezabrání napsat chybný test

To už ale nemá co dělat s problematikou testování, ale chápání řešené úlohy, zde nevznikne rozdíl při použití typového systému, nebo testů.

Samozřejmě.

[v]

já jsem ale o opakování implementace nic nepsal, pokud špatně pochopíte problém, můžete napsat test, který od funkce chce pro zadané vstupy jiné výstupy, než ty správné (z hlediska řešeného problému)

To je možné, ale je to spíše výjimečné. Daleko častější je případ, kdy ví správně, jaký výstup má být pro daný vstup, ale špatně to implementuje. Jednotkové testy řeší tenhle případ, a to silným typovým systémem nejde nahradit.

co si vlastně představujete pod pojmem "silný typový systém"? já přinejmenším ten implementovaný v GHC

[Reklama]

[Filip Jirsák]

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?

Vy jste se na nic netázal, vy jste konstatoval, že jednotkové testy nejsou při použití kvalitního typového systému potřeba (protože typový systém zajistí to, co jinak zajišťují jednotkové testy). Což není pravda, jak už zde bylo opakovaně dokázáno. Akorát to někteří nechápou a neustále navrhují různé typové systémy, které ovšem neodhalí chybu, která zde byla několikrát uvedena jako příklad, a kterou jednotkový test odhalí.

Pokud se příště budete chtít na něco dotázat, doporučuji zeptat se na to a ne tvrdit zjevný nesmysl.

[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.

[Filip Jirsák]

co si vlastně představujete pod pojmem "silný typový systém"? já přinejmenším ten implementovaný v GHC

Pro účely této diskuse si pod tím představuji ten nejsilnější teoreticky možný typový systém. Podstatou této diskuse je totiž to, že velká část problémů, které jsou podchycené jednotkovými testy, není řešitelná žádnými formálními mechanismy – protože formálně jsou přípustní všechny možnosti, ale pro řešení daného problému je přípustná jen jedna možnost.

[v]

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.

co tohle https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell ?
asi neumím říct, kde závislostní typy začínají
a "silný" je asi dost blbé označení

[v]

co si vlastně představujete pod pojmem "silný typový systém"? já přinejmenším ten implementovaný v GHC

Pro účely této diskuse si pod tím představuji ten nejsilnější teoreticky možný typový systém.

nevím, který to je, postněte odkaz

[BoneFlute]

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.

[Gődel]

nejdřív bych zdůraznil svůj postoj: neargumentuju proti testům, testy jsou dobrá věc
původní dotaz se zabývá tím (moje interpretace), jestli se testy dají teoreticky nahradit typovým systémem a já si vzhledem k tomu co jsem o tématu četl, myslím, že ano, dále mě zajímají praktické limity tohoto přístupu, protože z vlastní praxe ho považuju za extrémně užitečný

Chápeš to zcela přesně jak jsem to myslel.

Tohle téma je super (po dlouhé řadě trollotémat na Rootu), protože je zajímavé, aktuální a vybízí k hlubšímu zamyšlení. 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.

[BoneFlute]

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.

co tohle https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell ?
asi neumím říct, kde závislostní typy začínají
a "silný" je asi dost blbé označení

Tý vozo, jsem ani nedoufal, že to v Haskellu jde. To bude zase propálených hodin.

[JSH]

co si vlastně představujete pod pojmem "silný typový systém"? já přinejmenším ten implementovaný v GHC

Pro účely této diskuse si pod tím představuji ten nejsilnější teoreticky možný typový systém.

nevím, který to je, postněte odkaz

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.

[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ší