Skip to content

Instantly share code, notes, and snippets.

@vjeux
Last active Apr 26, 2020
Embed
What would you like to do?

tldr of https://serokell.io/blog/2018/12/17/why-dependent-haskell

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

In 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.

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment