I'm learning a bit of lambda calculus and one of the things that I'm quite curious about is how the totally-abstract functions might actually be applied in instructions. Let's take the following example, where I'm allowing small natural numbers (as a given) and a TRUE FALSE definition.
For example, let's use the following code, which should evaluate to 5:
# using python for the example but anything would suffice
TRUE = lambda x: lambda y: x # T = λab.a
FALSE = lambda x: lambda y: y # F = λab.b
TRUE(5)(2) # T('5')('2')
How might this be implemented in a lambda-calculus-like instruction to evaluate this? One thing I thought of is to "un-lambda-ify" it, so it just comes out to something like:
// uncurried
int TRUE(int x, int y) {
return x;
}
int FALSE(int x, int y) {
return y;
}
TRUE(2, 5);
Which might come out to something along the lines of:
SYS_EXIT = 60
.globl _start
TRUE: # faking a C calling convention
mov %edi, %eax
ret
_start:
mov $5, %edi
mov $2, %esi
call TRUE
mov %eax, %edi
mov $SYS_EXIT, %eax
syscall
Is that how this is done, or what's a closer explanation of how a functional/lambda-like language might be compiled into instructions?
This question is really too big for Stack Overflow.
But one way of answering it is to say that if you can mechanically translate some variant of λ-calculus into some other language, then you can reduce the question of how you might compile λ-calculus to asking how do you turn that substrate language into machine language for some physical machine: how do you compile that substrate language, in other words. That should give an initial hint as to why this question is too big.
Fortunately λ-calculus is pretty simple, so the translation into a substrate language is also pretty easy to do, especially if you pick a substrate language which has first-class functions and macros: you can simply compile λ-calculus into a tiny subset of that language. Chances are that the substrate language will have operations on numbers, strings, and all sorts of other types of thing, but your compiler won't target any of those: it will just turn functions in the λ-calculus into functions in the underlying language, and then rely on that language to compile them. If the substrate language doesn't have first-class functions you'll have to work harder, so I'll pick one that does.
So here is a specific example of doing that. I have a toy language called 'oa' (or in fact 'oa/normal' which is an untyped, normal-order λ-calculus. It represents functions in a slight variant of the traditional Lisp representation: (λ x y) is λx.y. Function application is (x y).
oa then get gets turned into Scheme (actually Racket) roughly as follows.
First of all there are two operations it uses to turn normal-order semantics into Scheme's applicative-order semantics:
(hold x) delays the evaluation of x – it is just a version of Scheme's delay which exists so I could instrument it to find bugs. Like delay, hold is not a function: it's a macro. If there were no macros the translation process would have to produce into the expression into which hold expands.(release* x) will force the held object made by hold and will do so until the object it gets is not a held object. release* is equivalent to an iterated force which keeps forcing until the thing is no longer a promise. Unlike hold, release* is a function, but as with hold it could simply be expanded out into inline code if you wanted to make the output of the conversion larger and harder to read.So then here is how a couple of λ-calculus expressions get turned into Scheme expressions. Here I'll use λ to mean 'this is a oa/λ-calculus-world thing' and lambda to mean 'this is a Scheme world thing'.
(define true (λ x (λ y x)))
(define false (λ x (λ y y)))
turns into
(define true (lambda (x) (lambda (y) x)))
(define false (lambda (x) (lambda (y) y)))
(define cond (λ p (λ a (λ b ((p a) b)))))
turns into
(define cond (lambda (p)
(lambda (a)
(lambda (b)
(((release* p) a) b)))))
Note that it releases p at the point it is about to call whatever it wraps: since the only operation that ever happens in the language is function call that's the only place where promises ever need to be forced.
And now
(((cond p) a) b)
Turns into
(((cond
(hold p))
(hold a))
(hold b))
So here you can see that all the arguments get held in function calls, which gives you normal-order semantics.
The rules which turn oa into Scheme, really, are just two, one for each construct in oa.
(λ x y) -> (lambda (x) y)(x y) -> ((release* x) (hold y))So it's clear you can mechanically turn λ-calculus into another language. It helps if that other language has things like macros and first-order functions, but if you were willing to work hard enough you could turn it into anything else. One nice thing about the approach above of turning oa into Scheme is that oa functions are just Scheme functions in fancy dress (or, really, Scheme functions are oa functions in fancy dress, or perhaps they have swapped each other's clothes or something).
So then we've reduced the question to a simpler one: how do you compile Scheme?
Well, first of all that's a big question to ask: far too big for a Stack Overflow answer. There are a lot of Scheme compilers out there, and although they probably have common features they're by no means the same. And, because a lot of them are fairly hairy, actually looking at the code they produce is often not very informative (the disassembly of (λ x x) in oa seems to be 154 lines).
There are, however, at least two particularly interesting references for compiling Scheme.
The first (or almost the first) Scheme compiler was called 'Rabbit', and was written by Guy Steele. I don't know if Rabbit itself is still available, but Steele's thesis on it is, and there's a texty version of it here which looks superficially more readable but has problems.
The Scheme dialect Rabbit compiled is a fairly distant ancestor of modern Scheme: I think enough of it is described in the thesis to understand how it worked.
Rabbit compiled to MACLISP not machine language. So now there's another problem: how do you compile MACLISP? But in fact it compiled to an extremely restricted subset of MACLISP for which it's reasonably easy to see how it could be turned into machine code, I think.
The second interesting reference is the Wizard book: Structure and Interpretation of Computer Programs. Chapter 5 of SICP is about register machines and compilation for them. It defines a simple register machine and the implementation of a compiler for Scheme (or a subset of Scheme) for it. Figure 5.17, on pages 597 & 597 contains the compiled output of an obvious recursive factorial function for the register machine defined in the book.
Finally: that chapter of SICP is 120 pages long: that's why this is too big a question for Stack Overflow.
As an addendum, I fixed what I think is an idiocy in oa/normal which makes the compiled output much more tractable. Using the disassemble package for Racket (with some glue to attach it to the oa/normal/pure language, and using Racket/CS):
> (disassemble (λ x x))
0: 4883fd01 (cmp rbp #x1)
4: 7507 (jnz (+ rip #x7)) ; => d
6: 4c89c5 (mov rbp r8)
9: 41ff6500 (jmp (mem64+ r13 #x0))
d: e96ecc35f8 (jmp (+ rip #x-7ca3392)) ; #<code doargerr> ; <=
12: 0f1f8000000000 (data)
I think it's even possible to work out what this is doing: the first two instructions are checking for a single argument and punting to an error handler if not. The third instruction is (I presume) moving the argument into wherever it needs to be when the function returns (which I guess is rbp, and the argument presumably comes in r8), and then it jumps to wherever it needs to be next. Compare this to
> (disassemble (λ x 1))
0: 4883fd01 (cmp rbp #x1)
4: 750b (jnz (+ rip #xb)) ; => 11
6: 48c7c508000000 (mov rbp #x8)
d: 41ff6500 (jmp (mem64+ r13 #x0))
11: e96acc0cc7 (jmp (+ rip #x-38f33396)) ; #<code doargerr> ; <=
16: 0f1f8000000000 (data)
This is the same but the (mov rbp #x8) is moving the fixnum 1 into rbp I assume, which has been shifted in the usual way because I guess the system uses low tags.
Obviously things get rapidly more hairy from there.