Error and correct code

Question

I've come to heavily rely on haskell's type system to avoid bugs and was looking if it could also be used to ensure a (weak?) form of code correctness.

The form of code correctness I have in mind goes as follows:

A function f :: a -> b is correct if f is guaranteed to produce an output of type b for any input of type a. This clearly fails for the well known function head (head:: [a] -> a).

One way I am aware of that the type system fails to guarantee this form of correctness is when code uses error (error :: Char -> a). The error function pretty much overrides the entire type system so I would like to avoid the use of this function unless explicitly intended.

My question is two-fold:

1. What other functions (or haskell snippets) besides error are exceptions to Haskell's type system?

2. More importantly, is there a method to forbid the use of such functions within a Haskell module?

Many thanks!

Answer 1

You can write your own functions that never produce a value. Consider the following function:

never :: a -> b
never a = never a

It fails to terminate, so it is considered to be the value _|_ (pronounced bottom). All types in Haskell are actually the sum of the type and this special value.

You can also write a function that is only partially defined, like

undefinedForFalse :: Bool -> Bool
undefinedForFalse True = True

undefinedForFalse False is undefined, which is a special value that is semantically equivalent to _|_ except that the runtime system can stop execution, because it knows it will never finish.

error is also special function that's result is always semantically equivalent to _|_, it tells the runtime system that it can stop execution, knowing it will never finish, along with an informative error message.

Haskell is incapable of proving that a type can never take the value _|_ because it is always possible for a type to take the value _|_. Values that can never be _|_ are called "total". Functions which always produce a value other than _|_ in a finite period of time are called "total functions". Languages that can prove this are called "total languages" or "total functional programming languages". If they can prove this for all types in the language, they are necessarily Turing incomplete.

Answer 2

It isn't possible to prove that any arbitrary function will produce a value in a Turing complete language. You can for some specific functions though, of course. This was covered well by Cirdec, but I would like to point out a couple things with regard to using the type system to guarantee (some level) of correctness.

The relevant topic is parametricity: the fact that given a polymorphic type signature, there is often only a limited set of possible implementations (if we exclude error, undefined and other things like that).

One example of this would be (a -> b) -> a -> b. There's in fact only one possible implementation of this function.

Another example is that given an f from some type A to some type B and a function r :: [a] -> [a], it can be shown that r . map f = map f . r. This is called the "free theorem" for map. Many other polymorphic types also have free theorems.

A (sometimes more useful) result is that if you can prove that a function mapper :: (a -> b) -> F a -> F b obeys the law mapper id = id, it can be shown that mapper f . mapper g = mapper (f . g). Also, this would be the fmap implementation for the type F since those two laws are the Functor laws. This particular "fusion" law can be useful for optimization purposes.

Source: Theorems for free! http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf