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 http://www.haskell.org/pipermail/haskell/2004-June/014271.html 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 documents). 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: http://pobox.com/~oleg/ftp/Haskell/KMP-deptype.hs 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: http://pobox.com/~oleg/ftp/Computation/lightweight-dependent-typing.html#For... 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.