UNB/ CS/ David Bremner/ teaching/ cs4613/ tutorials/ CS4613 Tutorial 7

Background

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

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. Extend the parser for with using e.g.

[(s-exp-match? `(with (SYMBOL ANY) ANY) sx)
 (let* ([def (sx-ref sx 1)]
        [id (s-exp->symbol (sx-ref def 0))]
        [val (parse (sx-ref def 1))]
        [expr (px 2)])
   (With id val expr))]

Step 2

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

Add the following tests to your interpeter.

      (test (run `{with {add3 {fun {x : ?} {+ x 3}}}
                        {with {add1 {fun {x : ?} {+ x 1}}}
                              {with {x 3}
                                    {add1 {add3 x}}}}})
            (NumV 7))
      (test (run `{with {identity {fun {x : ?} x}}
                        {with {foo {fun {x : ?} {+ x 1}}}
                              {{identity foo} 
                               123}}})
            (NumV 124))

      (test (run `{with {x 3}
                {with {f {fun {y : ?} {+ x y}}}
                  {with {x 5}
                    {f 4}}}}) 
            (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/type
   `{with {add3 {fun {x : ?} {+ x 3}}}
          {with {add1 {fun {x : ?} {+ x 1}}}
                {with {x 3}
                      {add1 {add3 x}}}}}

   (NumT))

  (test/type
   `{with {identity {fun {x : ?} x}}
          {with {foo {fun {x : ?} {+ x 1}}}
                {{identity foo}
                 123}}}
   (NumT))

 (test/type
  `{with {x 3}
         {with {f {fun {y : ?} {+ x y}}}
               {with {x 5}
                     {f 4}}}}
   (NumT))

Step 4 (Optional)

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