Dan Weston westondan at imageworks.com
Mon May 5 15:28:52 EDT 2008

```Hi Paul!

I'm not sure about the context of Hutton, but maybe "unapplying
functions" refers to the principle of extensionality.

Leibnitz' rule of the "indiscernibility of identicals" [1] says that if
two functions are equal, then the respective results of applying each to
*any* value of their common domain are equal:

f, g :: a -> b and f = g  ==>  forall (x :: a) . f x = g x

Since Haskell contains the undefined value in every type, this applies
as well to undefined: f x and g x must either both be undefined or equal.

We can keep going from left to right, so that for any validly typed y, f
x y = g x y, f x y z = g x y z, etc.

The converse of this is also true, and called the principle of
extensionality:

Two functions can be considered equal if they have a common domain
(type) and if, for each value in that domain (type), which in Haskell
includes undefined, they give the same result.

So if we have two functions f and g, and we know [2] that for *every* z
(i.e. z is a free variable or a universally quantified variable) that

f x y z = g x y z   ==>   f x y = g x y

We can keep going from right to left: if in addition, this is true for
all y, then f x = g x. And finally, if this is true for all x, then f = g.

Note that Leibnitz allows for "any" argument, extensionality requires
equality for "every" argument.

Dan Weston

[1]
http://en.wikipedia.org/wiki/Identity_of_indiscernibles#Identity_and_indiscernibility

[2] We know this because e.g. there is some definition or theorem saying
so. We cannot compute this (even for finite domains) by trying each
value. They need to give the same result even for undefined arguments,
so that you cannot give a computable extensional definition of function
equality even for finite domains, since if one function doesn't halt
when applied to 3, the other must also not halt, and you can't wait for
ever to be sure this is true.

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."
>
> Cheers
> Paul

```