Polytypic Programming in Maude

The idea of polytypic programming is to write programs that are defined by induction on the structure of user-defined datatypes. In this way, many functions with similar functionalities do not have to be written over and over again for different datatypes. So far, this programming style has been developed in functional languages like Haskell, extended with new syntactic constructs for defining polytypic programs. In this paper we show that polytypic programming can be reduced to metaprogramming, and that can be developed in a reflective first-order language like Maude, without having to extend the language. This has the additional advantage of allowing us to use standard formal tools to prove properties about polytypic programs. We illustrate our methodology via examples. In particular, we explain how to define in Maude two non-trivial generic functions, namely, the polytypic versions of the functions map, and cata, and how to prove properties about them using an inductive theorem prover for Maude modules.