Quote:

Bill Turkel writes:

I am trying to understand the process of currying. So far I have

[...deleted...]

Currying is useful in the Lambda calculus because it allows any

function with multiple arguments to be represented entirely

in terms of functions with 1 argument each - all theories and

so forth need only be proved for functions with one argument

[ ... deleted...]

Have I missed anything major, or misunderstood anything?

Actually it is tupling that lets one treat multiple arguments as

a single argument, currying unbundles. As I'd said in a posting

some months ago, currying in the lambda calculi (at least in the

typed lambda calculi, which are quintessential typed functional

languages) has a deep meaning --- the equivalence between the

formulas

A_1 /\ ... /\ A_n => B and A_1 => ... => A_n => B

[with /\ binding tighter than => and => associating right, as usual].

The formulas-as-types, terms-as-proofs correspondence with

Intuitionistic logic, as elucidated by Curry, Howard, DeBruijn et al,

lets us read /\ as * and => as ->.

---

European Computer Industry Research Centre Off: +49 89 92 69 91 58

Arabellastrasse 17 Fax: +49 89 92 69 91 70

8000 Muenchen 81, Germany Res: +49 89 16 33 59