CSE271: Principles of Programming Languages

Continuation

Jooyong Yi (UNIST)

Spec and Impl of Conditionals

       (value-of 𝑒𝑥𝑝₁ ρ) = 𝑣𝑎𝑙₁
---------------------------------------------
(value-of (if-exp 𝑒𝑥𝑝₁ 𝑒𝑥𝑝₂ 𝑒𝑥𝑝₃) ρ)
= --- (value-of 𝑒𝑥𝑝₂ ρ) if (expval->bool 𝑣𝑎𝑙₁) = #t
  |
  --- (value-of 𝑒𝑥𝑝₃ ρ) if (expval->bool 𝑣𝑎𝑙₁) = #f

;; value-of : Exp * Env -> ExpVal
(define value-of
  (lambda (exp env)
    (cases expression exp      
      ...
      (if-exp (exp1 exp2 exp3)
        (let ((val1 (value-of exp1 env)))
          (if (expval->bool val1)
              (value-of exp2 env)
              (value-of exp3 env))))
      ...)))

Impl of Conditionals by Continuation

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (if-exp (exp1 exp2 exp3)
        (value-of/k exp1 env
          (if-test-cont exp2 exp3 env cont)))
      ...)))

Example

(value-of/k <<if zero? (0) then 1 else 2>> ρ₀ end-cont)
=
(value-of/k <<zero? (0)>> ρ₀
  (if-test-cont <<1>> <<2>> ρ₀ end-cont))

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (if-exp (exp1 exp2 exp3)
        (value-of/k exp1 env
          (if-test-cont exp2 exp3 env cont)))
      ...)))

Spec and Impl of zero?

       (value-of 𝑒𝑥𝑝 ρ) = 𝑣𝑎𝑙                              
---------------------------------------------
(value-of (zero?-exp 𝑒𝑥𝑝) ρ) 
= --- (bool-var #t) if (expval->num 𝑣𝑎𝑙) = 0
  |
  --- (bool-var #f) if (expval->num 𝑣𝑎𝑙) ≠ 0

;; value-of : Exp * Env -> ExpVal
(define value-of
  (lambda (exp env)
    (cases expression exp      
      ...
      (zero?-exp (exp)
        (let ((val (value-of exp env)))
          (let ((num (expval->num val)))
            (if (zero? num)
                (bool-val #t)
                (bool-val #f)))))
      ...)))

Impl of zero? by Continuation

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (zero?-exp (exp1)
        (value-of/k exp1 env
          (zero1-cont cont))) 
      ...)))

Example

(value-of/k <<if zero? (0) then 1 else 2>> ρ₀ end-cont)
=
(value-of/k <<zero? (0)>> ρ₀
  (if-test-cont <<1>> <<2>> ρ₀ end-cont))
=
(value-of/k <<0>> ρ₀
  (zero1-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont)))  

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (zero?-exp (exp1)
        (value-of/k exp1 env
          (zero1-cont cont))) 
      ...)))

Impl of const

;; value-of : Exp * Env -> ExpVal
(define value-of
  (lambda (exp env)
    (cases expression exp
      ...
      (const-exp (n)
        (num-val n))
      ...)))

Impl of const by Continuation

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (const-exp (num)
        (apply-cont cont (num-val num)))
      ...)))

Example

(value-of/k <<0>> ρ₀
  (zero1-cont
    (if-test-cont <<1>> <<2>> ρ₀ end-cont)))  
=
(apply-cont (zero1-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont))
  (num-val 0)) 

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (const-exp (num)
        (apply-cont cont (num-val num)))
      ...)))

zero1-cont

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (zero1-cont (saved-cont)
        (apply-cont saved-cont
          (bool-val (zero? (expval->num val)))))
      ...)))

Example

(apply-cont (zero1-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont))
  (num-val 0)) 
=
(apply-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont)
  (bool-val #t))

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (zero1-cont (saved-cont)
        (apply-cont saved-cont
          (bool-val (zero? (expval->num val)))))
      ...)))

