Generalized Iteration and Coiteration for Higher-Order Nested Datatypes
Andreas Abel5
, Ralph Matthes6
and Tarmo Uustalu7 
| (5) |
Department of Computer Science, University of Munich, Munich |
| (6) |
Preuves, Programmes et Systèmes, CNRS, Université Paris VII (on leave from University of Munich), Munich |
| (7) |
Inst.of Cybernetics, Tallinn Technical University, Tallinn |
Abstract
We solve the problem of extending Bird and Paterson’s generalized folds for nested datatypes and its dual to inductive and
coinductive constructors of arbitrarily high ranks by appropriately generalizing Mendler-style (co)iteration.Characteristically
to Mendler-style schemes of disciplined (co)recursion,the schemes we propose do not rest on notions like positivity or monotonicity
of a constructor and facilitate programming in a natural and elegant style close to programming with the customary letrec construct,where the typings of the schemes,however, guarantee termination. For rank 2,a smoothened version of Bird and Paterson's
generalized folds and its dual are achieved;for rank 1,the schemes instantiate to Mendler's original (re)formulation of iteration
and coiteration. Several examples demonstrate the power of the approach. Strong normalization of our proposed extension of
system F
ω of higher-order parametric polymorphism is proven by a reduction-preserving embedding into pure F
ω.
The first author gratefully acknowledges the support by the PhD Programme Logic in Computer Science (GKLI)of the Deutsche Forschungs-Gemeinschaft.
The third author is partially supported by the Estonian Science Foundation (ETF)under grant No.4155. He is also grateful to
the GKLI for two invitations to Munich;the cooperation started during these visits.
References secured to subscribers.