[Haskell-cafe] Proving correctness

Tillmann Rendel rendel at informatik.uni-marburg.de
Mon Feb 14 12:54:55 CET 2011

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.


More information about the Haskell-Cafe mailing list