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_indisce... [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