Typový system versus unittesty

[BoneFlute]

Psal jsem, že v tom nejsem expert...ale ta idea je něco ve stylu

Kód: [Vybrat]

(ty typy musí být nějak jinak, ale nedám to dohromady)
add :: (HNat a, HNat b, HAdd a b c) => a -> b -> c
add ... následuje přičítání jedničky, pokud první argument není 0...
Je to dost zbytečné cvičení, a tak trošku to přesměrovává problém od "spletl jsem se v pojmenování" na "spletl jsem se v typu". Ale svým způsobem to je třeba odpověď na autorovu otázku - ano, typový systém odhalí chyby v kódu, ale jak odhalí chyby v typech?

Ano, křížová kontrola. Přiznávám unittestům bod :-)
Stejně jako se můžeš splést v typu, můžeš se splést v testu. Jenže jako v testu kontroluješ, zda to testuje co má pohledem, stejně tak můžeš u typu. Jako v testu kontroluješ změnu oproti předchozímu, stejně tak to umí elm u typů.

Takže zůstává jen ta křížová kontrola, kdy u testů to píšu dvakrát. Jenže, stejně tak může kompilátor generovat usecase, a ty ukazovat... No ale to už jsme zase trochu jinde.

Ale u typoveho systemu nutis nepritele, aby prinesl program s dalsimi (strojove overitelnymi) castmi...

Teď nerozumím - typový systém třeba Javy umí rozhodnout Null/NonNull (někdy...) bez ohledu na to, že to vlastně v tom typovém systému "není". Ty typeclassy FromJSON/ToJSON jsou udělány tak, že kompiler kompatibilitu prostě rozhodnout nemůže. Halting problém byl v tom smyslu, že i kdyby na to kompiler šel analýzou kódu jako Java, tak tu property "fromJSON . toJson = Just" stejně nemůže (obecně) rozhodnout.

Předpokládám, že kompiler:
Mám json element číslo, převést na string a zpět. Element string, detto. Element Struct obsahující číslo, na string a zpět. Dále je to rekursivní, takže to už nemusím.

Asi by se našlo něco, kde by to začalo být hodně divoké. Jenže pak je otázka, zda v takovém případě by si nevylámal zuby i unittest. Nevím.

[Reklama]

[Filip Jirsák]

elm-package odhalí

Cože? elm-package odhalí, že jste se překlepl v operátoru? Řekl bych, že nastal čas pro to, abyste také vy ukázal svůj kód.

Je to dost zbytečné cvičení, a tak trošku to přesměrovává problém od "spletl jsem se v pojmenování" na "spletl jsem se v typu". Ale svým způsobem to je třeba odpověď na autorovu otázku - ano, typový systém odhalí chyby v kódu, ale jak odhalí chyby v typech?

Ono by to vůbec bylo schování všech možných algoritmů do typů. Typy jsou ale součástí kódu, takže tím si nijak nepomůžeme.

[Filip Jirsák]

Jenže pak je otázka, zda v takovém případě by si nevylámal zuby i unittest. Nevím.

Jednotkový test testuje jenom to, co do testu napíše programátor. A spousta jednotkových testů se píše jednoduše tak, že kontrolují, zda pro zadané vstupní hodnoty dává jednotka očekávaný výstup. Není to nic světoborného, ale praxe ukazuje, že i hloupé třídění není snadné napsat na první pokus správně, takže i testy, které z miliard možných vstupů otestují těch pět správných dokážou odhalit většinu chyb, které v praxi nastávají.

[Kiwi]

Chjo, tak jinak.

Předpokládejme, že Pepa píše program a nechce v něm mít chyby. A chce využít všechny možnosti, ale co nejjednodušším způsobem. A co nejrychlej. Takže:
- Je lepší při chybě program nepřeložit a dostat rovnou hlášku "type mismatch @ line 256", než týden procházet logy
- Je lepší, pokud má funkci

Kód: [Vybrat]

