Typový system versus unittesty

[Kiwi]

Uz jsem si vpomel na nazev, to rucni odmocnovani je newtonuv vzorec.

Fi = F0 - f(x)/f'(x)

Konkrétně tzv. babylonská metoda. Newtonův vzorec je iterativní metoda obecně na řešení transcendentních rovnic.

[Reklama]

[JSH]

Tak za prvé, pomocí unittestů to taky implementuju ještě jednou.

Tak to ani náhodou. Unittesty obvykle testují jenom významné případy. Automaticky porovnat dvě implementace mezi sebou není vůbec jednoduché.
Ty vybrané případy můžou být významné na základě modelovaného problému, autorova odhadu, nebo prostě proto, že to na tomhle už někdy vybouchlo. Implementovat to ještě jednou je naopak kontraproduktivní. Pokud tu referenční implementaci nedělá někdo nezávislý, tak je velká šance, že tam autor naseká dost podobné chyby.

A za druhé, nikde jsem nepsal, že se to tak má dělat, nebo tak něco. Je to jen úvaha. Praktičnost toho není obsahem mé otázky.

V našem oboru neexistuje nic, co by se nedalo hrnout přímo v hexa. Všechno od assembleru výš je o té praktičnosti.

Jde mi o to, že typy a unittesty chytají s přiměřenou námahou různé druhy chyb. Třeba přehozené pořadí násobení matic nejde přes typy skoro odhalit. Leda že by sémantika výsledku byla celá zakódovaná v typech. Ale to pak přesune problém jenom o úroveň výš, protože je třeba nějak ověřit ty komplikované typy.

[v]

tohle vlákno mě přimělo juknout se znovu na kousek kódu se kterým jsem si nedávno hrál, a světe div se, našel jsem tam chybu v type family, která měla zajišťovat korektnost (jeden z aspektů) programu vygenerovaného překladačem (takovým překladačem na hraní), takže taky hlasuju za nezavrhování testů
najdi jeden rozdíl (a uvaž, který případ je vlastně "správně"):

Kód: [Vybrat]

type family Drop (a :: [*]) (b :: [*]) :: [*] where
Drop '[] b = b
Drop (a ': a') (b ': b') = Drop a' b'


Kód: [Vybrat]

type family Drop (a :: [*]) (b :: [*]) :: [*] where
Drop '[] b = b
Drop (a ': a') (a ': b') = Drop a' b'


[stejně jsme to tušili]

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

+1 

[BoneFlute]

Tak za prvé, pomocí unittestů to taky implementuju ještě jednou.

Tak to ani náhodou. Unittesty obvykle testují jenom významné případy. Automaticky porovnat dvě implementace mezi sebou není vůbec jednoduché.
Ty vybrané případy můžou být významné na základě modelovaného problému, autorova odhadu, nebo prostě proto, že to na tomhle už někdy vybouchlo. Implementovat to ještě jednou je naopak kontraproduktivní. Pokud tu referenční implementaci nedělá někdo nezávislý, tak je velká šance, že tam autor naseká dost podobné chyby.

A za druhé, nikde jsem nepsal, že se to tak má dělat, nebo tak něco. Je to jen úvaha. Praktičnost toho není obsahem mé otázky.

V našem oboru neexistuje nic, co by se nedalo hrnout přímo v hexa. Všechno od assembleru výš je o té praktičnosti.

Jde mi o to, že typy a unittesty chytají s přiměřenou námahou různé druhy chyb. Třeba přehozené pořadí násobení matic nejde přes typy skoro odhalit. Leda že by sémantika výsledku byla celá zakódovaná v typech. Ale to pak přesune problém jenom o úroveň výš, protože je třeba nějak ověřit ty komplikované typy.

Nejsme ve sporu.

[Reklama]

[BoneFlute]

tohle vlákno mě přimělo juknout se znovu na kousek kódu se kterým jsem si nedávno hrál, a světe div se, našel jsem tam chybu v type family, která měla zajišťovat korektnost (jeden z aspektů) programu vygenerovaného překladačem (takovým překladačem na hraní), takže taky hlasuju za nezavrhování testů
najdi jeden rozdíl (a uvaž, který případ je vlastně "správně"):

Kód: [Vybrat]

