Generic types and modules

Maude supports a powerful form of generic programming that substantially extends the parameterized programming capabilities of OBJ3 [44]. The analogous terminology to express these capabilities in higher-order type theory would be parametric polymorphism and dependent types. But in Maude the parameters are not just types, but theories, including operators and equations that impose semantic restrictions on the parameterized module instantiations. Thus, whereas a parametric LIST module can be understood just at the level of the parametric type (sort) of list elements, a parameterized SORTING module has the theory TOSET of totally ordered sets as its parameter, including the axioms for the order predicate, that must be satisfied in each correct instance for the sorting function to work properly. Types analogous to dependent types are also supported by making the parameter instantiations depend on specific parametric constants in the parameter theory, and by giving membership axioms depending on such constants. For example, natural numbers modulo $n$ (see Section 15.7), and arrays of length $n$, can be easily defined this way. The fact that entire modules, and not just types, can be parametric provides even more powerful constructs. For example, TUPLE[$n$] (see Section 14.3.1) is a ``dependent parameterized module'' that assigns to each natural number $n$ the parameterized module of $n$-tuples (together with the tupling and projection operations) with $n$ parameter sorts.