Je Rust jazyk budoucnosti?

[Idris]

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

[Reklama]

[Idris]

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

[Králík]

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ě - refcounting všeho. V JS a Java výstupu pochopitelně implicitně jsou GC i silný runtime. Vtables tam (v C) nejsou a ani dispatch na základě typových tagů - tohle jsem předpokládal na základě tvého nepravdivého výroku, že typové parametry jsou vymazány a vůbec ve výsledném kódu nefigurují - pokud tam typový parametr může zůstat, není pro tyto mechanismy důvod (alespoň v tomto příkladu - neznám všechny zákoutí toho jazyka). Takhle stačí?

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

Od BoneFlute by ses měl učit především ty.

[Králík]

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 si samozřejmě nemyslim, předpokládám, že kompilace Haskellu zahrnuje minimálně jednu (spíš bych předpokládal více) intermediate reprezentací.

Move sémantika není záležitost typového systému

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, potřebuje vědět hned několik vlastností daného typu - kromě linerarity a [ne]kopírovatelnosti ještě jednu, která je IMO zajímavá, ve starších implementacích kvůli tomu musela být do některých typů přidávána datová položka - pokud budeš vědět, co to je, dostaneš také malé bezvýznamné plus

[Idris]

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

[Reklama]

[Idris]

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/

[Králík]

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

Ještě se k tomuhle zeptám, z jakési morbidní zvědavosti 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 a jakou ownership/borrowing vlastnost k nim má návratová hodnota?

[Martin Sivák]

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

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.

Pokud se budeme bavit o generických maticích, tak tu informaci o velikosti si to samozřejmě musí nést s sebou, pokud není známá v době překladu. VTable tam být nemusí, protože matice jsou specializovaný případ a stačí číslo. Maximálně, kdyby to bylo tak chytré, že pro některé operace nad specifickými velikostmi použije speciální extrémně optimalizovanou implementaci. Ale opět, v runtime jde o vstup od uživatele, takže tam musí být parser, error handling a nějaký dynamický dispatch.

Pokud by vstupem od uživatele byl samotný typ i s hodnotou (řekněme program "kompot", který správně odpeckuje, pomele, vyrobí etiketu podle počtu a typu vstupního ovoce), tak to interně samozřejmě dynamický dispatch mít bude. Jednoduše pro to, že každé to ovoce (Typ) se zpracovává jinak a náš abstraktní turingův stroj (CPU) neumí nic jiného než skoky dle adres, které si někde přečte.

Procesor s matematickou indukcí ještě nikdo nenapsal a z hlediska strojového kódu to nakonec vždy skončí procedurálně, takže výhoda a nevýhoda těchto jazyků je hlavně ve formální analýze během překladu. Ale ta se dá podpořit i jinak.


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 (= něco dle designu musí žít déle než něco jiného). Tuto informaci čistě z kódu neodvodíte, protože algoritmus co tam vývojář napíše, může být z hlediska požadavků typu špatně.

Lifetime pro dokázání správnosti nakládání s pamětí teoreticky nepotřebujete, pokud životnost hlídá jiný mechanizmus jako ref count nebo GC. Ale to má zase runtime implikace.

[Králík]

Runtime tam žádný není.

Promiň, ale tohle už je opravdu hodně absurdní. Tak se podívej do zdrojáku, máš tam i dokonce soubor runtime.c, ve kterém je definovaný, jak TEN RUNTIME volá kód (funkce trampoline()). Tou funkcí trampoline() začíná provádění celého programu. Dále memoryManagement.c, mathFunctions.c atd., které implementují funkcioinalitu toho interpreteru.

Viděl jsi ten kód vůbec někdy? Začínám mít pocit, že ne...

[Idris]

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

[Idris]

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.

[Králík]

...

Díky za hezkou sumarizaci.

Dodám jen pro úplnost, že vtables jsem postuloval předevšim za předpokladu, že 1) typový parametr je zcela vymazán a 2) abych pokryl veškeré obecné možnosti HTKs a GADTs, zejména v situaci, kdy hraje roli dynamický vstup, IMO jsou nejobecnější způsob, jak to ve spustitelném kódu reprezentovat, i když samozřejmě optimalizace pro konkrétní případy mohou existovat...

[Idris]

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.

[Idris]

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.

[Idris]

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