Typový system versus unittesty

Bacsa

Re:Typový system versus unittesty
« Odpověď #765 kdy: 22. 08. 2018, 19:07:24 »
Pořádná typová kontrola prostě musí probíhat v mé pracovní době a pokud možno u mně na stole.
Toto je zásadní omyl. Nad záv. typy se korektnost dokazuje symbolicky, nevadí, není-li nějaká hodnota známa. Matoucí IMHO je, že se tomu říká typová kontrola, kterou lidi znají tak nanejvýš z Javy nebo céčka (pythonisti a spol. vůbec). Za to můžeme poděkovat Currymu a Howardovi (nezávisle). Můžu mít například funkci getVect, co mi načte od uživatele vektor nad ω libovolné délky (typu IO (Maybe ((n:Nat) ** Vect n Nat))). Where's the problem?
K tomu IO, nechápu význam IO (), proč to může jít do >>=, když ten vnitřní typ nemá žádné hodnoty?
() je normální hodnota
Kód: [Vybrat]
Idris> ()
() : ()
() je typ ;) Je to void bez hodnot.
neřekl bych, viz https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Builtins.idr
() je Unit, typ s jednou hodnotou
Jo, mea culpa, sorry  :-\


v

Re:Typový system versus unittesty
« Odpověď #766 kdy: 22. 08. 2018, 19:18:52 »

Bacsa

Re:Typový system versus unittesty
« Odpověď #767 kdy: 22. 08. 2018, 19:38:12 »
stane se
Pořád to ale neodpovídá na tu otázku.

v

Re:Typový system versus unittesty
« Odpověď #768 kdy: 22. 08. 2018, 19:45:31 »
stane se
Pořád to ale neodpovídá na tu otázku.
jaké je její aktuální znění?

Bacsa

Re:Typový system versus unittesty
« Odpověď #769 kdy: 22. 08. 2018, 19:49:34 »
stane se
Pořád to ale neodpovídá na tu otázku.
jaké je její aktuální znění?
"význam IO (), proč to může jít do >>="


Bacsa

Re:Typový system versus unittesty
« Odpověď #770 kdy: 22. 08. 2018, 20:58:12 »
stane se
Pořád to ale neodpovídá na tu otázku.
jaké je její aktuální znění?
"význam IO (), proč to může jít do >>="
Podle mě tu jsou otázky v podstatě dvě: Jakou vnitřní hodnotu vrací putStr (to je jeho výstupní typ) a co se cpe do getLine apod., když to jsou konstanty. Mě vysvětlení je, že něco jako
Kód: [Vybrat]
do
  putStr “...”
  x <- getLine
je ve skutečnosti putStr “...” >>= \_ => getLine, kde se využije toho, že ta konstanta je isomorfní s funkcí A1.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #771 kdy: 22. 08. 2018, 21:12:07 »
Ok, beru osobní věci zpět. Každopádně můj příspěvek byl z výrazně větší části k tématu, možná bys tedy mohl zareagovat spíš na ty věcné kusy.
Byl. Už jsem si myslel, že to tady nikoho nezajímá ;-)

Dependent typy z principu nemohou dokázat korektnost např. převodu stringu na číslo. Jak by se v typu fce convert: String -> Maybe Nat vyjádřilo, zda se očekává stringový vstup v desítkové nebo šestnáctkové soustavě? Podle mě je to principiálně nemožné, a stejně tak není možné ani vyjádřit korektnost implementace převodu. V Idris se asi dá vyjádřit, že funkce doběhne, a že nezpanikaří, ale to je málo.
Já v těch závislostních typech nejsem kovanej, takže takto si to předstvuju v pseudokódu, jak to chápe typový systém:

Kód: [Vybrat]
parseFromDec :: Str -> Int = ('0' -> 0) | ('1' -> 1) | ... | ('9' -> 9)
případně

Kód: [Vybrat]
parseFromDecM :: Str -> Maybe Int = ('0' -> Just 0) | ('1' -> Just 1) | ... | ('9' -> Just 9) | _ -> Nothing

Plus nějaká recurze.

Píšu, že tak to chápe ten typovej systém, ne, že to tak bude psát programátor. Ten na to musí mět nějaký cukřík - ale tady se zase dostávám do oblasti praktičnosti, a to nepovažuji za námět mé otázky.



