Skip to main content
SpringerLink
Log in

Unraveling Recursion: Compiling an IR with Recursion to System F

  • Conference paper
  • First Online:
Book cover Mathematics of Program Construction (MPC 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11825))

Included in the following conference series:

Abstract

Lambda calculi are often used as intermediate representations for compilers. However, they require extensions to handle higher-level features of programming languages. In this paper we show how to construct an IR based on \(\text {System}\ F_{\omega }^\mu \) which supports recursive functions and datatypes, and describe how to compile it to \(\text {System}\ F_{\omega }^\mu \). Our IR was developed for commercial use at the IOHK company, where it is used as part of a compilation pipeline for smart contracts running on a blockchain.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Why declare a matching function explicitly, rather than using case expressions? The answer is that we want to be local: matching functions can be defined and put into scope when processing the datatype binding, whereas case expressions require additional program analysis to mach up the expression with the corresponding datatype.

  2. 2.

    This is the same device usually employed when giving typing rules for existential types to ensure that the inner type does not escape.

  3. 3.

    An elegant extension of this approach would be to define an indexed family of languages with gradually fewer features. However, this would be a distraction from the main point of this paper, so we have not adopted it.

  4. 4.

    We here mean arbitrary recursive types, not merely strictly positive types. We cannot encode the Y combinator in Agda, for example, without disabling the positivity check.

  5. 5.

    We have defined \(\times \) as a simple datatype, rather than using the more sophisticated version in the Agda standard library. The standard library version has different strictness properties—indeed, for that version \(\texttt {repack}_2\) is precisely the identity.

  6. 6.

    It is well-known that abstract datatypes can be encoded with existential types [22]. The presentation we give here is equivalent to using a value of existential type which is immediately unpacked, and where existential types are given the typical encoding using universal types.

  7. 7.

    This is where the Scott encoding really departs from the Church encoding: the recursive datatype itself appears in our encoding, since we are only doing a “one-level” fold whereas the Church encoding gives us a full recursive fold over the entire datastructure.

  8. 8.

    The complete source can be found in the Plutus repository.

