Typový system versus unittesty

BoneFlute

  • *****
  • 1 859
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #795 kdy: 18. 09. 2018, 23:46:11 »
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!
« Poslední změna: 18. 09. 2018, 23:48:36 od BoneFlute »


Wichser

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

Re:Typový system versus unittesty
« Odpověď #797 kdy: 19. 09. 2018, 09:33:53 »
...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

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

  • ****
  • 429
    • Zobrazit profil
    • E-mail
Re:Typový system versus unittesty
« Odpověď #799 kdy: 19. 09. 2018, 11:27:00 »
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.


Wichser

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

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

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

Re:Typový system versus unittesty
« Odpověď #803 kdy: 19. 09. 2018, 18:16:47 »
Ta funkce musí být totální.

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

JSH

Re:Typový system versus unittesty
« Odpověď #804 kdy: 19. 09. 2018, 21:35:58 »
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

Re:Typový system versus unittesty
« Odpověď #805 kdy: 20. 09. 2018, 09:17:10 »
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

Re:Typový system versus unittesty
« Odpověď #806 kdy: 20. 09. 2018, 10:00:49 »
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

  • *****
  • 1 859
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #807 kdy: 20. 09. 2018, 16:26:30 »
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

Re:Typový system versus unittesty
« Odpověď #808 kdy: 21. 09. 2018, 11:35:55 »
Právě vyšla kniha k tématu: https://mitpress.mit.edu/books/little-typer

v

Re:Typový system versus unittesty
« Odpověď #809 kdy: 04. 10. 2018, 16:03:04 »
tady někdo píše k tématu https://blog.root.cz/scientia/