How does that work? If the length of the array is read from stdin for example, it would be impossible to know it at compile time. Presumably this is limited somehow?

If you check that the value is inside the range, and execute some different code if it's not, then congratulations, you now know at compile time that the number you will read from stdin is in the right range.

One option is dependent pairs, where one value of the pair (in this example) would be the length of the array and the other value is a type which depends on that same value (such as Vector n T instead of List T).

Type-Driven Development with Idris[1] is a great introduction for dependently typed languages and covers methods such as these if you're interested (and Edwin Brady is a great teacher).

[1] https://www.manning.com/books/type-driven-development-with-i...

Not sure about Idris, but in Lean `Fin n` is a struct that contains a value `i` and a proof that `i < n`. You can read in the value `n` from stdin and then you can do `if h : i < n` to have a compile-time proof `h` that you can use to construct a `Fin n` instance.

I've heard this can be a bit of a pain in practice, is that true? I can imagine it could slow me down to construct a proof of an invariant every time I call a function (if I understand correctly).

I haven't worked significantly with lean but I'm toying with my own dependently typed language. generally you only have to construct a proof once, much like a type or function, and then you reuse it. Also, depending on the language there are rewriting semantics ("elaboration") that let you do mathematical transformations to make two statements equivalent and then reuse the standardized proof.

If the length is read from outside the program it's an IO operation, not a static variable, but there are generally runtime checks in addition to the type system. Usually you solve this as in the article, with a constructor that checks it - so you'd have something like "Invalid option: length = 5 must be within 0-4" when you tried to create the Fin n from the passed in value

It doesn’t have to be a compile time constant. An alternative is to prove that when you are calling the function the index is always less than the size of the vector (a dynamic constraint). You may be able to assert this by having a separate function on the vector that returns a constrained value (eg. n < v.len()).

Imagine you read a value from stdin and parse it as:

Maybe Int

So your program splits into two branches:

1. Nothing branch: you failed to obtain an Int.

There is no integer to use as an index, so you can’t even attempt a safe lookup into something like Vect n a.

2. Just i branch: you do have an Int called i.

But an Int is not automatically a valid index for Vect n a, because vectors are indexed by Fin n (a proof carrying “bounded natural”).

So inside the Just i branch, you refine further:

3. Try to turn the runtime integer i into a value of type Fin n.

There are two typical shapes of this step:

* Checked conversion returning Maybe (Fin n)

If the integer is in range, you get Just (fin : Fin n). Otherwise Nothing.

Checked conversion returning evidence (proof) that it’s in range

For example: produce k : Nat plus a proof like k < n (or LTE (S k) n), and then you can construct Fin n from that evidence.

(But it’s the same basically, you end up with a “Maybe LTE…”

Now if you also have a vector: xs : Vect n a

… the n in Fin n and the n in Vect n a are the same n (that’s what “unifies” means here: the types line up), so you can do: index fin xs : a

And crucially:

there is no branch in which you can call index without having constructed the Fin n first, so out-of-bounds access is unrepresentable (it’s not “checked later”, it’s “cannot be expressed”).

And within _that_ branch of the program, you have a proof of Fin n.

Said differently: you don’t get “compile-time knowledge of i”; you get a compile-time guarantee that whatever value you ended up with satisfies a predicate.

Concretely: you run a runtime check i < n. _ONCE_

If it fails, you’re in a branch where you do not have Fin n.

If it succeeds, you construct fin : Fin n at runtime (it’s a value, you can’t get around that), but its type encodes the invariant “in bounds”/check was done somewhere in this branch.

I wish dependent types were more common :(

Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w

Which refers to https://docs.rs/anodized/latest/anodized/

Very cool and practical, but specs aren't dependent typing. (I actually think specs are probably more useful than dependent types for most people)

Dependent typing requires:

- Generic types that can take runtime values as parameters, e.g. [u8; user_input]

- Functions where the type of one parameter depends on the runtime value of another parameter, e.g. fn f(len: usize, data: [u8; len])

- Structs/tuples where the type of one field depends on the runtime value of another field, e.g. struct Vec { len: usize, data: [u8; self.len] }

Sadly I'm not sure Rust will ever get those sorts of features.

They've gone the Haskell route of adding a billion features to a non-dependent type system instead.

Not that I blame them, nobody has figured out practical dependent typing yet. (Idris is making good progress in the field though)