Typový system versus unittesty

[BoneFlute]

jednotkové testy nejsou potřeba máte-li kvalitní typový systém.

Typem jde vyjádřít jakákoliv vyčíslitelná vlastnost. Testy (nejen jednotkové) mají tu nevýhodu, že mohou prokázat přítomnost bugů, ale nikdy jejich absenci. Typový systém dokáže prokázat korektnost (absenci bugů).

Hezká formulace. Díky!

[Reklama]

[Wichser]

jednotkové testy nejsou potřeba máte-li kvalitní typový systém.

Typem jde vyjádřít jakákoliv vyčíslitelná vlastnost. Testy (nejen jednotkové) mají tu nevýhodu, že mohou prokázat přítomnost bugů, ale nikdy jejich absenci. Typový systém dokáže prokázat korektnost (absenci bugů).

Hezká formulace. Díky!

Není zač

[SB]

...Typový systém dokáže prokázat korektnost (absenci bugů).

Co když je v něm chyba (úplně stejně, jako může být ve výpočtu)?

[Ja]

Nechapu jednu vec. Mam funkci, ktera meni vstup na vystup:
5->3
3->5
Jak jde toto ošetřit typem bez použití unit testu?

[gll]

Nechapu jednu vec. Mam funkci, ktera meni vstup na vystup:
5->3
3->5
Jak jde toto ošetřit typem bez použití unit testu?

Na to už se tu ptalo hodně lidí. Odpověď nečekejte.

[Reklama]

[Wichser]

...Typový systém dokáže prokázat korektnost (absenci bugů).

Co když je v něm chyba (úplně stejně, jako může být ve výpočtu)?

Tak to je pak smůla, stejně jako když je chyba v testech.

[Wichser]

Nechapu jednu vec. Mam funkci, ktera meni vstup na vystup:
5->3
3->5
Jak jde toto ošetřit typem bez použití unit testu?

1. Ta funkce musí být totální. 2. V takto triviálních příkladech není moc co porovnávat, zápis těch typů bude v podstatě stejný jako zápis testů (akorát se vyhodnotí v době překladu). Zajímavějším příkladem by byla funkce s nekonečnem případů, např. f(n)=n+2, která nejde stoprocentně pokrýt testy.

[Wichser]

Jak jde toto ošetřit typem bez použití unit testu?

Zajímavějším příkladem by byla funkce s nekonečnem případů, např. f(n)=n+2, která nejde stoprocentně pokrýt testy.

Řešení:

Kód: [Vybrat]

plus2Proof : (n:Nat) -> plus2 n = n + 2
plus2Proof n = Refl


[A. F.]

Ta funkce musí být totální.

Můžete mi prosím vysvětlit, co to znamená totální funkce?

[JSH]

Ta funkce musí být totální.

Můžete mi prosím vysvětlit, co to znamená totální funkce?

Totální funkce má hodnotu pro všechny možné vstupy. V haskellu je třeba funkce head, která vrací první prvek seznamu

Kód: [Vybrat]

head :: [a] -> a
Ta není totální. Pro prázdný seznam nemá co vrátit a může leda tak nějak umřít. Jak přesně se to stane tady není podstatné.

Kód: [Vybrat]

head :: [a] -> Maybe a
by totální byla, protože Maybe (v jiných jazycích třeba optional) může být buď prázdný, nebo obsahovat hodnotu.

[SB]

Nechapu jednu vec. Mam funkci, ktera meni vstup na vystup:
5->3
3->5
Jak jde toto ošetřit typem bez použití unit testu?

Zkusím taky odpovědět: Např. závislostním typem duplikujícím výpočet dané funkce.

Jestli po celé té diskusi správně chápu závislostní typy, pak se jedná o (deklarativní) mechanismus omezení definičního oboru a oboru hodnot, případně vyjádření jejich závislosti. To lze určit v rozsahu od zcela volného až po zcela přesný, který pak ale obvykle (když nemá více řešení) kopíruje samotný výpočet. Takže buďto získám mechanismus omezeně kontrolující správnost výpočtu - otázkou je, zda to stačí, nebo zcela spolehlivě ověřím výpočet, ale samotná definice typu bude nutně stejně složitá jako samotný výpočet, takže můžu udělat tu samou chybu 2x. Závěr: Obecně neexistuje žádný magický mechanismus, který by dokázal (aťto v typu či jinde) rozhodnout, zda je můj výpočet správný.

To podstatné: Jednotkové testy se o hledání takového mechanismu ani nesnaží, protože to dle výše uvedené úvahy nejde. Využívají podmnožinu ZNÁMÝCH vstupů a jejich výstupů pro ověření výpočtu s tím, že je-li v pořádku, pro neznámé výstupy se výpočet považuje za pravděpodobně správný.

Takže z podstaty správnost výpočtu nezaručují ani jednotkové testy (to se vědělo), ani typový systém (to se tu někteří snažili dokázat). Tudíž jestli má smysl o něčem diskutovat, tak to, zda se vyplatí budovat typový systém nebo jednotkové testy.

[Bacsa]

Nechapu jednu vec. Mam funkci, ktera meni vstup na vystup:
5->3
3->5
Jak jde toto ošetřit typem bez použití unit testu?

Jestli po celé té diskusi správně chápu závislostní typy, pak se jedná o (deklarativní) mechanismus omezení definičního oboru a oboru hodnot, případně vyjádření jejich závislosti.

Spíš to druhé, když už. Typem jde vyjádřit vše, co je vyčíslitelné. Typické použití by bylo třeba u NP-úplných problémů. Na úrovni hodnot se hledá řešení, typový systém ověřuje řešení. Zásadní je, nakolik konkrétní překladač (resp. type checker) umí hledat důkazy automaticky, aby korektnost dokázal symbolicky bez pomoci.

[BoneFlute]

Takže buďto získám mechanismus omezeně kontrolující správnost výpočtu - otázkou je, zda to stačí, nebo zcela spolehlivě ověřím výpočet, ale samotná definice typu bude nutně stejně složitá jako samotný výpočet, takže můžu udělat tu samou chybu 2x. Závěr: Obecně neexistuje žádný magický mechanismus, který by dokázal (aťto v typu či jinde) rozhodnout, zda je můj výpočet správný.

Děkuji, moc pěkné.

[Bacsa]

Právě vyšla kniha k tématu: https://mitpress.mit.edu/books/little-typer

[v]

tady někdo píše k tématu https://blog.root.cz/scientia/