Editing Error vs. Exception (section)

== Errors and type system ==

It is generally considered, that errors in a program imply a lack in the type system. If the type system would be strong enough and the programmers would be patient enough to work out the proofs imposed by library functions, then there would be no errors in programs at all, only exceptions.

An alternative to extending the type system to [[dependent type]] system that allows for a wide range of proofs
is the [[Extended Static Checking]].
For example:
<haskell>
{-# CONTRACT head :: { xs | not (null xs) } -> Ok #-}
head :: [a] -> a
head []    = error "head: empty list"
head (x:_) = x
</haskell>

When there is a pre-condition (or a contract) like here, it is a programming error to give an empty list to <hask>head</hask>. This means that checking if the list is empty must be done before the call. It has to statically deductible from the call site.

If you write a function and cannot prove that you will not call head on the empty list then either you check before calling, or you use a safe-head function like <hask>viewL :: [a] -> Maybe (a, [a])</hask> or a <hask>case xs of x:_ -> doSomethingWithHead a; [] -> doSomethingElse</hask> or you add a pre-condition to your function.

These contracts somehow look like the exception declarations, but they specify something about preconditions, not about possible results. There would be no sense to give the contracts names in order to handle different ways of violating the contracts after the function has been called with inappropriate arguments.