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.

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.

You may find the following "old-school" notes from Dan, Will, and David of some use.

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) >

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)

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))