Abstract
Initial algebra semantics is a cornerstone of the theory of modern functional programming languages. For each inductive data type, it provides a fold combinator encapsulating structured recursion over data of that type, a Church encoding, a build combinator which constructs data of that type, and a fold/build rule which optimises modular programs by eliminating intermediate data of that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types. Specifically, the folds have been considered too weak to capture commonly occurring patterns of recursion, and no Church encodings, build combinators, or fold/build rules have been given for nested types. This paper overturns this conventional wisdom by solving all of these problems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abel, A., Matthes, R., Uustalu, T.: Iteration schemes for higher-order and nested datatypes. Theoretical Computer Science 333(1-2), 3–66 (2005)
Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453–468. Springer, Heidelberg (1999)
Bayley, I.: Generic Operations on Nested Datatypes. Ph.D. Dissertation, University of Oxford (2001)
Bird, R., Meertens, L.: Nested datatypes. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 52–67. Springer, Heidelberg (1998)
Bird, R., Paterson, R.: de Bruijn notation as a nested datatype. Journal of Functional Programming 9(1), 77–91 (1998)
Bird, R., Paterson, R.: Generalised folds for nested datatypes. Formal Aspects of Computing 11(2), 200–222 (1999)
Blampied, P.: Structured Recursion for Non-uniform Data-types. Ph.D. Dissertation, University of Nottingham (2000)
Fiore, M., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proc. Logic in Computer Science, pp. 193–202 (1999)
Gill, A.: Cheap Deforestation for Non-strict Functional Languages. Ph.D. Dissertation, Glasgow University (1996)
Gill, A., Launchbury, J., Peyton Jones, S.L.: A short cut to deforestation. In: Proc. Functional Programming Languages and Computer Architecture, pp. 223–232 (1993)
Ghani, N., Haman, M., Uustalu, T., Vene, V.: Representing cyclic structures as nested types. Presented at Trends in Functional Programming (2006)
Ghani, N., Johann, P., Uustalu, T., Vene, V.: Monadic augment and generalised short cut fusion. In: Proc. International Conference on Functional Programming, pp. 294–305 (2005)
Ghani, N., Uustalu, T., Vene, V.: Build, augment and destroy. Universally. In: Proc. Asian Symposium on Programming Languages, pp. 327–347 (2003)
Hinze, R.: Polytypic functions over nested datatypes. Discrete Mathematics and Theoretical Computer Science 3(4), 193–214 (1999)
Hinze, R.: Efficient generalized folds. In: Jazayeri, M., Musser, D.R., Loos, R.G.K. (eds.) Generic Programming. LNCS, vol. 1766, Springer, Heidelberg (2000)
Hinze, R.: Functional Pearl: Perfect trees and bit-reversal permutations. Journal of Functional Programming 10(3), 305–317 (2000)
Hinze, R.: Manufacturing datatypes. Journal of Functional Programming 11(5), 493–524 (2001)
Johann, P.: A generalization of short-cut fusion and its correctness proof. Higher-order and Symbolic Computation 15, 273–300 (2002)
MacLane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1971)
Martin, C., Gibbons, J., Bayley, I.: Disciplined efficient generalised folds for nested datatypes. Formal Aspects of Computing 16(1), 19–35 (2004)
McBride, C., McKinna, J.: View from the left. Journal of Functional Programming 14(1), 69–111 (2004)
Pitts, A.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 1–39 (2000)
Takano, A., Meijer, E.: Shortcut deforestation in calculational form. In: Proc. Functional Programming Languages and Computer Architecture, pp. 306–313 (1995)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Johann, P., Ghani, N. (2007). Initial Algebra Semantics Is Enough!. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)