[Haskell-cafe] Theory about uncurried functions
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? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theory about uncurried functions
On Tue, 2009-03-03 at 10:43 +0100, 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? There's the kappa calculus and also the related Freyd categories which are related to arrows. Theres also the theory induced by cartesian categories or the theory induced by (symmetric) monoidal categories (which are strengthenings of Freyd categories). You could probably also formalize such a language yourself. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theory about uncurried functions
On Tue, Mar 3, 2009 at 2:43 AM, Peter Verswyvelen bugf...@gmail.com 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? Well, this is not quite an answer to your question, but the curried multiple arguments convention in Haskell is exactly that: a convention. For example, in ML, most functions which take multiple arguments take them in the form of a tuple. They could just as well be curried, but the culture prefers tuples. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theory about uncurried functions
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theory about uncurried functions
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 hab...@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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theory about uncurried functions
Not a better programmer, just a better human being. Peter Verswyvelen wrote: 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*? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theory about uncurried functions
On Tue, 3 Mar 2009, Peter Verswyvelen wrote: 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 don't think one can forbid currying. It's just a question, whether people use it commonly or not. But that was already said in this thread. Somehow related: http://haskell.org/haskellwiki/Composing_functions_with_multiple_values ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theory about uncurried functions
On Wed, 2009-03-04 at 01:35 +0100, Henning Thielemann wrote: On Tue, 3 Mar 2009, Peter Verswyvelen wrote: 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 don't think one can forbid currying. Sure you can, just work in a category with finite products (and possibly finite co-products) but not exponentials. Of course, then your language is first order --- and this doesn't do anything to stop partial application, which is still easy --- but it's quite possible. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
