Abstract
We describe and implement an optimizing compiler transformation which turns non–tail-recursive functions into equivalent tail-recursive functions in an intermediate language of the CakeML compiler. CakeML is a strongly typed functional language based on Standard ML with call-by-value semantics and a fully verified compiler. We integrate our implementation into CakeML compiler, and provide a machine-checked proof verifying that the observational semantics of programs is preserved under the transformation. To the best of our knowledge, this is the first fully verified implementation of this transformation in any modern compiler. Moreover, our verification efforts uncover surprising drawbacks in some of the verification techniques employed in several parts of the CakeML compiler. We provide a work-around for these drawbacks, and compare it to potential alternatives.
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
References
Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM (JACM) 24(1), 44–67 (1977)
Chitil, O.: Type-inference based short cut deforestation (nearly) without inlining. In: Koopman, P., Clack, C. (eds.) IFL 1999. LNCS, vol. 1868, pp. 19–35. Springer, Heidelberg (2000). https://doi.org/10.1007/10722298_2
Kühnemann, A., Glück, R., Kakehi, K.: Relating accumulative and non-accumulative functional programs. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 154–168. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45127-7_13
Kumar, R., Myreen, M., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Principles of Programming Languages (POPL). ACM (2014)
Liu, Y.A., Stoller, S.D.: From recursion to iteration: what are the optimizations? ACM Sigplan Not. 34(11), 73–82 (1999)
Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 589–615. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_23
Owens, S., Norrish, M., Kumar, R., Myreen, M.O., Tan, Y.K.: Verifying efficient function calls in CakeML. In: International Conference on Functional Programming (ICFP). ACM Press, September 2017
Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A., Owens, S., Norrish, M.: A new verified compiler backend for CakeML. In: International Conference on Functional Programming (ICFP). ACM Press (2016)
Tan, Y.K., Owens, S., Kumar, R.: A verified type system for CakeML. In: Implementation and Application of Functional Programming Languages (IFL), p. 7. ACM (2015)
Wadler, P.: The concatenate vanishes. Note, University of Glasgow (1987)
Acknowledgments
This work was carried out as the first author’s M.Sc. project, under the supervision of the second author. The authors would like to extend their thanks to the Lars Pareto scholarship for sponsoring the travel to the TFP symposium. We are grateful for comments on drafts of this text provided by Johannes Åman Pohjola. Finally, we thank the anonymous reviewers for their helpful feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Abrahamsson, O., Myreen, M.O. (2018). Automatically Introducing Tail Recursion in CakeML. In: Wang, M., Owens, S. (eds) Trends in Functional Programming. TFP 2017. Lecture Notes in Computer Science(), vol 10788. Springer, Cham. https://doi.org/10.1007/978-3-319-89719-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-89719-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-89718-9
Online ISBN: 978-3-319-89719-6
eBook Packages: Computer ScienceComputer Science (R0)