Příspěvky

46

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 21:31:07 »

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/

47

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 17:17:02 »

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

48

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 16:43:02 »

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?

49

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 16:05:55 »

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.

50

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 16:03:29 »

ž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ě?

51

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 15:50:25 »

Popravdě mám dojem, že se v té teorii typů dost vyžíváte a děláte jí spíš medvědí službu.

Ano, indukční definice typu sudá čísla je pěkná ukázka. A v dalším kódu už pak opravdu můžeme mít jenom krásné garantované sudé číslo a optimalizátor tu informaci může pěkně využít.

Jenže co se stane, když načtete uživatelský vstup a bude tam číslo liché? Nějaký implicitní nebo explicitní parser musí rozhodnout, jestli ta hodnota je v pořádku nebo není a nějak zareagovat. A to je část, co se z ukázek síly funkcionálního programování typicky vypouští.

Naopak!
To je na tom právě to kouzelné, že staticky typované jazyky tě přinutí, aby si zohlednil situaci když je to číslo liché. To je právě ta smetana, po které toužíme. Garance.

Vysokoúrovňové informace pro optimalizátor nejsou navíc nezbytně omezeny jen na funkcionální jazyky. Ada a Eiffel mají třeba design by contract (= vstupní podmínky pro parametry), ostatní jazyky budou mít nějaký interface pro next, stream, iterátory nebo cokoliv podobného. (Lazy generátor v Haskellu interně stejně nic jiného nedělá). Dneska s LLVM a LTO se navíc optimalizace často dělají až nad mezikódem.

compile time?

52

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 15:35:59 »

Ten typový parametr rozměru se tam prostě zpropaguje jak v C tak i v JS kódu, žádný type-erasure, neměl jsem na ten výrok o type-erasure v první řadě vůbec skočit.

Jak zněl ten výrok?

->

kontrola toho typového parametru pro délku se provádí při překladu a pak se provede type erasure, v době běhu programu tam ten typový parametr vůbec není. Například Idris nebo Lean umí transpilaci do C, kde není runtime pro typy ani GC, veškerou kontrolu oddře překladač a když usoudí, že je kód typově správně, vyplivne výstup bez typových parametrů, ty právě slouží pouze ke statické kontrole.

JS kód vygenerovaný Idrisem:

Kód: [Vybrat]

function Main_getCol($0, $1, $2) {
 const $3 = Data_Nat_isLTE($0, 1000n);
 switch($3.h) {
  case 0: /* Yes */ return Main_getCol1($1, $2);
  default: return Main_getCol2($1, $2);
 }
}

$0 je velikost matice.

V Céčku je kód cca to samý, akorát mnohem výřečnější, protože úplně všechny hodnoty (i funkce) jsou boxovány do typu Value, které pak ten rozhodně-ne-interpretr, no, jaksi interpretuje

Tak buďme na Idrise krutí, a řekněme, že to nebylo úplně nejlépe formulováno. Ale:

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?

1/ Cítím určitý rozdíl mezi tím, když Python nebo Java jakožto dynamický jazyk narve spousta kontrol do runtime, protože nemá instrumenty na to, jak jinak. A mezi tím, že Idris by spousta typů do výsledného zdrojáku dávat nemusel, protože ty instrumenty má, ale také je ve verzi v0.6.0, a na optimalizace kašle.

2/ Také vidím určitý rozdíl mezi tím, když Idris při kompilaci oznámí, že kód je nekorektní, zatímco Java/Python by to oznámila až v runtime - a mezi tím, že Idris neprovádí optimalizace.

Jak jsem uváděl příklad s Amuletem, tam jsem se bavil tím, že opravdu optimalizoval. Z toho jsem čerpal já. Takže jsem pochopil, že to jde.

Pokud bylo tvým cílem dokázat, že Idris (jazyk) má před sebou ještě dlouhou cestu, protože neoptimalizuje kód jak by mohl - ok, máš boda.

Pokud bylo tvým cílem vysvětlit co je to type erasure, nebo jak probíhá optimalizace, nebo jaké jsou možnosti silných statických jazyků - tak to se ti nepovedlo.

Pokud bylo tvým cílem vysvětlit, že Rust je předvídatelnější (časově, paměťově) než Idris - ok, s tím nemám problém.

Dále jsem se ztratil v tom, co jsi chtěl vlastně dokazovat, promiň :-)

53

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 04:53:00 »

Ten typový parametr rozměru se tam prostě zpropaguje jak v C tak i v JS kódu, žádný type-erasure, neměl jsem na ten výrok o type-erasure v první řadě vůbec skočit.

Jak zněl ten výrok?
Co z této tvé zkušenosti vyplývá?

54

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 19:40:26 »

Jistěže je diskrétní (a také konečný), má jen dva konstruktory, nulu (Z) a následníka (S). Jenže ten druhý je rekurzivní, libovolné přirozené číslo n se vyjádří jako SⁿZ. Takže hodnot je nekonečně mnoho. Je to takto zřejmé?

Ano je.

Takže na místo Haskellovského

Kód: [Vybrat]

data Nat = 0,1,..., NatMax

je tam definice

Kód: [Vybrat]

data Nat : where
    Z  : Nat 0
    Succ : Nat n -> Nat (n+1)

nebo něco takového.

Haskell má Number jako buildin rozsah čísla. Zatímco Idris to má definováno vzorečkem.

Asi se chytám.

55

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 19:28:13 »

Říkáš, že Nat je Součtový (diskrétní) typ, takže tam nemůže být nekonečně mnoho čísel. Takže je nějak definováno něco jako NatMax, NatMin?

