A number of Maude's built-in operators are polymorphic in one or more
arguments, in the sense that the operator has meaning when these arguments are
of any known sort. Examples include Boolean operators such as the conditional,
if_then_else_fi, which is polymorphic in its second and third arguments,
and the equality test _==_ which is polymorphic in both arguments
(see Section 7.1). The user can also define polymorphic
operators using the polymorphic attribute (abbreviated poly).
This attribute takes a set of natural numbers enclosed in parentheses that
indicates which arguments are polymorphic, with 0 indicating the range.
For polymorphic operators that are not constants, at least one argument
should be polymorphic to avoid ambiguities. Since there are no polymorphic
equations, polymorphic operators are limited to constructors and
built-ins. Polymorphic operators are always instantiated with the polymorphic
arguments going to the kind level, which further limits their
generality. The sort name in a polymorphic position of an operator
declaration is purely a place holder--any legal type name
could be used. The recommended convention is to use Universal.
One reasonable use for polymorphic operators beyond the existing built-ins is to define heterogeneous lists, as follows, where CONVERSION denotes a predefined module described in Section 7.9 having types for different numbers as well as strings; this module is imported by means of a protecting declaration, which will be explained in Section 6.1.1.
fmod HET-LIST is
protecting CONVERSION .
sort List .
op nil : -> List .
op __ : Universal List -> List [ctor poly (1)] .
endfm
As an example, we can form the following heterogeneous lists:
Maude> red 4 "foo" 4.5 1/2 nil . result List: 4 "foo" 4.5 1/2 nil Maude> red (4 "foo" nil) 4.5 1/2 nil . result List: (4 "foo" nil) 4.5 1/2 nil