Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Theoretical Aspects of Computing

ICTAC 2018: Theoretical Aspects of Computing – ICTAC 2018 pp 153–172Cite as

Layer by Layer – Combining Monads

  • Conference paper
  • First Online:

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

Abstract

We develop a modular method to build algebraic structures. Our approach is categorical: we describe the layers of our construct as monads, and combine them using distributive laws.

Finding such laws is known to be difficult and our method identifies precise sufficient conditions for two monads to distribute. We either (i) concretely build a distributive law which then provides a monad structure to the composition of layers, or (ii) pinpoint the algebraic obstacles to the existence of a distributive law and suggest a weakening of one layer that ensures distributivity.

This method can be applied to a step-by-step construction of a programming language. Our running example will involve three layers: a basic imperative language enriched first by adding non-determinism and then probabilistic choice. The first extension works seamlessly, but the second encounters an obstacle, resulting in an ‘approximate’ language very similar to the probabilistic network specification language ProbNetKAT.

A. Silva—This work was partially supported by ERC grant ProfoundNet.

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   69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   89.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

Notes

  1. 1.

    We will never consider the notion of strong monoidal functor, so this terminology should not lead to any confusion.

References

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

    MATH  Google Scholar 

  2. Balan, A., Kurz, A.: On coalgebras over algebras. Theor. Comput. Sci. 412(38), 4989–5005 (2011). https://doi.org/10.1016/j.tcs.2011.03.021

    Article  MathSciNet  MATH  Google Scholar 

  3. Beck, J.: Distributive laws. In: Eckmann, B. (ed.) Seminar on Triples and Categorical Homology Theory: ETH 1966/67. LNM, vol. 80, pp. 119–140. Springer, Heidelberg (1969). https://doi.org/10.1007/BFb0083084

    Chapter  Google Scholar 

  4. Benton, N., Hughes, J., Moggi, E.: Monads and effects. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 42–122. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45699-6_2

    Chapter  Google Scholar 

  5. Bonchi, F., Silva, A., Sokolova, A.: The power of convex algebras. arXiv preprint 1707.02344 (2017). https://arxiv.org/abs/1707.02344

  6. Bonsangue, M.M., Hansen, H.H., Kurz, A., Rot, J.: Presenting distributive laws. Log. Methods. Comput. Sci. 11(3), Article no. 2 (2015). https://doi.org/10.2168/lmcs-11(3:2)2015

  7. Cheng, E.: Distributive laws for Lawvere theories. arXiv preprint 1112.3076 (2011). https://arxiv.org/abs/1112.3076

  8. Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 282–309. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_12

    Chapter  Google Scholar 

  9. Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: Proceedings of 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, January 2015, pp. 343–355. ACM Press, New York (2015). https://doi.org/10.1145/2676726.2677011

  10. Gautam, N.: The validity of equations of complex algebras. Arch. Math. Log. Grundl. 3(3–4), 117–124 (1957). https://doi.org/10.1007/bf01988052

    Article  MathSciNet  MATH  Google Scholar 

  11. Hyland, M., Levy, P., Plotkin, G., Power, J.: Combining algebraic effects with continuations. Theor. Comput. Sci. 375(1–3), 20–40 (2007). https://doi.org/10.1016/j.tcs.2006.12.026

    Article  MathSciNet  MATH  Google Scholar 

  12. Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006). https://doi.org/10.1016/j.tcs.2006.03.013

    Article  MathSciNet  MATH  Google Scholar 

  13. Jacobs, B.: Semantics of weakening and contraction. Ann. Pure Appl. Log. 69(1), 73–106 (1994). https://doi.org/10.1016/0168-0072(94)90020-5

    Article  MathSciNet  MATH  Google Scholar 

  14. Jacobs, B., Silva, A., Sokolova, A.: Trace semantics via determinization. In: Pattinson, D., Schröder, L. (eds.) CMCS 2012. LNCS, vol. 7399, pp. 109–129. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32784-1_7

    Chapter  Google Scholar 

  15. King, D.J., Wadler, P.: Combining monads. In: Launchbury, J., Sansom, P.M. (eds.) Functional Programming, Glasgow 1992. Workshops in Computing, pp. 134–143. Springer, London (1993). https://doi.org/10.1007/978-1-4471-3215-8_12

    Chapter  Google Scholar 

  16. Klin, B., Rot, J.: Coalgebraic trace semantics via forgetful logics. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 151–166. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46678-0_10

    Chapter  Google Scholar 

  17. Klin, B., Salamanca, J.: Iterated covariant powerset is not a monad. Electron. Notes Theor. Comput. Sci. (to appear)

    Google Scholar 

  18. Kock, A.: Bilinearity and Cartesian closed monads. Math. Scand. 29(2), 161–174 (1972). https://doi.org/10.7146/math.scand.a-11042

    Article  MathSciNet  MATH  Google Scholar 

  19. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. In: Proceedings of the 6th Annual Symposium on Logic in Computer Science, LICS 1991, Amsterdam, July 1991, pp. 214–225. IEEE CS Press, Washington, DC (1991). https://doi.org/10.1109/lics.1991.151646

  20. Liang, S., Hudak, P.: Modular denotational semantics for compiler construction. In: Nielson, H.R. (ed.) ESOP 1996. LNCS, vol. 1058, pp. 219–234. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61055-3_39

    Chapter  Google Scholar 

  21. Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Proceedings of 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1995, San Francisco, CA, USA, January 1995, pp. 333–343. ACM Press, New York (1995). https://doi.org/10.1145/199448.199528

  22. Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5, 2nd edn. Springer, Heidelberg (1978). https://doi.org/10.1007/978-1-4757-4721-8

    Book  MATH  Google Scholar 

  23. Manes, E., Mulry, P.: Monad compositions I: general constructions and recursive distributive laws. Theor. Appl. Categ. 18, 172–208 (2007). http://www.tac.mta.ca/tac/volumes/18/7/18-07abs.html

    MathSciNet  MATH  Google Scholar 

  24. Milius, S., Palm, T., Schwencke, D.: Complete iterativity for algebras with effects. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 34–48. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03741-2_4

    Chapter  Google Scholar 

  25. Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991). https://doi.org/10.1016/0890-5401(91)90052-4

    Article  MathSciNet  MATH  Google Scholar 

  26. Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45931-6_24

    Chapter  MATH  Google Scholar 

  27. Sato, T.: The Giry monad is not strong for the canonical symmetric monoidal closed structure on \(\mathbf{Meas}\). J. Pure Appl. Alg. 222(10), 2888–2896 (2017). https://doi.org/10.1016/j.jpaa.2017.11.004

    Article  MathSciNet  MATH  Google Scholar 

  28. Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets scott: semantic foundations for probabilistic networks. arXiv preprint 1607.05830 (2016). https://arxiv.org/1607.05830

  29. Sokolova, A., Jacobs, B., Hasuo, I.: Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3(4), Article no. 11 (2007). https://doi.org/10.2168/lmcs-3(4:11)2007

  30. Varacca, D.: Probability, nondeterminism and concurrency: two denotational models for probabilistic computation. BRICS Dissertation Series, vol. DS-03-14. Ph.D. thesis, Aarhus University (2003). http://www.brics.dk/DS/03/14/

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University College London, Gower Street, London, WC1E 6BT, UK

    Fredrik Dahlqvist, Louis Parlant & Alexandra Silva

Authors
  1. Fredrik Dahlqvist
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Louis Parlant
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexandra Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fredrik Dahlqvist .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  2. Reykjavík University, Reykjavik, Iceland

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dahlqvist, F., Parlant, L., Silva, A. (2018). Layer by Layer – Combining Monads. In: Fischer, B., Uustalu, T. (eds) Theoretical Aspects of Computing – ICTAC 2018. ICTAC 2018. Lecture Notes in Computer Science(), vol 11187. Springer, Cham. https://doi.org/10.1007/978-3-030-02508-3_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02508-3_9

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation