Typový system versus unittesty

Re:Typový system versus unittesty
« Odpověď #120 kdy: 19. 06. 2018, 10:50:32 »
že se v tom dá udělat chyba? no jistě, to jde všude
Jenže celá diskuse začala tvrzením, že s propracovaným typovým systémem nejsou potřeba jednotkové testy – kde je skrytý předpoklad, že se při použití propracovaného typového systému chyba udělat nedá.

Nebo-li v této diskusi se vyskytují dvě skupiny diskutujících – jedním připadá samozřejmé, že je možné chybu udělat všude, zatímco druzí tomu, že je možné udělat chybu všude, nevěří.


JSH

Re:Typový system versus unittesty
« Odpověď #121 kdy: 19. 06. 2018, 10:56:30 »
ptal jste se na typ, který garantuje, že kód provádí součet a ten jsem naznačil
nic se nepřesouvá, pořád máte zvlášť program a jeho typ, že se v tom dá udělat chyba? no jistě, to jde všude
Já se ptal v kontextu tohohle vlákna. Diskutujeme o tom, jestli se unittesty dají nahradit typovým systémem. Zeptám se jinak :

Píšu funkci, která skládá transformace. To je dost netriviální. A je tam pár věcí, které se dají jednoduše zvrtat. Třeba přehodit pořadí násobení matic. Jak dokážu typovým systémem ověřit, jestli to mám dobře? V unittestech otestuju pár jednoduchých případů a mám celkem jistotu.

v

Re:Typový system versus unittesty
« Odpověď #122 kdy: 19. 06. 2018, 10:57:33 »
že se v tom dá udělat chyba? no jistě, to jde všude
Jenže celá diskuse začala tvrzením, že s propracovaným typovým systémem nejsou potřeba jednotkové testy – kde je skrytý předpoklad, že se při použití propracovaného typového systému chyba udělat nedá.
myslím, že žádný takový předpoklad tam není
má to být náhrada, dá se předpokládat, že i s některými vlastnostmi původního řešení

v

Re:Typový system versus unittesty
« Odpověď #123 kdy: 19. 06. 2018, 11:09:14 »
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ý

ptal jste se na typ, který garantuje, že kód provádí součet a ten jsem naznačil
nic se nepřesouvá, pořád máte zvlášť program a jeho typ, že se v tom dá udělat chyba? no jistě, to jde všude
Já se ptal v kontextu tohohle vlákna. Diskutujeme o tom, jestli se unittesty dají nahradit typovým systémem.
asi nechápu
Píšu funkci, která skládá transformace. To je dost netriviální. A je tam pár věcí, které se dají jednoduše zvrtat. Třeba přehodit pořadí násobení matic. Jak dokážu typovým systémem ověřit, jestli to mám dobře? V unittestech otestuju pár jednoduchých případů a mám celkem jistotu.
napadají mě dvě možnosti, něco jako units of measure z F sharpu a pak prosté přejmenování typů, např místo (syntaxe haskellu) Float -> Float -> Float
 napsat Distance -> Time -> Speed (kde newtype Distance = Distance Float etc)

JSH

Re:Typový system versus unittesty
« Odpověď #124 kdy: 19. 06. 2018, 11:31:17 »
nejdřív bych zdůraznil svůj postoj: neargumentuju proti testům, testy jsou dobrá věc
Tak o čem tu diskutujeme? Vlákno začalo tvrzením
Citace
Dospěl jsem k nezdravému přesvědčení, že jednotkové testy nejsou potřeba máte-li kvalitní typový systém.
A všechny tyhle příklady, které sem házíme, jsou věci, které se dají ozkoušet triviálním unittestem, ale v typech je to přinejlepším strašně komplikované.

Citace
asi nechápu
Argumentujeme tu proti BoneFluteově extrémním postoji. Proti rozumnému využívání typů naše argumenty samozřejmě nedávají nejmenší smysl.


v

Re:Typový system versus unittesty
« Odpověď #125 kdy: 19. 06. 2018, 11:36:09 »
jeho extrémní postoj je zajímavý, rozumné použití typů je nuda (a co je dneska akademický blábol, může být zítra industry best practice)

Re:Typový system versus unittesty
« Odpověď #126 kdy: 19. 06. 2018, 11:42:18 »
myslím, že žádný takový předpoklad tam není
má to být náhrada, dá se předpokládat, že i s některými vlastnostmi původního řešení
Jednotkové testy se používají pro odhalení určitého typu chyb. Náhrada by musela alespoň odhalit stejný typ chyb, jinak to není náhrada.

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ý
A mohl byste tedy uvést konkrétní příklad? Zatím tady máme opakovaně příklad, kdy programátor omylem místo sčítání použije odčítání. Triviální jednotkový test takovou chybu odhalí. A zatím tady nebyl uveden žádný příklad typového systému, který by takové chybě zabránil. Viděli jsme jen příklady, že je možné operátor sčítání nahradit typem „výsledek součtu“, což ale neřeší ten problém, protože stejně, jako může programátor použít špatný operátor, může použít špatný typ.

