Looking at Maybe/Option, it's clear that you can write a total function head' :: [a] -> Maybe a. This is good because it allows to represent the function's "fai

Looking at Maybe/Option, it's clear that you can write a total function head' :: [a] -> Maybe a. This is good because it allows to represent the function's "failure" to return a head element with an unambiguous, non-magic sentinel value. But really, in many cases you don't want to return "Maybe a" just because you did some operation that involved (somewhere in its middle) taking the head of a list. In some languages you would use "fromJust" or other fundamentally unsafe (in that they can lead the program to terminate abruptly if misused, and in that the compiler cannot help you use them properly) methods to present the interface you want. But ideally, you would have a head function that the compiler would only allow to be called on lists that can be proven non-empty, and which wouldn't need to wrap its return value in Maybe. In a "typical" typesystem, encoding useful information (like how many times you can call tail on a list) into types can be very difficult. For this particular application, you could try to keep track of how many elements are in a list by constructing lists with a generic function that wraps the type it's given in a Cons<T> wrapper, but this approach can run into issues relatively quickly, depending on the language you're using. That said, in some typesystems which aren't fully dependently-typed, you can manage tricks like this, and they can solve this use-case in those contexts. What full dependent types give you is the ability to have types depend arbitrarily on terms (values), such that lists whose types "know their length" are very simple to write, and much more complex guarantees about what your values get up to become possible to implement as types. The downside to this is that running the typechecking algorithm essentially requires arbitrary computation to be performed by the compiler; this can't always be guaranteed to terminate, and may take a few minutes even when it does.