Una de las cosas más interesantes de Haskell es lo facil que resulta razonar sobre corrección de programas. Veamos un ejemplo simple; construiremos una función que tome 3 elementos ordenables y los devuelva como una triada ordenada (Ejercicio 2.40 de Razonando con Haskell):

ordena3:: Ord a => a -> a -> a -> (a, a, a )
ordena3 a b c 	| a <= b && b <= c = (a, b, c) 		-- Caso 1
	 	| a <= b = ordena3 a c b		-- Caso 2
		| b <= c = ordena3 b a c		-- Caso 3
		| otherwise = (c, b, a)			-- Caso 4

Las posibles permutaciones de un conjunto de 3 elementos distintos son obviamente 3! = 2 * 3 = 6. Sean 3 elementos ordenables distintos, a los que llamamos 1, 2, 3 tales que 1 < 2 < 3, veamos como trata el programa estas 6 permutaciones distintas:

ordena3 1 2 3	Caso 1 -> (1 ,2 ,3)
ordena3 1 3 2	Caso 2 -> ordena3 1 ,2 ,3; Caso 1 -> (1 ,2 ,3)
ordena3 2 1 3	Caso 3 -> ordena3 1 ,2 ,3; Caso 1 -> (1 ,2 ,3)
ordena3 2 3 1	Caso 2 -> ordena3 2 ,1 ,3; Caso 3 -> ordena3 1 ,2 ,3; Caso 1 -> (1 ,2 ,3)
ordena3 3 1 2	Caso 3 -> ordena3 1 ,3 ,2; Caso 2 -> ordena3 1 ,2 ,3; Caso 1 -> (1 ,2 ,3)
ordena3 3 2 1	Caso 4 -> (1 ,2 ,3)

Las condiciones exhaustuan todos los caso y el algoritmo termina siempre. ( No se consideran los casos en que existen elementos duplicados en la explicación ya que es trivial ver que por el uso de <= en las condiciones están contemplados en la definición de la función. )

Referencias

Razonando con Haskell;Blas C. Ruiz, Francisco Gutiérrez, Pablo Guerrero y José E. Gallardo;Thomson Editores Spain;2004