Typový system versus unittesty

[v]

typy můžou být definovány v knihovnách a mezi testem a tím v článku je přece jenom trochu rozdíl, ty záruky (pro všechny dvojice přirozených čísel) prostě testama nelze nahradit

Měl jem na mysli hlavně typy, které v knihovnách definovány nejsou a které je třeba definovat ke každé uživatelské funkci. Kdybych to aplikoval například na určitý integrál s mezemi a, b a funkcí f(x), tak ta definice typu bude buď nehorázně složitá, anebo bude duplicitou té funkce. Úplně se tím vytratí kouzlo jednoduchosti funkcionálního jazyka.

pokud se bavíme o tom co teoreticky jde, tak je jedno jestli je to komplikované, pokud se bavíme o tom co je praktické, tak na integrál apod. to nikdo () aplikovat nebude, použití v http://augustss.blogspot.com/2009/06/more-llvm-recently-someone-asked-me-on.html je aspoň pro mě takový sweet spot (viz též https://hackage.haskell.org/package/TTTAS-0.6.0)

[Reklama]

[v]

Pro pořádek, hodíte sem link na ten příspěvek, prosím? Protože je možné, že jsem to mezi spoustou toho smetí přehlédl.

Zde: https://forum.root.cz/index.php?topic=18804.msg270520#msg270520

myslím, že jsem vám psal (?), že tohle by se nepřeložilo

Když tu tak čtu tu diskusi (a některým věcem nerozumím), tak mě napadá, že by asi šlo testy nahradit nějakým typovým systémem, ale jeho složitost by byla extrémní. Z praktického hlediska testy vyměňují obecnost (kategorie) či případnou složitost typového systému za svoji neúplnost (testování diskrétních hodnot) - diskrétní hodnoty by musely být nahrazeny mnoha specifickými třídami vedoucími na výraznou složitost typového systému. Uvažuju správně?

kurz und gut, že něco jde ještě neznamená, že to je dobrý nápad

[ava]

Mě by zajímalo: Pokud tvrdíte, že typy dokáží nahradit unit testy, jak by se (jen teoreticky, ať se to překládá třeba sto let) naimplementovala funkce incrementString převádějící čísla uloženého ve stringu (třeba "42") na string obsahující číslo o jedna vyšší ("43") tak, aby typová kontrola dokázala nahradit alespoň (ne všechny případy pokrývající, situaci by mohl výrazně zlepšit např. nějaký property check test, ale to není pointou příspěvku) unit test

assertEqual("43", incrementString("42"))

? (nevalidní čísla není třeba pro potřeby příkladu uvažovat, můžeme pro ně např. chtít vrátit prázdný string)

[Radek Micek]

Mě by zajímalo: Pokud tvrdíte, že typy dokáží nahradit unit testy, jak by se (jen teoreticky, ať se to překládá třeba sto let) naimplementovala funkce incrementString převádějící čísla uloženého ve stringu (třeba "42") na string obsahující číslo o jedna vyšší ("43") tak, aby typová kontrola dokázala nahradit alespoň (ne všechny případy pokrývající, situaci by mohl výrazně zlepšit např. nějaký property check test, ale to není pointou příspěvku) unit test

assertEqual("43", incrementString("42"))

? (nevalidní čísla není třeba pro potřeby příkladu uvažovat, můžeme pro ně např. chtít vrátit prázdný string)

Treba v jazyce Idris existuje za timto ucelem datovy typ So : Bool -> Type, jehoz jedina hodnota je Oh a ta ma typ So True.

Pak staci psat

Kód: [Vybrat]

nazevTestu : So ("43" == incrementString("42"))
nazevTestu = Oh

Pokud tedy pozadovano rovnost neplati, ma nazevTestu typ So False jenze Oh ma typ So True, takze se program neprelozi.

[ava]

Mě by zajímalo: Pokud tvrdíte, že typy dokáží nahradit unit testy, jak by se (jen teoreticky, ať se to překládá třeba sto let) naimplementovala funkce incrementString převádějící čísla uloženého ve stringu (třeba "42") na string obsahující číslo o jedna vyšší ("43") tak, aby typová kontrola dokázala nahradit alespoň (ne všechny případy pokrývající, situaci by mohl výrazně zlepšit např. nějaký property check test, ale to není pointou příspěvku) unit test

assertEqual("43", incrementString("42"))

