[Haskell-cafe] unapplying function definitions?

[Dan Weston]

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