Aby bylo jasno, já souhlasím s tím, že silnější typový systém znamená, že není potřeba psát některé jednotkové testy. Ale v žádném případě to neznamená, že dostatečně silný typový systém by znamenal, že nebudou potřeba žádné jednotkové testy (jak tvrdil BoneFlute), protože by vše, co se kontroluje jednotkovými testy, kontroloval typový systém.

v

Re:Typový system versus unittesty
« Odpověď #127 kdy: 19. 06. 2018, 12:01:29 »
myslím, že žádný takový předpoklad tam není
má to být náhrada, dá se předpokládat, že i s některými vlastnostmi původního řešení
Jednotkové testy se používají pro odhalení určitého typu chyb. Náhrada by musela alespoň odhalit stejný typ chyb, jinak to není náhrada.
přesně tak

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ý
A mohl byste tedy uvést konkrétní příklad?
uvedl
Zatím tady máme opakovaně příklad, kdy programátor omylem místo sčítání použije odčítání. Triviální jednotkový test takovou chybu odhalí. A zatím tady nebyl uveden žádný příklad typového systému, který by takové chybě zabránil.
byl
Viděli jsme jen příklady, že je možné operátor sčítání nahradit typem „výsledek součtu“
myslím, že ne

Ale v žádném případě to neznamená, že dostatečně silný typový systém by znamenal, že nebudou potřeba žádné jednotkové testy (jak tvrdil BoneFlute), protože by vše, co se kontroluje jednotkovými testy, kontroloval typový systém.
no a já si myslím, že to teoreticky možné je (výše jsem k tomu dal nějaké odkazy), což neznamená, že to někdy bude i praktické

Re:Typový system versus unittesty
« Odpověď #128 kdy: 19. 06. 2018, 12:25:02 »
V tom případě by to asi chtělo ten příklad rozvést a ukázat, jak je zabráněné tomu, abych místo typu „n-tý následník„ použil typ „n-tý předchůdce“, nebo „n-tý následník“ s -n místo n.

Konkrétně už tu byl uveden tento slabě typový pseudokód:
Kód: [Vybrat]
int add(int a, int b) {
  return a + b;
}

int sub(int a, int b) {
  return a - b;
}

Jak by vypadal tentýž kód, který by pomocí silnějších typů zabránil tomu, aby někdo místo sčítání použil odčítání?

Podle mne je tedy nesmyslné vůbec se pokoušet nějaké takové typy vytvořit, protože to, jestli se má použít sčítání nebo odčítání, je vlastností řešené domény – tudíž musí programátor pochopit řešený problém, uvědomit si, zda použije sčítání nebo odčítání (případně něco úplně jiného), a pak použije vhodné prostředky programovacího jazyka. Tohle za programátora nevyřeší žádný typový systém, protože kompilátor neví nic o tom, zda se má např. částka přičíst nebo odečíst, když firma zaplatí fakturu.

v

Re:Typový system versus unittesty
« Odpověď #129 kdy: 19. 06. 2018, 12:33:46 »
V tom případě by to asi chtělo ten příklad rozvést a ukázat, jak je zabráněné tomu, abych místo typu „n-tý následník„ použil typ „n-tý předchůdce“, nebo „n-tý následník“ s -n místo n.

Konkrétně už tu byl uveden tento slabě typový pseudokód:
Kód: [Vybrat]
int add(int a, int b) {
  return a + b;
}

int sub(int a, int b) {
  return a - b;
}

Jak by vypadal tentýž kód, který by pomocí silnějších typů zabránil tomu, aby někdo místo sčítání použil odčítání?

Podle mne je tedy nesmyslné vůbec se pokoušet nějaké takové typy vytvořit, protože to, jestli se má použít sčítání nebo odčítání, je vlastností řešené domény – tudíž musí programátor pochopit řešený problém, uvědomit si, zda použije sčítání nebo odčítání (případně něco úplně jiného), a pak použije vhodné prostředky programovacího jazyka. Tohle za programátora nevyřeší žádný typový systém, protože kompilátor neví nic o tom, zda se má např. částka přičíst nebo odečíst, když firma zaplatí fakturu.
tady je to hezky rozepsané https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

JSH

