Haskell: The Craft of Functional Programming
	Simon Thompson
	(c) Addison-Wesley, 1999.

	Chapter 8


Reasoning about programs
^^^^^^^^^^^^^^^^^^^^^^^^

>	module Chapter8 where

>	import Prelude hiding (sum,length,(++),reverse,unzip)


Testing and verification
^^^^^^^^^^^^^^^^^^^^^^^^
A function supposed to give the maximum of three (integer) values.

>	mysteryMax :: Int -> Int -> Int -> Int
>	mysteryMax x y z
>	  | x > y && x > z      = x
>	  | y > x && y > z      = y
>	  | otherwise           = z

Definedness and termination
^^^^^^^^^^^^^^^^^^^^^^^^^^^

A factorial function, giving an undefined result on negative integers.

>	fact :: Int -> Int
>	fact n
>	  | n==0        = 1
>	  | otherwise   = n * fact (n-1)

An infinite list

>	posInts :: [Int]
>	posInts = [1, 2 .. ]


Induction
^^^^^^^^^

The sum function, defined recursively.

>	sum :: [Int] -> Int

>	sum []     = 0					-- (sum.1)
>	sum (x:xs) = x + sum xs				-- (sum.2)

Double every element of an integer list.

>	doubleAll :: [Int] -> [Int]

>	doubleAll []     = []				-- (doubleAll.1)
>	doubleAll (z:zs) = 2*z : doubleAll zs		-- (doubleAll.2)

The property linking the two:
	sum (doubleAll xs) = 2 * sum xs			-- (sum+dblAll)


Other functions used in the examples
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

The definitions given here use explicit recursion, rather than applying 
higher-order functions as may happen in the Prelude definitions.

>	length :: [a] -> Int

>	length []     = 0				-- (length.1)
>	length (z:zs) = 1 + length zs			-- (length.2)
 
>	(++) :: [a] -> [a] -> [a]

>	[]     ++ zs = zs				-- (++.1)
>	(w:ws) ++ zs = w:(ws++zs)			-- (++.2)

>	reverse :: [a] -> [a]

>	reverse []     = []				-- (reverse.1)
>	reverse (z:zs) = reverse zs ++ [z]		-- (reverse.2)

>	unzip :: [(a,b)] -> ([a],[b])

>	unzip [] = ([],[])
>	unzip ((x,y):ps) 
>	  = (x:xs,y:ys)
>	    where
>	    (xs,ys) = unzip ps                   


Generalizing the proof goal
^^^^^^^^^^^^^^^^^^^^^^^^^^^

The shunting function

>	shunt :: [a] -> [a] -> [a]

>	shunt []     ys = ys				-- (shunt.1)
>	shunt (x:xs) ys = shunt xs (x:ys) 		-- (shunt.2)

>	rev :: [a] -> [a]

>	rev xs = shunt xs []				-- (rev.1)

An alternative definition of the factorial function.

>	fac2 :: Int -> Int

>	fac2 n = facAux n 1

>	facAux :: Int -> Int -> Int

>	facAux 0 p = p
>	facAux n p = facAux (n-1) (n*p)