Je Rust jazyk budoucnosti?

Re:Je Rust jazyk budoucnosti?
« Odpověď #255 kdy: 05. 12. 2022, 13:10:39 »
To není pravda, 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í.
Ano, to je přesně to, o čem mluvim. Aby tohle fungovalo, musí být ta hodnota boxovaná (na-alokovaná na heapu a schovaná za, efektivně, pointer) a operace na ní se provádí přes dynamic dispatch (bude tam nějaký ekvivalent v-table), jinak by nebylo možné provést type erasure. Pokud budeš mít různé chování pro různé velikosti vektoru, bude se lišit minimálně ten vtable, případně chytřejší kompilátor nebo VM provede monomorfizaci pro různé instanciace, obojí ale efektivně znamená konstrukci typů v runtime. Tohle všechno je záležitost implementace runtimu.

Tohle Rust a C++ nemůžou udělat, protože nemůžou narozdíl od Idrisu libovolnou hodnotu implicitně boxovat a operace implicitně dynamicky dispatchovat, protože ten type systém musí být výkonově transparentní.

Borrowing v Rustu je implementován typovým systémem.
Není. Borrow checker provádí trochu chytřejší escape analýzu, kterážto je naprosto ortogonální k typům
Ne, borrowck využívá k té kontrole typové informace, co přesně ti není jasné na těch příkladech, které jsem uvedl? Ty dvě hodnoty prostě mají jiný typ, liší se typový parametr. Přijde mi, že se snažíš popřít očividné.

EDIT: To je argumentace, jako kdybych řekl, že tvoje GADT nejsou součást typového systému, protože přeci kontrolu velikosti pole mají i dynamické jazyky, které to při překladu vůbec neřeší. To je absurdní argumentace.
« Poslední změna: 05. 12. 2022, 13:14:38 od Králík »


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #256 kdy: 05. 12. 2022, 13:24:50 »
Tohle všechno je záležitost implementace runtimu.
Ne, není, v Idrisu, Leanu a podobných jazycích (pro které byl ten příklad) to je záležitost typové kontroly při překladu. Akorát je ta typová kontrola mnohem sofistikovanější než v C++ nebo Rustu (induktivní typy apod.).

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #257 kdy: 05. 12. 2022, 13:26:23 »
Tohle Rust a C++ nemůžou udělat, protože nemůžou narozdíl od Idrisu libovolnou hodnotu implicitně boxovat
Po tisící, Idris nic neboxuje, umí si to ověřit při překladu v rámci statické typové kontroly.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #258 kdy: 05. 12. 2022, 13:32:42 »
co přesně ti není jasné na těch příkladech, které jsem uvedl?
Jsou zcela irelevantní, vůbec se netýkají tématu. Kdybych escape analýzu, jak ji dělá Java nebo Go, použil pro borrow checking, bude to krásně fungovat i bez lifetimů jako typových parametrů. Rust má jen ten borrow checking o něco chytřejší, je to ostatně jeho jediná výhoda oproti srovnatelným jazykům.

Prostě borrow checking v Rustu používá typové parametry (pro lifetimy, to tady jistě všichni víme), ale není součástí typového systému (což zní jako blábol už na první pohled, je to jen konkrétní implementace escape analýzy).

Re:Je Rust jazyk budoucnosti?
« Odpověď #259 kdy: 05. 12. 2022, 14:17:20 »
Tohle všechno je záležitost implementace runtimu.
Ne, není, v Idrisu, Leanu a podobných jazycích (pro které byl ten příklad) to je záležitost typové kontroly při překladu. Akorát je ta typová kontrola mnohem sofistikovanější než v C++ nebo Rustu (induktivní typy apod.).

Po tisící, Idris nic neboxuje, umí si to ověřit při překladu v rámci statické typové kontroly.
Ano, ta typová kontrola probíhá při překladu, to já nijak nerozporuju, ale ten vygenerovaný kód, který je produktem toho kompilátoru, musí pak nutně záviset na runtime vlastnostech. V tom jednoduchém příkladě s vektorem by pravděpodobně opravu šlo tu velikost úplně vymazat a používat tu hodnotu bez indirekce atd., pokud to překladač dostatečně chytře zoptimalizuje, ale jakmile bude to bude složitější, nepůjde to. Třeba u těch matic, pokud budeš chtít použít jinou reprezentaci pro matice v závislosti na velikosti (například nějakou optimalizovanou/sparse reprezentaci pro velké matice), pak nutně bude potřeba ten typ s sebou nějakým způsobem mít v runtime, protože ty operace budou fungovat trochu jinak v závislosti na reprezentaci, minimálně nějaký tag tam bude muset být a runtime ho bude muset znát, vytvořit hodnotu se správným tagem apod.

