Although object-oriented subtyping has been efficiently resolved by compilers for years, this paper shows how subtyping in Extensible Markup Language (XML)-centric functional languages can be done with a SAT solver. It gives a tested formal specification for an efficient algorithm if such exists. The paper is the result of a decade of research, which is documented in the references. It will mainly interest graduate students and professors working in type theory and logic.

A SAT solver is a subprogram that either finds values for variables in a logical formula that satisfy it (make it true) or reports that they don’t exist. The worst-case time for all known SAT solvers grows exponentially with the size of the formula. The author’s paradigm is: 1) clearly define the property; 2) encode the property as a logical formula; 3) tune the formula; and 4) use a SAT solver on the formula. These steps are applied to testing if one LISP-like data type is a subtype of another one. The paper uses semantic subtyping. This is where one type is defined to be a subtype of another if all data of one type are elements of the other type. The types include function types, types defined by parametric (not object-oriented) polymorphism, and types defined by recursion. The authors’ logical model handles all of these. The resulting software has been tested and works well. They show that it has the same complexity as the SAT solver used.