[Haskell-cafe] head as a total function

[oleg at pobox.com]

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

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.