[Haskell-cafe] Theory about uncurried functions

[Hans Aberg]

On 3 Mar 2009, at 10:43, Peter Verswyvelen wrote:

> Lambda calculus is a nice theory in which every function always has
> one input and one output. Functions with multiple arguments can be
> simulated because functions are first class and hence a function can
> "return" a function. Multiple outputs cannot be done, one must embed
> these outputs in some data type, e.g. using a tuple, or one must use
> continuation passing style.
>
> Now, does a similar theory exist of functions that always have one
> input and one output, but these inputs and outputs are *always*
> tuples? Or maybe this does not make any sense?

I think most of the replies have already described it, but the  
Church's lambda-calculus is just a minimal theory describing a way to  
construct functions, which turns out to be quite general, including  
all algorithms. The first lambda-calculus he describes in his book  
does not even include the constant functions - for some reason it is  
convenient.

So if you want to have more, just add it. That is why functional  
computer languages like Haskell can exist.

As for currying, it builds on the fact that in the category of sets  
(but others may not have it) one has a natural equivalence (arguments  
can also be functions)
       psi: Hom(A x B, C) --> Hom(A, Hom(B, C))
                  f       |-> (a |-> (b |-> f(a, b)))
     ((a, b) |-> g(a)(b)) <-|      g
So it simply means that set-theoretic products can be rewritten into  
iterated functions. (Strictly speaking, currying involves a choice of  
natural equivalence psi.)

In axiomatic set theory, it is common to construct tuplets (i.e., set- 
theoretic products) so that (x) = x, (x_1, ..., x_n) = ((x_1, ...,  
x_(n-1), x_n), and one might set () to the empty set (so that, for  
example, the real R^0 has only one point). The recursive formula has  
slipped into functional languages. Pure math, unless there are special  
requirements, uses naive set theory in which that recursion formula  
would not be used: in computer lingo, it corresponds to the  
implementation (axiomatic set theory), and is not part of the  
interface (naive set theory).

By contrast, in lists, [x] is not the same as x. (If S is a set, the  
set of lists with elements from S is the free monoid on S.)

But you might view f() as passing the object () to f, f(x) passes x to  
f, and f(x_1, ..., x_n) passes (x_1, ..., x_n) to f.

So the only addition needed is to add the objects (x_1, ..., x_n), n =  
0, 1, 2, ..., to your language. You can still curry the functions if  
you like to - a convention, just as already noted.

   Hans Aberg