Nejmenší hodnota je nula, ale jinak to omezené není, těch hodnot je nekonečně (spočetně) mnoho, právě díky rekurzi toho druhého konstruktoru.

eee, tak je ten Nat diskrétní, nebo ne? :-)

Chápu to s tou rekurzí. Nechápu proč je podstatné, že Nat je diskrétní, když pak tvrdíš, že není 

56

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 19:07:33 »

Fajn. Takže ten první konstruktor, řekněme ZIsEven, je typu IsEven 0. To je zřejmé, ne?

A ten druhý konstruktor má argument typu IsEven, jeho typ je

Kód: [Vybrat]

SuccSuccIsEven : IsEven n -> IsEven (n+2)

Jasné zatím? Otázky?

Jasné. Chápu-li to správně, tak se to samozřejmě bude chovat rekurzivně, etc. Tak?

Komplet zápis takto?

Kód: [Vybrat]

data IsEven : Nat -> Type where
    ZIsEven  : IsEven 0
    SuccSuccIsEven : IsEven n -> IsEven (n+2)

Říkáš, že Nat je Součtový (diskrétní) typ, takže tam nemůže být nekonečně mnoho čísel. Takže je nějak definováno něco jako NatMax, NatMin? Tedy mohu klidně používat normálně Int, protože stejně ten Int není nekonečnej, ale nějakej automaticky zvětšující Number už bych použít nemohl... Tak?

Ten Type je zadrátovaný klíčový slovo/typ?

57

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 18:49:08 »

Typ chovající se jako funkce. Tomu rozumím. Jak se to liší a v čem je to podobné proti průmyslovým generikám:

Kód: [Vybrat]

type IsEven<T> where T is Nat

?

P.S. Tady bych ještě dodal, že Nat je induktivní typ, což třeba C++ vůbec nemá, takže rozdíl pod pokličkou je. Ale pro programátora se to tváří jako stejná věc.

Buď prosím vysvětli, proč je to zajímavé, že je to induktivní typ, nebo, pokud si myslíš, že to není tak podstatné pro vysvětlení, tak se můžeme přesunout dál.

Domnívám se, že to zajímavé je, protože Nat je součtový typ, takže to je, jako kdyby ten typový parametr byl enum (je to diskrétní typ se dvěma konstruktory). Kdyby to byl Int, bylo by možných hodnot nekonečně mnoho.

Rozumím. Důsledky mi dochází. Děkuji. Můžem pokračovat.

58

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 18:36:12 »

Ty tvrdíš, že nejenom, že to tam (v runtime) obecně musí být, ale navíc to v některých jazicích být musí (Haskel, Idris) a v některých (Rust) ne.

Mě by zajímalo proč.

To je možná nedorozumění. To co tvrdím v kostce je, že jazyky jako Rust nebo C++ nemůžou jen tak přejímat různé "sofistikované" abstrakce, protože musí dodržovat výkonovou transparenci svých abstrakcí (populárně "zero-cost abstractions"). Ano, ve spoustě případů může kompilátor v jazycích jako Haskell nebo Idris výsledný kód zoptimalizovat, takže výsledná cena není hrozná, to ale zkrátka není v jazyce jako Rust dostatečné, abstrakce v těchtoo jazycích musí být transparentnější, musí méně záviset na tom, jestli se zrovna v daném případě podařilo nebo nepodařilo kompilátoru kód zoptimalizovat, jestli bude GC dost rychlý a nebude moc brzdit atd.

Proti takovéto formulaci nic nemám.

Snad jen hnidopišskou poznámku, že v případě Haskellu je to záležitost "prostě se to tak stalo", nikoliv že by to z nějakého důvodu nešlo z principu. Dovedu si vyfantazírovat nějakou extenzi, která by přidávala pravidla, že tento a tento kód musí být takhle paměťově nebo rychlostně optimální etc. Možná by to ve výsledku znamenalo celej jazyk překopat, co já vím. Zde už jsem na tenkém ledě. V Haskellu jsem čistě uživatel.

59

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 18:21:13 »

Já vím přesně co je vtable, ať už v originále, nebo v tvém použití.

Co mě mate je type-erased metoda. Měl jsem za to, že type erased je chování, kdy za určitých okolností ztrácíme informaci o typu (respektive je nám zabráněno se k ní dostat). Wiki tvrdí toto: In programming languages, type erasure is the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time.

Dobře, tak nějaký konkrétní příklad, třeba Javu, ať je to jednoduchý - dejme tomu, že definuješ generickou funkci static <T> void writeAsString(T object) {} která vezme object, zavolá toString() a výsledek někam zapíše. Při kompilaci z toho java ty typy odstraní a vytvoří něco jako (ne doslova) void writeAsString(Object object) ... kód tý metody tedy při volání neví, jakej typ má argument, takže metodu toString() musí volat přes vtable, nemůže ji volat přímo.

Jistě. <sup>1)


1)</sup> Ignorujeme skutečnost, že Java bude brutálně optimalizovat, a JITovat, takže ve skutečnosti ten kód bude všelijakej.

60

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 18:18:50 »

Typ chovající se jako funkce. Tomu rozumím. Jak se to liší a v čem je to podobné proti průmyslovým generikám:

Kód: [Vybrat]

type IsEven<T> where T is Nat

?

P.S. Tady bych ještě dodal, že Nat je induktivní typ, což třeba C++ vůbec nemá, takže rozdíl pod pokličkou je. Ale pro programátora se to tváří jako stejná věc.

Buď prosím vysvětli, proč je to zajímavé, že je to induktivní typ, nebo, pokud si myslíš, že to není tak podstatné pro vysvětlení, tak se můžeme přesunout dál.

PS: Prosím, vůbec neuváděj C/C++. Java, Haskell, etc.