tldr of https://serokell.io/blog/2018/12/17/why-dependent-haskell
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.
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) → AIn JavaScript it would look like
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.
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.
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.