? (nevalidní čísla není třeba pro potřeby příkladu uvažovat, můžeme pro ně např. chtít vrátit prázdný string)

Treba v jazyce Idris existuje za timto ucelem datovy typ So : Bool -> Type, jehoz jedina hodnota je Oh a ta ma typ So True.

Pak staci psat

Kód: [Vybrat]

nazevTestu : So ("43" == incrementString("42"))
nazevTestu = Oh

Pokud tedy pozadovano rovnost neplati, ma nazevTestu typ So False jenze Oh ma typ So True, takze se program neprelozi.

Hmm, jestli chápu správně, tak pro tento příklad jedna (zřejmě dost pozdní) z fází překladu v jazyce Idris je vlastně spuštění kódu "43" == incrementString("42")?

Taková "typová kontrola" mi nakonec zní dost podobně jako unit test (což je také spuštění kódu), s tím rozdílem, že u unit testu si sám rozhodnu, že když dopadne červeně, mám kód považovat za nevalidní, kdežto v příkladu s Idris to za mě rozhodne překladač (kód je vždy nevalidní). Nebo je tam nějaký další rozdíl, který nevidím?

Každopádně je to zajímavé, ale jestli jsem to pochopil správně, paradoxně mi to vychází spíš jako argument pro unit testy

[Reklama]

[BoneFlute]

Pro pořádek, hodíte sem link na ten příspěvek, prosím? Protože je možné, že jsem to mezi spoustou toho smetí přehlédl.

Zde: https://forum.root.cz/index.php?topic=18804.msg270520#msg270520

Obávám se, že toto je ta samá věc, kterou uváděl Filip Jirsák. A tuším, že tu bylo minimálně dvakrát poukazováno, že to by problém být neměl - viz závislostní typy.

[BoneFlute]

V tomto vláknu https://forum.root.cz/index.php?topic=18370.0 , díky pěkné odpovědi od @andi-ho, jsem si uvědomil jednu věc:

Mám zápis, čitelný pro stroj:

Kód: [Vybrat]

    case s `hasMinimumLen` 4 of
        Just sn -> Str.sub sn 20
        Nothing -> "default"
Ale pro člověka je mnohem lepší zápis:

Kód: [Vybrat]

    if (Str.len s) < 4 then
        "default"
    else
        Str.sub s 20
Jenže není vůbec žádný problém naučit stroj, aby ten druhý, lidský zápis chápal a převedl si ho na ten svůj.

Tudíž já mohu napsat:

Kód: [Vybrat]

add x y = x + y

stroj si to převede na svou reprezentaci (něco jako x * succ y), ale podstatné je, že když změním implementaci:

Kód: [Vybrat]

add x y = y + x
add x y = if x == 0 then y else x + y

tak stroj pozná, že je to stejného typu, a nebude mět výhrady, zatímco

Kód: [Vybrat]

add x y = if x < 1 then y else x + y

odmítne.

Pointa je tedy taková, že možná není tak úplně nutné, aby psaní těch komplexních typů bylo nějak zvláště o tolik složitější než na to napsat test. Záleží, jak dobře se to navrhne.

[Filip Jirsák]

Obávám se, že toto je ta samá věc, kterou uváděl Filip Jirsák. A tuším, že tu bylo minimálně dvakrát poukazováno, že to by problém být neměl - viz závislostní typy.

Nazval bych to teologickým programováním: „Když něčemu nerozumím, musí to být všemocné“. (Po této fázi následuje fáze zklamání, že to příslušný jazyk nebo koncepce „neumí“, zařazení jazyka či koncepce na seznam špatných jazyků/koncepcí a vyhlédnutí dalšího kandidáta, který už určitě bude dokonalý.)

Vy se stále touláte někde ve výšinách, ale unikají vám základní věci. Testy se píšou proto, aby odhalily případné chyby v programu. Na tom se shodneme? Tedy pokud program může obsahovat chyby, má smysl psát testy. Na tom se také shodneme? Pak tedy platí, že testy nemá smysl psát jenom u programu, u kterého bezpečně víme, že neobsahuje žádnou chybu. I na tom se shodneme? Takže vy tu vlastně hledáte způsob, jak docílit toho, aby platilo „pokud to šlo  zkompilovat, není v tom žádná chyba“, je to tak?

[Filip Jirsák]

