Re: [Haskell-cafe] Proving correctness

Pedro Vasconcelos wrote:

This is because all input and output data flow is type checked in a function application, whereas imperative side effects might escape checking.

For example, the type signature for a variable swapping procedure in C:

void swap(int *a, int *b)

This will still type check even if it modified only one of the argument references. However, if written functionally, it must return a pair:

swap :: (Int,Int) -> (Int,Int)

This benefit of explicit input and output values can interact nicely with parametric polymorphism: swap :: (a, b) -> (b, a) This more general type signature makes sure we are not just returning the input values unswapped. Tillmann