Typový system versus unittesty

[BoneFlute]

Zdravím.

Dospěl jsem k nezdravému přesvědčení, že jednotkové testy nejsou potřeba máte-li kvalitní typový systém.

(Teď samozřejmě neřeším který jazyk a zda něco takového má.)

Zajímalo by mě, můžete zkusit uvést nějaký příklad konstrukce, na kterou je nutné napsat test, protože typem to podchytit nejde?

Díky.

[Reklama]

[Honza]

Kéž by toto vlákno skončilo konstatováním, že typový systém nemůže nahradit unit testy...

[Franta <xkucf03/>]

To je hodně nezdravé přesvědčení :-D Je pravda, že jednotkové testy se často přeceňují, ale tak daleko bych nešel. Spíš bych to formuloval:

jednotkové testy nejsou tolik potřeba máte-li kvalitní typový systém

Metody/funkce ale nemají jen rozhraní (vstup-výstup, definiční obor, obor hodnot), ale (a to hlavně) nějakou logiku uvnitř, nějaký algoritmus. A ten potřebuješ otestovat. Neznám typový systém, který by dokázal deklarativně popsat i tu logiku uvnitř a nahradit testy.

[andy]

Ono záleží na tom, jak jsou ty typy definované. Jeden ze způsobů (v Haskellu hodně využívaný) JSON serializace (aeson) jsou instance FromJSON a ToJSON. Mělo by platit

Kód [Vybrat] Rozbalit


fromJSON . toJSON = Just

Což jinak než jednotkovými testy zkontrolovat nejde (kontroluje se to typicky přes QuickCheck property). Na druhou stranu je pravda, že lze ten typ serializace vyrobit tak, že se popíše způsob té serializace a ta možnost, že by bylo možné vyrobit vzájemně nekompatibilní FromJSON/ToJSON prostě nebude. I tak je ale typicky potřeba nějak otestovat, že alespoň ta knihovna je korektní.

Jednotkové testy prostě typicky píšu pro parsery. Ono se dost blbě typově popisuje, co má ten parser dělat. Pak třeba pro různé výpočty - jestli to počítá fakt správně. Pak třeba pro nějaké multi-threadované problémy (messagebus), jestli to dělá to, co to má dělat.

Metody/funkce ale nemají jen rozhraní (vstup-výstup, definiční obor, obor hodnot), ale (a to hlavně) nějakou logiku uvnitř, nějaký algoritmus. A ten potřebuješ otestovat. Neznám typový systém, který by dokázal deklarativně popsat i tu logiku uvnitř a nahradit testy.

No... dependent types dokážou hodně. https://www.youtube.com/watch?v=n-b1PYbRUOY - ukázka implementace red-black tree. Ono je to v podstatě takový model checker.... Ono se v typových systémech dá popsat docela hodně, ale je to někdy takové práce, že je rychlejší napsat si ty unit testy (nebo ještě líp quickcheck property testy)

[BoneFlute]

Ono záleží na tom, jak jsou ty typy definované. Jeden ze způsobů (v Haskellu hodně využívaný) JSON serializace (aeson) jsou instance FromJSON a ToJSON. Mělo by platit

Kód [Vybrat] Rozbalit


fromJSON . toJSON = Just

Což jinak než jednotkovými testy zkontrolovat nejde (kontroluje se to typicky přes QuickCheck property). Na druhou stranu je pravda, že lze ten typ serializace vyrobit tak, že se popíše způsob té serializace a ta možnost, že by bylo možné vyrobit vzájemně nekompatibilní FromJSON/ToJSON prostě nebude. I tak je ale typicky potřeba nějak otestovat, že alespoň ta knihovna je korektní.

Jednotkové testy prostě typicky píšu pro parsery. Ono se dost blbě typově popisuje, co má ten parser dělat. Pak třeba pro různé výpočty - jestli to počítá fakt správně. Pak třeba pro nějaké multi-threadované problémy (messagebus), jestli to dělá to, co to má dělat.

Tento příklad mi zrovna přijde celkem na pohodu. Nadefinuju si jednotlivé elementy jsonu, serialize to string. Že to dává smysl zkouknu okem, a pak zafixuju ala Elm.

[Reklama]

[BoneFlute]

jednotkové testy nejsou tolik potřeba máte-li kvalitní typový systém

