Je Rust jazyk budoucnosti?

[BoneFlute]

že typové parametry se komplet vymažou a vůbec ve výstupu nefigurují a pak čekáš, až zjistim, že ten parametr tam můžeme zpropagovat, pokud to potřebujeme

Nevím jak Idris, ale já se snažil vždycky psát, že ty typové informace se vymažou (můžou vymazat), když nejsou potřeba. A když jsou potřeba, tak je samozřejmě třeba je neodstraňovat. Dokonce jsem na to psal kód, aby mi bylo dobře rozumět. Jaký zmatek je v tomto bodě?

[Reklama]

[BoneFlute]

Chceš na to ještě nějak navázat? Otázky k tomuto konkrétnímu příkladu?

Určitě ano, ale nyní mám povinnosti.
Večer.

[Idris]

já se snažil vždycky psát, že ty typové informace se vymažou (můžou vymazat), když nejsou potřeba. A když jsou potřeba, tak je samozřejmě třeba je neodstraňovat

Ono to je matoucí, protože k type erasure dochází vždy (v tom smyslu, že tam není žádný reifikovaný typ Vect nebo Matrix, tj. instance neví, jakého jsou typu), ale používané typové parametry se předávají přímo funkcím, které je potřebují.

[Králík]

Znamená to tedy, že ve výsledném kódu musí být tagy, typy, qqch? Že neprobíhá type erasure, tak nějak z principu? Že ve výsledném kódu musí být nějaké runtime, protože něco?

Asi nejlépe nechme type erasure apod. spát, IMO to vede spíše ke zmatení diskuse. Také s tebou souhasím, že type checking umožňuje optimalizovat a de-facto přebytečné informace z programu odstraňovat, ale IMO tady neplatí nějaký jednoduchý vztah typu čím víc proužků, tím víc adidas, tj. čím víc type-systému, tím víc optimalizace. Ironicky, uživatel Idris tohle tak trochu potvrdil tím, že odsoudil Rust type systém jako "primitivní" - pokud budeme souhlasit, pozorujeme skutečnost, kde jazyk s primitivním TS prodkuje rychlejší programy než jazyk se 'sofistikovanými' TS.

Abych ti konečně odpověděl - IMO ta otázka, jestli / jak moc sofistikované abstrakce (a které a s jakými omezeními atd.) vyžadují tlustější runtime, je otevřená. Nicméně máme určité datapointy - Haskell už existuje desítky let a má, pokud vím, celkem vymakaný kompilátor a produkovaný kód je relativně rychlý, ale - a to nemyslím jako kritiku - žádný dramatický trhač rekordů v rychlosti to není. Další datapoint je právě vývoj Rustu, kde pozoruju, jak velmi je náročné přidávat abstrakce (move semantics, korutiny, GATs, ...) při dodržení těch runtime constraints, korektnosti, ergonomie.

V sumě, můj názor je, že ten přístup, kdy se nespoutaně vyvíjí a opěvují vysoké, velmi 'sofistikované' abstrakce, s tím, že generování kódu se zoptimalizuje někdy později, není přínosný - tj. to, co dělá např. Idris/Idris2, ale nemám v úmyslu kritizovat specificky Idris, tohle se týká i spousty jiných jazyků. Vzpomínám si, že podobných diskusí o tom, jak $FPjazyk bude zanedlouho mít super optimalizující kompilátor a konkurovat C++, jsem se zúčastnil třeba 15 let zpátky... a mezitím se nic moc nezměnilo resp. zlepšení je pouze dílčí/malé. Takže ve výsledku jsem fanoušek přístupu, kdy se abstrakce vyvíjí trochu pomaleji, návrh jazyka zůstává nohama trochu více na zemi* a zároveň s tím se vyvíjí rovnou i schopnost produkovat pokudmožno optimální kód pro reálná CPU, protože to umožňuje ty zkušenosti s generováním strojového kódu reflektovat do návrhu těch abstrakcí, do návrhu IR reprezentací atd.

*) ať už si na to zvolíš víceméně jakýkoli metr, třeba lispisti nebo smalltalkisti/selfisti také rádi měří jazykům abstrakční penisy a sebe dávají na vrchol, ale metr mají jiný

[BoneFlute]

ale IMO tady neplatí nějaký jednoduchý vztah typu čím víc proužků, tím víc adidas, tj. čím víc type-systému, tím víc optimalizace. Ironicky, uživatel Idris tohle tak trochu potvrdil tím, že odsoudil Rust type systém jako "primitivní" - pokud budeme souhlasit, pozorujeme skutečnost, kde jazyk s primitivním TS prodkuje rychlejší programy než jazyk se 'sofistikovanými' TS.

