Hi there. I've been doing some thinking lately (oh-no!) about function definitions. Specifically, I'm considering functions with multiple parameters.
Now, I'm familiar with "the usual" definition in which a function from set $S$ to set $T$ has the signature $f : S \to T$, and where $f$ itself is a set of tuples $(s,t)$ such that $s \in S$ and $t \in T$ and we have the property that for all elements $s$ of $S$, and elements $t_1$ and $t_2$ of set $T$, $\left((s,t_1) \in f\right) \wedge \left((s,t_2) \in f\right) \rightarrow t_1 = t_2$ (to distinguish functions from relations).
I've also seen this used in two ways with regards to $n$-ary functions: in curried and uncurried forms. In the uncurried form, we can write an $n$-ary function with the signature $f : A_1 \times A_2 \times \cdots \times A_n \to B$; that is, we simply define $f$ to have a domain which is a Cartesian product of sets. Thus, in this definition, we can still write the signature of $f$ in the form $f : S \to T$ by allowing $S = A_1 \times A_2 \times \cdots \times A_n$.
In the curried form, we instead define $n$-ary functions as higher-order function; specifically, functions which return other function. In this case, the signature of $f$ would be of the form $f : A_1 \to \left[A_2 \to \left[\cdots[A_n \to B\right]\right]$ (I am using the notation $[X\to Y]$ to denote the space of all functions from $X$ to $Y$). By this definition $f$ takes a single parameter from set $A_1$ and returns another function which accepts a single parameter from set $A_2$, and so on, until we finally produce function which accepts a single parameter from set $A_n$ and returns an element of $B$. But this definition could still be written in the form $f : S \to T$ by setting $S = A_1$, and setting $T = \left[A_2 \to \cdots \left[A_n \to B\right]\right]$.
Both the above definitions for $n$-ary functions still boil down to the definition of a unary function. When I see the form $f : A_1 \times \cdots \times A_n$, I still read $f$ as being a unary function, not as an n-ary function. The same goes for the curried form. In no way do I get the feeling of $f$ being an n-ary function.
While I see the appeal to having the simple, yet general definition, I can't help but feel like something is missing by restricting all functions to (in essence) being unary. So does anyone know about, or does anyone have their own ideas of how a "truly n-ary" function could be defined. By "truly n-ary", I specifically mean that the function's signature could not be boiled down to $f : S \to T$, but instead was actually a function with n separate "domains".