Pointa je tedy taková, že možná není tak úplně nutné, aby psaní těch komplexních typů bylo nějak zvláště o tolik složitější než na to napsat test. Záleží, jak dobře se to navrhne.

Test pokrývá jen malou množinu vstupů z (často teoreticky nekonečné) množiny všech možných vstupů. Jak by asi „kompilátor“ doplnil definici toho komplexního typu pro vstupy, které by tím testem nebyly pokryté?

Napsat test může být takhle jednoduché:

Kód: [Vybrat]

assert 5 == fun(2, 3)
assert 3 == fun(1, 2)

Co k tomu přidáte, aby to popisovalo komplexní typ?

[wamba]

Napsat test může být takhle jednoduché:

Kód: [Vybrat]

assert 5 == fun(2, 3)
assert 3 == fun(1, 2)


V Perlu 6 by šel napsat typ (resp. podtyp), který jen kontroluje tyto případy

Kód: [Vybrat]

subset Add where { $++ || add(1,1) == 2 && add(2,3) == 5 };
sub add ( $a, $b --> Add ) { $a + $b };

say add 1,2 ;
ale samozřejmě chápu, že k tomuto původní dotaz nesměřoval

[JSH]

tak možná jsem zvolil trochu matoucí příklad, JIT je tam to co se implementuje, ne technika, která se využívá k implementaci něčeho jiného (uff)
kouzelný typ tam je "data TExp a" a pointa je, že nejde vytvořit hodnota tohoto typu, která by reprezentoval chybně typovaný syntaktický strom

Tak já zopakuju svůj blbý dotaz. Ty instance toho typu TExp se vytvářejí v runtime? Jestli ne, tak proč to neprohnat přímo skrz ghc (se všemi omezeními, které už jsem zmiňoval)?
Pokud se vytvářejí v runtime, tak je to argument pro unit (a ostatní) testy. Udělat z Haskellu dynamicky typovaný jazyk je sice cool, ale jako u každého jiného dynamicky typovaného jazyka ztrácím typovou kontrolu v době překladu a jsem odkázáný čistě na ty testy.

[v]

tak možná jsem zvolil trochu matoucí příklad, JIT je tam to co se implementuje, ne technika, která se využívá k implementaci něčeho jiného (uff)
kouzelný typ tam je "data TExp a" a pointa je, že nejde vytvořit hodnota tohoto typu, která by reprezentoval chybně typovaný syntaktický strom

Tak já zopakuju svůj blbý dotaz. Ty instance toho typu TExp se vytvářejí v runtime? Jestli ne, tak proč to neprohnat přímo skrz ghc (se všemi omezeními, které už jsem zmiňoval)?
Pokud se vytvářejí v runtime, tak je to argument pro unit (a ostatní) testy. Udělat z Haskellu dynamicky typovaný jazyk je sice cool, ale jako u každého jiného dynamicky typovaného jazyka ztrácím typovou kontrolu v době překladu a jsem odkázáný čistě na ty testy.

ano, v runtime, je to miniaturní překladač, překladače mají  dispozici překládaný kód až v runtime (TExp je syntaktický strom překládaného "jazyka")

[SB]

Zde: https://forum.root.cz/index.php?topic=18804.msg270520#msg270520

myslím, že jsem vám psal (?), že tohle by se nepřeložilo

Právěže přeložilo, syntakticky ani typově to nemá chybu, ale významově už ano.

[JSH]

ano, v runtime, je to miniaturní překladač, překladače mají  dispozici překládaný kód až v runtime (TExp je syntaktický strom překládaného "jazyka")

Konečně. Takže tady má BoneFlute příklad, kdy unittesty (nebo testy obecně) nejde nahradit typovým systémem. A to ani hypoteticky za jakýchkoliv předpokladů. Prostě proto, že se typový systém dostane ke slovu až v runtimu.

[v]

Zde: https://forum.root.cz/index.php?topic=18804.msg270520#msg270520

myslím, že jsem vám psal (?), že tohle by se nepřeložilo

Právěže přeložilo, syntakticky ani typově to nemá chybu, ale významově už ano.

nepřeložilo, reprezentace celých čísel, kterou to používá má pro každé konkrétní číslo jiný datový typ (to jsou ty "dependent types"), ale neznamená to, že musíte pro každé číslo implementovat funkcionalitu zvlášť, ten typový systém je docela chytrý