
On Tue, 18 Dec 2007, Benja Fallenstein wrote:
Hi Henning,
On Dec 18, 2007 5:17 PM, Henning Thielemann
wrote: The mathematical definition of "function" I know of, says that functions are special relations, and relations are sets of pairs. Their is nothing about intension.
That's the standard definition in set theory, but it's not the only mathematical definition of function. It also doesn't suffice for defining all Haskell functions-- consider
data T = T (T -> Int)
fn :: T -> Int fn _ = 7
We have (fn (T fn) == 7), so in the graph of 'fn' we must have a pair (T fn, 7). But if 'fn' is the same mathematical object as its graph, that would mean that the graph of 'fn' would have to contain a pair whose first element indirectly contains... the graph of fn!
This sort of circularity is not allowed in standard ZFC set theory, so if we're going to be precise, we will have to choose a different representation for functions than their graphs.
I see. I'm also wondering what 'total function' and 'partial function' might mean in Haskell, since values can be partially defined. Is Just undefined defined or undefined and is const (Just undefined) a total or a partial function?