Typový system versus unittesty

[Filip Jirsák]

Přijde mi zajímavější, aby ukázkové příklady generoval nástroj na základě specifikace.

Což ovšem význam ukázkových příkladů staví na hlavu. Ukázkové příklady mají ten význam, že je velmi jednoduché je vytvořit a pochopit, řádově jednodušší, než vytvořit správnou specifikaci. Proto je u nich také mnohem větší pravděpodobnost, že budou správně. Když se budou tvořit z té složité specifikace, budou pro její kontrolu k ničemu. Kdybyste chtěl vygenerovat ze specifikace hezké ukázkové příklady, které zkontroluje někdo neznalý programování, bude to ještě podstatně složitější (jak automaticky poznáte ty „hezké“ příklady?), a i pokud by se vám to podařilo, bude existovat velké nebezpečí, že programátor sestaví specifikaci tak, aby mu vycházely ty hezké příklady, a zbytek bude špatně. To je přece známý problém testů (a velké problémy s tím má třeba školství nebo věda), že když něco testujete stále stejnými testy, má to tendency degenerovat a uzpůsobit se tak, aby to perfektně procházelo těmi testy – a nic jiného rozumného to nedělá.

[Reklama]

[JSH]

Přijde mi zajímavější, aby ukázkové příklady generoval nástroj na základě specifikace. Včetně okamžiku vývoje.

Filip Jirsák to v

Což ovšem význam...

celkem vystihl.

Pokud bych psal např. daňový soft, tak mi dává smysl sednout si s účetní a spočítat si pár ukázkových lidí. Zároveň si tak utřídím vlastní představu o problému. Pak ty ukázky překlopím na testy. Jestli nebudou testy sedět, tak budu kontrolovat i kód a když nic nenajdu tak pak případně ručně přepočítáme pro kontrolu i ty ukázky.

Přijde mi to spolehlivější než kdybychom ručně kontrolovali něco nagenerovaného. Hledání chyb v cizích výsledcích mi nikdy moc nešlo. A taky to svádí k tomu, jenom to prolítnout. Pokud to nebude moc velký úlet, tak ta chyba může projít.

[gll]

Dobře, máš pravdu. Ale vzhledem k námětu tohoto vlákna nás zajímá právě ten sci-fi překladač.
Takže, dá se to napsat jinak? Typem?

jestli tomu rozumím správně, vy překladači zadáte dva vzorce a on ověří, že jsou ekvivalentní. Jak to souvisí s typem?

[gll]

v unittestu ty vzorce mohu otestoval nějak tak

Kód: [Vybrat]

from sympy import solve, symbols, var, sqrt, simplify

a, b, c = symbols('a b c')
x = var('x')

def roots():
    return [simplify((-b + sqrt(-4*a*c + b**2))/(2*a)),
            simplify(-(b + sqrt(-4*a*c + b**2))/(2*a))]

def test():
    assert roots() == solve(a*x**2 + b*x + c, x)

chci vidět, jak to stejné otestuješ typovým systémem

[andy]

No uměl bych si představit něco takového (hypoteticky):

Kód: [Vybrat]

getRoots :: a : Num -> b : Num -> c : Num -> [x] : [Num] | a * (x * x) + b * x + c = 0

Tak pro inty by to fungovat hypoteticky mohlo. Ale pro floaty si nedokážu představit ani to, jak bych takovýhle předpis ověřoval sám. Minimálně bych tam musel přidat hromadu dalších předpokladů o vstupech a o požadované toleranci.

Právě že by to fungovalo symbolicky pro reálná čísla. Zda by to pak při konkrétní implementaci třeba pro "Num=Double" bylo numericky stabilní je druhá věc.

Dokonalý typový systém (bez rozdílu na jeho druh), tj. takový, který přesně rozpozná chybu, by tedy musel mít kategorie mnohem užší (třeba až do kategorie pro každou hodnotu; včetně jejich vztahů), tedy by NĚJAKÝM způsobem musel duplikovat/nahrazovat testovaný výpočet, jinak by nebyl schopen posoudit správnost.

Třeba ta kvadratická rovnice je zrovna ukázka, že tomu tak vůbec být nemusí.

Na druhou stranu ta ukázka:

Kód: [Vybrat]

Op op a b -> op a b

