Typový system versus unittesty

[andy]

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

[Reklama]

[v]

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 )

[Kiwi]

(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]

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?

[Ondra Satai Nekola]

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.

[Reklama]

[andy]

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:

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]

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]

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]

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]

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]

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.

[Filip Jirsák]

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]

Ž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]

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]

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