Introduction

This tutorial consists of a simulated test, with the second question from a previous final exam, and the second in the style of previous midterm questions. You are given a single skeleton file for both questions, and you should hand the single modified file to the handin server before 11:30 on 2024-03-13. Unlike assignments, there is no requirement for test coverage, but the handin server will still limit you to 120 characters on a line.

IFLANG

Introduction

The TIFLANG algebraic data type represents abstract syntax for a toy language with lexically scoped functions and a new language feature that combines if and lambda. To reduce the amount of code, parsing is omitted here, and all code samples are given in abstract syntax.

The form

(iLamE 'arg <body0> <body1>)

is a cross between an if expression and a function value. More precisely, if evaluates as

(lamE 'arg <body0>)

if arg is 0, and as

(lamE 'arg <body1>)

otherwise. As an example, the following evaluates to 1/3

(let1E
 'f
 (iLamE 'x (varE 'x) (divE (numE 1) (varE 'x)))
 (plusE (appE (varE 'f) (numE 3)) (appE (varE 'f) (numE 0))))

Question

The provided skeleton contains a skeleton of a recursive typechecker for TIFLANG. Update the function typecheck to correctly handle iLamE and pass the following tests.

(module+ test
  (define (check iflang)
    (typecheck iflang mt-type-env))

  (test (check
         (appE
          (appE
           (lamE 'x (arrowTE (numTE) (arrowTE (numTE) (numTE))) (appE (varE 'x) (numE 1)))
           (lamE 'x (numTE) (iLamE 'y (numE -1) (plusE (varE 'x) (varE 'y)))))
          (numE 123)))
        (numT))

  (test (check
         (let1E 'f (iLamE 'x (varE 'x) (divE (numE 1) (varE 'x)))
                (plusE (appE (varE 'f) (numE 3)) (appE (varE 'f) (numE 0)))))
        (numT))

  (test (check
         (let1E 'x (numE 3)
                (let1E 'f (iLamE 'y (varE 'x) (divE (varE 'x) (varE 'y)))
                       (let1E 'x (numE 5)
                              (plusE (appE (varE 'f)
                                           (numE 3)) (appE (varE 'f) (numE 0)))))))
        (numT))

  (test/exn
   (check (iLamE 'x (numE 0) (lamE 'x (numTE) (varE 'x)))) "no type")

  (test/exn
   (check
    (appE (iLamE 'x (numE 0) (lamE 'x (numTE) (varE 'x))) (numE 0)))
   "no type")

  (test/exn
   (check
    (appE (iLamE 'x (numE 0) (numE 1)) (lamE 'x (numTE) (varE 'x))))
   "no type")
  )

Unification

In this question you are asked to write a much simplified version of the unify! function from the lectures. Instead of an expression tree, you are asked to unify two lists with the following type:

(define-type-alias BoxList (Listof (Boxof (Optionof Number))))

You should complete the given skeleton for unify-lists! so that the following tests pass:

(module+ test
  (let* ([l1 (list (box (some 0)) (box (some 1)) (box (none)))]
         [l2 (list (box (some 0)) (box (none)) (box (some 2)))]
         [result (list (box (some 0)) (box (some 1)) (box (some 2)))])
    (begin
      (unify-lists! l1 l2)
      (test l1 result)
      (test l2 result)))
  (test/exn (unify-lists! (list (box (some 1)) (box (none)))
                          (list (box (none)))) "length mismatch")
  (test/exn (unify-lists! (list (box (some 1)))
                          (list (box (some 2)))) "value mismatch"))