[Haskell-cafe] unapplying function definitions?

[Brent Yorgey]

On Sun, May 4, 2008 at 12:48 PM, PR Stanley <prstanley at ntlworld.com> 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.
>>
>>  What is the normal form?
>>>
>>
Essentially, a normal form is an expression where there are no more function
applications that can be evaluated.  For example, the expression '5' is a
normal form;  'succ 5' is not a normal form since the succ can be applied to
the 5, producing the normal form 6.

To give another example of what Hutton means, suppose we are given the
function definition

head (x:xs) = x

Then if we have the expression  'head (1:2:[])', noting that this matches
the left-hand side of the definition of head, we can apply that definition
to produce the equivalent expression '1'.  Given the expression '2', on the
other hand, and noting that this matches the *right*-hand side of the
definition of head, we can *unapply* the definition to produce the
equivalent expression 'head (2:[4,5,6])' (for example).  Applying a function
definition (moving from the left side of the definition to the right side)
brings us closer to a normal form, since there's one less function
application.  "Unapplying" a function definition (moving from the right side
to the left side) moves us further away from normal form since we have
introduced another function application.

Of course, you would never want an evaluator to "unapply" functions in this
way, but when reasoning about programs as humans, it can sometimes be useful
in proving things.

Does that help clear things up?
-Brent
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080504/0a5c7959/attachment.htm