[Haskell-cafe] head as a total function

oleg at pobox.com oleg at pobox.com
Thu Sep 7 02:28:00 EDT 2006

Jo'n Fairbairn wrote in response to Neil Mitchell:
> > And as you go on to say, if you apply it to the infinite
> > list, who cares if you used head. Head is only unsafe on
> > an empty list. So the problem then becomes can you detect
> > unsafe calls to head and let the programmer know.

> No, that's the wrong approach because it relies on detecting
> something that (a) the programmer probably knows already and
> (b) is undecidable in general. It would be far better for
> the programmer to express this knowledge in the
> programme.

It is indeed possible -- and quite easy -- to write programs where
head and tail are total functions. That issue was discussed, for
example, at the end of an old message:

	Exceptions in types and exception-free programming

The first two thirds of the message showed how to make exceptions
apparent in the signature of a function, so we can see if a function
could potentially raise the `head of an empty list' exception just by
looking at its (inferred) type.

The exception-free programming is far more rewarding, and practical as
well. We don't actually need to introduce subtyping; explicit
injection/projections don't seem to be as much of (syntactic)
overhead. There is absolutely no runtime overhead! The non-empty lists
have exactly the same run-time representation as the regular
lists. The technique generalizes to arrays, even numbers, sorted lists
(and, seemingly, to strings that are safe to include into HTML/SQL

That technique has been mentioned several times recently (perhaps not
on this forum). Quite complex algorithms like Knuth-Morris-Pratt
string search (with mutable arrays, packed strings, general recursion
and creative index expressions) can be handled. Again, without
introducing any runtime overhead:


The approach is formalizable; the recent PLPV talk by Chung-chieh Shan
presented the types systems and the proof techniques. Some of the
proofs have been formalized in Twelf:


In short, the safety property (absence of `head of an empty list'
exception) is a corollary to the Progress theorem, for a type system
with dependent-type flavor. The type system doesn't actually have
dependent types. Furthermore, whatever dependent-type flavor there
is, it can be erased while maintaining the safety guarantees, given
some precisely stated conditions on the safety kernel.

P.S. Algol68 was my favorite language too.

More information about the Haskell-Cafe mailing list