Příspěvky

181

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 11:05:41 »

Když to shrnu, veškeré typové parametry a konstruktory (lifetimy, reference…) jsou normálně součástí typového systému Rustu (tyto mu ale nijak nepřidávají na síle),

Takže bez nich by Rust type systém podle tebe byl stejně "sofistikovaný"?

Jistě, reference je normální typový konstruktor a lifetime je jen další typ pro typové parametry. Kdybych tam přidal typ “brambora”, mohl bych si ho přidat ke generické funkci, ale sofistikovanější to nebude.

Reference ostatně mají téměř všechny mainstreamové jazyky a lifetimy jsou implicitně v každém překladači provádějícím escape analýzu. Více či méně chytrý je ovšem ten algoritmus escape analýzy (Java nic moc, Go lepší, ale dost věcí mu unikne, Rust propracovaný).

182

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 10:50:17 »

veškeré obecné možnosti HTKs a GADTs, zejména v situaci, kdy hraje roli dynamický vstup

No a vidíš, že v Idrisu, Leanu, Agdě, Coqu (a OCamlu, Scale…) pro to žádné vtables nepotřebuješ.

183

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 10:47:32 »

Co se typů v Rustu týče, tak borrow checker je move sémantika + escape analysis. Ale lifetime specifier je jednoznačně součást definovaného typu a poskytuje borrow checkeru informace navíc

Přesně tak.

184

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 10:44:54 »

Jenže co se stane, když načtete uživatelský vstup a bude tam číslo liché?

Použije se funkce vracející hodnotu typu Dec (IsEven n), který je součástí standardní knihovny a implementuje rozhodnutelnost (nějaké vlastnosti, v tomto případě sudosti). To je součtový typ “zabalující” buď hodnotu typu IsEven n nebo Not (IsEven n). Myslím, že k tomu ta diskuse směřovala a pokud bude mít BoneFlute zájem, určitě dojde i na příklady.

185

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 10:39:16 »

Viděl jsi ten kód vůbec někdy?

Viděl, i když většinou jsem potřeboval JS.
Nicméně ptám se na runtime zachazející s těmi typovými parametry, o kterém jsi tvrdil, že je nutný. Že tam je funkce na počítání referencí by tě nemělo překvapovat, kde jsi použil backend nazvaný “ref-counting C”
Sorry, ale když řekneš, že typové parametry potřebuji runtime pro boxing a já nevím co, a pak píšeš něco o matematických funkcích, tam to není dobrý argument.

186

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 10:35:17 »

V tom příkladu, který jsem uváděl, tj.:

Kód: [Vybrat]

fn render_args<'j, 's: 'j>(&'s self, job: &'j RenderJob) -> Vec<&'j str> { ... }

Ty nepovažuješ lifetimes za součást typu té funkce? Anebo považuješ, ale nesouhlasíš, že popisují způsob, jakým ta funkce přesouvá (move) či si půjčuje (borrow) argumenty

Jsou to typové parametry a ta funkce je generická, takže ano, jsou součástí typu funkce. Ovšem o move vs. borrow rozhoduje, jestli je typ reference (to andítko je jiný typový konstruktor nesouvisející s lifetimy). A borrow checker kontroluje, že reference jsou vždy platné tam, kde se používají (escape analýza). Taky že jsou unikátní v případě mut, ale takových detailů tam je hodně. Když to shrnu, veškeré typové parametry a konstruktory (lifetimy, reference…) jsou normálně součástí typového systému Rustu (tyto mu ale nijak nepřidávají na síle), ale borrow checking/escape analýza jsou jen algoritmy, ty nemůžou být jeho součástí už z definice (quicksort taky není součástí pole nebo seznamu, ale umí ho seřadit).

187

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 10:20:36 »

Záleží na implementaci, v C++ je move sémantika naprasená víceméně pouze ve standardní knihovně (edit: nad typovou fíčurou "r-value references"). V Rustu je s typy provázána mnohem více

Tak jsme se konečně shodli, není součástí, ale je provázaná. Můžeme slavit

P.S. Jako bonus je tady odkaz na zmíněný seriál o Mercury, někde se tam probírají lineární typy a také IO ve funkcionálním paradigmatu (spoiler: není to tam jako v Haskellu): https://www.root.cz/serialy/mercury/

