Typový system versus unittesty

andy

Re:Typový system versus unittesty
« Odpověď #225 kdy: 20. 06. 2018, 14:59:10 »
Myslel jsem, že se bavíme o tom, co je reálně dosažitelné. Ne že prohlásíme, že program předhodíme nějakému orákulu nebo CML, který nám řekne, zda je správně nebo špatně. No a že takový CML neumíme vytvořit? To je „lidský faktor“…
To není lidský faktor, to je halting problem....


v

Re:Typový system versus unittesty
« Odpověď #226 kdy: 20. 06. 2018, 15:10:11 »
Kód: [Vybrat]
toNat :: Int -> SNat n
Kdy ten typ závisí na vstupu od uživatele. No a..ono to nějak jde (někdy)...doufám, že až si to implementuju, tak i pochopím jak...
hint: jestli na to ghc nemá nějaký nový trik, tak budete potřebovat něco jako je v článku "data ATExp = forall a . TExp a ::: TTyp a", já jsem to teda potřeboval (a kdybyste to zvládl bez ATExp tak to sem určitě napište :D )

Kiwi

Re:Typový system versus unittesty
« Odpověď #227 kdy: 20. 06. 2018, 15:28:20 »
(ne že by se to nedělalo, ale jde jen o velmi speciální případy v avionice nebo kódu pro jaderné elektrárny apod.).
O tom bych měl něco vědět. Pro které elektrárny konkrétně? A o jaký typ kódu?

Kiwi

Re:Typový system versus unittesty
« Odpověď #228 kdy: 20. 06. 2018, 15:30:24 »
Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.
No tak to bych řekl, že ani náhodou! Nějaké podklady/porovnání by nebyly?

Re:Typový system versus unittesty
« Odpověď #229 kdy: 20. 06. 2018, 15:39:20 »
Myslel jsem, že se bavíme o tom, co je reálně dosažitelné. Ne že prohlásíme, že program předhodíme nějakému orákulu nebo CML, který nám řekne, zda je správně nebo špatně. No a že takový CML neumíme vytvořit? To je „lidský faktor“…
To není lidský faktor, to je halting problem....

To neni halting problem.

Uvedom si, ze tomu orakulu nepredhazujes libovolny program, ale program v urcenem formatu s urcenymi omezenimi (v extremnim pripade si muzes predstavit, ze povinnou soucasti programu v danem jazyce je i jeho dukaz).

Samozrejme zdaleka nejsme tam, kde by tohle bylo prakticke. Ale je potreba si uvedomit, ze se to obecnemu halting problemu podoba, ale ta uloha je (resp. muze byt) lehci.


andy

Re:Typový system versus unittesty
« Odpověď #230 kdy: 20. 06. 2018, 22:23:03 »
Myslel jsem, že se bavíme o tom, co je reálně dosažitelné. Ne že prohlásíme, že program předhodíme nějakému orákulu nebo CML, který nám řekne, zda je správně nebo špatně. No a že takový CML neumíme vytvořit? To je „lidský faktor“…
To není lidský faktor, to je halting problem....

To neni halting problem.

Uvedom si, ze tomu orakulu nepredhazujes libovolny program, ale program v urcenem formatu s urcenymi omezenimi (v extremnim pripade si muzes predstavit, ze povinnou soucasti programu v danem jazyce je i jeho dukaz).
No já reagoval na:
Citace
Myslel jsem, že se bavíme o tom, co je reálně dosažitelné. Ne že prohlásíme, že program předhodíme nějakému orákulu nebo CML, který nám řekne, zda je správně nebo špatně.
Což bych řekl, že o omezení nemluví...

andy

Re:Typový system versus unittesty
« Odpověď #231 kdy: 20. 06. 2018, 22:25:05 »
Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.
No tak to bych řekl, že ani náhodou! Nějaké podklady/porovnání by nebyly?
No, neodvažoval bych se něco takového tvrdit, ale faktem je, že programy v Haskellu jsou typicky docela hodně úsporné, takže "ani náhodou" bych se teda neodvažoval tvrdit taky.

Gődel

