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:
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...
473 Odpovědí
95980 Zhlédnutí