Assignment 11: Type Inference
You must use this updated implementation of miniKanren:
mk.scm
mkneverequalo.scm
mkdefs.scm
The new implementation of miniKanren includes disequality constraints of the form
(=/= x y), which assert that x and y can never have the same value. A single disequality constraint is used in the lookupo helper relation to prevent misleading duplicate answers. Since lookupo is given to you, it is not critical that you understand disequality constraints for this assignment; if you are curious, please see the =/= tests at the beginning of mktests.scm.
When you are finished, submit a single file named a11.scm to Vincent.
Your extended inferencer should pass all of the test cases provided with the inferencer.
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.
You should closely examine the type inferencer tests provided, and remember that the inferencer expects expressions to be tagged. For example, the expression ((lambda (x) x) 5) would be represented as (app (lambda (x) (var x)) (intc 5)). You may wish to use the parser provided with the inferencer. You may also wish to examine the edited Scheme REPL transcript from yesterday's lecture.
Important hints: the type of a lambda expression is an arrow type. For example, the type of (lambda (x) (sub1 (var x))) is (-> int int), while the type of (lambda (x) (zero? (var x))) is (-> int bool).
Also, remember that 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.