Re:Typový system versus unittesty
« Odpověď #130 kdy: 19. 06. 2018, 12:48:37 »
V tom případě by to asi chtělo ten příklad rozvést a ukázat, jak je zabráněné tomu, abych místo typu „n-tý následník„ použil typ „n-tý předchůdce“, nebo „n-tý následník“ s -n místo n.

Konkrétně už tu byl uveden tento slabě typový pseudokód:
Kód: [Vybrat]
int add(int a, int b) {
  return a + b;
}

int sub(int a, int b) {
  return a - b;
}

Jak by vypadal tentýž kód, který by pomocí silnějších typů zabránil tomu, aby někdo místo sčítání použil odčítání?

Podle mne je tedy nesmyslné vůbec se pokoušet nějaké takové typy vytvořit, protože to, jestli se má použít sčítání nebo odčítání, je vlastností řešené domény – tudíž musí programátor pochopit řešený problém, uvědomit si, zda použije sčítání nebo odčítání (případně něco úplně jiného), a pak použije vhodné prostředky programovacího jazyka. Tohle za programátora nevyřeší žádný typový systém, protože kompilátor neví nic o tom, zda se má např. částka přičíst nebo odečíst, když firma zaplatí fakturu.
tady je to hezky rozepsané https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell
Vždyť ten odkazovaný článek je o něčem úplně jiném. "Avoiding boundary errors" a to, jestli kód odpovídá modelovanému problému jsou někde úplně jinde.

Kit

Re:Typový system versus unittesty
« Odpověď #131 kdy: 19. 06. 2018, 12:51:54 »
tady je to hezky rozepsané https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

Když tu délku článku srovnám s délkou jednotkového testu, tak test jednoznačně vítězí.

v

Re:Typový system versus unittesty
« Odpověď #132 kdy: 19. 06. 2018, 12:54:45 »
tady je to hezky rozepsané https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell
Vždyť ten odkazovaný článek je o něčem úplně jiném. "Avoiding boundary errors" a to, jestli kód odpovídá modelovanému problému jsou někde úplně jinde.
používá to peanovu aritmetiku na typové úrovni pro vynucení vlastností operací s vektorama (ve smyslu datové struktury), např. tahle funkce je vlastně to stejné jako sčítání:
append :: Vector a n -> Vector a m -> Vector a (n :+ m)
délka výsledného vektoru je součet délek vstupních vektorů (a typový systém to opravdu na implementaci vynutí)

SB

Re:Typový system versus unittesty
« Odpověď #133 kdy: 19. 06. 2018, 13:06:27 »
Zajímalo by mě, můžete zkusit uvést nějaký příklad konstrukce, na kterou je nutné napsat test, protože typem to podchytit nejde?

class Sčítačka {
    Int součet(Int a, Int b) {
        <cokoliv>
    }
}

Int je třídou pro celá čísla (třeba vlastní implementace). Výsledek je nutně typu (správně instancí) Int, to je ale jediná věc, kterou vám typový systém garantuje. To ale nestačí - jak tento typ (třída) garantuje, že 1+1 rovná se opravdu 2???

Diskusi jsem nečetl - má to po výše uvedeném ještě smysl číst?
třeba peanova čísla na typové úrovni, v haskellu docela banální
Kód: [Vybrat]
type family Append a b where ...
součet :: I a -> I b -> I (Append a b)
součet = ...

Tak jinak: Doplňuju svůj původní příspěvek:

místo <cokoliv> je "return 10"

Typově je vše správně, ale nějak nám to pro většinu vstupů nevychází, přičemž by to mělo vyjít alespoň pro ty, které budu používat.

Přeloženo: Typová kontrola by zafungovala pouze v případě, že pro každé dva sčítance a součet budete mít extra typy, což je ale v rozporu s jednoduchými, obecnými kategoriemi (zde celá čísla) a prakticky to neřeší problém.

JSH

Re:Typový system versus unittesty
« Odpověď #134 kdy: 19. 06. 2018, 13:08:30 »
používá to peanovu aritmetiku na typové úrovni pro vynucení vlastností operací s vektorama (ve smyslu datové struktury), např. tahle funkce je vlastně to stejné jako sčítání:
append :: Vector a n -> Vector a m -> Vector a (n :+ m)
délka výsledného vektoru je součet délek vstupních vektorů (a typový systém to opravdu na implementaci vynutí)
1) Ten typ ale vůbec nezaručuje, že ten append dělá to, co chceme. Ten typ je kompatibilní se spoustou věcí od appendu v libovolném pořadí až po nějaké pseudonáhodné promíchání.
2) V reálných programech se obvykle počet prvků dovídám až v runtimu.
3) A jak to vůbec souvisí s tím, jestli kód odpovídá řešenému problému?