Assignment 11: Type Inference

'Contrariwise,' continued Tweedledee, 'if it was so, it might be; and if it were so, it would be; but as it isn't, it ain't. That's logic.'

Make sure to get the latest versions of a12.scm, mk.scm, and minikanren.scm, which contains the miniKanren arithmetic system, among other useful tools.

Extend the given type inferencer with the definitions of sub1, not and if, as well as, lambda expressions and application as presented in lecture. Your extended inferencer should pass all of the test cases provided with a12.scm. Be sure and get the most up-to-date version of mk.scm.

To avoid divergence for some of the tests, you must carefully order goals within a conjunction to “fail fast”. Keep these rules in mind:

• Simple unifications should come before recursive calls. For example, (== 5 x) should come before (foo y z).
• Recursive calls with instantiated arguments should come before recursive calls with uninstantiated arguments.

For example, (foo `(,x ,y ,z) 5) should come before (foo u v), assuming x, y, z, u, and v are fresh.

Other important hints for this assignment:

• The type of a lambda expression is an arrow type. For example, the type of (lambda (x) (sub1 x)) is (-> nat nat), while the type of (lambda (x) (zero? x)) is (-> nat bool).
• Gamma is a type environment, similar to the environment used in our interpreter. The only difference is that a type environment binds lexical variables to types instead of values.
• Remember to require that lambda not be in the environment.
• You can complete this portion of the assignment by adding fewer than 30 lines of code to the provided file.

Extend your type inferencer to recognize pair types. You will need to add support for a pairof type to the type inferencer such that the following tests pass.

(test "pair-1"
  (run* (q) (!-o '() '(cons (zero? 1) (zero? 0)) q))
  '((pairof bool bool)))
 
(test "pair-2"
  (run* (q) (!-o '() '(cons (zero? 1) (cons (zero? 1) (zero? 0))) q))
  '((pairof bool (pairof bool bool))))
 
(test "pair-3"
  (run* (t) (!-o '() '(lambda (x) (cons x x)) t))
  '((-> _.0 (pairof _.0 _.0))))
 
(test "pair-4"
  (run* (t) (!-o '() '(lambda (x)
                               (lambda (y) (cons (zero? x) (+ x y)))) t))
  '((-> nat (-> nat (pairof bool nat)))))

Once you've done the above, add two more lines to the type inferencer such that the following tests pass. (By the way, these two new lines will be quite similar!)

(test "car-1"
  ;; a function that accepts a pair of an nat and anything
  (run* (t) (!-o '() '(lambda (x)
                               (zero? (car x))) t))
  '((-> (pairof nat _.0) bool)))
 
(test "car-2"
  (run* (t) (!-o '() '((lambda (x)
                               (zero? (car x))) (cons 0 1)) t))
  '(bool))
 
(test "car-3"
  (run* (t) (!-o '() '((lambda (x)
                               (zero? (car x))) (cons 0 #f)) t))
  '(bool))
 
(test "car-4"
  (run* (t) (!-o '() '((lambda (x)
                               (zero? (car x))) (cons #f 0)) t))
  '())
 
(test "cdr-1"
  ;; a function that accepts a pair of anything and an nat
  (run* (t) (!-o '() '(lambda (x)
                               (zero? (cdr x))) t))
  '((-> (pairof _.0 nat) bool)))
 
(test "cdr-2"
  (run* (t) (!-o '() '((lambda (x)
                               (zero? (cdr x))) (cons 0 1)) t))
  '(bool))
 
(test "cdr-3"
  (run* (t) (!-o '() '((lambda (x)
                               (zero? (cdr x))) (cons 0 #f)) t))
  '())
 
(test "cdr-4"
  (run* (t) (!-o '() '((lambda (x)
                               (zero? (cdr x))) (cons #f 0)) t))
  '(bool))