Assignment 11: Type Inference

It is reasonable to hope that the relationship between computation and logic in the next century will be as fruitful as that between calculus and physics in the last.

Assignment

Your assignment this week is to complete your own type inferencer and inhabiter in miniKanren. You should start with a11.rkt, the inferencer we began on Tuesday, and add to it +, not, lambda, fix, variables, and application. To be clear, your solution should not involve pmatch at all; it should be written entirely in miniKanren. You can use the a11-student-tests.rkt file to test your file.

Your extended inferencer should pass all of the test cases provided for the regular portion of the assigment. Honors students and real go-getters should adjust the expectations accordingly.

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 -> Boole).
  • 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.
  • In the fix and lambda lines, you must ensure that the symbols fix and lambda not appear as variables in the type environment. This is to avoid shadowing. You should use the not-in-envo operator provided to you.
  • In the lambda line, you should ensure that the binder (formal parameter to the function) is a symbol.
  • Your not operator should expect only expressions which type at Boole, unlike not in Racket.
> (run* (q) (!- '() #t q))
(Boole)
> (run* (q) (!- '() 17 q))
(Nat)
> (run* (q) (!- '() '(zero? 24) q))
(Boole)
> (run* (q) (!- '() '(zero? (sub1 24)) q))
(Boole)
> (run* (q)
    (!- '() '(zero? (sub1 (sub1 18))) q))
(Boole)
> (run* (q)
    (!- '()  '(lambda (n) (if (zero? n) n n)) q))
((Nat -> Nat))
> (run* (q)
    (!- '() '((lambda (n) (zero? n)) 5) q))
(Boole)
> (run* (q)
    (!- '() '(if (zero? 24) 3 4) q))
(Nat)
> (run* (q)
    (!- '() '(if (zero? 24) (zero? 3) (zero? 4)) q))
(Boole)
> (run* (q)
    (!- '() '(lambda (x) (sub1 x)) q))
((Nat -> Nat))
> (run* (q)
    (!- '() '(lambda (a) (lambda (x) (+ a x))) q))
((Nat -> (Nat -> Nat)))
> (run* (q)
    (!- '() '(lambda (f)
               (lambda (x)
                 ((f x) x)))
         q))
(((_.0 -> (_.0 -> _.1)) -> (_.0 -> _.1)))
> (run* (q)
    (!- '() '(sub1 (sub1 (sub1 6))) q))
(Nat)
> (run 1 (q)
    (fresh (t)
      (!- '() '(lambda (f) (f f)) t)))
()
> (length (run 20 (q)
             (fresh (lam a b)
               (!- '() `((,lam (,a) ,b) 5) 'Nat)
               (== `(,lam (,a) ,b) q))))
20
> (length (run 30 (q) (!- '() q 'Nat)))
30
> (length (run 30 (q) (!- '() q '(Nat -> Nat))))
30
> (length (run 500 (q) (!- '() q '(Nat -> Nat))))
500
;; At this point, stop and take a look at maybe the 500th 
;; program you generate
;; (last (run 500 (q) (!- '() q '(Nat -> Nat))))
;; You should be amazed at how quickly it's generating them.
;; If it isn't fast, consider reordering your clauses. 
> (length (run 30 (q) (!- '() q '(Boole -> Nat))))
30
> (length (run 30 (q) (!- '() q '(Nat -> (Nat -> Nat)))))
30
> (length (run 100 (q)
             (fresh (e t)
               (!- '() e t)
               (== `(,e ,t) q))))
100
> (length (run 100 (q)
             (fresh (g e t)
               (!- g e t)
               (== `(,g ,e ,t) q))))
100
> (length
   (run 100 (q)
     (fresh (g v)
       (!- g `(var ,v) 'Nat)
       (== `(,g ,v) q))))
100
> (run 1 (q)
       (fresh (g)
	 (!- g
	      '((fix (lambda (!)
		       (lambda (n)
			 (if (zero? n)
			     1
			     (* n (! (sub1 n)))))))
		5)
	      q)))
(Nat)
> (run 1 (q)
       (fresh (g)
	 (!- g
	      '((fix (lambda (!)
		       (lambda (n)
			 (* n (! (sub1 n))))))
		5)
	      q)))
(Nat)
>

Brainteaser

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.

> (run* (q) (!- '() '(cons (zero? 1) (zero? 0)) q))
((pairof Boole Boole))
> (run* (q) (!- '() '(cons (zero? 1) (cons (zero? 1) (zero? 0))) q))
((pairof Boole (pairof Boole Boole)))
> (run* (t) (!- '() '(lambda (x) (cons x x)) t))
((_.0 -> (pairof _.0 _.0)))
> (run* (t) (!- '() '(lambda (x) (lambda (y) (cons (zero? x) (+ x y)))) t))
((Nat -> (Nat -> (pairof Boole Nat))))

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

;; a function that accepts a pair of an Nat and anything
> (run* (t) (!- '() '(lambda (x) (zero? (car x))) t))
(((pairof Nat _.0) -> Boole))
> (run* (t) (!- '() '((lambda (x) (zero? (car x))) (cons 0 1)) t))
(Boole)
> (run* (t) (!- '() '((lambda (x) (zero? (car x))) (cons 0 #f)) t))
(Boole)
> (run* (t) (!- '() '((lambda (x) (zero? (car x))) (cons #f 0)) t))
()
;; a function that accepts a pair of anything and an Nat
> (run* (t) (!- '() '(lambda (x) (zero? (cdr x))) t))
(((pairof _.0 Nat) -> Boole))
> (run* (t) (!- '() '((lambda (x) (zero? (cdr x))) (cons 0 1)) t))
(Boole)
> (run* (t) (!- '() '((lambda (x) (zero? (cdr x))) (cons 0 #f)) t))
()
> (run* (t) (!- '() '((lambda (x) (zero? (cdr x))) (cons #f 0)) t))
(Boole)

Just Dessert: Let Polymorphism

Extend the type inferencer so that the following type is inferred:

> (run* (q)
    (!-o '() '(let ([f (lambda (x) x)])
                       (if (f #t) (f (cons (f 4) 5)) (f (cons 5 (f 6)))))
         q))
((pairof Nat Nat))
 

lp-a1.txt · Last modified: 2014/04/12 01:16 by jhemann