Abych ti konečně odpověděl - IMO ta otázka, jestli / jak moc sofistikované abstrakce (a které a s jakými omezeními atd.) vyžadují tlustější runtime, je otevřená. Nicméně máme určité datapointy - Haskell už existuje desítky let a má, pokud vím, celkem vymakaný kompilátor a produkovaný kód je relativně rychlý, ale - a to nemyslím jako kritiku - žádný dramatický trhač rekordů v rychlosti to není. Další datapoint je právě vývoj Rustu, kde pozoruju, jak velmi je náročné přidávat abstrakce (move semantics, korutiny, GATs, ...) při dodržení těch runtime constraints, korektnosti, ergonomie.

Dobře. Zkusme se na to podívat z nového směru.

Nejdřív úvod: Máme compile-time (Haskell, Idris, Rust) a run-time jazyky (Java, Python, JS, Lua).
A můžeme posuzovat kritéria:
- rychlost běhu
- předvídatelnost
- čitelnost
- garance

A teď se pojďme bavit o čitelnosti a garancích. Run-time jazyky neposkytují vůbec žádné záruky. To je věřím jasná věc.

1/ Dá se říct, že když porovnáme Rust a Haskell, tak Rust sice poskytuje značné záruky, ale také nutí uživatele aby řešil každou blbost? Zatímco Haskell a Idris jsou více abstraktní ve smyslu, že vyžadují od uživatele jen to nejnutnější?

2/ Kde jsou hranice záruk, které poskytuje Rust, ale Idris je ještě je schopen poskytnout?

[Reklama]

[Králík]

Run-time jazyky neposkytují vůbec žádné záruky. To je věřím jasná věc.

To se obávám, že až tak jasná věc není, typické runtime skriptovací jazyk (Python, JS, ... whatever) poskytují větší záruky než třeba C nebo C++ - nesegfaultují ti, neumožní divoce castovat typy, ...

1/ Dá se říct, že když porovnáme Rust a Haskell, tak Rust sice poskytuje značné záruky, ale také nutí uživatele aby řešil každou blbost? Zatímco Haskell a Idris jsou více abstraktní ve smyslu, že vyžadují od uživatele jen to nejnutnější?

Tohle IMO nemůžeme rozhodnout, protože to bude subjektivní. Za mě třeba pure funkce jsou víc řešení blbostí než co po mě chce Rust.

2/ Kde jsou hranice záruk, které poskytuje Rust, ale Idris je ještě je schopen poskytnout?

Tady asi nerozumim otázce...

[BoneFlute]

Run-time jazyky neposkytují vůbec žádné záruky. To je věřím jasná věc.

To se obávám, že až tak jasná věc není, typické runtime skriptovací jazyk (Python, JS, ... whatever) poskytují větší záruky než třeba C nebo C++ - nesegfaultují ti, neumožní divoce castovat typy, ...

Argumentace C/C++ je varianta Godwinova zákona.

2/ Kde jsou hranice záruk, které poskytuje Rust, ale Idris je ještě je schopen poskytnout?

Tady asi nerozumim otázce...

Rust je schopen zajistit, že nedojde k memory leaku.
Rust je schopen zajistit, že nedojde k race-condition.
A určitě umí další věci.
Je schopen Rust vynutit, aby programátor zkontroloval, že tady a tady bylo pouze sudé číslo? Idris to umí.

[Králík]

Argumentace C/C++ je varianta Godwinova zákona.

Dobře, ale principielně ten argument je IMO platný, ono by se dalo říct i třeba to, že JS v prohlížeči poskytuje větší záruky než i safe Rust, protože ti třeba neumožní omylem si smazat $HOME ... Stačí si tu metriku nadefinovat trochu jinak, než co ty asi předpokládáš...

Je schopen Rust vynutit, aby programátor zkontroloval, že tady a tady bylo pouze sudé číslo? Idris to umí.

No to zase záleží na tom, co myslíš tím "umí". Například Rust vynucuje u stringů, aby byly vždy utf8-korektní.

[Idris]

Chceš na to ještě nějak navázat? Otázky k tomuto konkrétnímu příkladu?

Určitě ano, ale nyní mám povinnosti.
Večer.

Teď mě napadlo, jak jsi zmiňoval to tehdejší forall, že existenční typy jdou vyjádřit jednodušeji pomocí GADT.

[BoneFlute]

Argumentace C/C++ je varianta Godwinova zákona.