if-test-cont

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (if-test-cont (exp2 exp3 saved-env saved-cont)
        (if (expval->bool val)
          (value-of/k exp2 saved-env saved-cont)
          (value-of/k exp3 saved-env saved-cont)))
      ...)))

Example

(apply-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont)
  (bool-val #t))
= 
(value-of/k <<1>> ρ₀ end-cont)

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (if-test-cont (exp2 exp3 saved-env saved-cont)
        (if (expval->bool val)
          (value-of/k exp2 saved-env saved-cont)
          (value-of/k exp3 saved-env saved-cont)))
      ...)))

Example

(value-of/k <<1>> ρ₀ end-cont)
=
(apply-cont end-cont (num-val 1))

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (const-exp (num)
        (apply-cont cont (num-val num)))
      ...)))

end-cont

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (end-cont ()
        val)
      ...)))

Example

(apply-cont end-cont (num-val 1))
=
(num-val 1)

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (end-cont ()
        val)
      ...)))

Example: Complete Derivation

  (value-of/k <<if zero? (0) then 1 else 2>> ρ₀ end-cont)
= (value-of/k <<zero? (0)>> ρ₀ (if-test-cont <<1>> <<2>> ρ₀ end-cont))
= (value-of/k <<0>> ρ₀ (zero1-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont)))  
= (apply-cont (zero1-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont)) (num-val 0))
= (apply-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont) (bool-val #t))
= (value-of/k <<1>> ρ₀ end-cont)
= (apply-cont end-cont (num-val 1))
= (num-val 1)

Continuation

• A procedure that represents the rest of the computation

  (value-of/k <<if zero? (0) then 1 else 2>> ρ₀ end-cont)
= (value-of/k <<zero? (0)>> ρ₀ (if-test-cont <<1>> <<2>> ρ₀ end-cont))
= (value-of/k <<0>> ρ₀ (zero1-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont)))  
= (apply-cont (zero1-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont)) (num-val 0))
= (apply-cont (if-test-cont <<1>> <<2>> ρ₀ end-cont) (bool-val #t))
= (value-of/k <<1>> ρ₀ end-cont)
= (apply-cont end-cont (num-val 1))
= (num-val 1)

Benefits of Using Continuations?

Exceptions

[Concrete Syntax]
Expression ::= ...
            | try Expression catch (Identifier) Expression
            | raise Expression

[Abstract Syntax]
Expression ::= ...
            | try-exp (exp1 var handler-exp)
            | raise-exp (exp)

Example 1

(value-of/k <<try 1 catch (x) -1>> ρ₀ end-cont)

try-exp

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of
  (lambda (exp env cont)
    (cases expression exp
      ...
      (try-exp (exp1 var handler-exp)
        (value-of/k exp1 env
          (try-cont var handler-exp env cont)))
      ...)))

Example 1

(value-of/k <<try 1 catch (x) -1>> ρ₀ end-cont)
= (value-of/k <<1>> ρ₀ (try-cont x <<-1>> ρ₀ end-cont))

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of
  (lambda (exp env cont)
    (cases expression exp
      ...
      (try-exp (exp1 var handler-exp)
        (value-of/k exp1 env
          (try-cont var handler-exp env cont)))
      ...)))

Example 1

(value-of/k <<try 1 catch (x) -1>> ρ₀ end-cont)
= (value-of/k <<1>> ρ₀ (try-cont x <<-1>> ρ₀ end-cont))
= (apply-cont (try-cont x <<-1>> ρ₀ end-cont) (num-val 1))

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (const-exp (num)
        (apply-cont cont (num-val num)))
      ...)))

try-cont

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (try-cont (var handler-exp saved-env saved-cont)
        (apply-cont saved-cont val))
      ...)))

Example 1

(value-of/k <<try 1 catch (x) -1>> ρ₀ end-cont)
= (value-of/k <<1>> ρ₀ (try-cont x <<-1>> ρ₀ end-cont))
= (apply-cont (try-cont x <<-1>> ρ₀ end-cont) (num-val 1))
= (apply-cont end-cont (num-val 1))
= (num-val 1)

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (try-cont (var handler-exp saved-env saved-cont)
        (apply-cont saved-cont val))
      ...)))

