Příspěvky

211

Vývoj / Re:Je Rust jazyk budoucnosti?

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

212

Vývoj / Re:Je Rust jazyk budoucnosti?

« 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

213

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 14:30:30 »

Borrow checking je jedna z fází typové kontroly

 

214

Vývoj / Re:Je Rust jazyk budoucnosti?

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

215

Vývoj / Re:Je Rust jazyk budoucnosti?

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

216

Vývoj / Re:Je Rust jazyk budoucnosti?

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

217

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 12:23:38 »

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 (ostatně mají ji i dynamické jazyky, které typy při překladu vůbec neřeší).

218

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 12:21:20 »

S runtimem i GC to souvisí, protože aby tvůj příklad fungoval, musí runtime jazyka být schopen za běhu instanciovat generický typ, vytvořit hodnotu takovéhu typu, dispatchovat na ní operace a nakonec být schopen tu hodnotu zase uvolnit.

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

219

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 11:32:48 »

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.

220

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 11:14:56 »

Ano, proto jsem psal staticky ověřovat. Co se týče te dynamické stránky, jazyky jako Rust nebo C++ tohle mít nemůžou

Pleteš si pojmy. Staticky znamená v době překladu. Ten příklad s Vect se taky ověřuje v době překladu, ale ten typový parametr pro délku vektoru nemusí být v době překladu znám. Rust a C++ pro to nemají formální prostředky, ale jiné jazyky to prostě umí (a nemusí mít GC ani runtime, to s tím vůbec nesouvisí).

A ještě jednou pro ty pomalejší, borrowing ani GC nijak nesouvisí s typovým systémem.

221

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 03:07:30 »

určitě žádné mlaskání

Mlaskat klidně mohli, v Africe se mlaská dodnes (viz lingvistický pojem “mlaskavka”) Koho současné poznání vývoje lidských jazyků zajímá, může si přečíst něco od Dietera Wunderlicha nebo Jerryho Hobbse, ti to popisují srozumitelně i pro laiky. Podle Chomského k vývoji dnešního typu jazyka došlo před 70000-100000 lety a od té doby se jazykový systém nezměnil (mění se slovní zásoba a tvarosloví, ne strukturní principy), to je ale jen jedna z hypotéz.

222

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 02:48:51 »

Přiznám se, že tyhle komentáře mě poněkud iritují

To je tvůj problém. Hierarchie sofistikovaných typových systémů (pořadí podle formální síly) je “no sophistication < HKT < GADT < DP”. Rust nemá ani HKT, je v té hierarchii úplně vlevo (ta hierarchie by se dala zjemnit, třeba Julia má sice silnější typový systém než Rust, ale plnohodnotné HKT taky nemá).

223

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 02:41:09 »

Počkat, staticky ověřovat dimenzi snad v C++ (a Rustu) jde, pomocí skalárních typových argumentů (v Rustu "const generics", stále dosti experimentální fíčura, ale to je principielně jedno).

Const generics vyžadují hodnotu známou v době překladu (pro méně nechápavé to mají přímo v názvu). Jazyky se silnějšími typovými systémy toto omezení nemají (silnější = méně primitivní, ovšem jde to vyjádřit i matematicky, zná-li člověk formální aparát).

224

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 04. 12. 2022, 20:21:32 »

Pokud jde o nutnost memory safe jazyku, s tim nepolemizuju, akorat stale nejsem presvedcen, ze cesta je prave pres Rust.

Pokud si jako kritérium vezmeš memory safe, tak ačkoliv Rust není dokonalý, tak čím by si mu chtěl konkurovat? (Bavíme se o nízkoúrovňovém jazyku. Na nějaké appky vždycky můžeš použít Javu, samozřejmě.) Jaké máš výhrady, nebo očekávání?

Spark?

225

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 04. 12. 2022, 16:35:34 »

Já tě jinak chci vyprovokovat, třeba něco napsat :-)

Jdeš na to fikaně Zrovna GADT nejsou žádná věda. Když definuju (běžný) ADT, určím typ, například “List a”, a k němu konstruktory. V případě GADT se určí typ pro každý konstruktor zvlášť. V případě “Vect” (Nat -> Type -> Type, Nat je typ přirozených čísel) mám konstruktor “Nil” typu “Vect 0 a” (ta nula je délka vektoru) a druhý konstruktor “Cons” typu “a -> Vect n a -> Vect (n+1) a”. To ADT neumí, protože jednou tam je nula a jednou “n+1”.