type-inference-engine

This is a simple type inference engine based on the paper by Marc Kaplan and Jeffrey Ullman (see below). This engine features custom type systems based on subtyping, a simple language based on S-expressions and allows you to create basic functions to start type inferece with. There are some examples below. These examples use a toy type system and a set of known functions from type-inference-engine/example package. Do not be afraid if you do not understand them, they will be explained in futher sections.

(defpackage examples
  (:use #:cl)
  (:local-nicknames (#:tie    #:type-inference-engine)
                    (#:tie/ex #:type-inference-engine/example)))
(in-package :examples)

(tie/ex:infer-types '(+ x (sin y))) ;; =>
((Y . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (#:RES486 . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (X . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (#:VAR487 . #<TIE:TYPE-NODE NUMBER {10155D1173}>))
#:RES486
;; The first value is a mapping from variables used in the expression to their
;; corresponding types. Variables which begin with #:VAR are intermediate
;; variables which do not appear in the expression explicitly. The second value
;; is a name of variable which contains the result of evaluation of the
;; expression. All in all, the output of TIE/EX:INFER-TYPES can be read as: the
;; expression takes two arguments of type NUMBER and returns a result of type
;; NUMBER.

(tie/ex:infer-types '(1+ (sin (floor y)))) ;; =>
((Y . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (#:VAR501 . #<TIE:TYPE-NODE INTEGER {10155D1113}>)
 (#:RES499 . #<TIE:TYPE-NODE FLOAT {10155D1143}>)
 (#:VAR500 . #<TIE:TYPE-NODE FLOAT {10155D1143}>))
#:RES499
;; Here Y becomes rounded with FLOOR before SIN is calculated. As a
;; result the most narrow type of (SIN (FLOOR Y)) is FLOAT (which is a
;; type for real numbers in floating point representation), not NUMBER
;; (which is a type for numbers in general). Hence the whole
;; expression takes an argument of type NUMBER and returns a FLOAT.

(tie/ex:infer-types '(+ (length y)(- x (floor (elt y x))))) ;; =>
((#:VAR517 . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (Y . #<TIE:TYPE-NODE SEQUENCE {10155D10B3}>)
 (X . #<TIE:TYPE-NODE INTEGER {10155D1113}>)
 (#:VAR516 . #<TIE:TYPE-NODE INTEGER {10155D1113}>)
 (#:RES513 . #<TIE:TYPE-NODE INTEGER {10155D1113}>)
 (#:VAR514 . #<TIE:TYPE-NODE INTEGER {10155D1113}>)
 (#:VAR515 . #<TIE:TYPE-NODE INTEGER {10155D1113}>))
#:RES513
;; Here the most narrow type for Y is a SEQUENCE (one dimensional array-like
;; collection). X can only be an INTEGER as it serves a role of an index into Y
;; in (ELT Y X). The result has a type INTEGER, because both LENGTH and FLOOR
;; return an INTEGER.

(tie/ex:infer-types '(+ x (length x))) ;; =>
((#:RES530 . #<TIE:TYPE-NODE NIL {10155D0F93}>)
 (X . #<TIE:TYPE-NODE NIL {10155D0F93}>)
 (#:VAR531 . #<TIE:TYPE-NODE NIL {10155D0F93}>))
#:RES530
;; The expression (+ x (length x)) maps values of type NIL to NIL which is a
;; special empty type, i.e. there are no such values for which the expression
;; can be evaluated. This is because X cannot be a number and a sequence at the
;; same time.

(tie/ex:infer-types '(if x (1+ (floor y))(sin z))) ;; =>
((Y . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (#:VAR549 . #<TIE:TYPE-NODE INTEGER {10155D1113}>)
 (Z . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (#:RES546 . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (X . #<TIE:TYPE-NODE BOOLEAN {10155D11A3}>)
 (#:VAR547 . #<TIE:TYPE-NODE INTEGER {10155D1113}>)
 (#:VAR548 . #<TIE:TYPE-NODE NUMBER {10155D1173}>))
#:RES546
;; This expression take a BOOLEAN x and returns a value of type NUMBER. IF is an
;; ordinary function in this example, i.e. it evaluates all its arguments and
;; returns either the second or the third argument depending on conditional.

(tie/ex:infer-types '(if (numberp (1+ x)) 3.2 4)) ;; =>
((X . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (#:VAR565 . #<TIE:TYPE-NODE NUMBER {10155D1173}>)
 (#:RES561 . #<TIE:TYPE-NODE FLOAT {10155D1143}>)
 (#:VAR562 . #<TIE:TYPE-NODE TRUE {10155D1023}>)
 (#:VAR563 . #<TIE:TYPE-NODE FLOAT {10155D1143}>)
 (#:VAR564 . #<TIE:TYPE-NODE INTEGER {10155D1113}>))
#:RES561
;; Here is an example of control flow analysis: (1+ X) is certainly a number, so
;; the result is of type FLOAT (the value 4 is never returned).

(tie/ex:-> (%fac)(integer integer) integer)
(tie/ex:compile-function
 '(defun %fac (acc n)
   (if (zerop n) acc
       (%fac (* n acc)(1- n))))) ;; =>
#S(TIE::SIMPLE-KNOWN-FUNCTION
   :NAME %FAC
   :ARG-TYPES (#<TIE:TYPE-NODE INTEGER {10155D1113}>
               #<TIE:TYPE-NODE INTEGER {10155D1113}>)
   :RES-TYPE #<TIE:TYPE-NODE INTEGER {10155D1113}>)
(tie/ex:compile-function
 '(defun fac (n)(%fac 1 n))) ;; =>
#S(TIE::SIMPLE-KNOWN-FUNCTION
   :NAME FAC
   :ARG-TYPES (#<TIE:TYPE-NODE INTEGER {10155D1113}>)
   :RES-TYPE #<TIE:TYPE-NODE INTEGER {10155D1113}>)
(tie/ex:compile-function
 '(defun c (n m)
   (/ (fac n)(* (fac m)(fac (- n m)))))) ;; =>
#S(TIE::SIMPLE-KNOWN-FUNCTION
   :NAME C
   :ARG-TYPES (#<TIE:TYPE-NODE INTEGER {10155D1113}>
               #<TIE:TYPE-NODE INTEGER {10155D1113}>)
   :RES-TYPE #<TIE:TYPE-NODE FLOAT {10155D1143}>)
;; Here custom functions FAC (factorial) and C (binomial coefficient) are
;; created. If you are defining a recursive function, it has to be declared
;; first (i.e. type-inference-engine works only as a type checker here).
   

For more understanding what is going on here, visit language of expressions and type system sections.

Reference to the paper: Marc A. Kaplan and Jeffrey D. Ullman. 1978. A general scheme for the automatic inference of variable types. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages (POPL '78). Association for Computing Machinery, New York, NY, USA, 60–75. https://doi.org/10.1145/512760.512768