Typový system versus unittesty

BoneFlute

  • *****
  • 1 842
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #75 kdy: 18. 06. 2018, 15:00:15 »
Psal jsem, že v tom nejsem expert...ale ta idea je něco ve stylu
Kód: [Vybrat]
(ty typy musí být nějak jinak, ale nedám to dohromady)
add :: (HNat a, HNat b, HAdd a b c) => a -> b -> c
add ... následuje přičítání jedničky, pokud první argument není 0...
Je to dost zbytečné cvičení, a tak trošku to přesměrovává problém od "spletl jsem se v pojmenování" na "spletl jsem se v typu". Ale svým způsobem to je třeba odpověď na autorovu otázku - ano, typový systém odhalí chyby v kódu, ale jak odhalí chyby v typech?
Ano, křížová kontrola. Přiznávám unittestům bod :-)
Stejně jako se můžeš splést v typu, můžeš se splést v testu. Jenže jako v testu kontroluješ, zda to testuje co má pohledem, stejně tak můžeš u typu. Jako v testu kontroluješ změnu oproti předchozímu, stejně tak to umí elm u typů.

Takže zůstává jen ta křížová kontrola, kdy u testů to píšu dvakrát. Jenže, stejně tak může kompilátor generovat usecase, a ty ukazovat... No ale to už jsme zase trochu jinde.

Citace
Ale u typoveho systemu nutis nepritele, aby prinesl program s dalsimi (strojove overitelnymi) castmi...
Teď nerozumím - typový systém třeba Javy umí rozhodnout Null/NonNull (někdy...) bez ohledu na to, že to vlastně v tom typovém systému "není". Ty typeclassy FromJSON/ToJSON jsou udělány tak, že kompiler kompatibilitu prostě rozhodnout nemůže. Halting problém byl v tom smyslu, že i kdyby na to kompiler šel analýzou kódu jako Java, tak tu property "fromJSON . toJson = Just" stejně nemůže (obecně) rozhodnout.

Předpokládám, že kompiler:
Mám json element číslo, převést na string a zpět. Element string, detto. Element Struct obsahující číslo, na string a zpět. Dále je to rekursivní, takže to už nemusím.

Asi by se našlo něco, kde by to začalo být hodně divoké. Jenže pak je otázka, zda v takovém případě by si nevylámal zuby i unittest. Nevím.


Re:Typový system versus unittesty
« Odpověď #76 kdy: 18. 06. 2018, 15:04:49 »
elm-package odhalí
Cože? elm-package odhalí, že jste se překlepl v operátoru? Řekl bych, že nastal čas pro to, abyste také vy ukázal svůj kód.

Je to dost zbytečné cvičení, a tak trošku to přesměrovává problém od "spletl jsem se v pojmenování" na "spletl jsem se v typu". Ale svým způsobem to je třeba odpověď na autorovu otázku - ano, typový systém odhalí chyby v kódu, ale jak odhalí chyby v typech?
Ono by to vůbec bylo schování všech možných algoritmů do typů. Typy jsou ale součástí kódu, takže tím si nijak nepomůžeme.

Re:Typový system versus unittesty
« Odpověď #77 kdy: 18. 06. 2018, 15:12:51 »
Jenže pak je otázka, zda v takovém případě by si nevylámal zuby i unittest. Nevím.
Jednotkový test testuje jenom to, co do testu napíše programátor. A spousta jednotkových testů se píše jednoduše tak, že kontrolují, zda pro zadané vstupní hodnoty dává jednotka očekávaný výstup. Není to nic světoborného, ale praxe ukazuje, že i hloupé třídění není snadné napsat na první pokus správně, takže i testy, které z miliard možných vstupů otestují těch pět správných dokážou odhalit většinu chyb, které v praxi nastávají.

Kiwi

Re:Typový system versus unittesty
« Odpověď #78 kdy: 18. 06. 2018, 15:53:17 »
Chjo, tak jinak.

Předpokládejme, že Pepa píše program a nechce v něm mít chyby. A chce využít všechny možnosti, ale co nejjednodušším způsobem. A co nejrychlej. Takže:
- Je lepší při chybě program nepřeložit a dostat rovnou hlášku "type mismatch @ line 256", než týden procházet logy
- Je lepší, pokud má funkci
Kód: [Vybrat]
speed_t avgSpeed( distance_t distance, time_t time) { ... }
a vyběhne na něj při překladu rovnou varování, že prohodil argumenty, než když na to přijde tesťák náhodou
- A chce mít podchyceno, že se opravdu implementuje správný vzorec, takže dá i unit test, který ho upoyorní, že ten výpočet je blbě.
- A protože chce vědět, jestli větší celek programu běhá správně, hodít am i integrační testy.

