Abstract
In this paper, I show that general recursive definitions can be represented in the free monad which supports the ‘effect’ of making a recursive call, without saying how these calls should be executed. Diverse semantics can be given within a total framework by suitable monad morphisms. The Bove-Capretta construction of the domain of a general recursive function can be presented datatype-generically as an instance of this technique. The paper is literate Agda, but its key ideas are more broadly transferable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
I write brackets for case analysis over a sum.
- 3.
Whenever I intend a monoidal accumulation, I say ‘crush’, not ‘fold’.
- 4.
Agda, Coq, etc., stratify types by ‘size’ into sets-of-values, sets-of-sets-of-values, and so on, ensuring consistency by forbidding the quantification over ‘large’ types by ‘small’.
- 5.
They observe also that
and
form a monad morphism.
References
Abel, A.: Type-based termination: a polymorphic lambda-calculus with sized higher-order types. Ph.D. thesis, Ludwig Maximilians University Munich (2007)
Abel, A., Chapman, J.: Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types. In: Levy, P., Krishnaswami, N. (eds.) Workshop on Mathematically Structured Functional Programming 2014, vol. 153 of EPTCS, pp. 51–67 (2014)
Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: Giacobazzi, R., Cousot, R. (eds.) ACM Symposium on Principles of Programming Languages, POPL 2013, ACM, pp. 27–38 (2013)
Altenkirch, T., Chapman, J., Uustalu, T.: Monads need not be endofunctors. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 297–311. Springer, Heidelberg (2010)
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)
Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84(1), 108–123 (2015)
Bove, A.: Simple general recursion in type theory. Nord. J. Comput. 8(1), 22–42 (2001)
Bove, A., Capretta, V.: Nested general recursion and partiality in type theory. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 121–135. Springer, Heidelberg (2001)
Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 115–129. Springer, Heidelberg (2004)
Capretta, V.: General recursion via coinductive types. Log. Meth. Comput. Sci. 1(2), 1–28 (2005)
Dybjer, P., Setzer, A.: A finite axiomatization of inductive-recursive definitions. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 129–146. Springer, Heidelberg (1999)
Dybjer, P., Setzer, A.: Indexed induction-recursion. In: Kahle, R., Schroeder-Heister, P., Stärk, R.F. (eds.) PTCS 2001. LNCS, vol. 2183, pp. 93–113. Springer, Heidelberg (2001)
Ghani, N., Hancock, P.: Containers, monads and induction recursion. Math. Struct. Comput. Sci. FirstView: 1–25, 2 (2015)
Ghani, N., Lüth, C., De Marchi, F., Power, J.: Algebras, coalgebras, monads and comonads. Electr. Notes Theor. Comput. Sci. 44(1), 128–145 (2001)
Giménez, E.: Codifying guarded definitions with recursive schemes. In: Smith, J., Dybjer, Peter, Nordström, Bengt (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1994)
Hancock, P., McBride, C., Ghani, N., Malatesta, L., Altenkirch, T.: Small Induction Recursion. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 156–172. Springer, Heidelberg (2013)
Martin-Löf, P.: Constructive mathematics and computer programming. In: Cohen, L.J., Los, J., Pfeiffer, H., Podewski, K.-P. (eds.) LMPS 6, pp. 153–175. North-Holland (1982)
Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), pp. 14–23. IEEE Computer Society, Pacific Grove, California, USA, 5–8 June 1989
Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)
Plotkin, G.D., Power, J.: Algebraic operations and generic effects. Appl. Categorical Struct. 11(1), 69–94 (2003)
Turner, D.A.: Total functional programming. J. Univ. Comput. Sci. 10(7), 751–768 (2004)
Uustalu, T.: Partiality is an effect. Talk Given at Dagstuhl Seminar on Dependently Typed Programming. http://www.ioc.ee/~tarmo/tday-veskisilla/uustalu-slides.pdf (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
McBride, C. (2015). Turing-Completeness Totally Free. In: Hinze, R., Voigtländer, J. (eds) Mathematics of Program Construction. MPC 2015. Lecture Notes in Computer Science(), vol 9129. Springer, Cham. https://doi.org/10.1007/978-3-319-19797-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-19797-5_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19796-8
Online ISBN: 978-3-319-19797-5
eBook Packages: Computer ScienceComputer Science (R0)