UNB/ CS/ David Bremner/ teaching/ cs4613/ assignments/ Assignment 2


In this assignment you will implement some of the type rules from Introduction to Types in the text.

You are given an initial interpreter based on the interpreter from Assignment 1

Hand in your work to the handin server via DrRacket (just like the lab tutorials) before 10:00PM on Friday, Feb 23.

A grading rubric is available.

Code Overview

Compared to Assignment 1, the abstract syntax (and parser) have been modified to introduce a syntax for types.

(define-type TypeExp
  [arrowTE (arg : TypeExp)
           (result : TypeExp)])

(define-type Exp
  [numE (n : Number)]
  [boolE (b : Boolean)]
  [plusE (left : Exp) (right : Exp)]
  [timesE (left : Exp) (right : Exp)]
  [minusE (left : Exp) (right : Exp)]
  [leqE (left : Exp) (right : Exp)]
  [lamE (var : Symbol) (te : TypeExp) (body : Exp)]
  [appE (fun : Exp) (arg : Exp)]
  [varE (name : Symbol)]
  [ifE (check : Exp) (zero : Exp) (non-zero : Exp)]
  [let1E (var : Symbol) (te : TypeExp) (value : Exp) (body : Exp)]
  [recE (var : Symbol) (te : TypeExp) (value : Exp) (body : Exp)])

As in the book, we also introduce a type to represent the results from our typechecker (analogous to Value for interp).

(define-type Type
  [arrowT (arg : Type) (result : Type)])

In this case the correspondence between abstract syntax and “type value” is trivial, given by the following function.

(define (interp-te te)
  (type-case TypeExp te
    [(numTE) (numT)]
    [(boolTE) (boolT)]
    [(arrowTE a b) (arrowT (interp-te a)
                           (interp-te b))]))

Similarly to the environments in Assignment 1, we define TypeEnv for use in the typechecker.

(define-type-alias TypeEnv (Hashof Symbol Type))

(define mt-type-env (hash empty)) ;; "empty type environment"
(define (type-lookup (s : Symbol) (n : TypeEnv))
  (type-case (Optionof Type) (hash-ref n s)
    [(none) (error s "not bound")]
    [(some b) b]))

(test/exn (type-lookup 'x mt-type-env) "not bound")

(define (type-extend (env : TypeEnv) (s : Symbol) (t : Type))
  (hash-set env s t))

Complete the typechecker

You are given a skeleton of a typechecker, with the easy cases filled in. Complete the remaining cases to implement the type rules from Introduction to Types.

(define (typecheck [exp : Exp] [env : TypeEnv]) : Type
      [(define (num2 l r type)
         (let ([left-t (typecheck l env)]
               [right-t (typecheck r env)])
           (if (and (equal? (numT) left-t) (equal? (numT) right-t))
               (error 'typecheck "expected 2 num"))))]
    (type-case Exp exp
      [(numE n) (numT)]
      [(boolE b) (boolT)]
      [(plusE l r) (num2 l r (numT))]
      [(minusE l r) (num2 l r (numT))]
      [(timesE l r) (num2 l r (numT))]
      [(leqE l r) (num2 l r (boolT))]
      [(varE s) (type-lookup s env)]
      [(lamE name te body) ....]
      [(appE fn arg) ....]
      [(ifE c t f) ....]
      [(let1E var te val body) ....]
      [(recE var te val body) ....]

Your completed solution should pass the following tests

(test (tc `{rec {[fact : (num -> num)]
                {lam {n : num} {if {<= n 0} 1 {* n {fact {- n 1}}}}}}
                {fact 10}})

(test (tc `{lam {n : num} {if {<= n 0} 1 2}}) (arrowT (numT) (numT)))

(test (tc `{let1 {[x : num] 3} {lam {y : num} {+ x y}}}) (arrowT (numT) (numT)))
(test/exn (tc `{lam {n : bool} {if {<= n 0} 1 2}}) "typecheck")

(test/exn (tc `{lam {n : num} {if n 1 2}}) "boolean")

(test/exn (tc `{1 1}) "function")


Referring to the grading grading rubric for guidance, add any needed tests for your solution.