Skip to main content
SpringerLink
Log in
Book cover

International Conference on Mathematics of Program Construction

MPC 2012: Mathematics of Program Construction pp 324–362Cite as

Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7342))

Abstract

Many program optimisations involve transforming a program in direct style to an equivalent program in continuation-passing style. This paper investigates the theoretical underpinnings of this transformation in the categorical setting of monads. We argue that so-called absolute Kan Extensions underlie this program optimisation. It is known that every Kan extension gives rise to a monad, the codensity monad, and furthermore that every monad is isomorphic to a codensity monad. The end formula for Kan extensions then induces an implementation of the monad, which can be seen as the categorical counterpart of continuation-passing style. We show that several optimisations are instances of this scheme: Church representations and implementation of backtracking using success and failure continuations, among others. Furthermore, we develop the calculational properties of Kan extensions, powers and ends. In particular, we propose a two-dimensional notation based on string diagrams that aims to support effective reasoning with Kan extensions.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Awodey, S.: Category Theory, 2nd edn. Oxford University Press (2010)

    Google Scholar 

  2. Backhouse, R., Bijsterveld, M., van Geldrop, R., van der Woude, J.: Category theory as coherently constructive lattice theory (1994), http://www.cs.nott.ac.uk/~rcb/MPC/CatTheory.ps.gz

  3. Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall Europe, London (1997)

    MATH  Google Scholar 

  4. Bird, R., Paterson, R.: Generalised folds for nested datatypes. Formal Aspects of Computing 11(2), 200–222 (1999)

    Article  MATH  Google Scholar 

  5. Böhm, C., Berarducci, A.: Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science 39(2-3), 135–154 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  6. Burstall, R., Darlington, J.: A tranformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cáccamo, M., Winskel, G.: A Higher-Order Calculus for Categories. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 136–153. Springer, Heidelberg (2001), http://dx.doi.org/10.1007/3-540-44755-5_11

    Chapter  Google Scholar 

  8. Claessen, K.: Functional pearl: Parallel parsing processes. Journal of Functional Programming 14(6), 741–757 (2004), http://dx.doi.org/10.1017/S0956796804005192

    Article  MATH  Google Scholar 

  9. Danvy, O., Filinski, A.: Abstracting control. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming, pp. 151–160. ACM Press (June 1990)

    Google Scholar 

  10. Eilenberg, S., Moore, J.C.: Adjoint functors and triples. Illinois J. Math 9(3), 381–398 (1965)

    MathSciNet  MATH  Google Scholar 

  11. Ghani, N., Uustalu, T., Vene, V.: Build, Augment and Destroy, Universally. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 327–347. Springer, Heidelberg (2004), http://dx.doi.org/10.1007/978-3-540-30477-7_22

    Chapter  Google Scholar 

  12. Hinze, R.: Efficient monadic-style backtracking. Tech. Rep. IAI-TR-96-9, Institut für Informatik III, Universität Bonn (October 1996)

    Google Scholar 

  13. Hinze, R.: Deriving backtracking monad transformers. In: Wadler, P. (ed.) Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), pp. 186–197. ACM, New York (2000)

    Chapter  Google Scholar 

  14. Hinze, R.: Adjoint folds and unfolds—an extended study. Science of Computer Programming (2011) (to appear)

    Google Scholar 

  15. Hinze, R., James, D.W.H.: Reason isomorphically! In: Oliveira, B.C., Zalewski, M. (eds.) Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming (WGP 2010), pp. 85–96. ACM, New York (2010)

    Chapter  Google Scholar 

  16. Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127–132 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  17. Huber, P.J.: Homotopy theory in general categories. Mathematische Annalen 144, 361–385 (1961), http://dx.doi.org/10.1007/BF01396534 , doi:10.1007/BF01396534

    Article  MathSciNet  MATH  Google Scholar 

  18. Hughes, J.: The Design of a Pretty-Printing Library. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 53–96. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  19. Hughes, R.J.M.: A novel representation of lists and its application to the function reverse. Information Processing Letters 22(3), 141–144 (1986)

    Article  Google Scholar 

  20. Hutton, G., Jaskelioff, M., Gill, A.: Factorising folds for faster functions. Journal of Functional Programming 20(Special Issue 3-4), 353–373 (2010), http://dx.doi.org/10.1017/S0956796810000122

    Article  MATH  Google Scholar 

  21. Jaskelioff, M.: Modular Monad Transformers. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 64–79. Springer, Heidelberg (2009), http://dx.doi.org/10.1007/978-3-642-00590-9_6

    Chapter  Google Scholar 

  22. Johann, P., Ghani, N.: Foundations for structured programming with GADTs. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 297–308. ACM, New York (2008), http://doi.acm.org/10.1145/1328438.1328475

    Chapter  Google Scholar 

  23. Kan, D.M.: Adjoint functors. Transactions of the American Mathematical Society 87(2), 294–329 (1958)

    Article  MathSciNet  MATH  Google Scholar 

  24. Kleisli, H.: Every standard construction is induced by a pair of adjoint functors. Proceedings of the American Mathematical Society 16(3), 544–546 (1965), http://www.jstor.org/stable/2034693

    Article  MathSciNet  MATH  Google Scholar 

  25. Lambek, J.: From lambda-calculus to cartesian closed categories. In: Seldin, J., Hindley, J. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 376–402. Academic Press (1980)

    Google Scholar 

  26. Leivant, D.: Reasoning about functional programs and complexity classes associated with type disciplines. In: Proceedings 24th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1983, Tucson, AZ, USA, pp. 460–469. IEEE Computer Society Press, Los Alamitos (1983)

    Chapter  Google Scholar 

  27. Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics. Springer, Berlin (1998)

    MATH  Google Scholar 

  28. McBride, C.: Functional pearl: Kleisli arrows of outrageous fortune. Journal of Functional Programming (to appear)

    Google Scholar 

  29. Mellish, C., Hardy, S.: Integrating Prolog into the Poplog environment. In: Campbell, J. (ed.) Implementations of Prolog, pp. 533–535. Ellis Horwood Limited (1984)

    Google Scholar 

  30. Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  31. Penrose, R.: Applications of negative dimensional tensors. In: Welsh, D. (ed.) Combinatorial Mathematics and its Applications: Proceedings of a Conference held at the Mathematical Institute, Oxford, July 7-10, 1969, pp. 221–244. Academic Press (1971)

    Google Scholar 

  32. Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. Springer Lecture Notes in Physics, vol. 813, pp. 289–355. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  33. Voigtländer, J.: Asymptotic Improvement of Computations over Free Monads. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 388–403. Springer, Heidelberg (2008), http://dx.doi.org/10.1007/978-3-540-70594-9_20

    Chapter  Google Scholar 

  34. Wadler, P.: Theorems for free! In: The Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA 1989), London, UK, pp. 347–359. Addison-Wesley Publishing Company (September 1989)

    Google Scholar 

  35. Wand, M., Vaillancourt, D.: Relating models of backtracking. In: Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, pp. 54–65. ACM, New York (2004), http://doi.acm.org/10.1145/1016850.1016861

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, Oxford, OX1 3QD, England

    Ralf Hinze

Authors
  1. Ralf Hinze
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Jeremy Gibbons

  2. Facultad de Informática, Universidad Politécnica de Madrid, Campus de Montegancedo s/n, 28660, Boadilla del Monte, Madrid, Spain

    Pablo Nogueira

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hinze, R. (2012). Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick. In: Gibbons, J., Nogueira, P. (eds) Mathematics of Program Construction. MPC 2012. Lecture Notes in Computer Science, vol 7342. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31113-0_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31113-0_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31112-3

  • Online ISBN: 978-3-642-31113-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation