Typový system versus unittesty

JS

Re:Typový system versus unittesty
« Odpověď #780 kdy: 23. 08. 2018, 13:35:57 »
Skoro se mi nechce věřit, že by se na root fóru dospělo k nějakému konsenzu :)

Jinak to je duvod, proc sem zase tak moc nechodim.. Nejvic mi asi vadi to, kdyz nekdo chce s necim pomoci, nekdo jiny mu odpovi, a hned se najde nejaky magor, ktery (misto aby upresnil nebo napsal lepsi odpoved a pomohl tak puvodnimu tazateli) se zacne navazet do toho, kdo odpovedel, a ukazovat, jak je "lepsi" programator.

Bohuzel ale to je asi vseobecne dnes v Cesku takova hulvatska kultura.


BoneFlute

  • *****
  • 1 859
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #781 kdy: 23. 08. 2018, 14:51:43 »
Zkusím tady nadhodit myšlenkový experiment, který snad ukáže, co se mi celé na té myšlence náhrady testů typy nelíbí.
...
Díky za příspěvek. Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá, ale děkuji za pěkný rozbor. V mnohém máš určitě i pravdu.

Myslím, že alespoň v tom, co dělám já, by ty ukázky často byly k ničemu. Třeba u toho polygonu by ze stroje vypadla řada čísel - souřadnic bodů polygonu, ale dokud si to nenakreslíš, tak nevidíš co to vlastně testuje. A to už je jednodušší si ty zajímavé příklady nejprve nakreslit a potom je, u komplikovaných případů třeba i okomentované a s naskenovaným obrázkem, zadat do unit testů.
Hmm, může být.

Bacsa

Re:Typový system versus unittesty
« Odpověď #782 kdy: 26. 08. 2018, 00:55:34 »
Díky za příspěvek. Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Ono ty typy nejsou moc praktické obecně, větší program se závislostními typy se klidně může překládat hodiny.

JSH

Re:Typový system versus unittesty
« Odpověď #783 kdy: 26. 08. 2018, 10:26:54 »
Díky za příspěvek. Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Ono ty typy nejsou moc praktické obecně, větší program se závislostními typy se klidně může překládat hodiny.
Já si dokážu nějaké praktické využití i představit. Při běžné kompilaci by se používaly jen nějak zjednodušené typy bez závislostí. Plný typový systém by se použil až na buildserveru, kde to v pohodě může překládat hodiny a hodiny.

Ale tohle je vlastně jen trochu jiná statická analýza. A anotace pro statický analyzátor se přidávají do spousty jazyků. Není to omezené na fukcionální jazyky.

Bacsa

Re:Typový system versus unittesty
« Odpověď #784 kdy: 26. 08. 2018, 13:44:07 »
Díky za příspěvek. Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Ono ty typy nejsou moc praktické obecně, větší program se závislostními typy se klidně může překládat hodiny.
Já si dokážu nějaké praktické využití i představit. Při běžné kompilaci by se používaly jen nějak zjednodušené typy bez závislostí. Plný typový systém by se použil až na buildserveru, kde to v pohodě může překládat hodiny a hodiny.
Ano, já nechtěl říct, že to je nepoužitelné, jen že to má trochu specifické použití.


Bacsa

Re:Typový system versus unittesty
« Odpověď #785 kdy: 27. 08. 2018, 21:22:17 »
Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Když už jsme u té praktičnosti, řekněme, že mám funkci "double" pro násobení přirozených čísel dvěma a chci zaručit, že výsledek je sudý tím, že vracím (závislostní) hodnoty typu (n ** Even n). Jak ale zařídím, aby na lichých hodnotách typová kontrola selhala, resp. aby všechny relevantní funkce byly totální?

BoneFlute

  • *****
  • 1 859
    • Zobrazit profil
Re:Typový system versus unittesty
« Odpověď #786 kdy: 27. 08. 2018, 21:40:15 »
Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Když už jsme u té praktičnosti, řekněme, že mám funkci "double" pro násobení přirozených čísel dvěma a chci zaručit, že výsledek je sudý tím, že vracím (závislostní) hodnoty typu (n ** Even n). Jak ale zařídím, aby na lichých hodnotách typová kontrola selhala, resp. aby všechny relevantní funkce byly totální?

Možná ti nerozumím, ale tak nepřeloží se to, ne?

Bacsa

Re:Typový system versus unittesty
« Odpověď #787 kdy: 27. 08. 2018, 21:57:14 »
Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Když už jsme u té praktičnosti, řekněme, že mám funkci "double" pro násobení přirozených čísel dvěma a chci zaručit, že výsledek je sudý tím, že vracím (závislostní) hodnoty typu (n ** Even n). Jak ale zařídím, aby na lichých hodnotách typová kontrola selhala, resp. aby všechny relevantní funkce byly totální?
Možná ti nerozumím, ale tak nepřeloží se to, ne?
Takhle ne, ale když chci totální funkce, tak ty úpravy mě v podstatě donutí řešit to až za běhu.

