Typový system versus unittesty

[JSH]

nepochopil a jestli máte podobný background jako já (v mém případě C, C++, C#, python), tak se ani nedivím, docela mi trvalo než jsem to vstřebal (s pauzama možná rok), vlastně to není nic tak komplikovaného, ale je to hodně odlišné od programátorského mainstreamu

Tak mi to prosím osvětlete. Můj background je primárně C++ a hned po tom právě Haskell. Jestli jsem ten článek pochopil dobře, tak je to o JIT kompilaci Haskellu. Kdy a kde ta JIT kompilace běží?
Jestli u mně, tak neznám všechny vstupy a nemůžu si dovolit třeba velikosti polí nacpat do typu.
Jestli to běží u uživatele, tak jsou důkladné unit testy jediná možnost, jak si užít klidnou dovolenou.

[Reklama]

[BoneFlute]

Proč @v dokázal pochopit, že se táži na limity toho typového systému vůči unittestům, zatímco jiní se mě pokouší přesvědčit že jsem idiot a ani nejsou schopni uvést zajímavé argumenty?

Omezené možnosti kontroly správnosti programu typovým systémem jsem vám přímočaře a bleskově (a vypadá to, že nejen já, nečetl jsem vše) předvedl na příkladu, víceméně důkazu sporem. Takže odpověď na váš původní dotaz už máte. Je třeba ještě něco řešit?

Pro pořádek, hodíte sem link na ten příspěvek, prosím? Protože je možné, že jsem to mezi spoustou toho smetí přehlédl.

[Kit]

viz článek hned pod větou "For example, singleton function for natural addition :+ can be implemented as follows:"

Nebudu líny jako ty a pošlu sem ten kus kódu, který má nahradit test na sčítání typem:

Kód: [Vybrat]

infixl 6 :+

(%:+) :: SNat n -> SNat m -> SNat (n :+ m)
SZ   %:+ m = m
SS n %:+ m = SS (n %:+ m)
Vypadá to skoro jako test.

[Gődel]

že těla formulí jsou "běh" a typové výrazy "překlad".

Možná ti jen nerozumím, ale:
mám množiny
Bool = True | False
RGB = Red | Green | Blue
pak mám funkci
isRed :: RGB -> Bool
která se dá zapsat takto:
isRed :: RGB -> Bool = (Red -> True) | (Green -> False) | (Blue -> False)
Té množině isRed ale obvykle říkáme funkce, a něco počítá, ale je to stejně jen množina, respektive pohled na průnik dvou množin. (Nebudu se pokoušet trefit se do přesného pojmosloví.)

Bavíme se cca o tom samém?

Ano, bavíme. Jen jsem psal (možná to trochu zapadlo), že operace (výpočty) na všech úrovních jsou dány formulemi a základními hodnotami. Co jde vypočítat na té které úrovni je dáno těmito hodnotami stanovenými úmluvou. Na té nejnižší úrovni se utvořeným výrazům říká funkce, protože odpovídají funkcím v teorii množin (nebo prostě aritmetice apod.). Stejně tvořeným výrazům na vyšší úrovni už se říká jinak (podle kontextu metavýrazy, metahodnoty apod.), ale v podstatě to je to samé, jen o úroveň výše. V případě isRed můžu jednoduše napsat funkci a stejně jednoduše můžu vytvořit součtový typ nad RGB implementující isRed o úroveň výše (něco jako "metaIsRed"), jenž by šel použít v typovém systému pro kontrolu v době překladu. Ale jak už jsem psal nejméně dvakrát, moc praktické takové počínání není, už jen proto, že takové typy by se nikdy nepoužily za běhu (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.).

[v]

nepochopil a jestli máte podobný background jako já (v mém případě C, C++, C#, python), tak se ani nedivím, docela mi trvalo než jsem to vstřebal (s pauzama možná rok), vlastně to není nic tak komplikovaného, ale je to hodně odlišné od programátorského mainstreamu

Tak mi to prosím osvětlete. Můj background je primárně C++ a hned po tom právě Haskell. Jestli jsem ten článek pochopil dobře, tak je to o JIT kompilaci Haskellu. Kdy a kde ta JIT kompilace běží?
Jestli u mně, tak neznám všechny vstupy a nemůžu si dovolit třeba velikosti polí nacpat do typu.
Jestli to běží u uživatele, tak jsou důkladné unit testy jediná možnost, jak si užít klidnou dovolenou.

tak možná jsem zvolil trochu matoucí příklad, JIT je tam to co se implementuje, ne technika, která se využívá k implementaci něčeho jiného (uff)
kouzelný typ tam je "data TExp a" a pointa je, že nejde vytvořit hodnota tohoto typu, která by reprezentoval chybně typovaný syntaktický strom

[Reklama]

[BoneFlute]

že těla formulí jsou "běh" a typové výrazy "překlad".

Možná ti jen nerozumím, ale:
mám množiny
Bool = True | False
RGB = Red | Green | Blue
pak mám funkci
isRed :: RGB -> Bool
která se dá zapsat takto:
isRed :: RGB -> Bool = (Red -> True) | (Green -> False) | (Blue -> False)
Té množině isRed ale obvykle říkáme funkce, a něco počítá, ale je to stejně jen množina, respektive pohled na průnik dvou množin. (Nebudu se pokoušet trefit se do přesného pojmosloví.)

Bavíme se cca o tom samém?

Ano, bavíme. Jen jsem psal (možná to trochu zapadlo), že operace (výpočty) na všech úrovních jsou dány formulemi a základními hodnotami. Co jde vypočítat na té které úrovni je dáno těmito hodnotami stanovenými úmluvou. Na té nejnižší úrovni se utvořeným výrazům říká funkce, protože odpovídají funkcím v teorii množin (nebo prostě aritmetice apod.). Stejně tvořeným výrazům na vyšší úrovni už se říká jinak (podle kontextu metavýrazy, metahodnoty apod.), ale v podstatě to je to samé, jen o úroveň výše. V případě isRed můžu jednoduše napsat funkci a stejně jednoduše můžu vytvořit součtový typ nad RGB implementující isRed o úroveň výše (něco jako "metaIsRed"), jenž by šel použít v typovém systému pro kontrolu v době překladu.

Neměl by si prosím nějakou pěknu demonstraci principu toho metaIsRed. Nebo link na nějaké zdroje. Přeci jenom to hned z fleku nedávám (už jen ty množiny mi chvilku trvaly, než jsem dosáhl aha efektu).

A hlavně díky :-)

Ale jak už jsem psal nejméně dvakrát, moc praktické takové počínání není, už jen proto, že takové typy by se nikdy nepoužily za běhu.

Jak už jsem psal taky nejméně dvakrát, na praktičnost vám prdim :-)

