A fold for all seasons

Tim Sheard, Leonidas Fegaras · 1993

Generic control operators, such as fold,, can be generated from algebraic type definitions.The class of types to which these techniques are applicable is generalized to all algebraic types definable in languages such as Miranda and ML, i.e. mutually recursive sums-of-products with tuplee and function types.Several other useful generic operators, aleo applicable to every type in thw class, also are described.A normalization algorithm which automatically calculates improvements to programs expressed in a language baaed upon folds is described.It rednces programs, expressed using fold sz the exclusive control operator, to a canonical form.Based upon a generic promotion theorem, the algorithm is facilitated by the explicit structure of fold programs rather than using an analysis phase to search for implicit structure.Canonical programs are minimal in the sense that they contain the fewest number of fold operations.Because of this property, the normalization algorithm haa important applications in program transformation, optimization, and theorem proving.In addition a generic promotion theorem ia identified for each of the other operators.It is hoped that these theorems can be the basis of normalization algorithms for the other operators as well.

Read the paper · More papers on PaperTik