CPS Interpreter: Exceptions and Reification of Continuations
Table of Contents
1 Introduction
The goal of this set of notes is to demonstrate how to
implement language features that deal with exceptional flow
of control. We call the resultant language LETCC.
We are interested in the following four types of exceptional flow of control:
- Aborting: Aborting a program with a value
- Break-resume: Breaking the execution of a program by returning a value and resuming its execution with a value.
- Exceptions: Throwing an exception and catching it inside a try-catch block.
- Letcc: Capture the current continuation and bind it to an identifier.
1.1 Examples and test cases
1.1.1 Recursive Functions
(check-equal?
(go '(recursive ([f (n) (ifte (0? n) 1 (* n (f (- n 1))))])
(f 3)))
6
"go-factorial")
(check-equal?
(go
'(recursive ([even? (n) (ifte (0? n) #t (odd? (- n 1)))]
[odd? (n) (ifte (0? n) #f (even? (- n 1)))])
(even? 3)))
#f
"go-even")
1.1.2 Errors with primitives
1.1.3 Abort
(check-equal? (go '(+ 2 (abort 5))) 5 "go-abort")
1.1.4 Break
(check-equal? (go '(+ 2 (break 3))) "breaking with value 3" "go-break-3") (check-equal? (*resume*) 5 "go-resume") (check-equal? (*resume* 4) 6 "go-resume-6") (check-equal? (go '(* (+ 2 (break 3)) (break 4))) "breaking with value 3" "go-break2-3") (check-equal? (*resume*) "breaking with value 4" "go-resume2") (check-equal? (*resume*) 20 "go-resume3") (check-equal? (*resume* 8) 40 "go-resume-8")
1.1.5 Throw
(check-equal? (go '(throw 5)) "uncaught exception" "throw-uncaught")
1.1.6 Try
(check-equal? (go '(+ 2 (try (* 3 4) v (+ v 7)))) 14 "try0") (check-equal? (go '(+ 2 (try (+ 3 (throw 7)) v (+ v 4)))) 13 "try1") (check-equal? (go '(+ 2 (try (+ 3 (throw (* 2 (throw 7)))) v (+ v 4)))) 13 "try2") (check-equal? (go '(+ 2 (try (+ 3 (throw (* 2 (throw 7)))) v (+ v (throw 6))))) "uncaught exception" "try3")
1.1.7 Letcc
(check-equal? (go '(letcc k (k 3))) 3 "letcc-1") (check-equal? (go '(letcc k (+ 2 (k 3)))) 3 "letcc-2") (check-equal? (go '(+ 2 (letcc k (* 3 (k 4))))) 6 "letcc-3")
2 Syntax
2.1 Concrete Syntax
<exp> ::= <literal> Literal (Number or Boolean)
| <id> Identifier reference
| (function (<id> ...) <exp>) Function
| (<exp> ...) Application
| (if <exp> <exp> <exp>) Conditional
| (let (<bind> ...) <exp>) Let
| (recursive (<fbind> ...) <exp>) Recursive Functions
| (abort <exp>) Abort
| (break <exp>) Abort
| (try <exp> catch <id> <exp>) Try-catch
| (throw <exp>) Throw
| (letcc <id> <exp> <exp>) Letcc
<bind> ::= [<id> <exp>] bind
<fbind> ::= [<id> (<id> ...) <exp>] fbind
2.2 Abstract Syntax
The define-datatype construct is used to define the
abstract syntax of the language LETCC.
(define-datatype ast ast?
[number (datum number?)]
[boolean (datum boolean?)]
[ifte (test ast?) (then ast?) (else-ast ast?)]
[function (formals (list-of id?)) (body ast?)]
[recursive (fbinds (list-of fbind?)) (body ast?)]
[app (rator ast?) (rands (list-of ast?))]
[id-ref (sym id?)]
[assume (binds (list-of bind?)) (body ast?)]
[abort (ans-ast ast?)]
[break (ans-ast ast?)]
[try (body ast?) (exn-id id?) (handler ast?)]
[throw (exn-ast ast?)]
[letcc (sym id?) (body ast?)])
(define-datatype bind bind?
[make-bind (b-id id?) (b-ast ast?)])
;;; bind-id : bind? -> id?
(define bind-id
(lambda (b)
(cases bind b
[make-bind (b-id b-ast) b-id])))
;;; bind-ast : bind? -> ast?
(define bind-ast
(lambda (b)
(cases bind b
[make-bind (b-id b-ast) b-ast])))
(define-datatype fbind fbind?
[make-fbind (fb-id id?)
(fb-formals (list-of id?))
(fb-body ast?)])
;;; fbind-id : fbind? -> id?
(define fbind-id
(lambda (b)
(cases fbind b
[make-fbind (fb-id fb-formals fb-body) fb-id])))
;;; fbind-formals : fbind? -> (list-of id?)
(define fbind-formals
(lambda (b)
(cases fbind b
[make-fbind (fb-id fb-formals fb-body) fb-formals])))
;;; fbind-body : fbind? -> ast?
(define fbind-body
(lambda (b)
(cases fbind b
[make-fbind (fb-id fb-formals fb-body) fb-body])))
(define id? symbol?)
2.3 Parser
2.3.1 Test cases
(check-equal? (parse 4) (number 4) "parse-number")
(check-equal? (parse #t) (boolean #t) "parse-boolean")
(check-equal? (parse 'x) (id-ref 'x) "parse-id")
(check-equal?
(parse '(ifte 3 4 8))
(ifte (number 3) (number 4) (number 8))
"parse-ifte")
(check-equal?
(parse '(function (x y) 4))
(function '(x y) (number 4))
"parse-function")
(check-equal?
(parse '(assume ([x 3]) 6))
(assume (list (make-bind 'x (number 3))) (number 6))
"parse-assume")
(check-equal?
(parse '(recursive ([f (x y) x] [g (m n) 5]) 9))
(recursive
(list
(make-fbind 'f '(x y) (id-ref 'x))
(make-fbind 'g '(m n) (number 5)))
(number 9))
"parse-recursive")
(check-equal?
(parse '(recursive () 9))
(recursive
(list)
(number 9))
"parse-empty-recursive")
(check-equal?
(parse '(x y))
(app (id-ref 'x)
(list (id-ref 'y)))
"parse-app")
(check-equal?
(parse '(abort 5))
(abort (number 5))
"parse-app")
(check-exn exn? (lambda () (parse "hello")) "parse-string-error")
(check-exn exn? (lambda () (parse '#(1 2))) "parse-vector-error")
(check-exn exn? (lambda () (parse '(1 . 2)) "parse-cons-error"))
(check-exn exn? (lambda () (parse '()) "parse-empty-error"))
2.3.2 Implementation
(define parse
(lambda (d)
(match d
[(? number? n) (number n)]
[(? boolean? b) (boolean b)]
[(list 'ifte a b c) (ifte (parse a) (parse b) (parse c))]
[(list 'function
(list (? id? x) ...)
body)
(function x (parse body))]
[(list 'assume
(list (list (? id? x) e) ...) body)
(let* ([a (map parse e)]
[b (map make-bind x a)])
(assume b (parse body)))]
[(list 'recursive
(list
(list
(? id? f)
(and formals (list (? id? x) ...))
fbody) ...)
body)
(let* ([fast (map parse fbody)]
[fbinds (map make-fbind f formals fast)])
(recursive fbinds (parse body)))]
[(list 'abort exp)
(abort (parse exp))]
[(list 'break exp)
(break (parse exp))]
[(list 'try body (? id? x) handler)
(try (parse body) x (parse handler))]
[(list 'throw exp) (throw (parse exp))]
[(list 'letcc (? id? x) exp) (letcc x (parse exp))]
[(? id? x) (id-ref x)]
[(list rator rands ...)
(let* ([rator (parse rator)]
[rands (map parse rands)])
(app rator rands))]
[_ (error 'parse "don't know how to parse ~a" d)])))
3 Semantic Domains
3.1 Expressible and Denotable Values
The expressible values are numbers, booleans and procedures:
;;; expressible-value? : any/c -> boolean? (define expressible-value? (or/c number? boolean? proc?))
Denotable values are identical to expressible values.
;;; denotable-value? :any/c -> boolean? (define denotable-value? expressible-value?)
Here proc? denotes procedures.
3.2 Procedures
A procedure is one of the following:
- Primitive
- Closure
- Continuation
(define-datatype proc proc?
[prim-proc
;; prim refers to a racket procedure
(prim procedure?)
;; sig is the signature, a list of type predicates
(sig (list-of procedure?))]
[closure
(formals (list-of symbol?))
(body ast?)
(env env?)]
[continuation-proc (kont procedure?)])
(define prim-proc?
(lambda (p)
(cases proc p
[prim-proc (prim sig) #t]
[else #f])))
(define closure?
(lambda (p)
(cases proc p
[closure (formals body env) #t]
[else #f])))
(define continuation-proc?
(lambda (p)
(cases proc p
[continuation-proc (kont) #t]
[else #f])))
4 Environments
An environment is either empty, extended or recursive:
(define-datatype env env?
[empty-env]
[extended-env
(syms (list-of symbol?))
(vals (list-of any/c))
(outer-env env?)]
[extended-rec-env
(fsyms (list-of symbol?))
(lformals (list-of (list-of symbol?)))
(bodies (list-of ast?))
(outer-env env?)])
(define *empty-env* (empty-env))
(define *top-env* (extended-env '(x y z) '(2 4 6) *empty-env*))
4.1 Environment Lookup
The lookup-env takes two continuations: success and
failure. When looking up a recursive environment, a closure
is built at the time of the lookup, which includes the
environment being looked up.
;;; lookup-env/k:
;;; [env? symbol? (K any/c) (K)] ->
(define lookup-env/k
(lambda (e x succ fail)
(cases env e
[empty-env () (fail)]
[extended-env (syms vals outer-env)
(list-index/k syms x
(lambda (j)
(succ (list-ref vals j)))
(lambda ()
(lookup-env/k outer-env x succ fail)))]
[extended-rec-env
(fsyms lformals bodies outer-env)
(list-index/k fsyms x
(lambda (j)
(let ([formals
(list-ref lformals j)]
[body (list-ref bodies j)])
(succ (closure formals body e)))) ;; builds closure
(lambda ()
(lookup-env/k outer-env x succ fail)))])))
(define list-index/k
(lambda (ls a succ fail)
(letrec
([loop
(lambda (ls ans)
(cond
[(null? ls) (fail)]
[(eq? (first ls) a) (succ ans)]
[#t (loop (rest ls) (+ 1 ans))]))])
(loop ls 0))))
5 Interpreter eval-ast/k
5.1 Answer domain
The interpreter maps ast's to answers. An answer is now either an expressible value or error string.
(define err-msg? string?) (define answer? (or/c expressible? err-msg?))
5.2 Evaluator
The interpreter eval-ast/k now has two continuations as
part of its state: a continuation k to capture normal flow
of control, and ex-k to capture exceptional flow of
control.
(define eval-ast/k
(lambda (a env k ex-k)
(cases ast a
5.2.1 Literals
Literals are simply passed to the waiting continuation k. #
[number (datum) (k datum)] [boolean (datum) (k datum)]
5.2.2 Identifier
An identifier is looked up in the environment with the the
failure continuation invoking *top-k* to report an
"unbound identifier" error. The cps style obviates the need
for Racket's built-in error function.
[id-ref (sym)
(lookup-env/k env sym k
(lambda ()
(*top-k*
(format "unbound identifier ~a" sym))))]
5.2.3 Conditional
The test condition needs to evaluate always to a boolean, otherwise it is a type error.
[ifte (test then else-ast)
(eval-ast/k test env
(lambda (b)
(if (boolean? b)
(eval-ast/k (if b then else-ast) env k ex-k)
(*top-k*
(format
"ifte test is not a boolean ~a" a))))
ex-k)]
5.2.4 Function
The case of function is simple. A closure is built and
passed to the waiting continuation k:
[function (formals body) (k (closure formals body env))]
5.2.5 Application
The rator evaluates to p. It is then checked that it is a
procedure. Then, the rands are evaluated to args and
apply-proc/k applies p to args. If p is not a
procedure, a runtime error is flagged.
[app (rator rands)
(eval-ast/k rator env
(lambda (p)
(if (proc? p)
(eval-asts/k rands env
(lambda (args)
(apply-proc/k p args k ex-k)) ex-k)
(*top-k*
(format
"application rator is not a proc ~a"
a)))) ex-k)]
5.2.6 Assume
bind-id and bind-ast are extractors (simple
expressions). The asts are evaluated to vals. The
environment is extended and then the body is evaluated in
this new environment. The continuations go along for a
ride.
[assume (binds body)
(let ([ids (map bind-id binds)]
[asts (map bind-ast binds)])
(eval-asts/k asts env
(lambda (vals)
(let ([new-env
(extended-env ids vals env)])
(eval-ast/k body new-env k ex-k))) ex-k))]
5.2.7 Recursive
The body of the recursive expression is evaluated in the
extended-rec-env built from the components of fbinds and
the existing env.
[recursive (fbinds body)
(let*
([fids (map fbind-id fbinds)]
[lformals (map fbind-formals fbinds)]
[bodies (map fbind-body fbinds)]
[new-env
(extended-rec-env
fids lformals bodies env)])
(eval-ast/k body new-env k ex-k))]
5.2.8 Abort
The subexpression ans-ast of the abort expression is
evaluated with *top-k* replacing the current continuation
k.
[abort (ans-ast) (eval-ast/k ans-ast env *top-k* ex-k)]
5.2.9 Break
The break expression's subexpression is evaluated in the
context of the regular continuation that takes
v and does two things:
- Sets The top-level variable
*resume*to function that invokes the current continuationkeither with the valuevor whatever is supplied in place ofv. - Escapes to the top-level with the top-level
continuation
*top-k*.
[break (ans-ast)
(eval-ast/k ans-ast env
(lambda (v)
(set! *resume*
(match-lambda*
['() (k v)]
[(list x) (k x)]
[_ (*top-k* "Error: *resume* takes at most one argument")]))
(*top-k* (format "breaking with value ~a" v))) ex-k)]
5.2.10 Throw
Evaluating a throw expression reduces to evaluating the
subexpression exn-ast in the context of the current
exception continuation.
[throw (exn-ast) (eval-ast/k exn-ast env ex-k ex-k)]
5.2.11 Try-catch
The try expression's body is evaluated in an exception
continuation that receives the exception exn.
The environment env is extended with the
binding that binds exn-id with the exception exn and the
handler is evaluated in this extended environment, the
current continuation k and the current exception
continuation ex-k.
[try (body exn-id handler)
(eval-ast/k body env k
(lambda (exn)
(let ([new-env (extended-env (list exn-id) (list exn) env)])
(eval-ast/k handler new-env k ex-k))))]
5.2.12 Let-cc
The current continuation k is packaged as a procedure and
bound to sym and this binding is used to extend the
environment to obtain new-env. The body of the letcc
expression is evaluated in new-env and the current regular
and exception continuations.
A continuation-proc is a procedure that when evaluated
applies k to its argument and escapes to the top level.
[letcc (sym body)
(let ([new-env (extended-env (list sym)
(list (continuation-proc k)) env)])
(eval-ast/k body new-env k ex-k))]
)))
5.2.13 eval-asts/k
eval-asts/k evaluates a list of asts in the current normal
and exception continuations:
(define eval-asts/k
(lambda (asts env k ex-k)
(if (null? asts)
(k '())
(eval-ast/k (first asts) env
(lambda (v)
(eval-asts/k (rest asts) env
(lambda (vals)
(k (cons v vals))) ex-k)) ex-k))))
5.3 Applying procedures
The job of apply-proc/k is to apply a procedure to
arguments. Recall that we have three kinds of procedures:
primitives, closures and continuations.
5.3.1 apply-proc/k
A primitive procedures comes with primitive operation and a signature. A closure has formal, body and environment. A continuation procedure comes with a continuatio (a Racket procedure).
When applying a primitive, any error (either due to
argument-signature mismatch, or say a divide by zero)
directly escapes to the top level. The current
ex-k has no role and hence is not an argument to
apply-prim-proc/k.
When applying a closure, the current environment has no role.
When applying a continuation procedure, the current
continuation k and ex-k have no role; they are ignored.
(define apply-proc/k
(lambda (p args k ex-k)
(cases proc p
[prim-proc (prim sig)
(apply-prim-proc/k prim sig args k)]
[closure (formals body env)
(apply-closure/k formals body env args k ex-k)]
[continuation-proc (kont)
(apply-continuation kont args)] ; ignore k and ex-k !
)))
5.3.2 apply-prim-proc/k
The length and types of the signature sig are compared
with the types of the argument. If everything matches,
prim is applied to args and the result passed to the
waiting normal continuation k. Otherwise, a runtime error
is raised and the answer is an error message.
(define apply-prim-proc/k
(lambda (prim sig args k)
(let* ([args-sig (rest sig)]) ; argument signatures
(cond
[(and
(= (length args-sig) (length args))
(andmap match-arg-type args-sig args))
(k (apply prim args))]
;; notice how the incoming k is dropped
[#t (*top-k* (format "incorrect number or type of arguments to ~a" prim))]))))
;;; match-arg-type : [procedure? any/c] -> boolean?
(define match-arg-type
(lambda (arg-type? val)
(arg-type? val)))
5.3.3 apply-closure/k
body is evaluated in new-env, which is the environment
obtained by extending env with the bindings of formals
with args. The control context is unchanged.
(define apply-closure/k
(lambda (formals body env args k ex-k)
(let ([new-env (extended-env formals args env)])
(eval-ast/k body new-env k ex-k))))
5.3.4 apply-continuation
(define apply-continuation
(lambda (k args)
(cond [(= (length args) 1)
(*top-k* (apply k args))]
[#t (*top-k* (format "incorrect number of arguments to continuation procedure ~a" k))])))
5.3.5 Top level continuations
;;; top-k : [] -> (K any/c)
(define top-k
(lambda ()
(lambda (v) ; v is an answer
v)))
;;; THE top-level continuation
(define *top-k* (top-k))
(define *top-ex-k*
(lambda (v) "uncaught exception"))
(define *resume-init*
(lambda args
(*top-k* "Error: nothing to resume")))
(define *resume* *resume-init*)
5.3.6 eval-ast
;;; eval-ast : [ast? env?] -> answer?
(define eval-ast
(lambda (ast env)
(eval-ast/k ast env *top-k* *top-ex-k*)))
6 Initial Environment and driver go
6.1 Primitive Procedures
;;; Primitive Procedures
;;; ====================
(define nonzero? (and/c number? (not/c zero?)))
(define +p
(prim-proc +
(list number? number? number?)))
(define -p
(prim-proc -
(list number? number? number?)))
(define *p
(prim-proc *
(list number? number? number?)))
(define /p
(prim-proc /
(list number? number? nonzero?)))
(define <p
(prim-proc <
(list boolean? number? number?)))
(define <=p
(prim-proc <=
(list boolean? number? number?)))
(define eq?p
(prim-proc eq?
(list boolean? expressible-value? expressible-value?)))
(define 0?p
(prim-proc zero?
(list boolean? number?)))
6.2 Initial Environment
(define *init-env* (extended-env '(+ - * / < <= eq? 0?) (list +p -p *p /p <p <=p eq?p 0?p) (empty-env)))
6.3 Run and go
run evaluates an ast in *init-env*. go parses an
expression and then runs it.
;;; run: ast? -> expressible-value?
(define run
(lambda (ast)
(eval-ast ast *init-env*)))
(define go
(lambda (e)
(run (parse e))))