►CSE P 505 Spring 2013 Homework #4
1 Continuations (and recursion)
2 Type Inference
3 Handin Details

CSE P 505 Spring 2013 Homework #4

Due: Thursday, May 30 at 11pm

1 Continuations (and recursion)

Part a.

Define a datatype to represent abstract syntax for a language with:

Write a parser for this syntax, then write an interpreter in continuation-passing style. Refer to the notes for the fifth lecture. You may either perform the CPS transformation ad hoc or using the monadic combinators discussed in class and in the lecture notes. This means the interpreter may be of the form:

(define (interp/k [expr : Expr]
                  [env : (Env Value)]
                  [k : (Value -> 'a)]) : 'a
  ...)

OR

(define (interp/k [expr : Expr]
                  [env : (Env Value)]) : (CPS Value)
  ...)

You can use Racket’s box to help implement rec. Please also define a run procedure that calls interp/k with an appropriate initial environment and continuation, as in the examples below.

Part b.

Extend the language with a construct called break, which takes a value and "breaks" execution, returning a new variant of Value called a breakV. A breakV contains the value that was passed to break and a Racket procedure that can be used to resume execution, optionally with a different value:

(define-type Value
  ...
  [breakV (value : Value)
          (resumer : ((optionof Value) -> 'a))])

An example of using break while evaluating an expression:

(define result
  (box (run (parse '((rec fact (fun (n)
                                 (if0 n
                                      1
                                      (* n (fact (break (- n 1)))))))
                      5)))))
 
> (unbox result)
- Value
(breakV (numV 4) #<procedure>)
> (set-box! result ((breakV-resumer (unbox result)) (none)))
> (unbox result)
- Value
(breakV (numV 3) #<procedure>)
... ; repeat a few more times
> (unbox result)
- Value
(numV 120)

Or, if we wanted to change the outcome of evaluation:

(define result
  (box (run (parse '((rec fact ...)
                      5)))))
 
> (unbox result)
- Value
(breakV (numV 4) #<procedure>)
> (set-box! result ((breakV-resumer (unbox result)) (none)))
> (unbox result)
- Value
(breakV (numV 3) #<procedure>)
> (set-box! result ((breakV-resumer (unbox result)) (some (numV 0))))
> (unbox result)
- Value
(numV 20)

2 Type Inference

The types of expressions for the language in Problem 1 can be represented by the following datatype:

(define-type Type
  ; numbers
  [numT]
  ; functions
  [funT (arg-t : Type) ; argument type
        (res-t : Type)] ; result type
  ; type variables (unknown initially but constrained by inference)
  [varT (id : number) ; a unique id for comparison
        (bound-t : (boxof (optionof Type)))]) ; type (if any) bound to this var

Part a.

Implement a function that infers the type of an expression (written in the language of Problem 1).

(define (infer-type [expr : Expr] [ty-env : (Env Type)]) : Type
  ...)

If an expression is not well-typed, infer-type should raise an error.

You’ll want to write a helper function that unifies two types, which in general involves binding type variables to each other and to other types. Handling the funT case will require recursive calls to unify the argument and result types. Self-application (like in omega or the Y-combinator) will create a cycle, which will (without special care) put the unification procedure into an infinite recursion. To prevent this, unify needs to keep track of the pairs of types that it’s already trying to unify, so if it’s called recursively with the same arguments, it can bail out. We normally fail in that case, but you can alternatively allow it to succeed, in which case the type system will be able to infer recursive types, though note that this will make the implementation of resolve (see below) more difficult.

; Attempts to unify t1 with t2, possibly performing side-effecting
; bindings of type variables in one or both types.
; 
; mem-table is a list of pairs of types that we're in the process of
; trying to unify, and which needs to be extended on each recursive
; call. If the pair (t1, t2) is in mem-table, then we've found
; a cycle and should break out in order to avoid looping forever.
; 
; Returns whether the unification was successful.
(define (unify [t1 : Type]
               [t2 : Type]
               [mem-table : (listof (Pair Type Type))]) : boolean
  ...)

You’ll almost certainly want another helper function that resolves a type variable by (recursively) following its bindings. (Note that a type variable may become bound to another type variable, and that variable may subsequently become bound to a concrete type, for example.) The result of a call to resolve should be either an unbound type variable or a non-variable type (i.e., numT or funT). In the case of a funT, the argument and result types may again be type variables, so a full resolution should recursively track these down as well.

So, you may find it’s helpful to have two functions: resolve (which returns a numT, funT, or varT with no binding) and fully-resolve (like resolve, but with the additional constraint that the argument and result types of a funT have also been fully resolved). The former is sufficient for unification, while the latter is useful when you’re ready to display a type for a person to read and understand. Ideally, you could go a step further and pretty-print types with infix arrows and other niceties:

> (pretty-print (infer-type (parse '(+ 3 5)) empty-env))
- string
"num"
> (pretty-print (infer-type (parse '(fun (x) x)) empty-env))
- string
"(var0 -> var0)"
> (pretty-print
    (infer-type (parse '(rec fact (fun (n)
                                    (if0 n
                                         1
                                         (* n (fact (- n 1)))))))
                empty-env))
- string
"(num -> num)"
> (pretty-print
    (infer-type (parse '(+ 3 (fun (x) (+ x x)))) empty-env))
- string
type error: expected a number but got (num -> num)
> (pretty-print
    (infer-type (parse '(3 (fun (x) (+ x x)))) empty-env))
- string
type error: expected a function but got num
> (pretty-print
    (infer-type (parse '(with (id (fun (x) x))
                          (+ (id 3) ((id id) 4))))
                empty-env))
- string
type error: function expected a num but got (num -> num)

Part b. (Optional, for extra credit.)

Extend the Type type and infer-type procedure to support let-polymorphism. To do this, add a typeClosureT variant and extend the withE case of infer-type to construct a type closure for the type of the bound expression. The variables in the closure should be all of the variables in the type that have not been bound to either a concrete type or unified with any type variable in the type environment used to infer the type. The typeClosureT variant should look something like this:

(define-type Type
  ... ; existing variants
  [typeClosureT (free-vars : (listof number)) ; ids of free vars in the type
                (type : Type)]) ; the type that this closure wraps

Additionally, in the varE case of infer-type, if you find that a variable is bound to a typeClosureT, you should make a fresh copy of each of the free variables, then return a copy of the type into which you’ve substituted the fresh variables for the free variables in the original type. This will allow the type to be used independently in different type contexts. In particular, the last example above should now type-check:

> (pretty-print
    (infer-type (parse '(with (id (fun (x) x))
                          (+ (id 3) ((id id) 4))))
                empty-env))
- string
"num"

3 Handin Details

Please submit a single .rkt file with all of the definitions from this homework.