ABSTRACT

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.