Prostě borrow checking v Rustu používá typové parametry (pro lifetimy, to tady jistě všichni víme), ale není součástí typového systému (což zní jako blábol už na první pohled, je to jen konkrétní implementace escape analýzy).
Ne, není. Escape analýza je optimalizační technika, která je pro progamátora transparentní a není součástí sémantiky jazyka. Oproti tomu borrowing je součástí sémantiky jazyka. Tak tedy ještě jeden příklad, který je přímo z praktického kódu:

Kód: [Vybrat]
fn render_args<'j, 's: 'j>(&'s self, job: &'j RenderJob) -> Vec<&'j str> { ... }
Tady specifikuju pomocí typového systému, jaké vlastnosti má ta funkce wrt. borrowing, že výsledek je borrow jednoho z argumentů a druhý argument má k němu subtyping vztah, a tudíž je borrowing korektní. Je to principielně stejné jako třeba funkce, která by dva vektory o velikosti N a M spojila do vektoru velikosti N+M - takovou vlastnost můžeš výjádřit díky typovému systému. Stejnětak v Rustu můžu tento borrowing vztah vyjádřit typovým systémem.

Borrow checking je jedna z fází typové kontroly v Rustu. Není na tom moc co vymýšlet, snažit se to ohnout na escape analýzu nedává smysl, to je jako kdybys řekl, že výše zmíněná funkce spojující vektory je "jen trochu chytřejší bounds-checking".

Wow. Opravdu jsem nečekal, že někdo půjde až do takového absurdna, aby potopil Rust type systém...
« Poslední změna: 05. 12. 2022, 14:19:00 od Králík »


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #260 kdy: 05. 12. 2022, 14:30:30 »
Borrow checking je jedna z fází typové kontroly
  ::)

Re:Je Rust jazyk budoucnosti?
« Odpověď #261 kdy: 05. 12. 2022, 15:16:38 »
(Kdyžtak pls ukázku, jak tohle specifikuju bez typového systému.)

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #262 kdy: 05. 12. 2022, 15:49:29 »
Já třeba hodně zhruba rozumím té syntaxi, kterou jsi použil, protože třeba Haskel, nebo OCaml cca znám. […] Já tě jinak chci vyprovokovat, třeba něco napsat :-)
Myslím, že kdysi jsme se bavili o pokročilých typech na příkladu definice sudosti na úrovni typů. Ten příslušný typ “IsEven” je vlastně taky GADT, klidně to můžeme rozebrat znova z tohoto úhlu, jestli si myslíš, že to bude pro tebe přínosné. Akorát to nebudu psát z mobilu, to je vopruz :-\ takže spíš až večer.
Už si bohužel nepamatuju, jak daleko jsme se tehdy dostali, ale opakování matka moudrosti ;)

Typ IsEven má (meta)typ Nat -> Type (je to tedy typový konstruktor), v podstatě je to "funkce" (funkce na úrovni typů), která dostane přirozené číslo (Nat je induktivní typ, to teď asi není důležité) a vrátí typ. Potud asi jasné (?). Hlavička definice tedy bude
Kód: [Vybrat]
data IsEven : Nat -> Type where
Tento typ má dva konstruktory, řekněme ZIsEven a SuccSuccIsEven, které generují hodnoty různých typů (proto se jedná o GADT), ten první je typu IsEven 0 a ten druhý typu IsEven (n+2) pro nějaké přirozené číslo n.

Tady zastavím a počkám na tvůj feedback ;)
« Poslední změna: 05. 12. 2022, 15:51:28 od Idris »

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #263 kdy: 05. 12. 2022, 16:02:11 »
Ano, ta typová kontrola probíhá při překladu, to já nijak nerozporuju, ale ten vygenerovaný kód, který je produktem toho kompilátoru, musí pak nutně záviset na runtime vlastnostech. ... ale jakmile bude to bude složitější, nepůjde to.
Nějakou dobu jsem si hrál s Amulet ML, který kompiloval statickej kód do Luy. Díky tomu j sem si mohl vcelku rozumě prohlédnout, co to vymejšlelo. Na základě této zkušenosti ti nemohu dát za pravdu.