Example 2

(value-of/k <<try raise (10) catch (x) -1>> ρ₀ end-cont)

raise-exp

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of
  (lambda (exp env cont)
    (cases expression exp
      ...
      (raise-exp (exp1)
        (value-of/k exp1 env
          (raise1-cont cont)))
      ...)))

Example 2

(value-of/k <<try raise (10) catch (x) -1>> ρ₀ end-cont)
= (value-of/k <<raise (10)>> ρ₀ (try-cont x <<-1>> ρ₀ end-cont))

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of
  (lambda (exp env cont)
    (cases expression exp
      ...
      (try-exp (exp1 var handler-exp)
        (value-of/k exp1 env
          (try-cont var handler-exp env cont)))
      ...)))

Example 2

(value-of/k <<try raise (10) catch (x) -1>> ρ₀ end-cont)
= (value-of/k <<raise (10)>> ρ₀ (try-cont x <<-1>> ρ₀ end-cont))
= (value-of/k <<10>> ρ₀ (raise1-cont (try-cont x <<-1>> ρ₀ end-cont)))

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of
  (lambda (exp env cont)
    (cases expression exp
      ...
      (raise-exp (exp1)
        (value-of/k exp1 env
          (raise1-cont cont)))
      ...)))

Example 2

(value-of/k <<try raise (10) catch (x) -1>> ρ₀ end-cont)
= (value-of/k <<raise (10)>> ρ₀ (try-cont x <<-1>> ρ₀ end-cont))
= (value-of/k <<10>> ρ₀ (raise1-cont (try-cont x <<-1>> ρ₀ end-cont)))
= (apply-cont (raise1-cont (try-cont x <<-1>> ρ₀ end-cont)) (num-val 10))

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (const-exp (num)
        (apply-cont cont (num-val num)))
      ...)))

raise1-cont

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (raise1-cont (saved-cont)          
        (apply-handler val saved-cont))
      ...)))

Example 2

  (apply-cont (raise1-cont (try-cont x <<-1>> ρ₀ end-cont)) (num-val 10))
= (apply-handler (num-val 10) (try-cont x <<-1>> ρ₀ end-cont))

(define apply-cont
  (lambda (cont val)
    (cases continuation cont
      ...
      (raise1-cont (saved-cont)          
        (apply-handler val saved-cont))
      ...)))

apply-handler

(define apply-handler
  (lambda (val cont)
    (cases continuation cont        
      (try-cont (var handler-exp saved-env saved-cont)
        (value-of/k handler-exp
          (extend-env var val saved-env)
          saved-cont))
      ...)))

Example 2

  (apply-cont (raise1-cont (try-cont x <<-1>> ρ₀ end-cont)) (num-val 10))
= (apply-handler (num-val 10) (try-cont x <<-1>> ρ₀ end-cont))
= (value-of/k <<-1>> (extend-env x (num-val 10) ρ₀) end-cont)

(define apply-handler
  (lambda (val cont)
    (cases continuation cont        
      (try-cont (var handler-exp saved-env saved-cont)
        (value-of/k handler-exp
          (extend-env var val saved-env)
          saved-cont))
      ...)))

Example 2

  (apply-cont (raise1-cont (try-cont x <<-1>> ρ₀ end-cont)) (num-val 10))
= (apply-handler (num-val 10) (try-cont x <<-1>> ρ₀ end-cont))
= (value-of/k <<-1>> (extend-env x (num-val 10) ρ₀) end-cont)
= (apply-cont end-cont (num-val -1))
= (num-val -1)

;; value-of : Exp * Env * Cont -> ExpVal
(define value-of/k
  (lambda (exp env cont)
    (cases expression exp
      ...
      (const-exp (num)
        (apply-cont cont (num-val num)))
      ...)))

Comparing Continuation and Environment

• Environment: abstraction of the data context

Comparing Continuation and Environment

• Environment: abstraction of the data context
• Continuation: abstraction of the control context