Standard Haskell: Ergonomics + Performance
He basically wants a language with a type system that lets you ensure that reading an element at an arbitrary position is safe and cannot crash because the index is always within the range of the array. He goes through all the mainstream languages and finds out that none would work.
Agda: Ergonomics + Correctness
He gives an example of a language that has this property, Agda. It's actually not a traditional language but a proof assistant. The way lookup is defined is the following way:
lookup : ∀ (xs : List A) → Fin (length xs) → A
function lookup<T>(array: Array<T>, index: LessThan<array.length>): T;
The novel thing that Agda gives is the ability to refer to an argument value (
array.length) in the type of another argument (
LessThan<array.length>). This is called dependent types.
Haskell Extended: Correctness + Performance
Look, Haskell is awesome and we can extend the type system in so many ways, here's how you can implement lookup in pure Haskell.
But, actually that implementation is not practical. We have to use a different implementation of Array so basically our code cannot work with any existing code, or you have to do a full copy every time you go between the two worlds, so the perf is horrible.
The Bright Future
Now he goes through everything that needs to change in Haskell to be able to introduce dependent types in a way that is actually practical. This is very specific to haskell and I don't follow everything, but if he convinces people that those changes should happen, then we'll be able to have dependent types in Haskell.