speed_t avgSpeed( distance_t distance, time_t time) { ... }
a vyběhne na něj při překladu rovnou varování, že prohodil argumenty, než když na to přijde tesťák náhodou
- A chce mít podchyceno, že se opravdu implementuje správný vzorec, takže dá i unit test, který ho upoyorní, že ten výpočet je blbě.
- A protože chce vědět, jestli větší celek programu běhá správně, hodít am i integrační testy.

Takže s čím se to dělá efektivně ohlídá datový typ (bez práce a před commitem), co se dělá ohlídá unit test.

Pokud se i "s čím to dělám" musí (v základu) hlídat unit testem, tak je něco blbě (= jazyk stojí za starou bačkoru)

Jestli to má být v C a jestli to jsou všechno ve skutečnosti jen doubly, tak na něj nevyběhne nic, protože všechny tři typy jsou kompatibilní. Pokud by kompilátor hlásil varování v každé takové situaci, tak by v programech rozsahem i jen málo nad rámec učebnicových příkladů vyhazoval tolik varování, že by se v nich ta relevantní ztratila, protože většina by byla planými poplachy. Další možností by bylo všude přetypovávat, což by zase vedlo k nepřehlednosti programu.

[.]

A zatímco úzká skupinka akademiků si posilovala své ego a pocit nadřazenosti teoretizováním o abstraktních problémech, někdo reálný napsal reálný program, který pomohl vyřešit konkrétní problém.

Nic proti akademikům, ale pokud chybí alespoň elementární porce pokory, zbude jen prázdnota a nadutost.

/* Možná je hodnocení moc příkré, ale po přečtení vlákna si nemohu pomoct. */

[Reklama]

[.]

Jestli to má být v C a jestli to jsou všechno ve skutečnosti jen doubly, tak na něj nevyběhne nic, protože všechny tři typy jsou kompatibilní. Pokud by kompilátor hlásil varování v každé takové situaci, tak by v programech rozsahem i jen málo nad rámec učebnicových příkladů vyhazoval tolik varování, že by se v nich ta relevantní ztratila, protože většina by byla planými poplachy. Další možností by bylo všude přetypovávat, což by zase vedlo k nepřehlednosti programu.

C nepatří mezi silně typové jazyky a pokud si na to člověk zvykne, má pocit, že to přece nemůže být jinak. Ale velké množství chyb a zkušenosti z takovýchto jazyků ukazují, že při správném návrhu to s tím přetypováváním není tak žhavé a vývoj to naopak značně zrychlí.

[BoneFlute]

A zatímco úzká skupinka akademiků si posilovala své ego a pocit nadřazenosti teoretizováním o abstraktních problémech, někdo reálný napsal reálný program, který pomohl vyřešit konkrétní problém.

Nic proti akademikům, ale pokud chybí alespoň elementární porce pokory, zbude jen prázdnota a nadutost.

/* Možná je hodnocení moc příkré, ale po přečtení vlákna si nemohu pomoct. */

Tak já mám k papírovým akademikům dost daleko. Ale to, že jsem přičichl k statickým typům, dokonce i nedobrovolně nakouklu do teorie typů (grupy axiomy a tyhlencty vymyšlenosti) mi dost otevřelo oči. A začal jsem se i u pitomejch jazyků jako je php, java, javascript, nebo python uvažovat jinak. Snad ku prospěchu věci.

Třeba u mě se opakuje scénář: píšu v Javě, načichnu tím stylem. Po nějaké době mě to začne rozčilovat. Pak zkouším nějaký projekt a tak si řeknu, že to tentokrát zkusím v Pythonu. Nejdřív nadšení, jak jde všechno snadno a krásně, a pak když navzdory incrementálnímu vývoji už třetí den nedělám nic jiného než že spouštím aplikaci a opravuju chyby mě to začne štvát z druhé strany. Tak se vrátím zpět k Javě. Tam mě začne štvát, že žádné typy neumí, tak zkusím Scalu, Haskell...

U Haskellu to byla zatím největší spokojenost. Poněkud náročné na hlavu, ale jinak se dá. Nejvíc mě zatím vadilo, když mi totálně vyhnil cabal. Tak ale za to jazyk nemůže.

[BoneFlute]

elm-package odhalí

Cože? elm-package odhalí, že jste se překlepl v operátoru?

