Numerous proposals have been made concerning typing systems for Prolog for the purposes of program analysis, correctness checking, etc. Analysis-based typing systems are typically lattice-based, following from their need to compare types to understand whether one type includes another, or from the need to determine the most specific type that is more general than two types. In addition the ISO standard specifies various types of allowable input or output arguments for various predicates.
Version 3.0 of XSB has the following approach to program typing. Typing in an XSB program is done through a type lattice, generated by primitive type elements. How a primitive type is defined is somewhat separate from how it is used by a type lattice. For our purposes we assume that each 1-ary type element is defined by a predicate of arity 1 that is written in a pure enough style so that its success or failure does not depend on the state of XSB or of any external state. Whether these types are recursive or not has no bearing on the type lattice. For instance, integer or listOfAtoms are primitive type elements. Similarly, variable, ground are also type elements. We say that a given term Term satisfies a primitive type element t if t(Term) succeeds. Given primitive type elements, complex type elements can be formed using the boolean operations, and, or and not. As an example, integer or not(listOfAtoms) is a non-primitive type element. There is also a product operation (,) on type elements, so that variable, integer or not(listOfAtoms) is a product of the above two types. Satisfiability is extended to complex type elements in the obvious manner, and an n-ary typle of terms satisfies a n-ary product type if each argument in the tuple satisfies the corresponding argument of the product type.
The above description is not yet suitable for a type system as it could not determine, for instance, that integer is a subtype of number. To determine this, an explicit inclusion statement can be made indicating that one type is included in another. Thus given two elements in a type lattice with inclusion statements, determining whether one element is more specific than another can be done using techniques for propositional satisfiability or stable model generation.
From an implementational level, types can be defined using the Cold Dead Fish (CDF) package and inclusion can be detected using the CDF theorem prover or XSB's Smodels interface. However, for the purposes in this section we use type elements to define inputs and outputs of predicates, via usage statements. A usage statement for an n-ary predicate p/n consists of an n-ary product of primitive types that should be satisfied on a call to p/n along with a n-ary product of primitive types that should hold on success of p/n given the types that hold at call. If both the the product types hold, the usage statement is satisfied. Each successful call to p/n should satisfy one of the usage statements.
As defined, usage statements are very general: they can check not only traditional Prolog types (atom, integer, etc), but also non-Prolog types, such as the fact that the input to a given argument should be a positive integer, and even instantiation patterns. For the various predicates defined in this section, we use the following conventions for usages and error reporting. domain, type and instantiation errors arise from the failure of an argument of a predicate to satisfy the corresponding type element in the input term of the usage statements. All of these could be called type errors given the system described above. However to (partially) conform to the ISO standard, we reserve the instantiation error to mean failure that occurs when an argument does not satisfy a type in a boolean lattice generated by var and ground. A type error occurs when an argument does not satisfy a type in a boolean lattice generated by other ISO types, such as integer, atom, etc. A domain error arises from other such errors. We note that in certain cases, our designation of an error type may differ from the ISO standard.