Typový system versus unittesty

[Filip Jirsák]

ž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ěří.

[Reklama]

[JSH]

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]

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

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]

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

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

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.

[Reklama]

[v]

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)

[Filip Jirsák]

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]

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é

[Filip Jirsák]

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]

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]

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]

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]

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]

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]

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?