Project 4 – Type Inference

Microproject

To get more acquainted with core.logic, visit https://logic.puzzlebaron.com/ and generate a new logic puzzle. An easy one is good enough to play with. Solve it using core.logic as we did in class! Copy the puzzle narrative and constraints into your source file so you don’t lose them and I can see as well!

Main Project

Below I have defined the syntax and type semantics of a small programming language.

[:int-lit n] - integer literal
[:string-lit n] - string literal
[:bool-lit b] - boolean literal
[:var-ref x] - variable reference. Resulting type is the type of x in the environment. 
[:lambda x body] - lambda abstraction (function). Result is the type of the function.
[:apply e1 e2] - lambda (function) application. e2 must have appropriate type as input to e1 (e1 must be a lambda). Result is output type of e1.
[:if pred then else] - conditional; pred is boolean typed and then/else are expressions of the same type. Resulting type is the type of then/else.
[:let x e1 e2] - let binding, x gets the type of the result of evaluating e1. Resulting type is the type of evaluating e2. 

We will represent types using the following scheme:

[:int] - integer type
[:string] - string type
[:bool] - boolean type
[:fn t1 t2] - function from t1 to t2

You will use the Clojure core.logic library to perform type inference on expressions in the above language. For example:

(type-of [:bool-lit true]) 
=> ([:bool])
(type-of [:if [:bool-lit true] [:int-lit 100] [:int-lit 200]])
=> ([:int])
(type-of [:lambda 'x [:var-ref 'x]])
=> ([:fn _0 _0])
(type-of [:apply [:lambda 'x [:var-ref 'x]] [:bool-lit true]])
=> ([:bool])
(type-of [:lambda 'x [:if [:var-ref 'x] [:int-lit 1] [:int-lit 0]]])
=> ([:fn [:bool] [:int]])
(type-of [:lambda 'x [:if [:apply [:var-ref 'x] [:int-lit 1]] [:int-lit 0] [:int-lit 1]]])
=> ([:fn [:fn [:int] [:bool]] [:int]])

Input which has no inferrable type will just return an empty list. For example: (type-of [:if [:bool-lit true] [:int-lit 0] [:string-lit "abc"]]) has no inferrable type.

Bootstrap

To get you started, I’ve provided skeletons of necessary functions. The lookup function looks up a variable’s type in the environment, and the type-of function is the main entry point to your program (this one is done and you won’t need to modify it).

(defn lookup
  "Look up a variable's type in the environment"
  [env var type]
  ;; Assume env, var, and type are all lvars
  )

(defn infer-type 
  "Infer the type of expr in environment env, unifying with type"
  [env expr type]
  ;; Implement cases for each language construct.
  ;; Use lookup to get types of variables in the environment.
  )

(defn type-of 
  "Find the type of expr in the empty environment"
  [expr]
  (l/run 1 [q]
         (infer-type [] expr q)))

Hints:

• Represent the environment as a vector of [variable type] pairs. A hash-map may seem more convenient but is more difficult to use with core.logic.
• Start with the easy cases, be sure you can get the type of the literals, then move up to if and let, finally deal with functions.
• Functions and let both introduce a new variable, so will need to extend the environment. Think about just adding to the list and storing the result in a new lvar.
• core.logic leaves logic variables unbound if there is no value, so [:var-ref 'x] on its own should result in type _0, which is good (we’ll take unbound logic variables to be polymorphic type variables).
• The lookup function can be fiddly, be sure to write a tester for it.