Ne. Překlep pozná už kompilátor. Že se změnila signatura oproti minule (tedy, to co dělají testy) odhalí elm-package.

[Gődel]

A zatímco úzká skupinka akademiků si posilovala své ego a pocit nadřazenosti teoretizováním o abstraktních problémech, někdo reálný napsal reálný program

Ti akademici jsou taky reální A museli tomu tvůrci "reálného programu" vymyslet a implementovat překladač nebo interpretr, aby to svoje veledílo mohl napsat a pustit

[Gődel]

Tak já mám k papírovým akademikům dost daleko. Ale to, že jsem přičichl k statickým typům, dokonce i nedobrovolně nakouklu do teorie typů (grupy axiomy a tyhlencty vymyšlenosti) mi dost otevřelo oči. A začal jsem se i u pitomejch jazyků jako je php, java, javascript, nebo python uvažovat jinak.

Gratuluju. To je normální vývoj u člověka, co se chce zdokonalovat a je schopen pochopit mírně abstraktní poznatky. V IT bohužel převažují zakrnělí pologramoti...

[Gődel]

U Haskellu to byla zatím největší spokojenost. Poněkud náročné na hlavu

Co tam je tak náročného?

[Filip Jirsák]

Ne. Překlep pozná už kompilátor.

Jak? Můžete to konkrétně ukázat na těch funkcích add() a sub().

Že se změnila signatura oproti minule (tedy, to co dělají testy) odhalí elm-package.

Ne, testy dělají něco jiného, svým způsobem přesný opak. Kdybyste si chtěl kód jenom vyzkoušet, nepotřebujete celou infrastrukturu kolem testů – prostě byste si to jednou zkusil, a kdyby to fungovalo, testovací kód byste smazal. Celá ta infrastruktura kolem testů a jejich pravidelné spouštění ale slouží právě k tomu, abyste odhalil chyby při změnách kódu. Takže test nemůže záviset na signatuře implementace, protože celý smysl testu je v tom, že implementace dává pro zadaný vstup očekávaný výstup bez ohledu na to, jaká je zrovna použitá implementace.

[BoneFlute]

U Haskellu to byla zatím největší spokojenost. Poněkud náročné na hlavu

Co tam je tak náročného?

Aktuálně se peru s existencionálními typy aka forall. Už mi to nějaký chlápek vysvětloval, ale nedostatečně jsem si to zažil, a zase zapoměl.

[BoneFlute]

Takže test nemůže záviset na signatuře implementace, protože celý smysl testu je v tom, že implementace dává pro zadaný vstup očekávaný výstup bez ohledu na to, jaká je zrovna použitá implementace.

Právě jsi popsal, co dělají typy. Je-li typem definováno, že výsledek funkce má být ytý succ x, tak to vždycky pozná, že je implementace správně (budeme-li o odvozování kompilátorem mluvit jako o jeho implementaci).

[BoneFlute]

Hrál jsem si typem Date, jen pro ukázku:
Naivní implementace, naprosto nedostatečná (a v reálu nejpoužívanější):

Kód: [Vybrat]

type Data = {year: Int, month: Int, day: Int}

O něco málo lepší:

Kód: [Vybrat]

type Data = {year: Int, month: Int 1 12, day: Int 1 31}

elm-package^* zařve, protože se změnila logika

Už použitelná:

Kód: [Vybrat]

type Data = {year: Int, month: 1|3|5|7|8|10|12, day: Int 1 31}
                | {year: Int, month: 4|6|9|11, day: Int 1 30}
                | {year: Int, month: 2, day: Int 1 28}
elm-package zařve, protože se změnila logika

A mohl bych pokračovat dál a dál, zohlednit rok nula, zohledňovat přestupné roky, ...

Každopádně ta elegance se s ukecanýmy a nedostatečnými testy nedá srovnat.

Nevěřím, že by ty typy skutečně dokázali popsat všechno. Ale těch hranic se nedokážu dopátrat :-)

^* elm-package ve skutečnosti samozřejmě nezařve, protože Elm neumí závislostní typy, ale jde o princip, kdy nějaký nástroj typů dokáže vykrást doménu testů.