Příspěvky

1351

Vývoj / Re:Typový system versus unittesty

« kdy: 19. 06. 2018, 14:25:00 »

Mimochodem v TDD je pravidlem, že se píší vybrakované metody, které se teprve na stížnost hotových testů vyplňují, případně (a teď pozor, soudruzi javaři nečtěte dále, aby vám z toho nehráblo) se tyto metody teprve vytvářejí! :O :O :O (No nekecej!)

Tohle není odpověď pro JSH, ale autora dotazu Boneflute.

Obnošená vesta.

Proč @v dokázal pochopit, že se táži na limity toho typového systému vůči unittestům, zatímco jiní se mě pokouší přesvědčit že jsem idiot a ani nejsou schopni uvést zajímavé argumenty?

1352

Vývoj / Re:Typový system versus unittesty

« kdy: 19. 06. 2018, 14:19:07 »

nejdřív bych zdůraznil svůj postoj: neargumentuju proti testům, testy jsou dobrá věc
původní dotaz se zabývá tím (moje interpretace), jestli se testy dají teoreticky nahradit typovým systémem a já si vzhledem k tomu co jsem o tématu četl, myslím, že ano, dále mě zajímají praktické limity tohoto přístupu, protože z vlastní praxe ho považuju za extrémně užitečný

Chápeš to zcela přesně jak jsem to myslel.

1353

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 21:17:47 »

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ě.

1354

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 21:13:11 »

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.

1355

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 19:23:17 »

Odmocni jde skoro z hlavy.

Mam cislo (50), vydelim dvema (25), sectu s 2 a udelam prumer(13,5).
Pokracuju 50:13=asi 3, zas sectu 13+3 a udelam prumer(.
Pokracuju 50:8=asi 6, zas prumer 6+8 a tak dal.

Sice to nebylo pointou mého příspěvku - ale hezký :-)

1356

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 19:00:28 »

Jak typy zajistis, ze tvoje metoda sum(a,b) vraci pro int a a int b spravny int soucet? Jako alternativu k primitivnimu assertEquals(3, sum(1,2)) ?

Teorie typů praví, že sum a b je pohled na množinu všech možných kombinací <a, b>. Takže stejně tak, jako víme, že po 1čce přijde dvojka (pomocí těch axiomů), tak víme že (sum 1 2) == 3. Je třeba to nějak definovat, nemusí to být triviální, ale co už.

Pamatuji si učitele, který nám pro zajímavost ukazoval, jak se vypočítá odmocnina. Byl to vzorec na několik řádek (jak moc to byla hloupost netuším, od té doby jsem se k tomu nikdy nevrátil). A v reálu se proto stejně používají tabulky. (Jak to počítají procesory, zda na to mají vzorec, nebo používají taky tabulku, to netuším.)

1357

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 18:53:22 »

computational trinitiarism

Můžeš prosím rozvést vo co de?

moc ne
https://existentialtype.wordpress.com/2011/03/27/the-holy-trinity/
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
https://ncatlab.org/nlab/show/computational+trinitarianism

Díky moc!

dívám se na to tak, že chování programu se (s dostatečně schopným typovým systémem) zcela odráží v typu programu (který by byl a->b)

Ano, taková je moje idea :-)

1358

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 18:41:56 »

computational trinitiarism

Můžeš prosím rozvést vo co de?

Jinak díky, píšu si do seznamu k nastudování :-)

1359

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 18:27:11 »

akorát bez pokročilé matematiky typu součet dvou čísel.

To mě připomíná, ono třeba v žádném mě známém typovaném jazyku není typ Int implemenován jako ...|1|2|3|4|5|6|7|8|9|10|... ale je na to nějaká zkratka na buildin typ, a stejně tomu ten kompilátor rozumí. Takže si představuji, že stejně tak se dá udělat i ta pokročilá matematika. Netřeba se utápět v detailech.

1360

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 18:21:16 »

Máte v tom pěkný hokej.

Zkuste si představit, že ta funkce v liché týdny přičítá a v sudé týdny odčítá. Budete definovat typ  y-tý_následník_x_v_liché_ týdny_union_y-tý_předchůdce_v_sudé_týdny? Celou bankovní aplikaci pak navrhnete jako funkci main vracející ten správný datový typ™ a kompilátor už to nějak vyřeší?

Ano, přesně tak. Žádný problém pane hokejisto.

1361

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 18:19:59 »

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).

Úžasné. Takže abych se vyhnul unittestům, tak si musím tu funkčnost naimplementovat ještě jednou, akorát bez pokročilé matematiky typu součet dvou čísel.

Tak za prvé, pomocí unittestů to taky implementuju ještě jednou.
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.

1362

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 17:15:41 »

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ů.

1363

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 17:09:46 »

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).

1364

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 17:05:40 »

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.

1365

Vývoj / Re:Typový system versus unittesty

« kdy: 18. 06. 2018, 16:29:09 »

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.