References

  1. Abadi, M., Cardelli, L., Plotkin, G.: Types for the Scott numerals (1993)

    Google Scholar 

  2. Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453–468. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48168-0_32

    Chapter  Google Scholar 

  3. Backhouse, R., Jansson, P., Jeuring, J., Meertens, L.: Generic programming — an introduction. In: Swierstra, S.D., Oliveira, J.N., Henriques, P.R. (eds.) AFP 1998. LNCS, vol. 1608, pp. 28–115. Springer, Heidelberg (1999). https://doi.org/10.1007/10704973_2

    Chapter  Google Scholar 

  4. Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552–593 (2013). https://doi.org/10.1017/S095679681300018X

    Article  MathSciNet  MATH  Google Scholar 

  5. Bredon, G.E.: Topology and Geometry. Graduate Texts in Mathematics, vol. 139. Springer, New York (1993). https://doi.org/10.1007/978-1-4757-6848-0

    Book  MATH  Google Scholar 

  6. Brown, M., Palsberg, J.: Typed self-evaluation via intensional type functions. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 415–428. ACM, New York (2017). https://doi.org/10.1145/3009837.3009853. http://doi.acm.org/10.1145/3009837.3009853

  7. Cai, Y., Giarrusso, P.G., Ostermann, K.: System F-omega with equirecursive types for datatype-generic programming. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 30–43. ACM, New York (2016). https://doi.org/10.1145/2837614.2837660. http://doi.acm.org/10.1145/2837614.2837660

  8. Chapman, J., Kireev, R., Nester, C., Wadler, P.: System \(F\) in Agda, for fun and profit. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 255–297. Springer, Cham (2019)

    Google Scholar 

  9. Danvy, O., Hatcliff, J.: Thunks (continued). In: Proceedings of Actes WSA 1992 Workshop on Static Analysis, Bordeaux, France, Laboratoire Bordelais de Recherche en Informatique (LaBRI), pp. 3–11, September 1992

    Google Scholar 

  10. Dreyer, D.: Understanding and evolving the ML module system. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA, USA (2005). aAI3166274

    Google Scholar 

  11. Dreyer, D.: A type system for recursive modules. In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, pp. 289–302. ACM, New York (2007). https://doi.org/10.1145/1291151.1291196. http://doi.acm.org/10.1145/1291151.1291196

  12. Fulton, W.: Algebraic Topology: A First Course. Graduate Texts in Mathematics, vol. 153. Springer, New York (1995). https://doi.org/10.1007/978-1-4612-4180-5

    Book  MATH  Google Scholar 

  13. Goldberg, M.: A variadic extension of curry’s fixed-point combinator. High. Order Symbol. Comput. 18(3–4), 371–388 (2005). https://doi.org/10.1007/s10990-005-4881-8

    Article  MATH  Google Scholar 

  14. Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press, New York (2012)

    Book  Google Scholar 

  15. Hirschowitz, T., Leroy, X., Wells, J.B.: Compilation of extended recursion in call-by-value functional languages. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, PPDP 2003, pp. 160–171. ACM, New York (2003). https://doi.org/10.1145/888251.888267. http://doi.acm.org/10.1145/888251.888267

  16. IOHK: Plutus, May 2019. https://github.com/input-output-hk/plutus. Accessed 01 May 2019

  17. IOHK: Plutus playground, May 2019. https://prod.playground.plutus.iohkdev.io/. Accessed 01 May 2019

  18. Kiselyov, O.: Many faces of the fixed-point combinator, August 2013. http://okmij.org/ftp/Computation/fixed-point-combinators.html. Accessed 21 Feb 2019

  19. Koopman, P., Plasmeijer, R., Jansen, J.M.: Church encoding of data types considered harmful for implementations: functional pearl. In: Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, IFL 2014, pp. 4:1–4:12. ACM, New York (2014). https://doi.org/10.1145/2746325.2746330. http://doi.acm.org/10.1145/2746325.2746330

  20. Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Ph.D. thesis, INRIA (1990)

    Google Scholar 

  21. Löh, A., Magalhães, J.P.: Generic programming with indexed functors. In: Proceedings of the Seventh ACM SIGPLAN Workshop on Generic Programming, WGP 2011, pp. 1–12. ACM, New York (2011). https://doi.org/10.1145/2036918.2036920. http://doi.acm.org/10.1145/2036918.2036920

  22. Mitchell, J.C., Plotkin, G.D.: Abstract types have existential types. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1985, pp. 37–51. ACM, New York (1985). https://doi.org/10.1145/318593.318606. http://doi.acm.org/10.1145/318593.318606

  23. Nordlander, J., Carlsson, M., Gill, A.J.: Unrestricted pure call-by-value recursion. In: Proceedings of the 2008 ACM SIGPLAN Workshop on ML, ML 2008, pp. 23–34. ACM, New York (2008). https://doi.org/10.1145/1411304.1411309. http://doi.acm.org/10.1145/1411304.1411309

  24. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)

    Google Scholar 

  25. Peyton Jones, S., Meijer, E.: Henk: A typed intermediate language. In: Proceedings of the First International Workshop on Types in Compilation (1997)

    Google Scholar 

  26. Peyton, S.L., Santos, A.L.M.: A transformation-based optimiser for haskell. Sci. Comput. Program. 32(1–3), 3–47 (1998). https://doi.org/10.1016/S0167-6423(97)00029-4

    Article  MATH  Google Scholar 

  27. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  28. Steele, G.L., Sussman, G.J.: Lambda: the ultimate imperative. Technical report, Cambridge, MA, USA (1976)

    Google Scholar 

  29. Steele Jr., G.L.: It’s time for a new old language. In: PPOPP, p. 1 (2017)

    Google Scholar 

  30. Stirling, C.: Proof systems for retracts in simply typed lambda calculus. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 398–409. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39212-2_36

    Chapter  Google Scholar 

  31. Syme, D.: Initializing mutually referential abstract objects: the value recursion challenge. Electron. Notes Theor. Comput. Sci. 148(2), 3–25 (2006). https://doi.org/10.1016/j.entcs.2005.11.038

    Article  Google Scholar 

  32. Yakushev, A.R., Holdermans, S., Löh, A., Jeuring, J.: Generic programming with fixed points for mutually recursive datatypes. SIGPLAN Not 44(9), 233–244 (2009). https://doi.org/10.1145/1631687.1596585. http://doi.acm.org/10.1145/1631687.1596585

    Article  Google Scholar 

Download references

Acknowledgments

The authors would like to thank Mario Alvarez-Picallo and Manuel Chakravarty for their comments on the manuscript, as well as IOHK for funding the research.

Author information

Authors and Affiliations

  1. IOHK, Hong Kong, China

    Michael Peyton Jones, Vasilis Gkoumas, Roman Kireev & Kenneth MacKenzie

  2. University of Edinburgh, Edinburgh, UK

    Chad Nester & Philip Wadler

Authors
  1. Michael Peyton Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vasilis Gkoumas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Roman Kireev
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Kenneth MacKenzie
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Chad Nester
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Philip Wadler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Peyton Jones .

Editor information

Editors and Affiliations

  1. University of Nottingham, Nottingham, UK

    Graham Hutton

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Peyton Jones, M., Gkoumas, V., Kireev, R., MacKenzie, K., Nester, C., Wadler, P. (2019). Unraveling Recursion: Compiling an IR with Recursion to System F. In: Hutton, G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science(), vol 11825. Springer, Cham. https://doi.org/10.1007/978-3-030-33636-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-33636-3_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-33635-6

  • Online ISBN: 978-3-030-33636-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation