Search code examples
schemeracketcontinuations

let vs define usage in continuations


I was trying to understand the call/cc execution in this example:

(let ((x (call/cc (lambda (k) k))))
    (x (lambda (ignore) "hi")))

which gives the value "hi".

The execution is described in the doc as:

Take the value, bind it to x, and apply the value of x to the value of (lambda (ignore) "hi").

I can understand that the continuation captured in let would be "Take the value, bind it to x" because that is what let does but NOT the "apply the value of x" part.

So I was expecting the output to be just binding x to (lambda (ignore) "hi") and not applying it.

For example, define works as expected:

(define x (call/cc (lambda (k) k)))
(x (lambda (ignore) "hi"))

It defines x as that value but doesn't apply it.

Can someone explain the difference between let and define in this case?

Probably an explanation of this would also help understand what is happening:

(let ((x (call/cc (lambda (k) k)))) (+ (x 1) 1))

I expected it to bind x to 1 and just evaluate to 2, but it says it expects a procedure.

EDIT: I believe that the work that remains to be done is actually bind x and evaluate the let expression also. In that case, it makes sense. Also, that means (let ((x (call/cc (lambda (k) k)))) (+ (x 1) 1)) can never be made to work.

EDIT: Indeed that is how it works. You can watch this video which explains this example. I think it can be informally summarized as "let" is more than "define" in the sense that it has to execute the expression as well.


