How can a language statically ensure a required index exists in a list?

Question

Suppose a language has a conventional list data structure that contains some dynamic number of values indexed sequentially. Some operations to access a value from the list require that a certain index exists, or that at least a certain number of values are included, and there will be an error at run time otherwise; a special case is needing just that the list be non-empty.

How can the language guarantee in advance that these operations will be safe, and reject any programs that would crash? What are the costs of adopting that solution?

---

To illustrate, a couple of examples of statically unsafe lists in different paradigms, firstly in Java:

List<String> l = new ArrayList<String>();
int i = 5;
l.get(i); // Throws IndexOutOfBoundsException at run time

then Haskell:

head [] -- *** Exception: Prelude.head: empty list

Both of the above are typechecked and compiled without issue, but will crash at run time; in real programs, these lists would be being provided as parameters, fields, etc, and the index could be a non-literal dynamic value. Ideally, these crashing programs would be rejected statically, while programs that only retrieve items that do exist would be allowed.

Answer 1

Dependent Types

A Dependent Type is one whose members can be described by a predicate depending on other values.
In your case, it is Index (xs: List a) = { i ∈ ℕ | i < |xs| }.
As you can deduce from the i ∈ ℕ clause, this is a strict subtype of ℕ.

Here's an example programme description using it:

List a = enum
    Cons: a -> List a -> List a
    Empty: List a

length: List a -> Natural
length l = f l 0 where
    f (Cons _ xs) n = f xs (n + 1)
    f Empty n = n

Index (xs: List a) = (i: Natural) when i < length xs

get: (xs: List a) -> Index xs -> a
get (Cons x _) 0 = x
get (Cons _ xs) n = get xs (n - 1)

main = do
    let xs = Cons "h" (Cons "42" Empty)
    putStrLn (get xs 0) //ok
    putStrLn (get xs 5) //Compiler Error

A question that arises then is that of get "knowing" it will never get Empty as input, at which point one will notice that length: List a -> ℕ has not a descriptive enough type.
Indeed: length's correct type is (Empty -> 0) & (Cons -> ℕ⁺), which explicitates the fact that Index Empty is not a type existing in the Universe.
(At which point one may notice how Cons/:: relates to NonEmpty a).
How smart a language and implementation has to be to automatically understand and report on those problems then is the realm of Automated Theorem Proving.

Naturally, when a value is not literal, one has to prove it indeed inhabits the type at hand.

let n: ℕ = userInput in
get xs n

is not a valid programme, for ℕ is a supertype of { i ∈ ℕ | i < |xs| }, meaning explicit type narrowing has to be involved:

let n: ℕ = userInput in
if n < |xs| then
    get xs n
else
    //deal with error

which should be reminiscent of C++'s dynamic_cast, and is already existing practice (you don't just use unsanitised user input as-is, do you?).
This also relates to the realm of Automatic Type Narrowing as featured in Kotlin, TypeScript, and, less automatic, Ceylon.

An other example is that of Min and Max: ∀(a: Comparable). MinMax (x: a, y: a) = { x, y }, which may be used to describe functions such as

MinMax = ∀a. Comparable a => (x: a) -> (y: a) -> (x | y)

max: MinMax
max x y = if x > y then x else y

min: MinMax
min x y = if x > y then y else x

where x and y are runtime values used as singleton types in a union type, where it is guaranteed that for each pair of x and y, min and max both will return precisely either that x or that y, and nothing else.
Naturally the result of min and max is a strict subset of a by virtue of { x ∈ a | f(x) } <: a.

Languages implementing those include, among others, Idris, Agda, Coq, F*, and ATS.

Answer 2

Let's get the easy solution out of the way first: you can just have these operations like get(int) and head() return an optional value, and then it's statically checked that you handle both cases where the element does or doesn't exist, the same way it's checked for an option type. Some notable languages which do this are Rust (get), OCaml (nth_opt) and F# (tryItem).

It's perhaps a bit cumbersome to force the user to handle an option every time they use a fundamental list operation; but in practice it's often not that big a deal, because most of the time you want to access the elements in a list, you do so through an iterator rather than the get method directly.

---

Other solutions could be based on theorem-proving; the goal is to statically prove that 0 ≤ i < n as a precondition for calling get(i), and reject the method call if this precondition can't be proved. There are different ways of going about this:

• You can include a sub-language in which the programmer can state and prove such propositions; normally, this is based on Hoare logic or a similar logic. This approach gives languages like F* or tools like KeY.
• You can have the compiler try to automatically prove them based on the conditions in branching statements; this would be something like control-flow type narrowing with dependent types. I don't know if any existing languages do this.

See also: What options are there for adding formal verification to a general purpose programming language?

Answer 3

A MimimumLengthList<int>/MaximumValueInteger<int> trait

I think this is basically the same as dependent types but maybe easier to understand

The operation a[5] requires a: MimimumLengthList<6>. There are a few ways to get a MimimumLengthList:

1. The list has a known size

list: a[6] = [1,2,3,4,5,6];
a[5]; // Ok

2. You assert the list is a mimimum length list:

fn f(a: MimimumLengthList<6>) { return a[5]; //ok }

3. An explicit check

let a = json_parse(input());
if (a.len() > 5)  {// this is a type assertion, special cased by the type checker
    return a[5];
}

Last case is similar to what languages that check bounds at runtime would do, but now you need to explicitly check and can choose other actions to perform in the false case besides just throwing an error.

Maximum Value Integer

You may sometimes want to do:

x: int = input();
if (x<5) {
    print([1,2,3,4,5][x]);
}

For this purpose, you can make a trait MaximumValueInteger which just represents an integer asserted to be less than a given value.

Combining the two

You could safely define a function like this:

fn get(a: MinimumLengthList<5>, b:MaximumValueInteger<4>){a[b]}
a([1,2,3,4,5,6,7,8], 2);

However, conditionals get a bit more complex:"

if (a < len(b)) {
    b[a]
}

In this case, it's hard for the type checker to actually assert what type a and b is since neither of them is known at compile time. Yet both are safe. You could implement this as a kind of generic only during the type checker phase, something like:

if (a < len(b))<T>: a:MaximumSizeInteger<T>, b:MimimumLengthList<T> {
     
}

I made up syntax for conditional type assertion here since I'm not aware of any languages that have it.