3 ms·

One interesting aspect, at least for us old systems guys where runtime is important, is that you can not only move errors into compile time, you can move valida

One interesting aspect, at least for us old systems guys where runtime is important, is that you can not only move errors into compile time, you can move validation checks into compile time. Simple example: returning the head of a list is partial; normally, you have to have a check if the list is empty and return an error. With dependent types, you can guarantee that the list is not empty, moving that test to some higher level where it's actually meaningful. If you're manipulating arrays, you can guarantee at compile time that the indices have the right values, moving the tests outside of a function that gets called often. (In fact, when I was playing with ATS, this is what I did: I picked one boring validation test in the code at a time and moved it into the type. It vastly simplified the code.)

chriswarbo 4y ago
> Simple example: returning the head of a list is partial; normally, you have to have a check if the list is empty and return an error. With dependent types, you can guarantee that the list is not empty, moving that test to some higher level where it's actually meaningful. You don't need dependent types for that. In particular, non-empty lists are isomorphic to a tuple containing a value for the head and a list for the tail: type NonEmptyList<T> = Pair<T, List<T>> Note that this is just the type of cons ( https://en.wikipedia.org/wiki/Cons https://en.wikipedia.org/wiki/Cons ). We can use this to define List recursively (representing an empty list (AKA nil) as the single value of type Unit): type List<T> = Either<Unit, NonEmptyList<T>> If we inline the definition of NonEmptyList, we get the usual definition of List<T> = Either<Unit, Pair<T, List<T>>>