[BoneFlute]

tak možná jsem zvolil trochu matoucí příklad, JIT je tam to co se implementuje, ne technika, která se využívá k implementaci něčeho jiného (uff)
kouzelný typ tam je "data TExp a" a pointa je, že nejde vytvořit hodnota tohoto typu, která by reprezentoval chybně typovaný syntaktický strom

Wow!
+1

[BoneFlute]

Ano, bavíme. Jen jsem psal (možná to trochu zapadlo), že operace (výpočty) na všech úrovních jsou dány formulemi a základními hodnotami. Co jde vypočítat na té které úrovni je dáno těmito hodnotami stanovenými úmluvou.

Nejsou ty formule náhodou takové ty "grupové axiomy"? Abych si to nějak srovnal.

[Kit]

typy můžou být definovány v knihovnách a mezi testem a tím v článku je přece jenom trochu rozdíl, ty záruky (pro všechny dvojice přirozených čísel) prostě testama nelze nahradit

Měl jem na mysli hlavně typy, které v knihovnách definovány nejsou a které je třeba definovat ke každé uživatelské funkci. Kdybych to aplikoval například na určitý integrál s mezemi a, b a funkcí f(x), tak ta definice typu bude buď nehorázně složitá, anebo bude duplicitou té funkce. Úplně se tím vytratí kouzlo jednoduchosti funkcionálního jazyka.

[Gődel]

Ano, bavíme. Jen jsem psal (možná to trochu zapadlo), že operace (výpočty) na všech úrovních jsou dány formulemi a základními hodnotami. Co jde vypočítat na té které úrovni je dáno těmito hodnotami stanovenými úmluvou.

Nejsou ty formule náhodou takové ty "grupové axiomy"? Abych si to nějak srovnal.

Vypadají tak. Formule se prostě poskládá z elementárních hodnot (ty závisí na úrovni, o kterou se jedná) a operací (grupy mají např. jen jednu). Hlavní rozdíl je, že u grup nejsou typy. Jakmile je přidáme, dostaneme kategorie, ale o těch se tu nemluví, jinak přijde Voldemort a sežere nám všechny monády...

[BoneFlute]

Nejsou ty formule náhodou takové ty "grupové axiomy"? Abych si to nějak srovnal.

Vypadají tak. Formule se prostě poskládá z elementárních hodnot (ty závisí na úrovni, o kterou se jedná) a operací (grupy mají např. jen jednu). Hlavní rozdíl je, že u grup nejsou typy. Jakmile je přidáme, dostaneme kategorie, ale o těch se tu nemluví, jinak přijde Voldemort a sežere nám všechny monády...

