A datatype declaration allows the concise declaration of a sort together with constructor and selector functions, with some implicit axioms relating the constructors and selectors.In a practical specification language, it is important to be able to avoid tedious, repetitive patterns of specification, as these are likely to be carelessly written, and never read closely. The CASL construct of a datatype declaration collects together several such cases into a single abbreviatory construct, which in many respects may be used analogously to a type definition in STANDARD ML, or to a context-free grammar in BNF.
A datatype declaration declares a sort, and lists some alternatives for that sort; further alternatives may be added separately. An alternative may be a constant, whose declaration is implicit; or it may be a sort, to be embedded as a subsort (of the sort of the type definition); or, finally, it may be a construct--essentially a product--given by a constructor function together with its argument sorts, each optionally accompanied by a selector. The declarations of the constructors and selectors, and the assertion of the expected axioms that relate them to each other, are implicit.
Special cases of datatype declarations are enumerations of constants (although no ordering relation or successor function is provided) and inclusion of subsorts. Notice that we now have three distinct ways of specifying subsorts: directly, or by subsort definitions, or by datatype declarations. (One may also represent a subsort as a unary predicate, although then it cannot be used in declarations of function or predicate symbols, nor when declaring the sorts of variables.)
Sort generation constraints may be used to restrict models to ones where all values of the declared sort are expressible using the declared constructors and subsort inclusions.The intended semantics is often that the only values of the sorts declared by a group of datatype declarations are those that can be expressed using the listed constants, subsort embeddings, and constructor functions. This may be specified in CASL by applying a sort-generation constraint to the group of datatype declarations. To `bundle' the sort generation constraint together with (groups of) datatype declarations would prevent extensions where further constructors are declared for existing sorts, e.g., when extending the CASL abstract syntax with higher-order constructs.
Structuring as free extensions may be used to restrict models to ones where, moreover, different constants or constructors of the same sort are supposed to have distinct values: there should be no `confusion'.Such properties could (at least in the absence of user-specified axioms) be spelled out using first-order axioms, but in fact the intended semantics is precisely captured by the notion of free extension, which can be expressed concisely using the structuring constructs of CASL, see the next section.