Typový systém: Iterated union

Rust má poměrně slabý typový systém, nelze například napsat takovouto funkci:

fn readVectN<T>(n: usize) -> Vect<T, n> { ... }

Překladač ohlásí chybu „attempt to use a non-constant value in a constant“, což nedává, pokud se nad tím zamyslíme, smysl, neexistuje žádný důvod, proč by typové parametry musely být konstantami. V Julii není problém mít například toto:

function readvect()::(Vect{Int64, N} where N)
    print("Enter an integer: ")
    n = parse(UInt64, readline())
    Vect{Int64, n}(fill(1, n))
end

Zde je vidět, že typová proměnná nemusí být konstantou, stačí, když je takzvaně vázaná. To v Julii zajistí typ zvaný „iterated union“: Vect{Int64, N} where N, sdělující překladači, že proměnná N má v místě použití vždy konkrétní hodnotu, byť nemusí být známa v době překladu. Funkce tedy není závislostní, což znamená, že plnou typovou kontrolu lze provést staticky.

Podobná funkce v jazyce Idris vypadá takto:

total readStrVect : IO (Either String (n ** Vect n String))
readStrVect = do
    Right n <- readNat | Left err => pure $ Left err
    v <- readStrVectN n
    pure $ Right (n ** v)

Místo iterated union se proměnná váže pomocí tzv. sigma typu: (n ** Vect n String), kde n odpovídá proměnné vázané existenčním kvantifikátorem v logice.