type-inference-engine

Type inference problem

Suppose you have an expression in our Language of expressions which is internally translated to a graph of parallel assignment statements. Let \(V\) be a set of variables which appear in all those statements. A mapping \(V \rightarrow I \) maps variables \((v_1 \in V, v_2 \in V,\dots) \) to types of values bound to those variables \((t_1 \in I, t_2 \in I,\dots) \) in some point of time during evaluation of our expression. Suppose our execution graph has \(n\) vertices (statements), then let \([V \rightarrow I]^n\) be a mapping from variables to types before execution of all \(n\) statements in the graph. A mapping \([V \rightarrow I]^n\) is called safe if for types \((t'_{1_m}, t'_{2_m}, \dots)\) of values bound to variables \((v_1, v_2, \dots)\) during any possible control flow graph execution before execution of any statement \(m\) holds the following: \(t'_{1_m} \le t_{1_m}\), \(t'_{2_m} \le t_{2_m}\) etc. For example a mapping \([v_1 \rightarrow T, v_2 \rightarrow T, \dots]^n\) is always safe. The problem of type inference is to find a mapping \([V \rightarrow I]^n\) which is safe and as narrow as possible.

When your type system and database of known functions are created, you can start to infer types of expressions. Let's add a function infer-types to our tie-example package: 

(defun infer-types (expression)
  "Infer types in the expression using our type system and function
database."
  (let ((graph (tie:parse-expr expression)))
    (values
     (tie:infer-types *fndb* *my-system* graph)
     graph (tie:result-variable graph))))
(export 'infer-types)

Here we give it a try: 

CL-USER> (tie-example:infer-types '(1+ x))
#(#((#:RES483 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE REAL {100E6E3B73}>)
    (X . #<TYPE-INFERENCE-ENGINE:TYPE-NODE REAL {100E6E3B73}>))
  #((#:RES483 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE T {100E6E3BD3}>)
    (X . #<TYPE-INFERENCE-ENGINE:TYPE-NODE REAL {100E6E3B73}>)))
((TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (1)(1)(#<TYPE-INFERENCE-ENGINE:STATEMENT X ← (INITIALIZE )>
                                                   #<TYPE-INFERENCE-ENGINE:STATEMENT RES483 ← (INITIALIZE )>))
 (TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (0)(0)(#<TYPE-INFERENCE-ENGINE:STATEMENT RES483 ← (1+ X)>)))
#:RES483

Here the first returned value is our \([V \rightarrow I]^2\) mapping which corresponds to two parallel assignment statements which are returned as the second value. The third value is a variable which will hold the result of (1+ x). The first element of the first returned value is of interest here. It is a mapping \(V \rightarrow I\) which corresponds to the fully evaluated expression (1+ x). As you can see it takes a value of type REAL and returns a REAL. Here is another example:

#(#((X . #<TYPE-INFERENCE-ENGINE:TYPE-NODE REAL {100E6E3B73}>)
    (#:RES497 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE INTEGER {100E6E3B43}>)
    (#:VAR498 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE INTEGER {100E6E3B43}>))
  #((X . #<TYPE-INFERENCE-ENGINE:TYPE-NODE REAL {100E6E3B73}>)
    (#:RES497 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE T {100E6E3BD3}>)
    (#:VAR498 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE T {100E6E3BD3}>))
  #((X . #<TYPE-INFERENCE-ENGINE:TYPE-NODE REAL {100E6E3B73}>)
    (#:RES497 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE T {100E6E3BD3}>)
    (#:VAR498 . #<TYPE-INFERENCE-ENGINE:TYPE-NODE INTEGER {100E6E3B43}>)))
((TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (2)(1)(#<TYPE-INFERENCE-ENGINE:STATEMENT X ← (INITIALIZE )>
                                                   #<TYPE-INFERENCE-ENGINE:STATEMENT RES497 ← (INITIALIZE )>
                                                   #<TYPE-INFERENCE-ENGINE:STATEMENT VAR498 ← (INITIALIZE )>))
 (TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (0)(2)(#<TYPE-INFERENCE-ENGINE:STATEMENT VAR498 ← (FLOOR X)>))
 (TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (1)(0)(#<TYPE-INFERENCE-ENGINE:STATEMENT RES497 ← (1+ #:VAR498)>)))
#:RES497

The first element of the first returned value says that an expression (1+ (floor x)) takes a REAL argument x and returns an INTEGER.