Type systems have been studied extensively for programs, but not for specifications. This paper presents a type system for the increasingly important class of specification languages based on first-order constraints over relational data models, which have applications in software modelling, architectural description, web ontologies, access control, etc.

The system has rather a different flavour from a traditional type system. From a users perspective, the type of an expression is nothing more than another relational expression approximating its value. Computationally, a type is a relation, and types are constructed from relational operators. Type errors indicate semantic redundancies, in which expressions could be replaced by constants without affecting the meaning of the specification as a whole. The system supports subtypes and union types without the need for downcasts, and a form of overloading that decouples semantics from typing. Its simplicity, it turns out, derives from the power and simplicity of relational join.