Tak tady je specifikace a konkrétní řešení identické.

Dneska je tendence když mám zadání alespoň trochu formálně popsané zadání to řešit tak, že si napíšu DSL, a v tom DSL pak popíšu tu specifikaci. A samozřejmě tam většina věcí bude vypadat jako to "op a b" - to prostě "je" ta specifikace. A tam se pak dostáváme k otázce, jak otestovat, že ta specifikace je správně - a tam nějaké testy (nevím, jestli zrovna "unit" testy) jsou asi jediné možné řešení.

[Reklama]

[v]

něco ostřejšího https://ncatlab.org/nlab/show/completion+monad ?

[ffd]

v unittestu ty vzorce mohu otestoval nějak tak

Kód: [Vybrat]

from sympy import solve, symbols, var, sqrt, simplify

a, b, c = symbols('a b c')
x = var('x')

def roots():
    return [simplify((-b + sqrt(-4*a*c + b**2))/(2*a)),
            simplify(-(b + sqrt(-4*a*c + b**2))/(2*a))]

def test():
    assert roots() == solve(a*x**2 + b*x + c, x)

chci vidět, jak to stejné otestuješ typovým systémem

Ja jsem prave myslel, ze unit test pro kvadratickou rovnici bude obsahovat
asserty pro a,b,c <0, = 0, >0, cili nejakych 8 assertu, ktere si vytvorim manualne...

[Kit]

Spíš se ptáme, jak ten kompilátor požádám, aby ověřil, že funkce řeší kvadratickou rovnici. Typem nebo testem? Jak bude vypadat zápis?

Ne, neptáme. Ptáme se kompilátoru typem. Tak zní zadání.

Ukázka by nebyla? Chci se tedy zeptat kompilátoru typem, zda daná funkce řeší kvadratickou rovnici. Jak to bude vypadat?

[Typolog]

Kvadratická rovnice je definovaná jako ax^2 + bx +c = 0. Takže když se člověk zeptá "kompilátore, řeší tenhle vzoreček ax^2+bx+c=0, tak se ptá, jestli řeší kvadratickou rovnici jazykem, kterému kompilátor rozumí. Když tam dá jiný (neekvivalentní) vzoreček, tak se na to neptá.

Pořád jde jen o to, že kompilátor dokáže vyřešit jenom to, co má formálně a bezrosporně zadané. Jenže takováhle zadání programátoři obvykle nemají, ostatně je to jejich práce převádět neformální a neúplné zadání popsané přirozeným jazykem do formální a přesné řeči počítačů. V tomhle převodu se dělají chyby a je snaha těm chybám předcházet, mimo jiné i testováním.

No, takže fakt říkáte, že když kompilátor nepožádám, aby ověřil, že funkce řeší kvadratickou rovnici, tak to kompilátor neověří. Bingo.

Spíš se ptáme, jak ten kompilátor požádám, aby ověřil, že funkce řeší kvadratickou rovnici. Typem nebo testem? Jak bude vypadat zápis?

Takový příklad je uveden v článku “If monads are the answer, what’s the question?” (který je jinak o něčem úplně jiném). Tamní typový systém umí líně vyhodnocovat a má něco jako “statické jednotkové testy” - to je tak trochu protimluv, překladač v podstatě umožňuje specifikovat podmínky integrity, které se symbolicky ověřují během překladu. Vychází to z nějaké disertace, jejíž název si už nevybavuji (je stará, 80.-90. léta, což naznačuje, že jsme se za pár desetiletí moc daleko neposunuli).

[listoper]

Nedavno jsem zmenil projekt a po trech mesicich na tom novem mi doslo k cemu vlastne jsou unit testy a vzpomel sem si na tohle vlakno. Rikal jsem si, ze ho doplnim.
Tak pro me je hlavni duvod proc pisu unit testy:
"Ochrana meho kodu pred neuvazenymi zmenami ostatnich"

Kdekdo mi hrabe do "mych" funkci a ohyba si je pro svuj use case a je mu jedno, ze tim rozbije ten muj.
Kdyz nenapisu testy tak mi pristanou defekty a ja budu slozite hledat kde,kdo a co rozbil.

