Typový system versus unittesty

[Filip Jirsák]

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

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, mezi typy a algoritmy není úplně pevná hranice, do určité míry mezi nimi lze přecházet, ale ta pružnost není nekonečná. Nezapomínejte na to, že nakonec to stejně někdo musí převést do strojových instrukcí procesoru. A že většinu věcí lidé snáze vyjádří algoritmem, než aby definovali složitou hierarchii typů.

[Reklama]

[Filip Jirsák]

Ale těch hranic se nedokážu dopátrat :-)

Tak si zkuste nadefinovat typ pro datum používané v Evropě a Severní Americe v období uplynulých pěti set let. Ne nějakou abstrakci, ale typ, který bude odpovídat tomu, co se v různých dobách a na různých územích skutečně používalo.

[JSH]

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.
Implementoval už jsi někdy nějakou netriviální logiku? Fakt bych chtěl vidět podobný typ pro funkci co počítá třeba daň z úroku.

Sice jsem bývalý akademik se závislostí na silném typování, ale co je moc, to je moc.

[BoneFlute]

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.

[BoneFlute]

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.

[Reklama]

[BoneFlute]

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.

[v]

tak já bych si tipnul, že to jde (computational trinitiarism) a že bych u toho fakt nechtěl být (ale paper bych si přečet)
k tomu s algoritmama - když si představíte, že by ty funkce byly asi čisté, tj. rekurzivní (tj. bez cyklů), tak s o tom hned uvažuje jinak

[BoneFlute]

computational trinitiarism

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

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

[v]

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í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)
disclaimer: tady jsem už dost daleko od věcí o kterých bych si troufnul říct, že jim rozumím

[BoneFlute]

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

[BoneFlute]

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

[uuuuuuuu]

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.

[BoneFlute]

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ý :-)

[Kiwi]

Jestli to má být v C a jestli to jsou všechno ve skutečnosti jen doubly, tak na něj nevyběhne nic, protože všechny tři typy jsou kompatibilní. Pokud by kompilátor hlásil varování v každé takové situaci, tak by v programech rozsahem i jen málo nad rámec učebnicových příkladů vyhazoval tolik varování, že by se v nich ta relevantní ztratila, protože většina by byla planými poplachy. Další možností by bylo všude přetypovávat, což by zase vedlo k nepřehlednosti programu.

C nepatří mezi silně typové jazyky a pokud si na to člověk zvykne, má pocit, že to přece nemůže být jinak. Ale velké množství chyb a zkušenosti z takovýchto jazyků ukazují, že při správném návrhu to s tím přetypováváním není tak žhavé a vývoj to naopak značně zrychlí.

To si právě spousta lidí myslí, ale v praxi to tak optimistické zdaleka není. Na akademických příkládcích se dá každá vlastnost předvést jako naprosto elegantní, ale v praxi na reálném projektu to pak vypadá poněkud odlišně. (např. Pascal je typově silnější než C a byl to jeden z důvodů, proč lidi tolik iritoval a pro praktickou práci se sahalo raději po C, přestože na školách snad každý ve své době absolvoval pascalskou průpravu)

Třeba u mě se opakuje scénář: píšu v Javě, načichnu tím stylem. Po nějaké době mě to začne rozčilovat. Pak zkouším nějaký projekt a tak si řeknu, že to tentokrát zkusím v Pythonu. Nejdřív nadšení, jak jde všechno snadno a krásně, a pak když navzdory incrementálnímu vývoji už třetí den nedělám nic jiného než že spouštím aplikaci a opravuju chyby mě to začne štvát z druhé strany. Tak se vrátím zpět k Javě. Tam mě začne štvát, že žádné typy neumí, tak zkusím Scalu, Haskell...

U Haskellu to byla zatím největší spokojenost. Poněkud náročné na hlavu, ale jinak se dá. Nejvíc mě zatím vadilo, když mi totálně vyhnil cabal. Tak ale za to jazyk nemůže.

A o jak rozsáhlé věci asi tak šlo?

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

To mi teda smysl nedává.

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

Je docela možné, že algoritmus výpočtu odmocniny by šlo nějak vměstnat do vzorce, ale ten procedurální přístup (1. rozděl číslo na skupinky po dvou, 2. najdi největší číslo, které po umocnění na druhou bude menší nebo rovno než skupinka vlevo, 3...) je poměrně názorný. Ale ta pointa mi stejně uniká.

[uuuuuuuu]

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

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