Unit testy slouží jako vždy up-to-date dokumentace. U jednoduchých věcí se dá samozřejmě hodně věcí vyčíst z typů (hezký příklad je tady: http://funkcionalne.cz/2014/08/types-will-carry-you-over-the-monads/), ale u složitějších je prostě hezké mít chování zdokumentované na příkladech, místo potřeby rozjímat nad důsledky komplikované typové signatury. Navíc je slušnost mít knihovny zdokumentované, tak proč to rovnou nedělat unit testy? (podívejte např. sem: https://doc.rust-lang.org/std/iter/trait.Iterator.html), všechny Examples jsou rovnou spustitelné unittesty zapsané do docstringů funkcí.
Obecně s tebou naprosto souhlasím. Však já jsem nikde nepsal, že testy jsou zlo.

Ale co by si řekl na to, když by ty ukázkové příklady generoval stroj na požádání? Vzal by sis nějakou funkci, předal jí třeba první argument (a nebo žádný), a stroj by si domyslel tři různé příklady a výsledky, a ty by ti ukázal.

Ono totiž moje zkušenost je taková, že ty ukázky jsou sice fajn, ale stejně mě vždycky zajímala hlavně ta myšlenka, jakási idea té funkce/knihovny/kódu. A na tu většinou autoři zapomínaj - tam ti testy (ale ani typy) nepomůžou.


Unit testy jednoduchým způsobem ověřují chování v krajních a nečekaných případech. Když jsem psal implementaci funkce testující, zda je bod uvnitř polygonu, rovnou napíšu test, jak se chová bod na hraně, jak se chová v polygonu, který není uzavřený, jak se chová v polygonu který protíná sám sebe. Nedovedu si představit, jak by mohlo být takové chování zřejmé z typu funkce. Možná, až BoneFlute přestane "být stále student", nějak pěkně to vyřeší, to by mě pak docela zajímalo.
Byl jsem línej, a napsal jsem si generátor unittestů. Takovej ten postup, kdy si napíšeš prototyp, a pak na něj začneš psát testy - úplně špatně podle TDD, já vím.

Ten generátor měl takové patterny: Int = [INT_MIN, -2, -1, 0, 1, 2, INT_MAX], plus jednoduchá kombinatorika.

Možná, opravdu jen možná, by se z těchto základních patternů dali komponovat/odvozovat složitější třeba pro ten polygon.

Z typu funkce to asi zřejmé nebude. Ale když by ten stroj dokázal vygenerovat ukázky na požádání?

Unit testy jsou šablony funkčního kódu, který používá knihovnu kanonickým způsobem. Kód mohu copy'n'pastnout do vlastního projektu a upravit podle potřeby. Typy tohle neumí.
Viz ten generátor.
A co se týče kanonického způsobu, je otázka jak k tomu přistupovat. Z Haskellu jsem zvyklej, že jinak, než kanonicky to napsat nejde. Prostě ti to nedovolí. (Jen jednou se mi stalo, že jsem kompilátoru zamotal hlavu takovým způsobem, že mi kód napůl blbě přeložil. A bůví, so jsem to ve skutečnosti prováděl.)

Re:Typový system versus unittesty
« Odpověď #772 kdy: 23. 08. 2018, 00:35:25 »
Ale co by si řekl na to, když by ty ukázkové příklady generoval stroj na požádání? Vzal by sis nějakou funkci, předal jí třeba první argument (a nebo žádný), a stroj by si domyslel tři různé příklady a výsledky, a ty by ti ukázal.

[…]

Byl jsem línej, a napsal jsem si generátor unittestů. Takovej ten postup, kdy si napíšeš prototyp, a pak na něj začneš psát testy - úplně špatně podle TDD, já vím.

Ten generátor měl takové patterny: Int = [INT_MIN, -2, -1, 0, 1, 2, INT_MAX], plus jednoduchá kombinatorika.
To jsou ale úplně triviální funkce, kterých je maličko a pro které se jednotkové testy píšou spíš pro pocit, že testy pokrývám opravdu maximum kódu (navíc se na nich dá snadno nahnat procento pokrytí testy), než že by někdo věřil, že  ten test opravdu odhalí nějakou chybu. Mnohem zajímavější a užitečnější testy jsou na takové funkce, u kterých není takhle na první pohled patrné, co jsou ty významné hodnoty, se kterými je vhodné funkci testovat.

ava

Re:Typový system versus unittesty
« Odpověď #773 kdy: 23. 08. 2018, 09:04:39 »
Dependent typy z principu nemohou dokázat korektnost např. převodu stringu na číslo. Jak by se v typu fce convert: String -> Maybe Nat vyjádřilo, zda se očekává stringový vstup v desítkové nebo šestnáctkové soustavě? Podle mě je to principiálně nemožné, a stejně tak není možné ani vyjádřit korektnost implementace převodu. V Idris se asi dá vyjádřit, že funkce doběhne, a že nezpanikaří, ale to je málo.
Já v těch závislostních typech nejsem kovanej, takže takto si to předstvuju v pseudokódu, jak to chápe typový systém:

Kód: [Vybrat]
parseFromDec :: Str -> Int = ('0' -> 0) | ('1' -> 1) | ... | ('9' -> 9)
případně

Kód: [Vybrat]
parseFromDecM :: Str -> Maybe Int = ('0' -> Just 0) | ('1' -> Just 1) | ... | ('9' -> Just 9) | _ -> Nothing
Plus nějaká recurze.

Zkusím tady nadhodit myšlenkový experiment, který snad ukáže, co se mi celé na té myšlence náhrady testů typy nelíbí.

Testy by vypadaly asi takhle (pseudokód):

assert(parseFromDecM "0" == Just 0)
assert(parseFromDecM "42" == Just 42)
assert(parseFromDecM "foo" == Nothing)
assert(parseFromDecM "" == Nothing) // Empty string is not a zero, but parse error
assert(parseFromDecM " 42" == Nothing) // Whitespace results in parse error
∀x: Int( assert(parseFromDecM . toString x == Just x ) // quickcheck test

Když píšu TDD, tedy nejprve testy, rovnou si rozmyslím, co má implementace umět. Dovedu si třeba dost představit, že naivní implementace by pro prázdný string vrátila 0. Neříkám že je to nutně špatně, ale možná že jo, a určitě je dobré mít takové chování zdokumentované. Když píšu testy first, ještě před implementací si chování rozmyslím. Navíc jsem vybral takové příklady, které dobře vystihují "ideu" chování, tady si myslím přesný opak toho co ty, testy jsou pro vystižení myšlenky funkce dost užitečné, naopak nějaké generátory unit testů tam tu "intuici za smyslem funkce" nemají moc šanci postihnout.

A teď dejme tomu, že bych chtěl implementovat tu samou funkci v nějakém vysněném jazyce s typovým systémem který mi umožní úplně všechno co chci.

Když jí dám typ String -> Maybe Int, je možné udělat nekorektní implementaci, to je z typu evidentní. Není například jasné, jestli je převod každé jedné číslice správně implementován (je to převod z binární soustavy? šestnáctové? desítkové?).

Tak do typu přidáme omezení na převodní funkci: String -> (Char -> Maybe Int) -> Maybe Int.

Pořád můžeme mít nekorektní implementaci. Co když by funkce brala znaky ze stringu v opačném pořadí? V rekurzi a násobení základem 10 se člověk snadno sekne... Tak přidáme nějaké hypotetické omezení TraversalOrder. Typová signatura nám naroste na String -> (Char -> Maybe Int) -> TraversalOrder -> Maybe Int. Ale chybí nám tu vlastně ten základ 10, kterým se to má násobit, a ten je navíc svázaný s funkcí ze znaku do čísla. No tak uděláme nějaké String -> ({convertDigit: Char -> Maybe Intů base: Int}) -> TraversalOrder -> Maybe Int. A taky potřebujeme nějak zahrnout speciální případ, že prázdný string není Just 0 ale Nothing. Naštěstí můj typový systém umí trochu číst myšlenky: OnEmptyInputNothing: String -> ({convertDigit: Char -> Maybe Int, base: Int}) -> TraversalOrder -> Maybe Int. Taky bych asi měl dodat, že všechny znaky se skutečně použijí, atp.... Každopádně pokud bych chtěl pomocí typového systému opravdu dokázat 100% korektnost implementace, v zásadě musím v tom typovém systému tu implementaci nakonec naimplementovat znovu, což jaksi nedává smysl, a jak už tu někdo psal, stejně bych pak asi pro jistotu ještě musel napsat testy na ty typy...


Možná, opravdu jen možná, by se z těchto základních patternů dali komponovat/odvozovat složitější třeba pro ten polygon.

Z typu funkce to asi zřejmé nebude. Ale když by ten stroj dokázal vygenerovat ukázky na požádání?


Myslím, že alespoň v tom, co dělám já, by ty ukázky často byly k ničemu. Třeba u toho polygonu by ze stroje vypadla řada čísel - souřadnic bodů polygonu, ale dokud si to nenakreslíš, tak nevidíš co to vlastně testuje. A to už je jednodušší si ty zajímavé příklady nejprve nakreslit a potom je, u komplikovaných případů třeba i okomentované a s naskenovaným obrázkem, zadat do unit testů.

Re:Typový system versus unittesty
« Odpověď #774 kdy: 23. 08. 2018, 09:27:52 »
Když píšu TDD, tedy nejprve testy, rovnou si rozmyslím, co má implementace umět.
Celý váš komentář bych podepsal, ale tohle ještě zvlášť vypíchnu. TDD znamená, že se na tu funkci nejprve dívám z pohledu jejího uživatele. Takže se mi daleko spíš podaří API navrhnout tak, aby se dobře používalo, ne hlavně aby se mi dobře psala implementace. A když se API dobře používá, je zase menší pravděpodobnost, že ho někdo použije špatně.

JS

Re:Typový system versus unittesty
« Odpověď #775 kdy: 23. 08. 2018, 11:25:40 »
Dependent typy z principu nemohou dokázat korektnost např. převodu stringu na číslo. Jak by se v typu fce convert: String -> Maybe Nat vyjádřilo, zda se očekává stringový vstup v desítkové nebo šestnáctkové soustavě? Podle mě je to principiálně nemožné, a stejně tak není možné ani vyjádřit korektnost implementace převodu. V Idris se asi dá vyjádřit, že funkce doběhne, a že nezpanikaří, ale to je málo.

Myslim, ze se pletes. Dostatecne silnym typem se da vyjadrit, ze ta konverzni funkce vrati Nothing pokud vstup nebude cislo v desitkove soustave. Potiz je v tom, ze pak tim vlastne cim dal vic implementujes znovu celou funkci...

Z meho pohledu je to tak, ze jak (dostatecne pokryvajici) testy, tak (dostatecne silne) typy jsou urcitou aproximaci toho, co ma program delat (a nekdy i za jakou cenu). V limitnim pripade obe tyto aproximace znamenaji napsat cely program znovu.

Napriklad vezmi si scitani dvou cisel. Typova aproximace typicky je "funkce vraci zase cislo". Ale muzeme to vzit dal a reprezentovat typem stale silnejsi invariant (treba vyznacny bit vysledku souvisi s vyznacnymi bity argumentu), az budeme typem reprezentovat, ze vysledkem operace je cislo.

Podobne, testova aproximace je typicky "funkce funguje na techto 100 prikladech cisel". Muzeme test rozsirovat a testovat stale vetsi mnozstvi pripadu, az dojdeme k situaci, kdy budeme mit (treba pro soucet 16-bit integeru) 2^32 testovacich pripadu a pokryji vsechny moznosti. (Pripadne muzeme delat neco jako QuickCheck a rozsirovat test o invarianty jako v pripade typu, az dojdeme k invariantu ktery popisuje presne, co testovana  funkce dela.)

Takze podle me, neni (teoreticka) cesta ven - pokud chces neco dokonale otestovat nebo dokonale typove popsat, znamena to napsat znovu nezavisle celou implementaci.

Ale v praxi samozrejme obe aproximace jsou uzitecne a obe ma smysl pouzivat a znat jejich silne a slabe stranky. Otazka z titulku je asi podobne podivna jako ptat se, je lepsi pouzivat Taylorovu nebo Fourierovu radu?

ava

Re:Typový system versus unittesty
« Odpověď #776 kdy: 23. 08. 2018, 11:41:10 »
Jj, něco takového si v zásadě myslím taky, na konkrétnějších případech jsem to ukazoval ve svém předchozím příspěvku, pěkně jsi to shrnul z trochu jiné stránky. Skoro se mi nechce věřit, že by se na root fóru dospělo k nějakému konsenzu :)

v

Re:Typový system versus unittesty
« Odpověď #777 kdy: 23. 08. 2018, 11:50:04 »
konsenzu
a ten je? a co na to zastánci dynamických jazyků?

JS

Re:Typový system versus unittesty
« Odpověď #778 kdy: 23. 08. 2018, 13:06:35 »
konsenzu
a ten je? a co na to zastánci dynamických jazyků?

Zastanci dynamickych jazyku maji misto staticke typove kontroly kontrolu za behu, a misto "zavislostnich typu" maji asserty. Testy maji oba tabory. Takze pro ne plati to, co jsem napsal, takrka stejne.

(Jinak dynamickou typovou kontrolu a asserty lze samozrejme pouzit i ve staticky typovanych jazycich, a ma to sve vyhody.)

ava

Re:Typový system versus unittesty
« Odpověď #779 kdy: 23. 08. 2018, 13:24:19 »
konsenzu
a ten je? a co na to zastánci dynamických jazyků?

Za mě je ten konsenzus JS-eho veta "obe aproximace jsou uzitecne a obe ma smysl pouzivat a znat jejich silne a slabe stranky.". I když "konsenzus za mě" je samozřejmě protimluv, spíš jsem to s tím konseznem plácnul..

Zastánci dynamických jazyků (tedy spíš jazyků bez statického typového systému) ... se musí obejít bez statického typového systému :) Typicky za to získávají větší flexibilitu, větší možnosti introspekce a modifikace programu za běhu, z komerčně používaných jazyků to podle mě nejdál dotáhl Smalltalk, kde je třeba možné za běhu debuggovat a upravovat debugger a nikomu na tom nepřijde nic zvláštního. Ale to už je zase jiné téma.