> 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, yo

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