Typový system versus unittesty

[BoneFlute]

Mně připadá, že je triviálně vidět, že ta funkce add() je špatně pojmenovaná (a případně má špatnou dokumentaci), což nevyřeší žádný typový systém. Ale budu rád, když mne vyvedete z omylu.

Ukaž mi unittest s témže.

Bavíme se (doufám) o tvrzení, že typy plně nahradí unittesty. Nic víc neřeším.

Kód: [Vybrat]

def add(x: int, y: int) -> int:
    """
    >>> add(1, 1)
    2
    """
    return x - y


Stejně tak může být:

Kód: [Vybrat]

def add(x: int, y: int) -> int:
    """
    >>> add(1, 1)
    3
    """
    return x + y

Každopádně toto by měli řešit závislostní typy. Já jsem si to přeložil jako:

Kód: [Vybrat]

add x y == y * succ x

[Reklama]

[Ondra Satai Nekola]

Kód: [Vybrat]

(toJSON json) -> str == (fromJSON str) -> json by nešlo? Kompiler by musel ověřit, zda všechny varianty stromu, když se vygenerují do stringu a pak následně naparsují jsou shodné.

No, obvávám se, že to je ale obecně vzato nerozhodnutelný problém... (i.e. halting problem). tímpádem to řešit typy  nejde. Těch "všech variant stromu" může být nekonečno, takže to nejde ani po jednom projít.

S timhle opatrne...
Halting problem je, kdyz ti nekdo (nepritel...) prinese program a ty mas rozhodovat o nem. Ty jsi v situaci, kdy sam pises program a typovy system ti na nej klade nejake omezeni. Takze ten zkoumany program neni libovolny, ale vznikly nejakym zpusobem (trebas tak, ze spolu s nim vznika "dukaz" jeho korektnosti).

[BoneFlute]

Chces inspiraci nebo jednoduchou a celkem rozumnou odpoved?

Tak ideálně to druhé. Ale spokojím se i s tím prvním.

[BoneFlute]

Jirsák by musel udělat tu stejnou chybu na dvou místech nezávisle, aby ji neodhalil. Tobě stačí překlep na jednom místě ve znaménku.

Křížová kontrola, tomu rozumím. Mám výhrady, ale beru :-) Takže to máme dva.

[andy]

Kód: [Vybrat]

(toJSON json) -> str == (fromJSON str) -> json by nešlo? Kompiler by musel ověřit, zda všechny varianty stromu, když se vygenerují do stringu a pak následně naparsují jsou shodné.

No, obvávám se, že to je ale obecně vzato nerozhodnutelný problém... (i.e. halting problem). tímpádem to řešit typy  nejde. Těch "všech variant stromu" může být nekonečno, takže to nejde ani po jednom projít.

S timhle opatrne...
Halting problem je, kdyz ti nekdo (nepritel...) prinese program a ty mas rozhodovat o nem. Ty jsi v situaci, kdy sam pises program a typovy system ti na nej klade nejake omezeni. Takze ten zkoumany program neni libovolny, ale vznikly nejakym zpusobem (trebas tak, ze spolu s nim vznika "dukaz" jeho korektnosti).

Já to tak myslel - ty typeclassy jsou interface, nepřítel přinese program a kompilere rozhodni, zda to platí. No a protože možných vstupů je nekonečno, tak to nejde projít, tak by připadalo v úvahu nějaké rozhodnutí na jiné úrovni - ale to je halting problém. Takže s takto definovanými typy (FromJSON, ToJSON) nejde typově ošetřit, že ty instance jsou navzájem kompatibilní. (s jinak definovanými instancemi by to samozřejmě jít mohlo)

[Reklama]

[gll]

Stejně tak může být:

Kód: [Vybrat]

def add(x: int, y: int) -> int:
    """
    >>> add(1, 1)
    3
    """
    return x + y

Každopádně toto by měli řešit závislostní typy. Já jsem si to přeložil jako:

Kód: [Vybrat]

add x y == y * succ x

když udělám chybu v testu, tak test neprojde a chybu odhalím. Je nepravděpodobné, že bude stejná chyba v testu i v kódu.

[Filip Jirsák]

To není to co tvrdíš.

Jak to, že ne? Je to chyba v kódu, jednotkový test tu chybu odhalí, žádný použitelný typový systém jí nezabrání ani neodhalí. Je to tedy vyvrácení vašeho tvrzení, že by bylo možné všechny jednotkové testy nahradit typovým systémem.

Sorry, tvé příspěvky nejsou vůbec inspirativní. Nebudu se tedy tebou již zabejvat.

Ona vůbec inspirativní není vaše otázka, protože je triviální přijít na to, že existují algoritmy, které jsou platné a legitimní, a které je možné zaměnit za jiné platné a legitimní algoritmy. To typový systém nemůže zachytit, protože musí povolit oba dva algoritmy, ale nedokáže rozlišit, že jste chtěl použít jiný algoritmus. Sčítání a odčítání jsou ty nejjednodušší případy (někdy potřebujete sčítat, někdy odčítat, a žádný typový systém nezajistí, abyste nemohl použít odčítání tam, kde správně má být sčítání).