Re:Typový system versus unittesty
« Odpověď #232 kdy: 20. 06. 2018, 22:59:02 »
Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.
No tak to bych řekl, že ani náhodou! Nějaké podklady/porovnání by nebyly?
Je směšně triviální nahlédnout, že čím silnější typový systém, tím lepší znovupoužitelnost (ve smyslu DRY). V Javě a spol. nejde např. napsat obecná monáda kvůli absenci HKT (v C++ jde). S HKT bez závislostních typů se ale taky brzy narazí a musí se duplikovat. V několika iteracích to je názorně vidět na Swiftu, na začátku bylo v stdlib hodně duplicitního kódu kvůli slabému typovému systému. V poslední verzi (4.2) se kvanta kódu mohla smazat díky podmíněné konformanci a dalším vymoženostem. Až přidají HKT (je to v plánu), stdlib opět zeštíhlí. Tím to asi skončí, protože v 5. verzi už má být (konečně) stabilní ABI, ale i tak je docílená minimalizace kódu úctyhodná (nemluvě o vyšší bezpečnosti).

Kiwi

Re:Typový system versus unittesty
« Odpověď #233 kdy: 20. 06. 2018, 23:39:14 »
Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.
No tak to bych řekl, že ani náhodou! Nějaké podklady/porovnání by nebyly?
Je směšně triviální nahlédnout, že čím silnější typový systém, tím lepší znovupoužitelnost (ve smyslu DRY). V Javě a spol. nejde např. napsat obecná monáda kvůli absenci HKT (v C++ jde). S HKT bez závislostních typů se ale taky brzy narazí a musí se duplikovat. V několika iteracích to je názorně vidět na Swiftu, na začátku bylo v stdlib hodně duplicitního kódu kvůli slabému typovému systému. V poslední verzi (4.2) se kvanta kódu mohla smazat díky podmíněné konformanci a dalším vymoženostem. Až přidají HKT (je to v plánu), stdlib opět zeštíhlí. Tím to asi skončí, protože v 5. verzi už má být (konečně) stabilní ABI, ale i tak je docílená minimalizace kódu úctyhodná (nemluvě o vyšší bezpečnosti).
Ale já myslel nějaké konkrétní příklady v porovnání s dynamickými jazyky, ne s Javou. Že vymakaný typový systém zjednoduší program oproti neohrabanému jako je třeba v Javě, o tom bych se asi nepřel. Ale ten samý efekt vidím i u dynamických jazyků. Jenže zatímco takový Lisp nebo Smalltalk jsou směšně jednoduché, tak třeba ten Haskell mi vždycky připadal jako poměrně složitý.

andy

Re:Typový system versus unittesty
« Odpověď #234 kdy: 21. 06. 2018, 00:07:09 »
Ale já myslel nějaké konkrétní příklady v porovnání s dynamickými jazyky, ne s Javou.
Tohle možná půjde díky širokým knihovnám v některých dynamických jazycích, ale typicky to bývá dost problém... setřiď lidi sestupně podle věku, vzestupně podle příjmení - využívá typeclass Monoid a "rekurzivní" instance.
Kód: [Vybrat]
sortBy (flip (comparing age) <> comparing surname)

Monady - callback hell - JS vs. PureScript (nový JS na to má "await", takže tam už ten rozdíl není tak velký).

Polymorfní v návratové hodnotě - parsing JSONu. Tenhle kód provede kontrolu - nahlásí chybu, pokud vstupní data neobsahují položky s korektním typem. Dekóduje čas ve stringu na odpovídající typ, se kterým se dá normálně pracovat (UTCTime je něco jako "new Date()").

Vysvětlení: operátor ".:" je polymorfní v návratové hodnotě, takže hledá v objektu ten typ, který je požadován. Celé to běží v Parser monadu, takže v případě chyby se to celkem rozumně reportuje. Operátor <|> je "nebo" a funguje podobně jako "try...catch", dá se hezky řetězit.

Kód: [Vybrat]
data Person = Person Text Double UTCTime
instance FromJSON Person where
  parseJSON = withObject "person" $ \o -> do
    jmeno <- o .: "name" <|> o .: "jmeno"
    vyska <- o .: "height" <|> o .: "vyska"
    narozeni <- o .: "birthdate" <|> o .: "narozeni"
    return (Person jmeno vyska narozeni)

