Layer by Layer – Combining Monads

  • Fredrik DahlqvistEmail author
  • Louis Parlant
  • Alexandra Silva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)


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.


  1. 1.
    Awodey, S.: Category Theory. Oxford Logic Guides, vol. 49, 2nd edn. Oxford University Press, Oxford (2010)zbMATHGoogle Scholar
  2. 2.
    Balan, A., Kurz, A.: On coalgebras over algebras. Theor. Comput. Sci. 412(38), 4989–5005 (2011). Scholar
  3. 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). Scholar
  4. 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). Scholar
  5. 5.
    Bonchi, F., Silva, A., Sokolova, A.: The power of convex algebras. arXiv preprint 1707.02344 (2017).
  6. 6.
    Bonsangue, M.M., Hansen, H.H., Kurz, A., Rot, J.: Presenting distributive laws. Log. Methods. Comput. Sci. 11(3), Article no. 2 (2015).
  7. 7.
    Cheng, E.: Distributive laws for Lawvere theories. arXiv preprint 1112.3076 (2011).
  8. 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). Scholar
  9. 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).
  10. 10.
    Gautam, N.: The validity of equations of complex algebras. Arch. Math. Log. Grundl. 3(3–4), 117–124 (1957). Scholar
  11. 11.
    Hyland, M., Levy, P., Plotkin, G., Power, J.: Combining algebraic effects with continuations. Theor. Comput. Sci. 375(1–3), 20–40 (2007). Scholar
  12. 12.
    Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006). Scholar
  13. 13.
    Jacobs, B.: Semantics of weakening and contraction. Ann. Pure Appl. Log. 69(1), 73–106 (1994). Scholar
  14. 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). Scholar
  15. 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). Scholar
  16. 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). Scholar
  17. 17.
    Klin, B., Salamanca, J.: Iterated covariant powerset is not a monad. Electron. Notes Theor. Comput. Sci. (to appear)Google Scholar
  18. 18.
    Kock, A.: Bilinearity and Cartesian closed monads. Math. Scand. 29(2), 161–174 (1972). Scholar
  19. 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).
  20. 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). Scholar
  21. 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).
  22. 22.
    Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5, 2nd edn. Springer, Heidelberg (1978). Scholar
  23. 23.
    Manes, E., Mulry, P.: Monad compositions I: general constructions and recursive distributive laws. Theor. Appl. Categ. 18, 172–208 (2007). Scholar
  24. 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). Scholar
  25. 25.
    Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991). Scholar
  26. 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). Scholar
  27. 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). Scholar
  28. 28.
    Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets scott: semantic foundations for probabilistic networks. arXiv preprint 1607.05830 (2016).
  29. 29.
    Sokolova, A., Jacobs, B., Hasuo, I.: Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3(4), Article no. 11 (2007).
  30. 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).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Fredrik Dahlqvist
    • 1
    Email author
  • Louis Parlant
    • 1
  • Alexandra Silva
    • 1
  1. 1.Department of Computer ScienceUniversity College LondonLondonUK

Personalised recommendations