Kdyz testy mam tak "ohybac" musi zmenit i ty testy aby prosel build a tim padem se snad lepe zamysli.
A kdyz se nezamysli (jako treba ze cele vnitrky testu zakomentuje) tak mam aspon dukazy jakej to je lempl...

Myslim, ze tohle typovy system nedokaze podchytit.

[Bacsa]

Nedavno jsem zmenil projekt a po trech mesicich na tom novem mi doslo k cemu vlastne jsou unit testy a vzpomel sem si na tohle vlakno. Rikal jsem si, ze ho doplnim.
Tak pro me je hlavni duvod proc pisu unit testy:
"Ochrana meho kodu pred neuvazenymi zmenami ostatnich"

Kdekdo mi hrabe do "mych" funkci a ohyba si je pro svuj use case a je mu jedno, ze tim rozbije ten muj.
Kdyz nenapisu testy tak mi pristanou defekty a ja budu slozite hledat kde,kdo a co rozbil.

Kdyz testy mam tak "ohybac" musi zmenit i ty testy aby prosel build a tim padem se snad lepe zamysli.
A kdyz se nezamysli (jako treba ze cele vnitrky testu zakomentuje) tak mam aspon dukazy jakej to je lempl...

Myslim, ze tohle typovy system nedokaze podchytit.

Toto je velice zajímavý postřeh. +1

[BoneFlute]

...

Myslim, ze tohle typovy system nedokaze podchytit.

Je to myslím moc pěkný usecase, ač už jsem na něco podobného tuším reagoval.

Zdá se, že mnoho přispěvovatelů si tu vyláme zuby na rozdílu mezi "tohle typový systém nedokáže podchytit protože princip" versus "nesetkal jsem se s typovým systémem, který by to dokázal podchytit".

Například jazyk Elm by toto mohl dát. Jakmile někdo vezme funkci, a ohne si ji, tak se změní major verze té funkce a už nepůjde napasovat, a celé to nepůjde zkompilovat. Což je IMHO právě ta ochrana (ochrana rozhodně užitečná), o které mluvíš.

[BoneFlute]

Dobře, máš pravdu. Ale vzhledem k námětu tohoto vlákna nás zajímá právě ten sci-fi překladač.
Takže, dá se to napsat jinak? Typem?

jestli tomu rozumím správně, vy překladači zadáte dva vzorce a on ověří, že jsou ekvivalentní.

Ano. Taky.

Jak to souvisí s typem?

Proč se ptáš?

[Filip Jirsák]

Například jazyk Elm by toto mohl dát. Jakmile někdo vezme funkci, a ohne si ji, tak se změní major verze té funkce a už nepůjde napasovat, a celé to nepůjde zkompilovat. Což je IMHO právě ta ochrana (ochrana rozhodně užitečná), o které mluvíš.

Při popisu toho, proč se používají testy, jste popsal jenom jednu možnou změnu. Druhá možná změna je, že někdo vezme funkci, zachová její API na kterém závisí ostatní a které testují testy, ale upraví její implementaci (např. funkci optimalizuje). Užitečnost ochrany testy spočívá i v tom, že testy dále úspěšně procházejí, přestože se implementace změnila. Testy nejsou určené k tomu, aby nacházely změny, ale aby nacházely takové změny, které něco rozbijí.

[listoper]

Například jazyk Elm by toto mohl dát. Jakmile někdo vezme funkci, a ohne si ji, tak se změní major verze té funkce a už nepůjde napasovat, a celé to nepůjde zkompilovat. Což je IMHO právě ta ochrana (ochrana rozhodně užitečná), o které mluvíš.

Při popisu toho, proč se používají testy, jste popsal jenom jednu možnou změnu. Druhá možná změna je, že někdo vezme funkci, zachová její API na kterém závisí ostatní a které testují testy, ale upraví její implementaci (např. funkci optimalizuje). Užitečnost ochrany testy spočívá i v tom, že testy dále úspěšně procházejí, přestože se implementace změnila. Testy nejsou určené k tomu, aby nacházely změny, ale aby nacházely takové změny, které něco rozbijí.

Ale ne. On ma BoneFlute zase pravdu. Uz mi to doslo.
Kdyz bude funkce ochranena typem tam nepujde ohnout aniz by se zmenil ten typ a tudiz kompilator stejne zarve protoze tam kde ji volam ja bude typ nekompatibilni.