Prosím, toto není námětem mé otázky.

[Gődel]

jednotkové testy nejsou potřeba máte-li kvalitní typový systém.

Jednotkové testy a typový systém řeší ortogonální problémy. Je ale pravda, že závislostní typy jsou nesmírně mocný nástroj a odchytí neuvěřitelné množství chyb. I tak je ale vhodné použít unit testy pro otestování logiky kódu (to typově dost dobře nejde).

[BoneFlute]

I tak je ale vhodné použít unit testy pro otestování logiky kódu (to typově dost dobře nejde).

Proč?

[tdvorak]

I tak je ale vhodné použít unit testy pro otestování logiky kódu (to typově dost dobře nejde).

Proč?

Jak typy zajistis, ze tvoje metoda sum(a,b) vraci pro int a a int b spravny int soucet? Jako alternativu k primitivnimu assertEquals(3, sum(1,2)) ?

[Ondra Satai Nekola]

Kéž by toto vlákno skončilo konstatováním, že typový systém nemůže nahradit unit testy...

...a naopak.

[uuuuuuuu]

Kéž by toto vlákno skončilo konstatováním, že typový systém nemůže nahradit unit testy...

...a naopak.

A naopak:  kez by to vlakno zacalo konstatovanim.....

[Kit]

Kéž by toto vlákno skončilo konstatováním, že typový systém nemůže nahradit unit testy...

...a naopak.

Prosil bych ukázku použití typového systému, ve které není možné provést náhradu jednotkovými testy.

[Filip Jirsák]

Prosil bych ukázku použití typového systému, ve které není možné provést náhradu jednotkovými testy.

Jedna věc je, zda je to teoreticky možné, druhá věc je, zda opravdu ručně psanými jednotkovými testy pokryjete všechny možnosti.

A snad ještě podstatnější je to, že typový systém používá programátor přímo při psaní (jako dokumentaci) – což je úplně něco jiného, než když bude zkoušet náhodně psát kód a zkoušet, jestli to projde jednotkovými testy.

[listoper]

Zdravím.

Dospěl jsem k nezdravému přesvědčení, že jednotkové testy nejsou potřeba máte-li kvalitní typový systém.

(Teď samozřejmě neřeším který jazyk a zda něco takového má.)

Zajímalo by mě, můžete zkusit uvést nějaký příklad konstrukce, na kterou je nutné napsat test, protože typem to podchytit nejde?

Díky.

Je to kacir. Upalte ho!

A ted vazne. Budeme povazovat napriklad clojure.spec za soucast typoveho systemu, nebo nastroj pro testovani?
A co generativni property based testing (napr. QuickCheck)? Je definice vlastnosti funkce typova zalezitost nebo testovaci?

Btw. diky za to otazku. Samotneho by me ani nenapadlo o tom premyslet a ted mam pocit ze jsem dosahl dilciho osviceni.

[andy]

Tento příklad mi zrovna přijde celkem na pohodu. Nadefinuju si jednotlivé elementy jsonu, serialize to string. Že to dává smysl zkouknu okem, a pak zafixuju ala Elm.

Tomu asi nerozumím - je poměrně jednoduché vytvořit ToJSON a FromJSON tak, aby to navzájem kompatibilní nebylo. Tak, jak jsou ty typeclassy oddělené, nejde typově zajistit, že to kompatibilní je. Je možné vyrobit ty typy jinak. Nicméně parsing obecně typově kontrolovat nejde - ten soulad se specifikací prostě do typu té funkce

Kód [Vybrat] Rozbalit

Text -> ParsedValue nenakóduju.

Jak typy zajistis, ze tvoje metoda sum(a,b) vraci pro int a a int b spravny int soucet? Jako alternativu k primitivnimu assertEquals(3, sum(1,2)) ?

No já bych řekl, že to pude (nejsem teda vůbec expert na dependent types), ale Nat (natural number) jako typ existuje, udělat součet v peanově algebře (fakt nevim o čem mluvim) jde taky a dopsat k tomu ty důkazy do těl funkcí je poměrně primitivní záležitost. Ale pravda, je to trošku cvičení o ničem...

A co generativni property based testing (napr. QuickCheck)? Je definice vlastnosti funkce typova zalezitost nebo testovaci?

IMO testovací.