Solution

  • TL; DR: The real difference between define and let is in top level program expressions because define can only be done once on a identifier and there are usually continuation prompts between top level statements.

    I'm going to use CPS in this answer. The definitions for common procedures I use are:

    ;; returns argument
    (define halt values) 
    
    ;; call/cc in CPS version
    (define (call/cc-k f k)
      (f (lambda (v k-ignore) (k v)) k))
    

    let and define in a procedure does similar things:

    (let ()
      (define x (call/cc (lambda (k) k)))
      (x (lambda (ignore) "hi")))
    

    ; ==

    (let ()
      (letrec ((x (call/cc (lambda (k) k)))
        (x (lambda (ignore) "hi")))
    

    And the same in just let becomes:

    (let ()
      (let ((x 'undefined))
        (set! x (call/cc (lambda (k) k)))
        (x (lambda (ignore) "hi"))))
    

    The same in CPS (though I have omitted the update of binding since shadowing does the same in this code:

    ((lambda (x k)
       (call/cc-k
        (lambda (k2 real-k) (real-k k2))
        (lambda (x)
          (x (lambda (ignore k2) (k2 "hi")) k))))
     'undefined halt)
    
    ;; ===
    
    ((lambda (x k)
       ((lambda (f5 k5) (f5 (lambda (v k-ignore) (k5 v)) k5))
        (lambda (k3 real-k) (real-k k3))
        (lambda (x)
          (x (lambda (ignore k2) (k2 "hi")) k))))
     'undefined halt)
    
    ;; ===
    
    ((lambda (x k)
       (define hi-k (lambda (x) (x (lambda (ignore k2) (k2 "hi")) k)))
       ((lambda (f5 k5) (f5 (lambda (v k-ignore) (k5 v)) k5))
        (lambda (k3 real-k) (real-k k3))
        hi-k))
     'undefined halt)
    
    
    ;; === this is starting to look like a combinator :-)
    
    ((lambda (x k)
       ((lambda (ignore k2) (k2 "hi"))
        (lambda (ignore k2) (k2 "hi")) k))
     'undefined halt)
    
    ;; ===
    
    ((lambda (x k)
       (k "hi"))
     'undefined halt)
    
    ;; ===
    
    (halt "hi")
    

    While your let version does this:

    (let ((x (call/cc (lambda (k) k))))
        (x (lambda (ignore) "hi")))
    
    
    ;;; === in terms of lambda instead of let
    
    ((lambda (x)
       (x (lambda (ignore) "hi")))
     (call/cc (lambda (k) k)))
    
    
    ;;; === in CPS
    
    (call/cc-k
     (lambda (k real-k) (real-k k))
     (lambda (x)
       (x (lambda (ignore k2) (k2 "hi")) halt)))
    
    ;;; ===
    
    (define hi-k (lambda (x) (x (lambda (ignore k2) (k2 "hi")) halt)))
    ((lambda (k real-k) (real-k k)) (lambda (v k-ignore) (hi-k v)) hi-k))
    
    
    ;;; ===
    
    ((lambda (ignore k2) (k2 "hi"))
     (lambda (ignore k2) (k2 "hi"))
     halt)
    
    ;;; ===
    
    (halt "hi")
    

    define used in top level is much different and since define cannot be done on the same variable twice your code in invalid Scheme code for top level evaluation. To mend that I imagine we rewrite it to:

    (define x #f)
    (set! x (call/cc (lambda (k) k)))
    (x (lambda (ignore) "hi"))
    

    I'll skip the define and write the CPS on the continuation:

    (call/cc-k
     (lambda (k real-k) (real-k k))
     (lambda (v)
       (set!-k x
               v
               (lambda (undefined)
                 (x (lambda (ignore k2) (k2 "hi")) halt)))))
    
    ;;; ===
    
    (define set-k (lambda (v)
                    (set!-k x
                            v
                            (lambda (undefined)
                              (x (lambda (ignore k2) (k2 "hi")) halt)))))
    (call/cc-k
     (lambda (k real-k) (real-k k))
     set-k)
    
    ;; ===
    
    (define set-k (lambda (v)
                    (set!-k x
                            v
                            (lambda (undefined)
                              (x (lambda (ignore k2) (k2 "hi")) halt)))))
    ((lambda (k real-k) (real-k k))
     (lambda (v k-ignore) (set-k v))
     set-k)
    
    
    ;; ===
    
    (define set-k (lambda (v)
                    (set!-k x
                            v
                            (lambda (undefined)
                              (x (lambda (ignore k2) (k2 "hi")) halt)))))
    (set-k (lambda (v k-ignore) (set-k v)))
    
    ;; ===
    
    (define set-k (lambda (v)
                    (set!-k x
                            v
                            (lambda (undefined)
                              (x (lambda (ignore k2) (k2 "hi")) halt)))))
    (set!-k x
            (lambda (v k-ignore) (set-k v))
            (lambda (undefined)
              (x (lambda (ignore k2) (k2 "hi")) halt)))
    
    ;; ===
    
    (set!-k x
            (lambda (v k-ignore) (set-k v))
            (lambda (undefined)
              ((lambda (v k-ignore) (set-k v)) (lambda (ignore k2) (k2 "hi")) halt)))
    
    ;; ===
    
    (set!-k x
            (lambda (v k-ignore) (set-k v))
            (lambda (undefined)
              (set!-k x
                      (lambda (ignore k2) (k2 "hi"))
                      (lambda (undefined)
                        (x (lambda (ignore k2) (k2 "hi")) halt)))))
    
    ;;; ===
    
    (set!-k x
            (lambda (v k-ignore) (set-k v))
            (lambda (undefined)
              (set!-k x
                      (lambda (ignore k2) (k2 "hi"))
                      (lambda (undefined)
                        ((lambda (ignore k2) (k2 "hi")) (lambda (ignore k2) (k2 "hi")) halt)))))
    
    
    ;;; ===
    
    (set!-k x
            (lambda (v k-ignore) (set-k v))
            (lambda (undefined)
              (set!-k x
                      (lambda (ignore k2) (k2 "hi"))
                      (lambda (undefined)
                        (halt "hi")))))
    
    ;;; ===
    
    (halt "hi")
    

    This is strange however since if you try this you might not get anything at all. The reason for this is that top level expressions are separated by continuation prompts. Thus the continuation caught by call/cc for every top level statement is halt instead of the rest of the program. Lets try that:

    (call/cc-k
     (lambda (k real-k) (real-k k)) 
     (lambda (v)
       (set!-k x
               v
               halt)))
    
    (x (lambda (ignore k2) (k2 "hi")) halt)
    
    ;; ===
    
    (define set-k
      (lambda (v)
       (set!-k x
               v
               halt)))
    ((lambda (k real-k) (real-k k)) (lambda (v k-ignore) (set-k v)) set-k)
    (x (lambda (ignore k2) (k2 "hi")) halt)
    
    ;; ===
    
    (set-k (lambda (v k-ignore) (set-k v)))
    (x (lambda (ignore k2) (k2 "hi")) halt)
    
    ;; ===
    
    ((lambda (v)
       (set!-k x
               v
               halt))
     (lambda (v k-ignore) (set-k v)))
    (x (lambda (ignore k2) (k2 "hi")) halt)
    
    ;; ===
    
    (set!-k x (lambda (v k-ignore) (set-k v)) halt)
    (x (lambda (ignore k2) (k2 "hi")) halt)
    
    ;; ===
    
    (set!-k x (lambda (v k-ignore) (set-k v)) halt)
    ((lambda (v k-ignore) (set-k v))
     (lambda (ignore k2) (k2 "hi"))
     halt)
    
    ;; ===
    
    (set!-k x (lambda (v k-ignore) (set-k v)) halt)
    (set-k (lambda (ignore k2) (k2 "hi")))
    
    ;; ===
    
    (set!-k x (lambda (v k-ignore) (set-k v)) halt)
    ((lambda (v)
       (set!-k x
               v
               halt))
     (lambda (ignore k2) (k2 "hi")))
    
    ;; ===
    
    (set!-k x (lambda (v k-ignore) (set-k v)) halt)
    (set!-k x (lambda (ignore k2) (k2 "hi")) halt)
    

    Because of the continuation prompts the full continuation is not executed and the only thing the code really does is set x twice.

    Your last example doesn't work because x switched between being a continuation and a number.

    (let ((x (call/cc (lambda (k) k))))
      (+ (x 1) 1))
    
    ;; in CPS
    
    (call/cc-k
     (lambda (k real-k) (realk k))
     (lambda (x)
       (x 1 (lambda (v1)
              (+-k v1 1 halt)))))
    
    ;; ===
    
    (define k (lambda (x)
                (x 1 (lambda (v1)
                       (+-k v1 1 halt)))))
    ((lambda (k real-k) (realk k))
     (lambda (v k-ignore) (k v))
     k)
    
    
    ;; ===
    
    (define k (lambda (x)
                (x 1 (lambda (v1)
                       (+-k v1 1 halt)))))
    (k (lambda (v k-ignore) (k v)))
    
    ;; ===
    
    ((lambda (x)
       (x 1 (lambda (v1)
              (+-k v1 1 halt))))
     (lambda (v k-ignore) (k v)))
    
    
    ;; ===
    
    ((lambda (v k-ignore) (k v))
     1
     (lambda (v1)
       (+-k v1 1 halt)))
    
    ;; ===
    
    (k 1)
    
    ;; ===
    
    ((lambda (x)
                (x 1 (lambda (v1)
                       (+-k v1 1 halt))))
     1)
    
    
    ;; ===
    (1 1 (lambda (v1) (+-k v1 1 halt)))
    
    ERROR: 1 is not a procedure!
    

    YMMV and thus all this might be noise, but the second you get that call/cc is just peeking at the CPS version of the code without having to write CPS understanding how it works is quite easy. Happy hacking!