Many typed functional languages provide excellent support for defining
and manipulating concrete instances of inductively defined recursive
types. However, few of these languages provide good support for
treating these types in a more abstract way. There have been a number
of language extensions proposed to provide abstract facilities for
manipulating these types. Unfortunately none have been widely adopted.
We show several programming idioms based on recursion schemas that
provide many of the benefits of several proposed extensions without
any needed language extensions. By using recursion schemas we can
completely hide the representation of an algebraic type while still
fully supporting pattern matching with patterns of arbitrary depth,
similar in many ways to Wadler's views (Wadler, 1987; Okasaki, 1998).
We also can simulate or encode many features of refinement types
(Freeman & Pfenning, 1991; Davies, 1997), polytypic recursion
operators (Meijer et al., 1991), and declarative rewriting. Our
programming idiom is more cumbersome in some areas when compared to
the various proposed language extensions but provides a good deal of
bang for the buck. Our experience demonstrates that these techniques
are especially useful for developing compilers which manipulate
various specialized forms of lambda terms. Programming with recursion
schemas gain many of the benefits of views, refinement types,
polytypic programming, and declarative rewriting without the need for
any extensions to the underlying language.