The problem with Int -> Int -> Int is that it doesn't explain how the two arguments ever get summed into one result, using only 1-adic calls. It simply presupposes some internal magic of the final function. The computation of addition requires, at minimum, an operation upon two values at once.

@Steve Hmm, I don't think I understand. You can implement natural numbers (as Church numerals) and addition using only the lambda calculus, which only has single argument functions. You can implement any computable function like that, in fact. There's no magic there. There are no secret "multi-argument functions" hidden anywhere.

@DavidYoung, I'm from a computing background rather than a mathematical one, but my understanding of Church numerals is that it relies on repeated application. The problem is that you can't express iterative application in terms of pure, 1-adic functions.

@Steve I also come from a computing background. Can you explain what you mean in more detail, maybe with an example? I don't quite understand your comment. I can promise you that lambda calculus does not have multi-argument functions, other than through currying. I can also promise you that every computable function can be written in it.

Lambda calculus is just a very simple programming language that only consists of anonymous functions (with one argument) and function application. And nothing else.

The lambda-calculus form operates on two values at once by just using two variables in the same scope. You can even avoid the need for that—if you use SK combinators, then the “closures” become explicit, and are just those terms where no evaluation rule applies yet. But in the end, I think people are just going to differ in terms of when an equivalence constitutes a satisfying explanation for them.

@JonPurdy, how do you operate on two variables in one scope, if you don't have dyadic operators? You're putting the cart before the horse. There must be dyadic operators.

@Steve There is a binary operator in lambda calculus, namely function application. You could argue that it's a two-argument function. With equal justification you could argue that $f(x)$ in standard mathematics is an application of a two-argument function. You could also argue that every mathematical function takes only one argument: an element of its domain. I think this philosophical issue is unrelated to the lambda calculus, and is largely just a matter of definition.

@benrg, as I say I'm no expert on the lambda calculus. An "element of its domain" could, I presume, be a tuple? If so, we are back to admitting the dyadic addition operator, just in the alternate but equivalent guise of a 1-adic operator taking a 2-tuple.

Maybe you can remove the Haskell code and replace it with words? Haskell helps only people who speak Haskell. For most of the other it is as useful as an answer in Latin.

@Steve What if instead of taking a 2-tuple I take an integer, representing two integers using the cantor pairing function? At some point the distinction between "one argument" and "two arguments encoded in some way" breaks down.

@Steve The untyped lambda calculus, which is what everyone is talking about in this discussion, has no notion of tuples. It is very literally only anonymous functions, function application and variables (but the only thing you can do with a variable is apply it to an argument, apply a function to it or give it back as a result). Is there another way I can describe the language that would help? I could give a BNF grammar if that helps. Or I could give a simple implementation of the lambda calculus. There are web-based REPLs that can demonstrate these things (implementing pairs as fns, etc).

@RydwolfPrograms, I did consider such a strategy - it's common enough in computing to pack a low word and high word into a double-word, for example. But obviously the packing type has to have enough space for its members - you can't pack two arbitrary ints into a single int. The general problem to which you allude is that there can be conceptual data structures in the mind of the programmer, which have no explicit representation and whose only mark of existence is in patterns of access and manipulation.

@DavidYoung, it's interesting to see the disagreement between yourself saying there are no tuples, others who thought it strange that the OP didn't consider the possibility of tuples, and mine and RydwolfPrograms's comment immediately above discussing whether scalars can even be distinguished from tuples systematically! There's clearly a can of worms here, and I think attempting to analyse the conceptual clashes would exceed the space and facilities available here.

@Steve Regarding your first sentence: I am making the very specific claim that there is no builtin tuple data type (or structs, records, classes, etc) in the untyped lambda calculus and that you can build something that behaves like a tuple with a Church encoding using only functions. Both of those two parts are important to what I'm saying. I mostly agree with your last sentence, unfortunately. I think this could be clarified by having a discussion about the lambda calculus, where we interactively evaluate some expressions. But the comment format here does not work well for that.

@Steve "The problem is that it doesn't explain how the two arguments ever get summed into one result. It simply presupposes some internal magic of the final function." - how is that any different between languages with unary and binary functions? We always presuppose some internal magic if the language provides addition. The beautiful thing about languages is that you can define them to provide whatever you want, ignoring how that is going to be implemented in a concrete compiler or interpreter.

@Bergi, basic arithmetic is not magic, insofar as I can do it on paper or in my head. And the CPU implements the add instruction just as it would be done on paper - one instruction operating upon two registers. What you call a beautiful thing - defining languages with no thought to implementation - I call a grotesque thing.

@Steve it's magic insofar as not being defined via some other element of the language. The language provides a data type for numbers, and it provides an addition operation, with defined semantics (in this case by the rules of basic arithmetic). And no, I can define this language however I want, ignoring how one would implement it with C or Python or Assembly to run on a physical computer, as long as I give it enough thought so that I can evaluate expressions on paper or in my head. Which is certainly possible for languages with closures.