Dobře, ale principielně ten argument je IMO platný, ono by se dalo říct i třeba to, že JS v prohlížeči poskytuje větší záruky než i safe Rust, protože ti třeba neumožní omylem si smazat $HOME ... Stačí si tu metriku nadefinovat trochu jinak, než co ty asi předpokládáš...

Rust běžící v prohlížeči ti také neumožní smazat $HOME. JS běžící z příkazové řádky ti $HOME smaže klidně.

Je schopen Rust vynutit, aby programátor zkontroloval, že tady a tady bylo pouze sudé číslo? Idris to umí.

No to zase záleží na tom, co myslíš tím "umí". Například Rust vynucuje u stringů, aby byly vždy utf8-korektní.

OK, doplním zadání:

Kde jsou hranice záruk, které poskytuje Rust, ale Idris je ještě je schopen poskytnout?

Rust je schopen zajistit, že nedojde k memory leaku. Idris také.
Rust je schopen zajistit, že nedojde k race-condition. Idris také.
Rust je schopen zajistit, že že string bude vždy utf8-korektní. Idris také.
A určitě umí další věci.
Je schopen Rust vynutit, aby programátor zkontroloval, že tady a tady bylo pouze sudé číslo? Idris to umí.
Je schopen Rust vunutit, aby text byl neprázdný? Haskell to umí ¹⁾.

¹⁾ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/

[Idris]

Je schopen Rust vunutit, aby text byl neprázdný? Haskell to umí

A Idris to umí ještě lépe, nemusíš kvůli tomu definovat nový typ

[BoneFlute]

Je schopen Rust vunutit, aby text byl neprázdný? Haskell to umí

A Idris to umí ještě lépe, nemusíš kvůli tomu definovat nový typ

Teď jsem ve fázi, zda. Jak je jiná otázka.

Třeba to forall mi přišlo poněkud složité oproti přímočarým rozhraním v průmyslových jazycích. Ale je fakt, že to nemám v krvi a mé seznámení s ním bylo jen zběžné, a tak to neumím docenit. Asi to umí víc, nebo to nějak elegantněji zapadá, co já vím.

[Idris]

Třeba to forall mi přišlo poněkud složité oproti přímočarým rozhraním v průmyslových jazycích.

Ono je složitější, protože typové třídy mají typový parametr, kdežto rozhraní v Javě nebo Go ho mít nemusí. Jsou to rozdílné věci. Ale jak jsem psal, forall se dá zbavit použitím GADT.

[Králík]

Rust je schopen zajistit, že nedojde k memory leaku.

Tady nevim přesně jak to myslíš, ale absence leaků nepatří do záruk Rust safe kódu, leaking není unsafe. OTOH  díky různým vlastnostem neleakující kód není nějak těžké psát.

Je schopen Rust vunutit, aby text byl neprázdný?

To je to samé jako utf8-korektnost, ne? Spíš rovnou vysvětli, kam tím míříš, a já zkusim líp odpovědět.

[BoneFlute]

Rust je schopen zajistit, že nedojde k memory leaku.

Tady nevim přesně jak to myslíš, ale absence leaků nepatří do záruk Rust safe kódu, leaking není unsafe. OTOH  díky různým vlastnostem neleakující kód není nějak těžké psát.

Je schopen Rust vunutit, aby text byl neprázdný?

To je to samé jako utf8-korektnost, ne? Spíš rovnou vysvětli, kam tím míříš, a já zkusim líp odpovědět.

Nehledej v tom žádný podraz ani žádnou složitost. Čti přesně co píšu.

Rust poskytuje záruky. Proto ho mám rád.
Haskell, Idris, etc - poskytují záruky.

Rust u některých věcí není schopen záruky poskytnout. Neumí to.
Java není schopna zaručit, že přeložený kód nepadne na NullException.
Haskell není schopen zaručit... - já nevím, určitě tam něco bude, ale jsem línej to vymejšlet.

Java je méně schopná jak Rust, Rust je méně schopnej jak Haskell (asi - neber mě za slovo).

No, a já se zajímám, kde ta hranice je.

Umí Java vynutit, aby v kódu nenastala situace, že na místě kde je potřeba neprázdný string se objevil prázdný string? Odpověď: ani za zlatý prase.
Umí Java zajistit, aby v kódu nenastala situace, že na místě, kde je třeba sudé číslo přišlo číslo liché? Odpověď: LOL.

Co Rust? Hodně toho umí. Co už neumí? Kde cca stojí ta hranice?

btw: To, že Rust některé záruky nedokáže zajistit je fakt, nikoliv hendikep. I tak je to zjevení, a jsem nadšen, že existuje.