Maude has two varieties of types: sorts, which correspond to well-defined data, and kinds, which may contain error elements. Sorts can be structured in subsort hierarchies, with the subsort relation understood semantically as subset inclusion. For example, for numbers we can have subsort inclusions
Nat < Int < Rat
indicating that the natural numbers are contained in the integers, and these in
turn are contained in the rational numbers. All these sorts determine a kind
(say the ``number kind'') which is interpreted semantically as the set
containing all the well-formed numerical expressions for the above number
systems as well as error expressions such as, for example, 4 + 7/0.
This allows support for partial functions in a total setting, in the
sense that a function whose application to some arguments has a kind
but not a sort should be
considered undefined for those arguments (but notice that functions
can also map undefined to defined results, for example in the context of
error recovery). Furthermore, operators
can be subsort-overloaded, providing a useful form of subtype
polymorphism. For example, the addition operation _+_ is subsort
overloaded and has typings for each of the above number sorts. A further
feature, greatly extending the expressive power for specifying partial
functions, is the possibility of defining sorts by means of equational
conditions. For example, a sequential composition operation _;_
concatenating two paths in a graph is defined if and only if the target of
the first path coincides with the source of the second path. In Maude this
can be easily expressed with the ``conditional membership'' (see
Section 4.3):
vars P Q : Path . cmb (P ; Q) : Path if target(P) = source(Q) .