Advertisement

Layer by Layer – Combining Monads

  • Fredrik Dahlqvist
  • Louis Parlant
  • Alexandra Silva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

References

  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).  https://doi.org/10.1016/j.tcs.2011.03.021MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/BFb0083084CrossRefGoogle 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).  https://doi.org/10.1007/3-540-45699-6_2CrossRefGoogle Scholar
  5. 5.
    Bonchi, F., Silva, A., Sokolova, A.: The power of convex algebras. arXiv preprint 1707.02344 (2017). https://arxiv.org/abs/1707.02344
  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).  https://doi.org/10.2168/lmcs-11(3:2)2015
  7. 7.
    Cheng, E.: Distributive laws for Lawvere theories. arXiv preprint 1112.3076 (2011). https://arxiv.org/abs/1112.3076
  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).  https://doi.org/10.1007/978-3-662-49498-1_12CrossRefGoogle 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).  https://doi.org/10.1145/2676726.2677011
  10. 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/bf01988052MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1016/j.tcs.2006.12.026MathSciNetCrossRefzbMATHGoogle Scholar
  12. 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.013MathSciNetCrossRefzbMATHGoogle Scholar
  13. 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-5MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-32784-1_7CrossRefGoogle 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).  https://doi.org/10.1007/978-1-4471-3215-8_12CrossRefGoogle 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).  https://doi.org/10.1007/978-3-662-46678-0_10CrossRefGoogle 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).  https://doi.org/10.7146/math.scand.a-11042MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1109/lics.1991.151646
  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).  https://doi.org/10.1007/3-540-61055-3_39CrossRefGoogle 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).  https://doi.org/10.1145/199448.199528
  22. 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-8CrossRefzbMATHGoogle Scholar
  23. 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.htmlMathSciNetzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-03741-2_4CrossRefGoogle Scholar
  25. 25.
    Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991).  https://doi.org/10.1016/0890-5401(91)90052-4MathSciNetCrossRefzbMATHGoogle 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).  https://doi.org/10.1007/3-540-45931-6_24CrossRefzbMATHGoogle 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).  https://doi.org/10.1016/j.jpaa.2017.11.004MathSciNetCrossRefzbMATHGoogle 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). https://arxiv.org/1607.05830
  29. 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. 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/

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

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

Personalised recommendations