188

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 10:18:26 »

Aha. Tak nám v tom transpilovaném kódu ukaž, kde jsou ty tvoje runtimy, GC a vtables, o kterýchs tvrdil, že tam určitě musí být.

Runtime v tom C kódu pochopitelně je velmi silně. GC tam je, byť v primitivní formě

Runtime tam žádný není. Ukaž nám, co tam je podle tebe runtime. GC je pro hodnoty, tys tvrdil, že se tam boxují, alokují a uvolňují typové parametry. To tam taky není.

189

Studium a uplatnění / Re:CoolPeople - zkušenosti

« kdy: 06. 12. 2022, 10:15:42 »

A speciálně to platí pro pseudo-podnikatele ze Slovenska

s cim konkretne mas problem "Don Kokot"?  Ze nemate kvalitnu silu, to uz je vas problem. Preto sa hladaju kvalitnejsi kandidati u nas. Zmier sa s tym

To je presna ukazka ega Slovaka v "Prahe".
Mam bohuzel celkem dost Slovaku v praci.
O nejake kvalitnejsi praci bych teda pomlcel.
Prumerni programatori a "operations" coz jsou spis cviceny opice tahajici za paku, kterym hrdost vzrostla po povoleni pristupu na barevnou kopirku.

A ty kecy.... "ve vsech statech ma chceli, ale som so rozhodl ist sem". Jaka smula pro nas.

Mé zkušenosti se Slováky v Praze (a Brně) jsou vesměs pozitivní. I se Slováky na Slovensku (a že jich tam je, kromě jihu teda). Asi jsi měl smůlu na lidi.

190

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 09:48:14 »

si strašně vymýšlíš

Aha. Tak nám v tom transpilovaném kódu ukaž, kde jsou ty tvoje runtimy, GC a vtables, o kterýchs tvrdil, že tam určitě musí být. Kampak se nám ty čerchmanti schovali? Neznáš pořádně ani Rust, natož GADT, ale myslím, že už ses z této diskuse dost naučil (díky, BoneFlute) a klidně můžeme ještě nějakou dobu pokračovat

191

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 09:45: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?

Chceš na to ještě nějak navázat? Otázky k tomuto konkrétnímu příkladu?
Pokud ne, možná by tě ještě zajímaly implicitní parametry v kvantitativních typových systémech (které teď s velkou slávou objevil Králík)?

192

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 06. 12. 2022, 09:42:52 »

Také jsem zjistil, že Idris [...] - měl jsem dříve představu, že to je kompilovaný jazyk jako Haskell.

Je kompilovaný, ty si to pleteš a asi myslíš, že generuje přímo nativní kód. To je ovšem tvůj problém, nikdo to tady netvrdil. Naopak ti bylo řečeno, že má různé backendy (C, JS, ...). Defaultně používá Scheme (Chez).

Btw. v této přednášce Simon Peyton Jones mluví o možnostech linearity v Haskellu a také trochu o Rustu, borrowing/ownership označuje jako "Linearity on the Kinds".

Ale to je velmi trefné, linearita je prostě určitá sémantika předávání argumentů (hezky to má například Mercury, viz seriál zde na Rootu, v Rustu to je v podstatě move sémantika). Move sémantika není záležitost typového systému, ale v kombinaci s ním (v Rustu jde zejména o reference, to asi víš, co je) zaručuje paměťovou bezpečnost. BoneFlute ti to možná vysvětlí, má s tebou evidentně větší trpělivost

P.S. Máš malé nevýznamné plus za ten odkaz

193

Vývoj / Re:Je Rust jazyk budoucnosti?

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

Co z této tvé zkušenosti vyplývá?

Že Králík neví, co je interpretr Ale aspoň už zjistil, co jsou v Idrisu implicitní parametry.

194

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 19:45:49 »

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é?

je tam definice

Kód: [Vybrat]

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

nebo něco takového.

Ano, akorát bez těch typových parametrů. Takto to mají všechny funkcionální jazyky, i třeba OCaml. Prostě Peanova definice

195

Vývoj / Re:Je Rust jazyk budoucnosti?

« kdy: 05. 12. 2022, 19:32:31 »

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

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é?