[Haskell-cafe] Re: Haskell Weekly News: Issue 85 - September 13, 2008

[Benjamin L.Russell]

On Sat, 13 Sep 2008 21:06:21 -0700, "Daryoush Mehrtash"
<dmehrtash at gmail.com> wrote:

>I have a newbie question....  Does theorem proofs have a use for an
>application?  Take for example the IRC bot example (
>http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot)  listed below.  Is
>there any insight to be gained by theorem proofs (as in COQ) into the app?

Yes.

Basically, if you can prove that the program is correct, then you
don't need to test it.  While proofs can become very tedious for huge
programs with many different kinds of control flow involving very
complicated logic, if the program size can be shortened to a
reasonable size, then proofs can help shorten development time.

This was actually part of the motivation for developing Haskell as a
pure functional programming language (i.e., one that prohibits side
effects -- see
http://www.haskell.org/haskellwiki/Functional_programming).  It is
generally easier to write proofs for pure functional programming
languages than for impure ones.

Theorem provers help to automate the process of writing proofs for
programs.

Djinn (see http://lambda-the-ultimate.org/node/1178) is an example of
a theorem prover for Haskell.  Given a (Haskell function), it returns
a function of that type if one exists.  Here is a sample Djinn session
(courtesy of http://lambda-the-ultimate.org/node/1178):

>   calvin% djinn
>   Welcome to Djinn version 2005-12-11.
>   Type :h to get help.
># Djinn is interactive if not given any arguments.
># Let's see if it can find the identity function.
>   Djinn> f ? a->a
>   f :: a -> a
>   f x1 = x1
># Yes, that was easy.  Let's try some tuple munging.
>   Djinn> sel ? ((a,b),(c,d)) -> (b,c)
>   sel :: ((a, b), (c, d)) -> (b, c)
>   sel ((_, v5), (v6, _)) = (v5, v6)
>
># We can ask for the impossible, but then we get what we
># deserve.
>   Djinn> cast ? a->b
>   -- cast cannot be realized.
>
># OK, let's be bold and try some functions that are tricky to write:
># return, bind, and callCC in the continuation monad
>   Djinn> type C a = (a -> r) -> r
>   Djinn> returnC ? a -> C a
>   returnC :: a -> C a
>   returnC x1 x2 = x2 x1
>
>   Djinn> bindC ? C a -> (a -> C b) -> C b
>   bindC :: C a -> (a -> C b) -> C b
>   bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17))
>
>   Djinn> callCC ? ((a -> C b) -> C a) -> C a
>   callCC :: ((a -> C b) -> C a) -> C a
>   callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11)
># Well, poor Djinn has a sweaty brow after deducing the code
># for callCC so we had better quit.
>   Djinn> :q
>   Bye.

Other theorem provers include COQ (see http://coq.inria.fr/) and
Sparkle (see http://www.cs.ru.nl/Sparkle/) (a theorem prover for the
alternative non-strict, purely function programming language Clean
(see http://clean.cs.ru.nl/)).

-- Benjamin L. Russell