Takže s čím se to dělá efektivně ohlídá datový typ (bez práce a před commitem), co se dělá ohlídá unit test.

Pokud se i "s čím to dělám" musí (v základu) hlídat unit testem, tak je něco blbě (= jazyk stojí za starou bačkoru)
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.

.

Re:Typový system versus unittesty
« Odpověď #79 kdy: 18. 06. 2018, 15:53:33 »
A zatímco úzká skupinka akademiků si posilovala své ego a pocit nadřazenosti teoretizováním o abstraktních problémech, někdo reálný napsal reálný program, který pomohl vyřešit konkrétní problém.

Nic proti akademikům, ale pokud chybí alespoň elementární porce pokory, zbude jen prázdnota a nadutost.

/* Možná je hodnocení moc příkré, ale po přečtení vlákna si nemohu pomoct. */


.

Re:Typový system versus unittesty
« Odpověď #80 kdy: 18. 06. 2018, 16:01:01 »
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í.

BoneFlute

  • *****
  • 1 842
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #81 kdy: 18. 06. 2018, 16:05:12 »
A zatímco úzká skupinka akademiků si posilovala své ego a pocit nadřazenosti teoretizováním o abstraktních problémech, někdo reálný napsal reálný program, který pomohl vyřešit konkrétní problém.

Nic proti akademikům, ale pokud chybí alespoň elementární porce pokory, zbude jen prázdnota a nadutost.

/* Možná je hodnocení moc příkré, ale po přečtení vlákna si nemohu pomoct. */
Tak já mám k papírovým akademikům dost daleko. Ale to, že jsem přičichl k statickým typům, dokonce i nedobrovolně nakouklu do teorie typů (grupy axiomy a tyhlencty vymyšlenosti) mi dost otevřelo oči. A začal jsem se i u pitomejch jazyků jako je php, java, javascript, nebo python uvažovat jinak. Snad ku prospěchu věci.

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.

BoneFlute

  • *****
  • 1 842
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #82 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.

Gődel

Re:Typový system versus unittesty
« Odpověď #83 kdy: 18. 06. 2018, 16:35:28 »
A zatímco úzká skupinka akademiků si posilovala své ego a pocit nadřazenosti teoretizováním o abstraktních problémech, někdo reálný napsal reálný program
Ti akademici jsou taky reální ;) A museli tomu tvůrci "reálného programu" vymyslet a implementovat překladač nebo interpretr, aby to svoje veledílo mohl napsat a pustit ;)

Gődel

Re:Typový system versus unittesty
« Odpověď #84 kdy: 18. 06. 2018, 16:38:05 »
Tak já mám k papírovým akademikům dost daleko. Ale to, že jsem přičichl k statickým typům, dokonce i nedobrovolně nakouklu do teorie typů (grupy axiomy a tyhlencty vymyšlenosti) mi dost otevřelo oči. A začal jsem se i u pitomejch jazyků jako je php, java, javascript, nebo python uvažovat jinak.
Gratuluju. To je normální vývoj u člověka, co se chce zdokonalovat a je schopen pochopit mírně abstraktní poznatky. V IT bohužel převažují zakrnělí pologramoti...

Gődel

Re:Typový system versus unittesty
« Odpověď #85 kdy: 18. 06. 2018, 16:39:01 »
U Haskellu to byla zatím největší spokojenost. Poněkud náročné na hlavu
Co tam je tak náročného?

Re:Typový system versus unittesty
« Odpověď #86 kdy: 18. 06. 2018, 16:39:23 »
Ne. Překlep pozná už kompilátor.
Jak? Můžete to konkrétně ukázat na těch funkcích add() a sub().

Že se změnila signatura oproti minule (tedy, to co dělají testy) odhalí elm-package.
Ne, testy dělají něco jiného, svým způsobem přesný opak. Kdybyste si chtěl kód jenom vyzkoušet, nepotřebujete celou infrastrukturu kolem testů – prostě byste si to jednou zkusil, a kdyby to fungovalo, testovací kód byste smazal. Celá ta infrastruktura kolem testů a jejich pravidelné spouštění ale slouží právě k tomu, abyste odhalil chyby při změnách kódu. 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.

BoneFlute

  • *****
  • 1 842
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #87 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.

BoneFlute

  • *****
  • 1 842
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #88 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 ysucc x, tak to vždycky pozná, že je implementace správně (budeme-li o odvozování kompilátorem mluvit jako o jeho implementaci).

BoneFlute

  • *****
  • 1 842
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #89 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ů.