API

Conditions

inference-error

General type inference error

cycle-detected

Signaled when a cycle is detected during a graph traversal and that graph cannot contain cycles.

node
An already seen node
Option Value
Allocation: instance
Type: nil
Initarg: :node
Readers: (cycle-detected-node)

typesystem-error

Signaled when a type system is defined incorrectly.

type-system
A top node of the type system
Option Value
Allocation: instance
Type: nil
Initarg: :type-system
Readers: (typesystem-error-system)

incorrect-definition

Signaled when type inference function is defined incorrectly.

arity-error

Signaled when a known function is called with wrong number of arguments.

actual-arity
Arity of a function seen in the code
Option Value
Allocation: instance
Type: alexandria:non-negative-fixnum
Initarg: :actual
Readers: (actual-arity)
expected-arity
Arity of a function in FNDB
Option Value
Allocation: instance
Type: alexandria:non-negative-fixnum
Initarg: :expected
Readers: (expected-arity)

unknown-function

Signaled when an unknown function is called in the code which needs to be type-checked.

unknown-literal

Signaled when S-expression looks like a literal but its type cannot be determined.

code
An expression which contains unknown literal
Option Value
Allocation: instance
Type: nil
Initarg: :code
Readers: (unknown-literal-code)

fndb-entry-exists

Signaled when you want to place an entry in fndb which tries to overwrite another existing entry.

parser-error

Signaled when parsing malformed code.

code
Parser error
Option Value
Allocation: instance
Type: nil
Initarg: :code
Readers: (parser-error-code)

typecheck-error

Signaled when a definition of a function contains type errors

varname
Name of the variable which holds a value of invalid type
Option Value
Allocation: instance
Type: nil
Initarg: :varname
Readers: (typecheck-error-varname)
actual
Actual type of a value stored in the variable
Option Value
Allocation: instance
Type: nil
Initarg: :actual
Readers: (typecheck-error-actual)
expected
Expected type of a value stored in the variable
Option Value
Allocation: instance
Type: nil
Initarg: :expected
Initform: nil
Readers: (typecheck-error-expected)

cannot-redefine

Signaled when an attempt to redefine a primitive function is made.

Type system

During to serapeum limitations, the type type-node and the corresponding constructor cannot be documented. Look at examples in this section.

type-node-ordernil

An order between two types. Can be :EQ, :LT, :GT or NIL. The latter is to indicate that there is no order between two types.

le(order)

Return t if order is either :eq or :lt, nil otherwise.

ge(order)

Return t if order is either :eq or :gt, nil otherwise.

type-node-order(top t1 t2)

Return :eq when t1 = t2, :lt when t1 < t2, :gt when t1 > t2 or nil otherwise. Top is the top type of the type system.

find-type-node(name type-node)

Find a type node A which has the name name and

A ⊂
type-node

flatten-type-graph(type-node)

Return a list of all types in a type system with the top node type-node.

check-type-system(type-node)

Return type-node if a type system for which this node is a top node is defined correctly, otherwise signal typesystem-error or just do not return control.

join(top t1 t2)

Return the join of types t1 and t2. Join t is the minimal type for which t1 ⊂ t and t2 ⊂ t. Top is the top type for the type system.

meet(top t1 t2)

Return the meet of types t1 and t2. Meet t is the maximal type for which t ⊂ t1 and t ⊂ t2. Top is the top type for the type system.

types-intersect-p(top t1 t2)

Return t if t1 ∧ t2 is not the bottom type, nil otherwise. Top is the top type of the type system.

print-graphviz-representation(top &optional (stream *standard-output*))

Print representation of a type system with the top node top in Graphviz format to the output stream stream.

Known functions

defknown

(db top names arguments-clause type-bindings-clause (&key (bottom-guard nil bottom-guard-p)) t0-cond-clauses &optional t1+-cond-clauses)

Add new known functions to the database db. Top is the top type of a type system. Names is a list of function names to be added. The new functions all have the same arity and the same functions \(T_0\), \(T_1\), etc.Arguments-clause is a form (arglist (result-variable top-variable narg-variable)) and contains some important variables which can be used in the body of functions \(T_i\). Arglist is a list of variables which are bound to types of arguments of the defined functions. Top-variable is bound to the top type of a type-system, result-variable is bound to type of the result of the defined function and narg-variable is bound to \(i-1\) in the body of \(T_i\) when \(i > 0\).Type-bindings-clause is an associative list with entries in the form (variable-name . type-name) which contains additional bindings of variables to types inside \(T_i\) functions.Bottom-guard argument must always be present and be either nil or name of a variable bound to the bottom type. If bottom-guard is not null then bottom guards will be present in \(T_i\) functions.T0-cond-clauses define a body of function T₀ in which bindings to top-variable and variables in arglist are in effect. This body is an explicit cond, so t0-cond-clauses may be like this

((condition-1 form-1)
 (condition-2 form-2)
 etc)

