Odpověď na názor

To by mě zajímalo, jak se řeší indexy do pole, když je to pole plněné dynamicky a indexy mohou být vzaty v podstatě odkudkoli.

Funkce jsou schopny přijmout "důkazy" (vhodné typy). Například funkce pro indexování pole

fun{a:t@ype}
indexuj_pole
  {n:int}{i:nat | i < n} (A: arrayref(a, n), i: size_t i): (a)

má dva normální parametry v kulatých závorkách A (pole s prvky typu a o délce n) a i (index do pole, který má hodnotu typového parametru i).
Pak ale potřebuje dva typové parametry. První typový parametr n s velikostí pole. Druhý i s velikostí indexu a omezením jeho velikosti.

Konkrétní hodnoty n a i nemusí být známy v době kompilace. V době kompilace se jen ověří, že to jsou čísla, a že i má požadovaný rozsah.

Jinak vždy, když vidím nějaký podobný akademický superjazyk, který dává na zadek nějakému jazyku z praxe, říkám si, proč tedy všichni nepoužíváme ten superjazyk.

To je dobrá otázka. V tomhle by asi také šlo psát jádro.

Osobně si myslím, že je to jazyk z rodiny Standard ML, která není moc oblíbená. Ale nevím proč.