![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
sniffnoyI remember on Friday I started explaining lambda calculus to Youlian, and I remember that this was because I started telling him something about it but he didn't know anything about lambda calculus, but I don't remember what that thing was.
In any case, it's really something I hadn't thought much about in a few years. But this got me thinking about something I was wondering a few years back, when I was first learning about this stuff. Suppose we want to write a function that takes a variable number of arguments. Now of course we can easily write down a function that takes a list and then does stuff with the list. But that's not how we like to pass arguments in lambda calculus, is it? For a fixed number of arguments, I mean. So could we write a function that takes a variable number of arguments - passed (almost) in the normal lambda calculus way? The first argument would be a number, telling it how many arguments are to follow; and then come the actual arguments.
ADDENDUM later: (I guess now that I think about it later, the answer is, of course, "No shit that's computable!" But I guess I wasn't thinking so much in those terms.)
For simplicity, let's suppose our function is to take those n arguments and wrap them up into a list - because we all know how to use lists, so if we can do that, we can do anything, surely? (For convenience, we may want to instead use reverse-order lists.) So: Can we do that? Define a function list, such that list n x1 ... xn yields a list of x1 through xn?
When I thought about it a few years ago, I wasn't able to figure it out. I couldn't come up with one, and I certainly couldn't prove it impossible, but repeated failures were giving me the distinct idea it's impossible. But not just the failures, the reason for them.
Here's the thing: It looks to me like under any decent typing system - e.g. in Haskell or ML or something - this is impossible. Just look at it - what the hell would the type of this function "list" be? It just isn't sensible. (And practically speaking, it would be a pretty dumb function, too - why would you ever use it?) Perhaps Scheme could handle it, as Scheme doesn't have static typing (though of course curried functions aren't the norm in Scheme). Of course, with something weird like this, you probably want lazy evaluation, and Scheme certainly doesn't do that... maybe I should try it and see if it works; I think it might. Hm.
In any case, you've probably guessed from the paragraph above that yes, I have now, thinking about it again, found such a function. Because lambda calculus laughs at your silly typing systems. Actually, for convenience, I went with reverse lists instead of lists; but in any case I furthermore wrote down multi-arg-ify, where if f is a function that takes a reverse list, F=multi-argify f is the "multi-argument version" as described above (so reverse-list itself (i.e. the reverse-list builder, not the list "reverse" function) is just multi-argify of the identity), and unmulti-argify, which, well, you can guess.
So, yay, totally impractical functions exist. Now I should go see if these work in Scheme...
(Y is a fixpoint combinator, other function names should be obvious (pred is predecessor, nil means empty list, if is if-then-else in usual way). You can figure out for yourself how these actually work - their non-typability makes it look a bit weird, but it's certainly not at all hard. Note that each is defined in terms of a recursively-defined helper function.)
multi-argify=λf.Y(λg.λl.λn.if(iszero? n)(f l)(λx.g(cons x l)(pred n)))nil
unmulti-argify=λF.Y(λG.λn.λl.if(isnil? l)(F n)(G(succ n)(cdr l)(car l)))0
ADDENDUM after eating dinner: Yup, it works in Scheme. (Obviously, using direct recursion, not a fixpoint combinator, and using Scheme's built-in stuff, not Church representations. :P Also, I only tested reverse-list, as I was too lazy how to write in Scheme the rest. But if it works, surely the general principle does.)
-Harry
In any case, it's really something I hadn't thought much about in a few years. But this got me thinking about something I was wondering a few years back, when I was first learning about this stuff. Suppose we want to write a function that takes a variable number of arguments. Now of course we can easily write down a function that takes a list and then does stuff with the list. But that's not how we like to pass arguments in lambda calculus, is it? For a fixed number of arguments, I mean. So could we write a function that takes a variable number of arguments - passed (almost) in the normal lambda calculus way? The first argument would be a number, telling it how many arguments are to follow; and then come the actual arguments.
ADDENDUM later: (I guess now that I think about it later, the answer is, of course, "No shit that's computable!" But I guess I wasn't thinking so much in those terms.)
For simplicity, let's suppose our function is to take those n arguments and wrap them up into a list - because we all know how to use lists, so if we can do that, we can do anything, surely? (For convenience, we may want to instead use reverse-order lists.) So: Can we do that? Define a function list, such that list n x1 ... xn yields a list of x1 through xn?
When I thought about it a few years ago, I wasn't able to figure it out. I couldn't come up with one, and I certainly couldn't prove it impossible, but repeated failures were giving me the distinct idea it's impossible. But not just the failures, the reason for them.
Here's the thing: It looks to me like under any decent typing system - e.g. in Haskell or ML or something - this is impossible. Just look at it - what the hell would the type of this function "list" be? It just isn't sensible. (And practically speaking, it would be a pretty dumb function, too - why would you ever use it?) Perhaps Scheme could handle it, as Scheme doesn't have static typing (though of course curried functions aren't the norm in Scheme). Of course, with something weird like this, you probably want lazy evaluation, and Scheme certainly doesn't do that... maybe I should try it and see if it works; I think it might. Hm.
In any case, you've probably guessed from the paragraph above that yes, I have now, thinking about it again, found such a function. Because lambda calculus laughs at your silly typing systems. Actually, for convenience, I went with reverse lists instead of lists; but in any case I furthermore wrote down multi-arg-ify, where if f is a function that takes a reverse list, F=multi-argify f is the "multi-argument version" as described above (so reverse-list itself (i.e. the reverse-list builder, not the list "reverse" function) is just multi-argify of the identity), and unmulti-argify, which, well, you can guess.
So, yay, totally impractical functions exist. Now I should go see if these work in Scheme...
(Y is a fixpoint combinator, other function names should be obvious (pred is predecessor, nil means empty list, if is if-then-else in usual way). You can figure out for yourself how these actually work - their non-typability makes it look a bit weird, but it's certainly not at all hard. Note that each is defined in terms of a recursively-defined helper function.)
multi-argify=λf.Y(λg.λl.λn.if(iszero? n)(f l)(λx.g(cons x l)(pred n)))nil
unmulti-argify=λF.Y(λG.λn.λl.if(isnil? l)(F n)(G(succ n)(cdr l)(car l)))0
ADDENDUM after eating dinner: Yup, it works in Scheme. (Obviously, using direct recursion, not a fixpoint combinator, and using Scheme's built-in stuff, not Church representations. :P Also, I only tested reverse-list, as I was too lazy how to write in Scheme the rest. But if it works, surely the general principle does.)
-Harry
