[Haskell-cafe] Proving correctness

[Pedro Vasconcelos]

On Sat, 12 Feb 2011 19:38:31 +0530
C K Kashyap <ckkashyap at gmail.com> wrote:

> Anyway, how can one go about explaining to an imperative programmer
> with no FP exposure - what aspect of Haskell makes it easy to
> refactor?


Like other people have said, the static type system is a major factor.
It's true that Haskell's type system is more advanced than most
imperative languages but it's also the often not mentioned that static
typing gives a stronger check in a functional language than an
imperative ones even in simple cases. 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)

Now the type checker will reject any implementation that fails to
return a pair of results in every case. Of course for a trivial example
like swap this is easy to ensure in any imperative language, but for
more complex programs it is actually quite common to forget some update
some component of the state.

BTW, I found this and other interesting reflections on the avantages of
FP vs. imperative in Martin Oderski's book "Programming in Scala".

Best regards,

Pedro Vasconcelos