let vs define usage in continuations

Question

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.

Answer 1

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!

Answer 2

(let ((x (call/cc (lambda (k) k))))    ; binds x to the value of (call/cc ...)
    (x (lambda (ignore) "hi")))        ; applies x to the value of (lambda ...)

translates as

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

which becomes

(let ((x #f))
  (set! x (lambda (ignore) "hi"))
  (x (lambda (ignore) "hi")))

and the code with define translates the same (for the purposes of interpreting this code snippet; with internal, non top-level defines only).

Both let and define evaluate the expression to find out the value for the variable's binding -- which is what you asked about, as if they are somehow different in that respect. They aren't.

Your third snippet translates as

(let ((x #f))
  (set! x (call/cc (lambda (k) k)))
  (+ (x 1) 1))

which becomes

(let ((x #f))
  (set! x 1)
  (+ (x 1) 1))

which becomes

(let ((x #f))
  (+ (1 1) 1))

Answer 3

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

call/cc takes one argument, a function that takes one argument, and calls that function. The argument passed to it (The continuation) is itself a function of one argument, that, when called, makes call/cc return its argument. If that function is never called, call/cc returns whatever value its argument returns. So...

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

At this point, x holds a continuation that, when invoked with a value, makes call/cc return that value. Even if call/cc has already exited, calling that continuation makes it jump to that point again.

(x (lambda (ignore) "hi")))

And now that continuation is called, with a lambda (call it A) that takes one argument and returns "hi". So it jumps back up to

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

and x is now bound to that lambda A since calling the continuation acts like call/cc just returned it.

(x (lambda (ignore) "hi")))

and now x, which is A, is invoked, ignores its argument, and returns "hi". The example using define works the same way: x gets bound to one value, and then when that value is called, x gets bound to a new value, and called with that new value.