Bacsa

Re:Typový system versus unittesty
« Odpověď #788 kdy: 28. 08. 2018, 12:33:26 »
Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Když už jsme u té praktičnosti, řekněme, že mám funkci "double" pro násobení přirozených čísel dvěma a chci zaručit, že výsledek je sudý tím, že vracím (závislostní) hodnoty typu (n ** Even n). Jak ale zařídím, aby na lichých hodnotách typová kontrola selhala, resp. aby všechny relevantní funkce byly totální?
Možná ti nerozumím, ale tak nepřeloží se to, ne?
Tak si odpovím sám, musí se vytvořit koprodukt implementující Uninhabited, aby ty funkce byly totální. Člověk se pořád učí...

v

Re:Typový system versus unittesty
« Odpověď #789 kdy: 28. 08. 2018, 15:53:41 »
Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Když už jsme u té praktičnosti, řekněme, že mám funkci "double" pro násobení přirozených čísel dvěma a chci zaručit, že výsledek je sudý tím, že vracím (závislostní) hodnoty typu (n ** Even n). Jak ale zařídím, aby na lichých hodnotách typová kontrola selhala, resp. aby všechny relevantní funkce byly totální?
Možná ti nerozumím, ale tak nepřeloží se to, ne?
Tak si odpovím sám, musí se vytvořit koprodukt implementující Uninhabited, aby ty funkce byly totální. Člověk se pořád učí...
ukažte kód :)

Bacsa

Re:Typový system versus unittesty
« Odpověď #790 kdy: 28. 08. 2018, 16:05:30 »
Já jsem to celé sice původně podával jako, že praktičnost mě až tak moc nezajímá
Když už jsme u té praktičnosti, řekněme, že mám funkci "double" pro násobení přirozených čísel dvěma a chci zaručit, že výsledek je sudý tím, že vracím (závislostní) hodnoty typu (n ** Even n). Jak ale zařídím, aby na lichých hodnotách typová kontrola selhala, resp. aby všechny relevantní funkce byly totální?
Možná ti nerozumím, ale tak nepřeloží se to, ne?
Tak si odpovím sám, musí se vytvořit koprodukt implementující Uninhabited, aby ty funkce byly totální. Člověk se pořád učí...
ukažte kód :)

Kód: [Vybrat]
data OnlyEven : Parity n -> Type where
  OnlyEvenC : OnlyEven (Even n)

Uninhabited (OnlyEven (Odd n)) where
  uninhabited _ impossible

test : (par:Parity n) -> {auto prf:OnlyEven par} -> String
test n = (show n) ++ " is provably even"
Ať žije type-driven programming :)

v

Re:Typový system versus unittesty
« Odpověď #791 kdy: 28. 08. 2018, 16:09:58 »
Kód: [Vybrat]
data OnlyEven : Parity n -> Type where
  OnlyEvenC : OnlyEven (Even n)

Uninhabited (OnlyEven (Odd n)) where
  uninhabited _ impossible

test : (par:Parity n) -> {auto prf:OnlyEven par} -> String
test n = (show n) ++ " is provably even"
Ať žije type-driven programming :)
díky, máte k tomu i tu nějakou tu double nebo něco podobného (co vyžaduje sudý Nat v argumentu nebo tak) ?

Bacsa

Re:Typový system versus unittesty
« Odpověď #792 kdy: 28. 08. 2018, 16:17:42 »
Kód: [Vybrat]
data OnlyEven : Parity n -> Type where
  OnlyEvenC : OnlyEven (Even n)

Uninhabited (OnlyEven (Odd n)) where
  uninhabited _ impossible

test : (par:Parity n) -> {auto prf:OnlyEven par} -> String
test n = (show n) ++ " is provably even"
Ať žije type-driven programming :)
díky, máte k tomu i tu nějakou tu double nebo něco podobného (co vyžaduje sudý Nat v argumentu nebo tak) ?
Ne, psal jsem to celé znova a "double" už jsem pak neřešil, to mi už přišlo triviální.

Bacsa

Re:Typový system versus unittesty
« Odpověď #793 kdy: 28. 08. 2018, 16:26:37 »
Kód: [Vybrat]
data OnlyEven : Parity n -> Type where
  OnlyEvenC : OnlyEven (Even n)

Uninhabited (OnlyEven (Odd n)) where
  uninhabited _ impossible

test : (par:Parity n) -> {auto prf:OnlyEven par} -> String
test n = (show n) ++ " is provably even"
Ať žije type-driven programming :)
díky, máte k tomu i tu nějakou tu double nebo něco podobného (co vyžaduje sudý Nat v argumentu nebo tak) ?
Pro argument to bude asi něco jako
Kód: [Vybrat]
double : (n:Nat) -> {default (parity n) par:Parity n} -> {auto prf:OnlyEven par} -> Nat
double n = n * 2

Wichser

Re:Typový system versus unittesty
« Odpověď #794 kdy: 18. 09. 2018, 23:21:39 »
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ů).