Introduction

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.

Code Overview

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

(define-type TypeExp
  [numTE]
  [boolTE]
  [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
  [numT]
  [boolT]
  [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
  (local
      [(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))
               type
               (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}})
      (numT))

(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")

Tests

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