UNB/ CS/ David Bremner/ teaching/ cs3613/ tutorials/ CS3613 Tutorial 9

Background

In this tutorial you will get more familiar with typechecking and (in particular) the unification based interepreter discussed in Lecture 18.

Step 0

Download the unification based TIFAE interpreter. You will modify this interpeter in the remaining steps of this tutorial.

Step 1

Add a With variant to the FAE type, and add dummy clauses (using ....) to the type-case statements in eval and typecheck.

Step 2

If needed, consult your notes for some of the previous interpreters (e.g. the one discussed in Lecture 8 to impliment the eval functionality for With.

Add the following tests to your interpeter.

  (test (eval
         (With
          'add3
          (Fun 'x (GuessTE) (Add (Id 'x) (Num 3)))
          (With
           'add1
           (Fun 'x (NumTE) (Add (Id 'x) (Num 1)))
           (With 'x (Num 3) (Call (Id 'add1) (Call (Id 'add3) (Id 'x))))))
         (mtSub))
        (NumV 7))

  (test (eval
         (With 'identity (Fun 'x (GuessTE) (Id 'x))
          (With 'foo (Fun 'x (NumTE) (Add (Id 'x) (Num 1)))
                (Call (Call (Id 'identity) (Id 'foo)) (Num 123))))
         (mtSub))
        (NumV 124))

  (test (eval (With 'x  (Num 3)
                    (With
                     'f (Fun 'y (GuessTE) (Add (Id 'x) (Id 'y)))
                     (With 'x (Num 5) (Call (Id 'f) (Num 4)))))
              (mtSub))
        (NumV 7))

  (test (eval
         (Call (With 'x (Num 3) (Fun 'y (GuessTE) (Add (Id 'x) (Id 'y)))) (Num 4))
         (mtSub))
        (NumV 7))

Step 3

Consider the following typechecking rule for with.

    Γ ⊢ e₁ : τ₁,  Γ[x←τ₁] ⊢ e₂ : τ₂
    ——————————————————————————————–
    Γ ⊢ {with {x e₁} e₂} : τ₂

Impliment this rule in your typecheck function. It is possible to do this without explicitly calling unify!. The skeleton of my solution is as follows:

    [(With id bound-exp body)
     (let* ([id-type ....]
            [new-env ....])
       (typecheck ....))]

Your completed interpreter should pass the following tests

  (test
   (resolve
    (typecheck
     (With
      'add3
      (Fun 'x (GuessTE) (Add (Id 'x) (Num 3)))
      (With
       'add1
       (Fun 'x (NumTE) (Add (Id 'x) (Num 1)))
       (With 'x (Num 3) (Call (Id 'add1) (Call (Id 'add3) (Id 'x))))))
     (mtEnv)))
   (NumT))

  (test
   (resolve
    (typecheck
     (With 'identity (Fun 'x (GuessTE) (Id 'x))
           (With 'foo (Fun 'x (NumTE) (Add (Id 'x) (Num 1)))
                 (Call (Call (Id 'identity) (Id 'foo)) (Num 123))))
     (mtEnv)))
   (NumT))

  (test
   (resolve
    (typecheck (With 'x  (Num 3)
                     (With
                      'f (Fun 'y (GuessTE) (Add (Id 'x) (Id 'y)))
                      (With 'x (Num 5) (Call (Id 'f) (Num 4)))))
               (mtEnv)))
   (NumT))

  (test
   (resolve
    (typecheck
     (Call (With 'x (Num 3) (Fun 'y (GuessTE) (Add (Id 'x) (Id 'y)))) (Num 4))
     (mtEnv)))
   (NumT))

Step 4 (Optional)

{with {x e₁} e₂}
;; is equivalent to
{call {fun {x} e₂} e₁}