11 Assignment 11: Relational Interpreter and 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. "

——John McCarthy, 1967

Assignment

Relational Interpreter

In the last week’s lecture, we learned how to miniKanrenize an interpreter

(defrel (valofo expr vars vals o)

(disj

(fresh (v)

(conj

(== `(quote ,v) expr)

(not-in-envo 'quote vars)

;; new constraint

(absento 'clos v)

(== v o)))

(fresh (a*)

(conj

(== `(list . ,a*) expr)

(not-in-envo 'list vars)

;; new constraint

(absento 'clos a*)

(valof-listo a* vars vals o)))

...))

In the first two branches, we added the following constraint: (absento 'clos v) and (absento 'clos a*).

If we remove the two constraints as below

(defrel (valofo expr vars vals o)

(disj

(fresh (v)

(conj

(== `(quote ,v) expr)

(not-in-envo 'quote vars)

;; this is commented out

;; (absento 'clos v)

(== v o)))

(fresh (a*)

(conj

(== `(list . ,a*) expr)

(not-in-envo 'list vars)

;; this is commented out

;; (absento 'clos a*)

(valof-listo a* vars vals o)))

;; the rest branches are kept unchanged

...))

• What result will we get for the following example?

  (run! 1 (p q)

  (conj

  (=/= p q)

  (valofo q '() '() p)

  (valofo p '() '() q)))

• Use the result of this example to explain why we need the two constraints above.

Type Inferencer

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

Your task in this assignment is to modify the type inference relation ⊢ in the class notes. This means that you need to add cases for new expressions that aren’t covered in ⊢ such as the plus + expression. Your extended inferencer should pass all of the test cases provided for the regular portion of the assignment. 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.

> (length (car (run 30 q (!- '() q '(Bool -> Nat)))))

30

> (length (car (run 30 q (!- '() q '(Nat -> (Nat -> Nat))))))

30

> (length (car (run 100 q

(fresh (e t)

(!- '() e t)

(== `(,e ,t) q)))))

100

> (length (car (run 100 q

(fresh (g e t)

(!- g e t)

(== `(,g ,e ,t) q)))))

100

> (length

(car (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 Bool Bool))

> (run* q (!- '() '(cons (zero? 1) (cons (zero? 1) (zero? 0))) q))

((pairof Bool (pairof Bool Bool)))

> (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 Bool 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!)

> (run* t (!- '() '(lambda (x) (zero? (car x))) t))

(((pairof Nat _0) -> Bool))

The above answer represents a function type that accepts a pair of a Nat and anything as input.

> (run* t (!- '() '((lambda (x) (zero? (car x))) (cons 0 1)) t))

(Bool)

> (run* t (!- '() '((lambda (x) (zero? (car x))) (cons 0 #f)) t))

(Bool)

> (run* t (!- '() '((lambda (x) (car x)) (cons (cons 0 0) #f)) t))

((pairof Nat Nat))

> (run* t (!- '() '((lambda (x) (zero? (car x))) (cons #f 0)) t))

()

> (run* t (!- '() '(lambda (x) (zero? (cdr x))) t))

(((pairof _0 Nat) -> Bool))

The above answer represents a function type that accepts a pair of anything and a Nat as input.

> (run* t (!- '() '((lambda (x) (zero? (cdr x))) (cons 0 1)) t))

(Bool)

> (run* t (!- '() '((lambda (x) (zero? (cdr x))) (cons 0 #f)) t))

()

> (run* t (!- '() '((lambda (x) (zero? (cdr x))) (cons #f 0)) t))

(Bool)

Just Dessert: Let Polymorphism

The hallmark feature of the Hindley-Milner type system is let polymorphism . You can understand more about let polymorphism by refering to Milner’s implementation of Algorithm W for this type system described in his original publication.

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

> (run* q

(!- '() '(let ([f (lambda (x) x)])

(if (f #t) (f (cons (f 4) 5)) (f (cons 5 (f 6)))))

q))

((pairof Nat Nat))

> (run* q

(!- '() '(let ([f (lambda (x) #t)])

(if #t (f (f 5)) (f #t)))

q))

(Bool)