Typový system versus unittesty

Re:Typový system versus unittesty
« Odpověď #150 kdy: 19. 06. 2018, 14:18:41 »
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.


BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #151 kdy: 19. 06. 2018, 14:19:07 »
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #152 kdy: 19. 06. 2018, 14:25:00 »
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

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #153 kdy: 19. 06. 2018, 14:30:09 »
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

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


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

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

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

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

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

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

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

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

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

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