Re:Je Rust jazyk budoucnosti?
« Odpověď #264 kdy: 05. 12. 2022, 16:08:01 »
Ano, ta typová kontrola probíhá při překladu, to já nijak nerozporuju, ale ten vygenerovaný kód, který je produktem toho kompilátoru, musí pak nutně záviset na runtime vlastnostech. ... ale jakmile bude to bude složitější, nepůjde to.
Nějakou dobu jsem si hrál s Amulet ML, který kompiloval statickej kód do Luy. Díky tomu j sem si mohl vcelku rozumě prohlédnout, co to vymejšlelo. Na základě této zkušenosti ti nemohu dát za pravdu.
Já mam na mysli tu situaci, kdy zkonstruuješ parametrizovaný typ jako např. ten vektor nebo matici dynamicky ze vstupních dat. Lua úplně není dobrej příklad, protože to je dynamicky typovaný jazyk, tj. pochopitelně obsahuje runtime typové informace. Spíš by bylo lepší se podívat na ten C výstup.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #265 kdy: 05. 12. 2022, 16:10:59 »
Já třeba hodně zhruba rozumím té syntaxi, kterou jsi použil, protože třeba Haskel, nebo OCaml cca znám. […] Já tě jinak chci vyprovokovat, třeba něco napsat :-)
Myslím, že kdysi jsme se bavili o pokročilých typech na příkladu definice sudosti na úrovni typů. Ten příslušný typ “IsEven” je vlastně taky GADT, klidně to můžeme rozebrat znova z tohoto úhlu, jestli si myslíš, že to bude pro tebe přínosné.
Mám o to zájem, a předem děkuji.

Už si bohužel nepamatuju, jak daleko jsme se tehdy dostali, ale opakování matka moudrosti ;)
Dost mi to dalo, ale jak říkáš. Hlavně jsme se točily kolem forall, to bylo v tu dobu pro mě hodně zajímavé.

Typ IsEven má (meta)typ Nat -> Type (je to tedy typový konstruktor), v podstatě je to "funkce" (funkce na úrovni typů), která dostane přirozené číslo (Nat je induktivní typ, to teď asi není důležité) a vrátí typ. Potud asi jasné (?). Hlavička definice tedy bude
Kód: [Vybrat]
data IsEven : Nat -> Type where
Tento typ má dva konstruktory, řekněme ZIsEven a SuccSuccIsEven, které generují hodnoty různých typů (proto se jedná o GADT), ten první je typu IsEven 0 a ten druhý typu IsEven (n+2) pro nějaké přirozené číslo n.

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>
případně:
Kód: [Vybrat]
type IsEven<T> where T is Nat
?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Je Rust jazyk budoucnosti?
« Odpověď #266 kdy: 05. 12. 2022, 16:16:42 »
Typ IsEven má (meta)typ Nat -> Type (je to tedy typový konstruktor), v podstatě je to "funkce" (funkce na úrovni typů), která dostane přirozené číslo (Nat je induktivní typ, to teď asi není důležité) a vrátí typ. Potud asi jasné (?). Hlavička definice tedy bude
Kód: [Vybrat]
data IsEven : Nat -> Type where
Tento typ má dva konstruktory, řekněme ZIsEven a SuccSuccIsEven, které generují hodnoty různých typů (proto se jedná o GADT), ten první je typu IsEven 0 a ten druhý typu IsEven (n+2) pro nějaké přirozené číslo n.

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>
případně:
Kód: [Vybrat]
type IsEven<T> where T is Nat
?

Zatím v ničem. Pro GADT jsou relevantní až ty konstruktory hodnot.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #267 kdy: 05. 12. 2022, 16:22:09 »
Ano, ta typová kontrola probíhá při překladu, to já nijak nerozporuju, ale ten vygenerovaný kód, který je produktem toho kompilátoru, musí pak nutně záviset na runtime vlastnostech. ... ale jakmile bude to bude složitější, nepůjde to.
Nějakou dobu jsem si hrál s Amulet ML, který kompiloval statickej kód do Luy. Díky tomu j sem si mohl vcelku rozumě prohlédnout, co to vymejšlelo. Na základě této zkušenosti ti nemohu dát za pravdu.
Já mam na mysli tu situaci, kdy zkonstruuješ parametrizovaný typ jako např. ten vektor nebo matici dynamicky ze vstupních dat. Lua úplně není dobrej příklad, protože to je dynamicky typovaný jazyk, tj. pochopitelně obsahuje runtime typové informace. Spíš by bylo lepší se podívat na ten C výstup.
C je bordel na kolečkách. S tím se odmítám zabejvat.

Není podstatné, že Lua je dynamický jazyk. Chtěl jsem tím uvést, že když jsem se kouknul do toho zdrojáku, tak tam žádné typové informace, které tvrdíš, že tam musí zůstat aby něco, nebyly. Prostě Amulet vzal ty typové informace, provedl z toho transformaci na Luu, a všechny ostatní věci zahodil.

