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
---
Že Králík neví, co je interpretr 
Ale aspoň už zjistil, co jsou v Idrisu implicitní parametry.
Především jsem zjistil, že si strašně vymýšlíš. Také jsem zjistil, že Idris je jen jakési experimentální skriptovadlo - měl jsem dříve představu, že to je kompilovaný jazyk jako Haskell.
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". Asi by to chtělo mu dát vědět, že to má špatně, že uživatel Idris prohlásil, že borrowing/ownership nemá s typovým systémem vůbec nic společného...
473 Odpovědí
96511 Zhlédnutí