
On 4 May 2008, at 17:33, PR Stanley wrote:
Hi What on earth is unapplying function definitions? The following is taken from chapter 13 of the Hutton book: "...when reasoning about programs, function definitions can be both applied from left to right and unapplied from right to left."
Well, because of referential transparency, we can say that the left hand side of a function is exactly equal to the right hand side. Thus, we can instead of applying functions, and making progress towards a normal form, unapply them and get further away from a normal form... for example: 5 = head [5,6,7,8,9] = head ([5,6] ++ [7] ++ [8,9]) = head (([] ++ [5] ++ [6]) ++ [7] ++ [8,9]) ....... There are of course an infinite number of ways of doing this, so it's usually only interesting, if we have some reason for applying a specific expansion. Bob