[Haskell-cafe] Proving correctness

[Tillmann Rendel]

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