Is there a way to see the body of a lambda in Racket?

Question

Say I have this code:

#lang racket

(define a
  ((λ (x) x)
   ((λ (y) y)
    (λ (z)
      ((λ (w) w) z)))))

I know intuitively that this lambda expression is (extensionally) equal to (λ (z) z)

My question is if there is a way to print out the body of a in case I want to see how much the function got simplified internally by Racket.

---

More information:

By default, if I type a into the interpreter, I get #<procedure:y> (This seems to give a hint as to how much evaluation happened). I can change the output style to "constructor", say, and then the result is (lambda (a1) ...) which is closer to what I want, but I still don't know what's in the body which is the important part.

I imagine one could answer this with a more thorough knowledge of Racket's evaluation strategy, but I'm still interested if displaying procedure bodies is a thing that can happen in general.

Answer 1

In general there is no way to see body of a closure at runtime. The "body" is part of the source code. It gets compiled into bytecode (and later to machine code by the JIT). The closure consists at runtime of the captured values for the free variables in the body and a pointer to the code.

That said, you might be satisfied with studying the output of expand or compile.

Now expand only expands syntax, so you won't be able to see any optimizations yet:

> (expand-syntax #'(define a
                     ((λ (x) x)
                      ((λ (y) y)
                       (λ (z)
                         ((λ (w) w) z))))))
(define-values (a) 
   (#%app (lambda (x) x) 
            (#%app (lambda (y) y) 
                   (lambda (z) 
                     (#%app (lambda (w) w) z)))))

Note that #%app means "application".

To see the result after optimizations are applied we need to invoke the compiler. The builtin compile produces bytecodes, so we use compile-zo which converts the bytecode into structures representing bytecode (and they print nicely in the repl).

> (compile-zo '((λ (x) x)
                ((λ (y) y)
                 (λ (z)
                   ((λ (w) w) z)))))
'#s((compilation-top zo 0)
    1
    #s((prefix zo 0) 0 () ())
    #s((application expr 0 form 0 zo 0)
       #s((closure expr 0 form 0 zo 0)
          #s((lam expr 0 form 0 zo 0)
             ()
             (preserves-marks single-result)
             1
             (val)
             #f
             #()
             ()
             #f
             6
             #s((localref expr 0 form 0 zo 0) #f 0 #f #f #f))
          closure64862)
       (#s((closure expr 0 form 0 zo 0)
           #s((lam expr 0 form 0 zo 0)
              y
              (preserves-marks single-result)
              1
              (val)
              #f
              #()
              ()
              #f
              6
              #s((localref expr 0 form 0 zo 0) #f 0 #f #f #f))
           y64863))))

There is only one application left, so the program was indeed simplified during compilation.

See https://github.com/soegaard/meta/blob/master/runtime/racket-eval.rkt for a definition of compile-zo.

Finally yet another option is to look at the machine code produced by the JIT. See https://github.com/samth/disassemble

UPDATE

If I read the bytecode correctly, it corresponds to:

((λ (x) x)
 (λ (y) y))