[Haskell-cafe] Theory about uncurried functions

[Peter Verswyvelen]

Thank you all for this information. It was very enlightening.

Too bad I don't know category theory, since I think it would give me a
better view on the different forms and essence of "computing".

Maybe this raises a new question: does understanding category theory
makes you a better *programmer*?

On Tue, Mar 3, 2009 at 8:45 PM, Hans Aberg <haberg at math.su.se> wrote:
> 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
>
>
>