type family Drop (a :: [*]) (b :: [*]) :: [*] where
Drop '[] b = b
Drop (a ': a') (b ': b') = Drop a' b'


Kód: [Vybrat]

type family Drop (a :: [*]) (b :: [*]) :: [*] where
Drop '[] b = b
Drop (a ': a') (a ': b') = Drop a' b'


Mám vyhrabat nějaký unittesty?

To je jako ten oblíbenej hejt na Lisp, že je to plné závorek. To ano, protože každá závorka v Lispu reprezentuje jednu třídu v Javě.

[Filip Jirsák]

Nejsme ve sporu.

Jste. Vy jste napsal nesmysl, že v jednotkových testech něco implementujete znovu, JSH vám to správně vyvracel, že implementovat něco v jednotkovém testu znova je obvykle velmi špatně.

Mám vyhrabat nějaký unittesty?

Ano, myslím, že už je na čase.

[Gœdel]

Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.

[JSH]

Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.

Šlo by to tvrzení trochu rozvést? Generika, nebo i implicitní typy bych bral, ale silné typování samo o sobě tyhle věci neimplikuje.

[Gœdel]

Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.

Šlo by to tvrzení trochu rozvést? Generika, nebo i implicitní typy bych bral, ale silné typování samo o sobě tyhle věci neimplikuje.

“Silné” ve smyslu aspoň s HKT, prostě něco víc než Java. Generika jsou prvním stupněm. HKT umožní ještě více sdílení a závislostní typy ještě o stupeň více.

[SB]

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

Jak jste k tomu dospěl?

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?

class Sčítačka {
    Int součet(Int a, Int b) {
        <cokoliv>
    }
}

Int je třídou pro celá čísla (třeba vlastní implementace). Výsledek je nutně typu (správně instancí) Int, to je ale jediná věc, kterou vám typový systém garantuje. To ale nestačí - jak tento typ (třída) garantuje, že 1+1 rovná se opravdu 2???

Diskusi jsem nečetl - má to po výše uvedeném ještě smysl číst?

[v]

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?

class Sčítačka {
    Int součet(Int a, Int b) {
        <cokoliv>
    }
}

Int je třídou pro celá čísla (třeba vlastní implementace). Výsledek je nutně typu (správně instancí) Int, to je ale jediná věc, kterou vám typový systém garantuje. To ale nestačí - jak tento typ (třída) garantuje, že 1+1 rovná se opravdu 2???

Diskusi jsem nečetl - má to po výše uvedeném ještě smysl číst?

třeba peanova čísla na typové úrovni, v haskellu docela banální

Kód: [Vybrat]

type family Append a b where ...
součet :: I a -> I b -> I (Append a b)
součet = ...


[JSH]

třeba peanova čísla na typové úrovni, v haskellu docela banální

Kód: [Vybrat]

type family Append a b where ...
součet :: I a -> I b -> I (Append a b)
součet = ...


Jak by to mělo pomoct?
Součet dvou čísel je jenom příklad nějakého (netriviálního) výpočtu. Pokud ho popíšu v typu, tak jenom přesunu potenciálně vadný kód někam jinam. Pořád nevím, jestli je dobře. Akorát jsem se přesunul z deště pod okap, protože ten typ se čte hůř než původní kód.

[Filip Jirsák]

Diskusi jsem nečetl - má to po výše uvedeném ještě smysl číst?

Záleží na tom. Ten váš příklad je v diskusi uveden několikrát, ale nepomohlo to…

[v]

třeba peanova čísla na typové úrovni, v haskellu docela banální

Kód: [Vybrat]

type family Append a b where ...
součet :: I a -> I b -> I (Append a b)
součet = ...


Jak by to mělo pomoct?
Součet dvou čísel je jenom příklad nějakého (netriviálního) výpočtu. Pokud ho popíšu v typu, tak jenom přesunu potenciálně vadný kód někam jinam. Pořád nevím, jestli je dobře. Akorát jsem se přesunul z deště pod okap, protože ten typ se čte hůř než původní kód.

ptal jste se na typ, který garantuje, že kód provádí součet a ten jsem naznačil
nic se nepřesouvá, pořád máte zvlášť program a jeho typ, že se v tom dá udělat chyba? no jistě, to jde všude