Spíš to vypadá, že jste z toho zmatený a není vám moc jasné, co zajišťuje typový systém a k čemu slouží jednotkové testy.

Tak snad pro vás bude inspirativní alespoň to, že největší slabinou jednotkových testů je to, že testují jenom případy, u kterých autor testů předpokládá, že by u nich mohl nastat problém. A dále to, že jedna z nejpodstatnějších dovedností programátora je právě schopnost odhalit ty problematické situace.

[Gődel]

Dále jsem se poučil studiem nějakých věcí, že typy jsou mnohem víc, než to, co nám ukazuje Java.

To rozhodně, v Javě je typový systém dost primitivní. Na druhou stranu čím mocnější typový systém, tím delší doba překladu, na jedné přednášce o Coqu si pochvalovali, jak jim překladač dokazuje korektnost, ale překlad trval hodiny kvůli závislostním typům.

[BoneFlute]

Akorát nevím jestli je v původním dotazu míněn typový systém javy - hádám že jsou míněny mnohem silnější typové systémy, které toho garantují mnohem víc. Možná by mohl BoneFlute upřesnit?

Úplně ten nejlepší (Agda, Idris, Eff) a ještě o kousek dál. Bavím se čistě na poli teorie. Takže to, že to bude nepraktické nevadí. Nerozhodnutelnost už samozřejmě ano. Přičemž zase ne zas tak teorie, abych třeba nemohl prohlásit, že "typový systém má omezení, že dokáže rozhodnout jen pro prvních milión prvočísel", třeba.

[Ondra Satai Nekola]

Kód: [Vybrat]

(toJSON json) -> str == (fromJSON str) -> json by nešlo? Kompiler by musel ověřit, zda všechny varianty stromu, když se vygenerují do stringu a pak následně naparsují jsou shodné.

No, obvávám se, že to je ale obecně vzato nerozhodnutelný problém... (i.e. halting problem). tímpádem to řešit typy  nejde. Těch "všech variant stromu" může být nekonečno, takže to nejde ani po jednom projít.

S timhle opatrne...
Halting problem je, kdyz ti nekdo (nepritel...) prinese program a ty mas rozhodovat o nem. Ty jsi v situaci, kdy sam pises program a typovy system ti na nej klade nejake omezeni. Takze ten zkoumany program neni libovolny, ale vznikly nejakym zpusobem (trebas tak, ze spolu s nim vznika "dukaz" jeho korektnosti).

Já to tak myslel - ty typeclassy jsou interface, nepřítel přinese program a kompilere rozhodni, zda to platí. No a protože možných vstupů je nekonečno, tak to nejde projít, tak by připadalo v úvahu nějaké rozhodnutí na jiné úrovni - ale to je halting problém. Takže s takto definovanými typy (FromJSON, ToJSON) nejde typově ošetřit, že ty instance jsou navzájem kompatibilní. (s jinak definovanými instancemi by to samozřejmě jít mohlo)

Ale u typoveho systemu nutis nepritele, aby prinesl program s dalsimi (strojove overitelnymi) castmi...

[BoneFlute]

To není to co tvrdíš.

Jak to, že ne? Je to chyba v kódu, jednotkový test tu chybu odhalí, žádný použitelný typový systém jí nezabrání ani neodhalí. Je to tedy vyvrácení vašeho tvrzení, že by bylo možné všechny jednotkové testy nahradit typovým systémem.

elm-package odhalí

Tak snad pro vás bude inspirativní alespoň to, že největší slabinou jednotkových testů je to, že testují jenom případy, u kterých autor testů předpokládá, že by u nich mohl nastat problém. A dále to, že jedna z nejpodstatnějších dovedností programátora je právě schopnost odhalit ty problematické situace.

Je mi líto, to moc dobře vím. Je to jeden z důvodů proč typy mám rád.

[BoneFlute]

Dále jsem se poučil studiem nějakých věcí, že typy jsou mnohem víc, než to, co nám ukazuje Java.

To rozhodně, v Javě je typový systém dost primitivní. Na druhou stranu čím mocnější typový systém, tím delší doba překladu, na jedné přednášce o Coqu si pochvalovali, jak jim překladač dokazuje korektnost, ale překlad trval hodiny kvůli závislostním typům.

Jsem si toho vědom. Na druhou stranu se to dá (snad) obejít. Třeba tím (naivně), že při dev procesu ty typy mám vypnuté, a teprve při releasu tomu dám nažrat.

[PetrM]

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)

[BoneFlute]

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)

Integrační testy sem prosím netahat.

[andy]

Ale pokud si myslíte, že je to řešitelné typovým systémem, ukažte váš kód. Ukažte, jak byste navrhl typový systém, který by u následujícího kódu odhalil chybu.

Kód: [Vybrat]

int add(int x, int y) {
  return x - y;
}

int sub(int x, int y) {
  return x - y;
}


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?

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.