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:
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ň :-)
473 Odpovědí
96517 Zhlédnutí