Díky!

[SB]

Pro pořádek, hodíte sem link na ten příspěvek, prosím? Protože je možné, že jsem to mezi spoustou toho smetí přehlédl.

Zde: https://forum.root.cz/index.php?topic=18804.msg270520#msg270520

Když tu tak čtu tu diskusi (a některým věcem nerozumím), tak mě napadá, že by asi šlo testy nahradit nějakým typovým systémem, ale jeho složitost by byla extrémní. Z praktického hlediska testy vyměňují obecnost (kategorie) či případnou složitost typového systému za svoji neúplnost (testování diskrétních hodnot) - diskrétní hodnoty by musely být nahrazeny mnoha specifickými třídami vedoucími na výraznou složitost typového systému. Uvažuju správně?

[Gődel]

Nejsou ty formule náhodou takové ty "grupové axiomy"? Abych si to nějak srovnal.

Vypadají tak. Formule se prostě poskládá z elementárních hodnot (ty závisí na úrovni, o kterou se jedná) a operací (grupy mají např. jen jednu). Hlavní rozdíl je, že u grup nejsou typy. Jakmile je přidáme, dostaneme kategorie, ale o těch se tu nemluví, jinak přijde Voldemort a sežere nám všechny monády...

Díky!

Abych to ještě uvedl přesněji: jsou dány základní typy (Church měl například ι a ο pro individua a pravdivostní hodnoty) a typované operace nad těmito typy. Funkčním výrazům odpovídají výhradně uzavřené formule, kupříkladu +≡(λx:ω)(λy:ω)x+y. Tělo je "x+y" a je vidět, že formule je uzavřená a výsledek je typu ω, takže typ formule je ωωω (asociativita je doleva). Tady je názorně vidět, že jediná operace u typů je v případě Churchova systému kompozice (v Haskellu se říká typový konstruktor). Když připustíme silnější typy, například se závislostmi (λ-kalkulu to je jedno, funguje s jakýmkoliv typovým systémem), můžeme počítat s typy a hodnoty na té nižší úrovní budou triviální (pro účely kontroly "překladu"), třeba u toho metaIsRed bychom měli jednotkové typy True a False. Největší sranda je, že jakmile začneme takto šaškovat s typy, neskončíme u dvou úrovní, ale nekonečně mnoha V praxi (jakmile to chceme implementovat) nás pak omezuje jen ta podmínka na konečnou dobu překladu (i když nekonečno vs. 100 let už zase takový rozdíl v praxi není...).

[Gődel]

Pro pořádek, hodíte sem link na ten příspěvek, prosím? Protože je možné, že jsem to mezi spoustou toho smetí přehlédl.

Když tu tak čtu tu diskusi (a některým věcem nerozumím), tak mě napadá, že by asi šlo testy nahradit nějakým typovým systémem, ale jeho složitost by byla extrémní.

Přesně, výhody by rozhodně nepřevažovaly. Ale výslovně byla žádána teorie bez ohledu na praxi.

[Filip Jirsák]

Když tu tak čtu tu diskusi (a některým věcem nerozumím), tak mě napadá, že by asi šlo testy nahradit nějakým typovým systémem, ale jeho složitost by byla extrémní. Z praktického hlediska testy vyměňují obecnost (kategorie) či případnou složitost typového systému za svoji neúplnost (testování diskrétních hodnot) - diskrétní hodnoty by musely být nahrazeny mnoha specifickými třídami vedoucími na výraznou složitost typového systému. Uvažuju správně?

Nešlo by takto nahradit ani zdaleka všechny testy. Vycházíte z toho, že test pokryje jenom některé možné vstupy, a nějakým typovým systémem byste omezil typy tak, aby byly možné jenom ty vstupy, které dávají správné výstupy. Jenomže tím se dostáváte do cyklu, protože to, zda jsou výstupy správné, není vlastností toho typového systému, ale je to arbitrární vlastnost – něco, co tomu přisuzujeme z venku. A k tomu právě slouží ty testy, abychom ověřili, že implementace (libovolná, klidně jako „typový systém“) odpovídá těm námi stanoveným pravidlům.

Jinak řečeno – o nějakém algoritmu ani typu nelze říci, zda je nebo není správně (sám o sobě). Jestli je nebo není správně závisí na tom, k čemu ho chceme použít. A to právě dělají testy – dají dohromady implementaci (algoritmus) a způsob použití a testují, zda daný algoritmus je správný pro daný způsob použití.

Typový systém nás může omezit, abychom něco nemohli použít způsobem, který pravděpodobně nikdy nebude správně. Ale už nás nemůže omezovat ve způsobu použití, který někdy správně je ale jindy správně není.