Abstract
The combination of probabilistic and nondeterministic choice in program calculi is a notoriously tricky problem, and one with a long history. We present a simple functional programming approach to this challenge, based on algebraic theories of computational effects. We make use of the powerful abstraction facilities of modern functional languages, to introduce the choice operations as a little embedded domain-specific language rather than having to define a language extension; we rely on referential transparency, to justify straightforward equational reasoning about program behaviour.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer (1998), graduate Texts in Computer Science
Beck, J.: Distributive laws. In: Seminar on Triples and Categorical Homology Theory. Lecture Notes in Mathematics, vol. 80, pp. 119–140. Springer (1969)
Bird, R., de Moor, O.: Algebra of Programming. Prentice-Hall (1997)
Dean, J., Ghemawat, S.: MapReduce: Simplified data processing on large clusters. In: Operating Systems Design & Implementation, pp. 137–150. USENIX Association (2004)
Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C., Zhang, C.: Remarks on testing probabilistic processes. Electronic Notes in Theoretical Computer Science 172, 359–397 (2007)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice-Hall (1976)
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification. Springer (1985)
Eilenberg, S., Moore, J.C.: Adjoint functors and triples. Illinois Journal of Mathematics, 381–398 (1965)
Erwig, M., Kollmansberger, S.: Probabilistic functional programming in Haskell. Journal of Functional Programming 16(1), 21–34 (2006)
Gibbons, J., Hinze, R.: Just do it: Simple monadic equational reasoning. In: Danvy, O. (ed.) International Conference on Functional Programming, pp. 2–14. ACM, New York (2011)
Giry, M.: A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis. Lecture Notes in Mathematics, vol. 915, pp. 68–85. Springer (1981)
He, J., Seidel, K., McIver, A.: Probabilistic models for the Guarded Command Language. Science of Computer Programming 28, 171–192 (1997)
Hehner, E.C.R.: Predicative programming, parts I and II. Communications of the ACM 27(2), 134–151 (1984)
Hinze, R.: Deriving backtracking monad transformers. In: International Conference on Functional Programming, pp. 186–197 (2000)
Hoare, C.A.R.: A couple of novelties in the propositional calculus. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 31(2), 173–178 (1985)
Hoare, C.A.R., Hanna, F.K.: Programs are predicates. Philosophical Transactions of the Royal Society, Part A 312(1522), 475–489 (1984)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall (1998)
Hutton, G., Fulger, D.: Reasoning about effects: Seeing the wood through the trees. In: Preproceedings of Trends in Functional Programming (May 2008)
Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. Electronic Notes in Theoretical Computer Science 172, 437–458 (2007)
Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: Logic in Computer Science, pp. 186–195 (1989)
Kiselyov, O., Shan, C.-c.: Embedded Probabilistic Programming. In: Taha, W.M. (ed.) DSL 2009. LNCS, vol. 5658, pp. 360–384. Springer, Heidelberg (2009)
Kleisli, H.: Every standard construction is induced by a pair of adjoint functors. Proceedings of the American Mathematical Society 16, 544–546 (1965)
Knuth, D.E., Yao, A.C.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 357–428. Academic Press (1976); reprinted in Selected Papers on Analysis of Algorithms (CSLI 2000)
Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22, 328–350 (1981)
Launchbury, J.: Lazy imperative programming. In: ACM SIGPLAN Workshop on State in Programming Languages (June 1993)
Lawvere, F.W.: Functorial Semantics of Algebraic Theories. Ph.D. thesis, Columbia University, also available with commentary as Theory and Applications of Categories Reprint 5 (1963), http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html
Lawvere, F.W.: The category of probabilistic mappings (1962) (preprint)
Linton, F.E.J.: Some aspects of equational theories. In: Categorical Algebra, pp. 84–95. Springer, La Jolla (1966)
Lowe, G.: Representing nondeterministic and probabilistic behaviour in reactive processes (1993) (manuscript) Oxford University Computing Laboratory
Mac Lane, S.: Categories for the Working Mathematician. Springer (1971)
McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005)
McIver, A.K., Weber, T.: Towards Automated Proof Support for Probabilistic Distributed Systems. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 534–548. Springer, Heidelberg (2005)
McKinna, J.: Why dependent types matter. In: Principles of Programming Languages, p. 1. ACM (2006), full paper available at, http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Meinicke, L., Solin, K.: Refinement algebra for probabilistic programs. Formal Aspects of Computing 22, 3–31 (2010)
Mislove, M.W.: Nondeterminism and Probabilistic Choice: Obeying the Laws. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 350–364. Springer, Heidelberg (2000)
Moggi, E.: Notions of computation and monads. Information and Computation 93(1) (1991)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall (1994)
Morgan, C.: Elementary Probability Theory in the Eindhoven Style. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol. 7342, pp. 48–73. Springer, Heidelberg (2012)
Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects of Computing 8(6), 617–647 (1996)
Peyton Jones, S.: Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In: Hoare, T., Broy, M., Steinbruggen, R. (eds.) Engineering Theories of Software Construction, pp. 47–96. IOS Press (2001)
Piróg, M., Gibbons, J.: Tracing monadic computations and representing effects. In: Mathematically Structured Functional Programming (March 2012)
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)
Plotkin, G., Pretnar, M.: Handlers of Algebraic Effects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 80–94. Springer, Heidelberg (2009)
Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Principles of Programming Languages, pp. 154–165 (2002)
Rosenhouse, J.: The Monty Hall Problem: The Remarkable Story of Math’s Most Contentious Brain Teaser. Oxford University Press (2009)
Spivey, M.: A functional theory of exceptions. Science of Computer Programming 14, 25–42 (1990)
Spivey, M., Seres, S.: Combinators for logic programming. In: Gibbons, J., de Moor, O. (eds.) The Fun of Programming, pp. 177–200. Cornerstones in Computing, Palgrave (2003)
Turner, D.A.: Total functional programming. Journal of Universal Computer Science 10(7), 751–768 (2004)
Varacca, D., Winskel, G.: Distributing probability over nondeterminism. Mathematical Structures in Computer Science 16, 87–113 (2006)
Vos Savant, M.: Ask Marilyn. Parade Magazine (September 9th, 1990), http://www.marilynvossavant.com/articles/gameshow.html
Wadler, P.: How to Replace Failure by a List of Successes: A Method for Exception Handling, Backtracking, and Pattern Matching in Lazy Functional Languages. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 113–128. Springer, Heidelberg (1985), http://dx.doi.org/10.1007/3-540-15975-4_33
Wadler, P.: Theorems for free? In: Functional Programming Languages and Computer Architecture, pp. 347–359. ACM (1989), http://doi.acm.org/10.1145/99370.99404
Wadler, P.: Comprehending monads. Mathematical Structures in Computer Science 2(4), 461–493 (1992)
Wadler, P.: Monads for functional programming. In: Broy, M. (ed.) Program Design Calculi: Proceedings of the Marktoberdorf Summer School (1992)
Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. In: Linn Jr., R.J., Uyar, M.Ü. (eds.) Protocol Specification, Testing and Verification, pp. 47–61. North-Holland (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gibbons, J. (2013). Unifying Theories of Programming with Monads. In: Wolff, B., Gaudel, MC., Feliachi, A. (eds) Unifying Theories of Programming. UTP 2012. Lecture Notes in Computer Science, vol 7681. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35705-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-35705-3_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35704-6
Online ISBN: 978-3-642-35705-3
eBook Packages: Computer ScienceComputer Science (R0)