Co se týče toho vtable, na které jsi narážel - tomu se mi nechce věřit. To je nějaké matení. Protože:
1/ Jistě, Haskell má své hranice, a některé věci prostě už neutáhne compiletime, a tak se ty věci, které nejdou, převedou do runtime - v tomto samozřejmě souhlas.
2/ Cílem je, abychom dosáhli situace, kdy všechny věci budou podchyceny v compiledtime. Viz Idris.
3/ Výsledný kód nemusí nutně záviset na runtime - to je to tvrzení, které rozporuji.
4/ Já se neodvažuji tvrdit, zda borrowing je otázka typu nebo ne. Ale každopádně si představuji, že když dám v Rustu x.get_borrow() tak mi to může udělat různé věci. Od nějaké lokální proměnný, kde bude uchovanej výsledek, přes volání nějaké runtime obsluhy. Nic není daný musem.
5/ Samozřejmě, nikde nic nemusí být boxované, nebo boxovatelné.
« Poslední změna: 05. 12. 2022, 16:25:06 od BoneFlute »

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Je Rust jazyk budoucnosti?
« Odpověď #268 kdy: 05. 12. 2022, 16:28:44 »
Aby tohle fungovalo, musí být ta hodnota boxovaná (na-alokovaná na heapu a schovaná za, efektivně, pointer) a operace na ní se provádí přes dynamic dispatch (bude tam nějaký ekvivalent v-table), jinak by nebylo možné provést type erasure.
Teda, já jsem to vždycky chápal tak, že type erasure je způsob, jak typy odrbat. Kde by tam jako měla být schovaná vtable? A proč? Ve skutečnosti tam tu vtable potřebuješ v případě, kdy nechceš dělat type erasure...

Já té formulaci asi nerozumím.

Re:Je Rust jazyk budoucnosti?
« Odpověď #269 kdy: 05. 12. 2022, 17:00:25 »
Aby tohle fungovalo, musí být ta hodnota boxovaná (na-alokovaná na heapu a schovaná za, efektivně, pointer) a operace na ní se provádí přes dynamic dispatch (bude tam nějaký ekvivalent v-table), jinak by nebylo možné provést type erasure.
Teda, já jsem to vždycky chápal tak, že type erasure je způsob, jak typy odrbat. Kde by tam jako měla být schovaná vtable? A proč? Ve skutečnosti tam tu vtable potřebuješ v případě, kdy nechceš dělat type erasure...

Dobře, tak mějme ten příklad s maticí. Dejme tomu, že od nějaké velikosti Thr (jako threshold) používá implementace matice nějakou vymakanou reprezentaci v paměti kvůli ušetření místa pro velké matice. Ok? Teď dejme tomu, že máme operaci `col` na matici, která vrátí daný sloupec jako vektor. Tahle operace bude muset fungovat různě v závislosti na Thr, z úsporné reprezentace se čte sloupec jinak než z jednoduché.

Tak, a teď, ty napíšeš program, který načte matici ze souboru a bude chtít číst sloupce. Pokud by ta typová informace - v tomto případě velikost matice - byla komplet odstraněna, metoda `col` by neměla jak poznat, jak je konkrétní matice v paměti reprezentována, a tedy jak extrahovat sloupec. Proto bude muset ta matice si s sebou tu informaci vzít a držet si ji během runtime, buďto to může být nějaký tag, podle kterého udělá ta metoda `col` vidličku, anebo si s sebout vezme vtable, která bude u různých konkrétních hodnoty ukazovat na různé implementace `col`. Řešení s vtable je obecnější - těch typových parametrů může být více, chování se může v závislosti na nich více lišit.

V jazyce jako Rust nebo C++ tohle není potřeba, protože kompilátor zná dopředu všechny instanciace a provede monomofrizaci, ie. v podstatě z toho udělá různé typy s různými metodami, ale cena za to je, že není možné vytvořit tu hodnotu at runtime.

Není podstatné, že Lua je dynamický jazyk. Chtěl jsem tím uvést, že když jsem se kouknul do toho zdrojáku, tak tam žádné typové informace, které tvrdíš, že tam musí zůstat aby něco, nebyly.
Jak jsi poznal, že tam nebyly typové informace? V jazyce jako Lua má každá hodnota runtime typovou informaci, tak fungují dynamicky typované jazyky, tzn. ty typy tam nemohly nebýt :)

---

Jinak podíval jsem se na C výstup Idris kompilátoru a je to prostě VM (verze idris je u mě 1.3.4). Toto je funkce alokující hodnotu, okopírováno z Idris runtime:

Kód: [Vybrat]
static inline Con * allocConF(VM * vm, uint32_t tag, uint16_t arity, int outer) { ... }
Hádejte, co je `tag` :D