Lambda the Ultimate

I thought STG stood for Spineless Tagless G-Machine...

Yes, you are correct. I always get those terms mixed up for some reason.

http://www.cs.chalmers.se/~boquist/phd/index.html

The ideas from Boquist's thesis inspired some of the choices in JHC.

http://research.microsoft.com/~simonpj/papers/papers.html#language

Most, if not all machines you describe are based on the idea that lambda terms can be compiled to combinator terms, and combinators define graph rewrite rules on the graph/term/program being evaluated, and all combinators therefore can be efficiently be represented as functions which rewrite part of the graph/term/program.

For that, most people in the 70s/80s looked at abstract machines with a calling stack for the combinators and a graph for the representation of the current state of the term.

TIM is the easiest, the G-machine, and the ABC machine are basically extensions on TIM to compile to very efficient programs.

The G-machine and ABC-machines are very good implementations of graph rewrite machines, and they are liked a lot because they allow peep-hole optimizations on the generated abstract machine code, but also can be very efficiently translated to native code.

1) Are there any other interesting machines out there?

Lots, but I wouldn't study all of them. I would start out with any of the closure evaluation machines, because these are the clearest. Of course you can then study CAM, ZINC, SECD, Krivine, whatever.

2) Where can I find some information on the ABC machine?

Hehe, you can buy the book. [not true any more, see Ronny's link below]. You will find that it's actually a lot like the SLPJ book, which you can download for free. I think they treat a lot of lambda-calculus better, and maybe type-theory better, but I am not too sure. It's been a long time since I read it.

3) Why do Haskell implementers love STG so much?

See the above post, it is a natural representation of an efficient abstract machine for graph rewriting. (Actually, I don't think they love it that much. It is a pretty clear representation. But the last 10 years or so I think they shifted a bit in attitude that compiling to an imperative machine might as well have been a good choice since the difference between a thunk/hypercombinator rewrite is not that different from a plain function call. [As exposed by the lisp/ML implementations]).

Actually, small secret if you wish, if you want to understand the basis of all these machines I think it suffices to understand the following 6 rules for evaluating a lambda term (in reverse polish notation).

Constants, variables, abstractions and applications:

c, x, \x. T, (T T)

The six rules define rewrites on a reduction machine in reverse polish notation. We push closures on the stack, a closure holds an environment, a lambda term being evaluated, and a local stack.

0. (cc, v, aa) ..                           => (cc, cc(v), aa) ..
1. (cc, (T0 T1), aa) ..                     => (cc, T1, []) (cc, T0 T1, aa) ..
2. (cc, (\x. T0), a aa) ..                  => (cc x:=a, T0, aa) ..
3. (cc0, (\x. T0), []) (cc1, T1 T2, aa1) .. => (cc1, T1, (cc0, (\x. T0), []) aa1) ..
4. (cc0, c, aa0) (cc1, T0 T1, aa1) ..       => (cc1, T0, (c aa0) aa1) ..
5. (cc1, (cc0, (\x. T0), aa0), aa1) ..      => (cc0, (\x. T0), aa0 aa1) ..

Rule 0, evaluate a variable (look it op in the environment). Rule 1, for an application push the argument. Rule 2, for an abstraction which has an argument, remember the argument in the environment. Rule 3, an abstraction which has no arguments any more is seen as a constant, so supply it to the application which pushed the evaluation. Rule 4, similar for a constant. Rule 5, if a continuation is being evaluated, evaluate that with the local context and the fresh arguments supplied.

These rules are for an eager language. You can see that they evaluate a program since (A) the term being evaluated is 'broken down', not replaced with fresh terms not occurring in the original term/program, and (B) only reduced terms occur on the stack (since only constants and closures are pushed), and environments only hold reduced values (since they only bind values from the stack). If you want lazy evaluation, you can just replace a few rules such that functions are pushed first, instead of their arguments.

All ZINC, CAM, Krivine, SECD machines are basically optimizations on these rules (don't copy the whole environment, don't copy all the arguments, keep the reduced terms in the heap instead of the stack, keep a pointer to the return statement, etc.)

(NOTE: I never really checked these rules, just wrote them down.)