Typový system versus unittesty

[JS]

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.

[Reklama]

[BoneFlute]

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]

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]

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]

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

[Reklama]

[Bacsa]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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ů).