IMO kód v dynamických jazycích může být kratší, protože třeba v případě toho parsingu by se člověk prostě vybodnul na kontrolu korektního vstupu... v některých jaycích a knihovnách to ještě nějak relativně dobře funguje přes generic parsing, ale jak do toho člověk potřebuje trochu víc hrábnout (zpětná kompatibilita apod.), tak už ten kód hodně roste a je dost nepřehledný.

Gődel

Re:Typový system versus unittesty
« Odpověď #235 kdy: 21. 06. 2018, 00:35:33 »
Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.
No tak to bych řekl, že ani náhodou! Nějaké podklady/porovnání by nebyly?
Je směšně triviální nahlédnout, že čím silnější typový systém, tím lepší znovupoužitelnost (ve smyslu DRY). V Javě a spol. nejde např. napsat obecná monáda kvůli absenci HKT (v C++ jde). S HKT bez závislostních typů se ale taky brzy narazí a musí se duplikovat. V několika iteracích to je názorně vidět na Swiftu, na začátku bylo v stdlib hodně duplicitního kódu kvůli slabému typovému systému. V poslední verzi (4.2) se kvanta kódu mohla smazat díky podmíněné konformanci a dalším vymoženostem. Až přidají HKT (je to v plánu), stdlib opět zeštíhlí. Tím to asi skončí, protože v 5. verzi už má být (konečně) stabilní ABI, ale i tak je docílená minimalizace kódu úctyhodná (nemluvě o vyšší bezpečnosti).
Ale já myslel nějaké konkrétní příklady v porovnání s dynamickými jazyky, ne s Javou. Že vymakaný typový systém zjednoduší program oproti neohrabanému jako je třeba v Javě, o tom bych se asi nepřel. Ale ten samý efekt vidím i u dynamických jazyků. Jenže zatímco takový Lisp nebo Smalltalk jsou směšně jednoduché, tak třeba ten Haskell mi vždycky připadal jako poměrně složitý.
U dynamických jazyků to vyjde nastejno, akorát člověk nemá tu typovou kontrolu. Přínos mocných typových systémů je právě v tom, že při plné typové kontrole umožňuje značnou flexibilitu (“dynamičnost”). Jinak Haskell složitý není, jen jiný - matoucí je možná syntax.

Re:Typový system versus unittesty
« Odpověď #236 kdy: 21. 06. 2018, 07:27:26 »
IMO kód v dynamických jazycích může být kratší, protože třeba v případě toho parsingu by se člověk prostě vybodnul na kontrolu korektního vstupu...
Byl bych velmi opatrný s tvrzením, že kratší kód se automaticky rovná lepší kód. Vy jste napsal konkrétní případ, kdy je kód kratší ale jiný, ale ani kratší kód, který dělá přesně to samé, jako delší kód, nemusí být lepší.

v

Re:Typový system versus unittesty
« Odpověď #237 kdy: 21. 06. 2018, 08:25:30 »
Že vymakaný typový systém zjednoduší program oproti neohrabanému jako je třeba v Javě, o tom bych se asi nepřel. Ale ten samý efekt vidím i u dynamických jazyků.
někdo tvrdí, že pokud máte dostatečné pokrytí testy, tak nepotřebujete statický typový systém - myslíte, že by ten efekt nezmizel kdybychom započítali i testy? přece jenom typy umožňují množinu možných testcasů dost zmenšit

SB

Re:Typový system versus unittesty
« Odpověď #238 kdy: 21. 06. 2018, 11:20:46 »
Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.

Nechci spekulovat, ale jednoduchá úvaha, že když netypový systém otypuju, tj. omezím jej, dosáhnu tak větší znovupoužitelnosti, neboli obecnosti, mi nedává smysl.

Gődel

Re:Typový system versus unittesty
« Odpověď #239 kdy: 21. 06. 2018, 11:24:51 »
Ještě tu nezaznělo, že kromě vyšší bezpečnosti přináší silný typový systém také úsporu kódu díky větší znovupoužitelnosti. To jen tak pro úplnost.
Nechci spekulovat, ale jednoduchá úvaha, že když netypový systém otypuju, tj. omezím jej, dosáhnu tak větší znovupoužitelnosti, neboli obecnosti, mi nedává smysl.
Co je “netypový systém”? Dynamické typování je netypové nebo ne? Jinak znovupoužitelnost nesouvisí s obecností.