A type definition group allows the concise declaration of one or more sorts 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 type definition group collects together several such cases into a single abbreviatory construct, which in many respects corresponds to a type definition in STANDARD ML, or to a context-free grammar in BNF.
A type definition group consists of one or more type definitions (possibly together with some axioms). Each type definition declares a sort, and lists the alternatives for that sort. 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 type definitions are enumerations of constants (although no ordering relation or successor function is provided) and unions of subsorts. Notice that we now have three distinct ways of specifying subsorts: directly, or by predicative sort definitions, or by type definitions. (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.)
The semantics of a type definition group involves free extension.The intended semantics is that the only values of the sorts declared by a type definition group are those that can be expressed using the listed constants, subsort embeddings, and constructor functions. 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 sort-generation constraints and first-order axioms, but in fact the intended semantics is precisely captured by the notion of initial semantics (or, in the case that alternatives involve sorts declared outside the type-definition group, free extension).
A type definition group may be used as an item of a basic specification.A type definition group is essentially something like a complete basic specification, and can be combined with other specifications in structured specifications. But especially when specifying `small' type definitions, e.g., enumerations of constants or unions of subsorts, it would often be awkward to have to separate this part and make an explicit extension of it. Thus CASL allows a type definition group to be used directly as an item of a basic specification, with semantics corresponding to the introduction of an implicit extension.