[Haskell-cafe] Proving correctness

[Pedro Vasconcelos]

On Mon, 14 Feb 2011 15:07:01 +0100
Gábor Lehel <illissius at gmail.com> wrote:

> I'm not completely sure, but I suspect another part of it (or maybe
> I'm just rephrasing what you said?) has to do with the fact that in
> Haskell, basically everything is an expression. 
> 

Yes, the fact that control statements (e.g. if-then-else) are
expressions makes type checking much more effective. However, I think
this is somewhat lost when programming imperative code in Haskell using
a state or I/O monad (because a monadic type such as "IO t" does not
discriminate what effects might take place, only the result type t).
Of course one can use a more specialized monad (such ST for
mutable references, etc.). I don't think that my imperative
programs are automatically made more correct by writing them as
monadic code in Haskell --- only that in Haskell I can opt for the
functional style most of the time.

BTW (slightly off topic) I found particularly annoying when
teaching Python to be forced to use an imperative style
(e.g. if-then-else are always statements). Scala is must better in this
regard (altought it is not purely functional language); a statement is
simply an expression whose return is unit.


Pedro