Known functions

Now, suppose you have defined your type system \( I \) with properties described in the previous section. Now, you want to define some basic primitives to work with. Remember, the part of this section which describes known functions and literals is relevant for an example in the type-inference-engine/example package/system and you may wish to define your own set of functions.

Suppose you have a function \( f \) which takes \( n \) arguments. To add this function to your language as a known primitive you must define \( n + 1 \) supplementary functions \(T^f_0, T^f_1, \dots, T^f_n \). Here is their meaning:

\( T^f_0 \) takes \( n \) arguments \( t_1, t_2, \dots, t_n \) and returns the least type of a result of application of \(f\) to values of types \( t_1, t_2, \dots, t_n \). For example, \( T^{1+}_0\)(INTEGER) may be defined as INTEGER because 1+ maps integers to integers.
\( T^f_k \) takes \( n + 1 \) arguments \( t_0, t_1, \dots, t_k, \dots, t_n \) and returns the least type \( t \) in a statement \( v_0 \leftarrow f(v_1, \dots, v_k, \dots, v_n) \) such that \(t \le t_k\) and variables \(v_i\) are bound to values of types \(t'_i\) after execution of that statement, where \(t'_i = t_i\) if \(i \ne k\) and \(t'_i = t\) otherwise. This can be hard to understand, but intuitively \(T^f_i, i>0\) are used to narrow a type of \(i\)-th argument when a type of the result is known and \(T^f_0\) is used to determine a type of the result. For example \( T^{1+}_1\)(INTEGER, NUMBER) may be defined as INTEGER and \(T^{1+}_1\)(SEQUENCE, NUMBER) is NIL

Functions \(T^f_i\) must be monotonic with respect to all arguments to guarantee execution of the type inference algorithm in finite time. An unary function \(f\) is monotonic if for any \(x, y: x \le y \), \(f(x) \le f(y)\) follows. To learn how to define known functions in type-inference-engine look at defknown macro in API section. Note, that you need to be careful when defining \(T^f_i\) functions, but not very careful: defknown will signal an error if you violate monotinicity of one of the functions.

Being in our previously defined package, tie-example, let's create a database of known functions and add a function 1+ to it, which adds 1 to its only argument:

(defparameter *fndb* (tie:make-fndb *my-system*))
(tie:defknown *fndb* *my-system* (1+)
    ;; The next form defines some important bindings inside T_i
    ;; functions. It says that a type of the result will be available in
    ;; the variable RES and N can take integer values from 0 to a-1,
    ;; where a is arity of the defined function. N correspond to the
    ;; function T_{N+1}. In the case of 1+, we just need to define T₁
    ;; and hence N is always 0 and can be ignored. TOP is just bound to
    ;; *MY-SYSTEM*. X is a type of an argument of 1+.
    ((x)(res top n))
  ;; Bind some variables (on the left side) to needed types (on the right side)
  ((real   . real)
   (bottom . nil))
  ;; This will be explained later
  (:bottom-guard nil)
  ;; Define T₀ function. The following form is an implicit cond form
  (;; If we pass a value of type t ≤ REAL, then 1+ returns a value of
   ;; type t
   ((tie:le (tie:type-node-order top x real)) x)
   ;; Now, if t ≥ REAL (i.e. T), then 1+ returns a value of type REAL
   ((tie:ge (tie:type-node-order top x real)) real)
   ;; Otherwise, 1+ returns a value of type BOTTOM (i.e. it does not
   ;; return anything at all and, for example, signals an error or
   ;; causes your PC to explode).
   (t bottom))
  ;; Here we define T₁. The following form is also an implicit cond.
  ((t
    ;; A type of an argument always can be narrowed to X ∧ RES ∧ REAL
    (tie:meet top (tie:meet top res x) real))))

Here (:bottom-guard nil) does not produce any effect, but if you replace nil with a variable which is bound to the bottom type (in our case, bottom), two other checks will be added to \(T_i\) functions. Firstly, \(T_i\) functions will always check if any of its arguments is bottom, and if yes, they will immediately return bottom. Secondly, after all other cond cases are checked and none of them pass, \(T_i\) functions will return bottom. Setting (:bottom-guard bottom) is a good practice and saves you from writing boilerplate code and making errors. Let's add another function, floor, which takes a number and rounds it to a value of type INTEGER:

(tie:defknown *fndb* *my-system* (floor)((x)(res top n))
  ;; Bind some variables to types which we need
  ((real    . real)
   (integer . integer)
   (bottom  . nil))
  (:bottom-guard bottom)
  ;; Define T₀ function.
  (;; The case x = BOTTOM is already checked by a bottom guard.
   ;; Here if X intersects with REAL (i.e. X = INTEGER, REAL or T)
   ;; then FLOOR returns a value of type INTEGER.
   ((tie:types-intersect-p top x real) integer)
   ;; All other cases (e.g. x = STRING) are covered by a bottom guard
   )
  ;; Define T₁.
  (((tie:ge (tie:type-node-order top res integer))
    ;; If a result is of type T, REAL or INTEGER, when narrow X to X ∧
    ;; REAL
    (tie:meet top x real))))

In the next section we will learn the problem solved by type-inference-engine and see what can be done with our toy type system and these two known functions.