Note to other potential contributors: Please don't hesitate to use abstract or mathematical notations to make your point. If I find your answer unclear, I will ask for elucidation, but otherwise feel free to express yourself in a comfortable fashion.
To be clear: I am not looking for a "safe" head
, nor is the choice of head
in particular exceptionally meaningful. The meat of the question follows the discussion of head
and head'
, which serve to provide context.
I've been hacking away with Haskell for a few months now (to the point that it has become my main language), but I am admittedly not well-informed about some of the more advanced concepts nor the details of the language's philosophy (though I am more than willing to learn). My question then is not so much a technical one (unless it is and I just don't realize it) as it is one of philosophy.
For this example, I am speaking of head
.
As I imagine you'll know,
Prelude> head []
*** Exception: Prelude.head: empty list
This follows from head :: [a] -> a
. Fair enough. Obviously one cannot return an element of (hand-wavingly) no type. But at the same time, it is simple (if not trivial) to define
head' :: [a] -> Maybe a
head' [] = Nothing
head' (x:xs) = Just x
I've seen some little discussion of this here in the comment section of certain statements. Notably, one Alex Stangl says
'There are good reasons not to make everything "safe" and to throw exceptions when preconditions are violated.'
I do not necessarily question this assertion, but I am curious as to what these "good reasons" are.
Additionally, a Paul Johnson says,
'For instance you could define "safeHead :: [a] -> Maybe a", but now instead of either handling an empty list or proving it can't happen, you have to handle "Nothing" or prove it can't happen.'
The tone that I read from that comment suggests that this is a notable increase in difficulty/complexity/something, but I am not sure that I grasp what he's putting out there.
One Steven Pruzina says (in 2011, no less),
"There's a deeper reason why e.g 'head' can't be crash-proof. To be polymorphic yet handle an empty list, 'head' must always return a variable of the type which is absent from any particular empty list. It would be Delphic if Haskell could do that...".
Is polymorphism lost by allowing empty list handling? If so, how so, and why? Are there particular cases which would make this obvious? This section amply answered by @Russell O'Connor. Any further thoughts are, of course, appreciated.
I'll edit this as clarity and suggestion dictates. Any thoughts, papers, etc., you can provide will be most appreciated.
The free theorem for
head
states thatApplying this theorem to
[]
implies thatThis theorem must hold for every
f
, so in particular it must hold forconst True
andconst False
. This impliesThus if
head
is properly polymorphic andhead []
were a total value, thenTrue
would equalFalse
.PS. I have some other comments about the background to your question to the effect of if you have a precondition that your list is non-empty then you should enforce it by using a non-empty list type in your function signature instead of using a list.
There are a number of different ways to think about this. So I am going to argue both for and against
head'
:Against
head'
:There is no need to have
head'
: Since lists are a concrete data type, everything that you can do withhead'
you can do by pattern matching.Furthermore, with
head'
you're just trading off one functor for another. At some point you want to get down to brass tacks and get some work done on the underlying list element.In defense of
head'
:But pattern matching obscures what's going on. In Haskell we are interested in calculating functions, which is better accomplished by writing them in point-free style using compositions and combinators.
Furthermore, thinking about the
[]
andMaybe
functors,head'
allows you to move back and forth between them (In particular theApplicative
instance of[]
withpure = replicate
.)It's only natural to expect the following to hold:
xs === head xs : tail xs
- a list is identical to its first element, followed by the rest. Seems logical, right?Now, let's count the number of conses (applications of
:
), disregarding the actual elements, when applying the purported 'law' to[]
:[]
should be identical tofoo : bar
, but the former has 0 conses, while the latter has (at least) one. Uh oh, something's not right here!Haskell's type system, for all its strengths, is not up to expressing the fact that you should only call
head
on a non-empty list (and that the 'law' is only valid for non-empty lists). Usinghead
shifts the burden of proof to the programmer, who should make sure it's not used on empty lists. I believe dependently typed languages like Agda can help here.Finally, a slightly more operational-philosophical description: how should
head ([] :: [a]) :: a
be implemented? Conjuring a value of typea
out of thin air is impossible (think of uninhabited types such asdata Falsum
), and would amount to proving anything (via the Curry-Howard isomorphism).If in your use case an empty list makes no sense at all, you can always opt to use
NonEmpty
instead, whereneHead
is safe to use. If you see it from that angle, it's not thehead
function that is unsafe, it's the whole list data-structure (again, for that use case).I think this is a matter of simplicity and beauty. Which is, of course, in the eye of the beholder.
If coming from a Lisp background, you may be aware that lists are built of cons cells, each cell having a data element and a pointer to next cell. The empty list is not a list per se, but a special symbol. And Haskell goes with this reasoning.
In my view, it is both cleaner, simpler to reason about, and more traditional, if empty list and list are two different things.
...I may add - if you are worried about head being unsafe - don't use it, use pattern matching instead:
Why does anyone use
head :: [a] -> a
instead of pattern matching? One of the reasons is because you know that the argument cannot be empty and do not want to write the code to handle the case where the argument is empty.Of course, your
head'
of type[a] -> Maybe a
is defined in the standard library asData.Maybe.listToMaybe
. But if you replace a use ofhead
withlistToMaybe
, you have to write the code to handle the empty case, which defeats this purpose of usinghead
.I am not saying that using
head
is a good style. It hides the fact that it can result in an exception, and in this sense it is not good. But it is sometimes convenient. The point is thathead
serves some purposes which cannot be served bylistToMaybe
.The last quotation in the question (about polymorphism) simply means that it is impossible to define a function of type
[a] -> a
which returns a value on the empty list (as Russell O'Connor explained in his answer).