T0-cond-clauses must evaluate to a type. If bottom-guard is not nil an implicit conditional is inserted before all other conditionals in cond. This conditional checks if any of variables in arglist are bound to the bottom type, and if so the bottom type is returned. Also another conditional is inserted after all other conditionals which just returns the bottom type in any case.T1+-cond-clauses define a body of functions T₁, T₂, etc in which bindings to top-variable, res-variable, narg-variable and variables in arglist are in effect. This body is an explicit cond and must evaluate to a type, just like T0-cond-clauses.

For example the following code

(defknown *fndb* *type-system* (length)((x)(res top n))
  ((integer  . integer)
   (sequence . sequence)
   (bottom   . nil))
  (:bottom-guard bottom)
  ;; T₀
  (((types-intersect-p top x sequence) integer))
  ;; T₁
  (((ge (type-node-order top res integer))
    (meet top x sequence))))

creates a function T₀

(lambda (top x)
  (let ((integer  (find-type-node 'integer  top))
        (sequence (find-type-node 'sequence top))
        (bottom   (find-type-node nil       top)))
    (cond
      ((eq x bottom) bottom)
      ((types-intersect-p top x sequence) integer)
      (t bottom))))

and T₁

(lambda (top n res x)
  (assert (< n 1))
  (let ((integer  (find-type-node 'integer  top))
        (sequence (find-type-node 'sequence top))
        (bottom   (find-type-node nil       top)))
    (cond
      ((or (eq x   bottom)
           (eq res bottom))
       bottom)
      ((ge (type-node-order top res integer))
       (meet top x sequence))
      (t bottom))))

and adds a corresponding entry about the function length in *fndb*.

defknown*(db top names arg-types res-type)

Add functions with names contained in the list names to the function database fndb. This is a simplified SBCL-like version of DEFKNOWN. Everything what is known about added functions is that they take arguments of types arg-types and return a value of type res-type.

definitializer(db top name type)

Add a function with the name name which takes zero arguments and returns a value of type type to FNDB db

(definitializer db top name type)

is equivalent to

(defknown db top (name)(() res top n)
  ((type-var . type))
  (:bottom-guard nil)
  ((t type-var))
  ())

make-fndb(top-node)

Make a functions database for a type system with the top node top-node.

Code parsing

NB: This API is subject to change.

parse-expr(code &optional literal-initializers)

Parse an expression code and construct a control flow graph. Literal-initializers is an associative list which contains predicates as keys and initializer functions as values. When parse-code sees a term of the expression, it runs predicates in literal-initializers(in the order of appearance) on that term. If a predicate returns T then that term is considered as a literal and the corresponding initializer function is used to initialize a constant variable with a value of type of the literal. For example:

CL-USER> (parse-code '(+ x 3)) ; => Signals UNKNOWN-LITERAL
CL-USER> (type-inference-engine:parse-expr
          '(+ x 3)
          (list
           (cons #'integerp 'init/integer)))
((TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (2)(1)(#<TYPE-INFERENCE-ENGINE:STATEMENT X ← (INITIALIZE )>
                                                   #<TYPE-INFERENCE-ENGINE:STATEMENT RES567 ← (INITIALIZE )>
                                                   #<TYPE-INFERENCE-ENGINE:STATEMENT VAR568 ← (INITIALIZE )>))
 (TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (0)(2)(#<TYPE-INFERENCE-ENGINE:STATEMENT VAR568 ← (INIT/INTEGER )>))
 (TYPE-INFERENCE-ENGINE:FLAT-CONTROL-NODE (1)(0)(#<TYPE-INFERENCE-ENGINE:STATEMENT RES567 ← (+ X
                                                                                                 #:VAR568)>)))

This function returns a control flow graph which can be passed to infer-types.

compile-function(form fndb top-type &optional literal-initializers)

Infer types for a function defined by the defun form (just like in Common Lisp) and add this function to the database if it typechecks.

Example (tie/ex is a local nickname for the package type-inference-engine/example):

TIE-EXAMPLE> (tie:compile-function
 '(defun foo (x y)
   (let ((z (elt x (1+ y))))
     (* z (+ y z))))
  tie/ex:*fndb* tie/ex:*type-system*)
#S(TIE::SIMPLE-KNOWN-FUNCTION
   :NAME FOO
   :ARG-TYPES (#<TIE:TYPE-NODE SEQUENCE {102E78D253}>
               #<TIE:TYPE-NODE INTEGER {102E78D2B3}>)
   :RES-TYPE #<TIE:TYPE-NODE NUMBER {102E78D313}>)

Type inference

infer-types(db top graph)

Get the best safe program-wide varible->type mappings for a control flow graph in flat format returned by parse-expr. Graph is an internal representation of an expression in the form of parallel assignment statements. Db is a database of known functions and top is the top type of your type system. This function returns an array of variable->type mappings for each parallel assignment statement in the flattened control flow graph. The first element in that array is the most important as it corresponds to a fully evaluated expression.

Option	Value
Allocation:	instance
Type:	`nil`
Initarg:	`:node`
Readers:	`(cycle-detected-node)`