Assignment 10: Type Inference

Revisions and Clarifications

Make sure you have the miniKanren implementation with never-equalo:

Part I

  • Identify the type of each of the expressions below and place them in a comment at the beginning of your submission file. Note: You may be tempted to simply plug these into the inferencer and let it do the work for you. However, you may see some problems very similar to these on the exam and this would be an excellent time to do some practice. Of course you should verify the correctness of your answers by using the inferencer.

    1. #f
    2. (+ 5 6)
    3. (if (zero? 0) (+ 5 4) (sub1 8))
    4. (lambda (x) (+ x x))
    5. (lambda (x) (lambda (y) (+ x y)))
    6. (lambda (x) (lambda (y) (zero? (y (sub1 x)))))
    7. (if ((lambda (x) #t) 9) 5 8)
    8. ((lambda (x) x) (+ 5 7))
    9. ((lambda (x) (sub1 x)) ((lambda (y) (+ 5 ((lambda (z) z) 6))) 8))
    10. (car (cons (cons 3 4) #t))

    Part II

  • Download the type inferencer that you were given in lecture this week. The inferencer currently supports:
  • Extend the inferencer to support the following operations: You can find inference rules for the last four operations here. You also must implement the lookup helper relation, described below. Your inferencer should pass all of the tests at the bottom of the file. Each test should terminate in under ten seconds when using Petite Chez Scheme. Remember to choose the ordering of your goals carefully (for example, calls to == should come before calls to recursive goals).

    lookup

    The lookup helper relation is similar to the apply-env function used in your interpreter. apply-env looks up the value of a variable in an environment, which we might represent as an association list:

    (apply-env 'x '((x . 5) (y . 6) (x . 3)) => 5.

    Similarly, the lookup relation succeeds when x appears in the type environment gamma, associating x with some type t:

    (run* (q) (lookup 'y '((y . bool) (z . int) (y . int)) q)) => (bool)

    Important: even though y appears twice in the type environment, the run* expression returns (bool) instead of (bool int). In order words, lookup must handle variable shadowing.

    Hint: if you are having trouble implementing lookup, you might begin by translating the apply-env function into miniKanren, using the transformations from the previous assignment.

    Optional Challenge Question 1

    Add letrec to your type inferencer. To simplify the problem, assume that the right-hand-side of each letrec binding is a lambda expression of one argument.

    Optional Challenge Question 2

    Add ML-style polymorphic let to your type inferencer. Polymorphic let is described in Exercise 7.28 on page 273 of Essentials.

    Revisions and Clarifications