Jeremy Gibbons
Ralf Hinze
ABSTRACT
One of the appeals of pure functional programming is that it is so amenable to equational reasoning. One of the problems of pure functional programming is that it rules out computational effects. Moggi and Wadler showed how to get round this problem by using monads to encapsulate the effects, leading in essence to a phase distinction - a pure functional evaluation yielding an impure imperative computation. Still, it has not been clear how to reconcile that phase distinction with the continuing appeal of functional programming; does the impure imperative part become inaccessible to equational reasoning? We think not; and to back that up, we present a simple axiomatic approach to reasoning about programs with computational effects.
Supplemental Material
- N. Benton, J. Hughes, and E. Moggi. Monads and effects. In G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors, APPSEM 2000, volume 2395 of LNCS, pages 42--122. Springer, 2002. Google Scholar
Digital Library
- L. Erkök and J. Launchbury. Recursive monadic bindings. In ICFP, pages 174--185. ACM, September 2000. Google ScholarDigital Library
- M. Erwig and S. Kollmansberger. Probabilistic functional programming in Haskell. J. Funct. Prog., 16(1):21--34, 2006. Google ScholarDigital Library
- J. Gibbons and R. Bird. Effective reasoning about effectful traversals. Work in progress, Mar. 2011.Google Scholar
- M. Giry. A categorical approach to probability theory. In Categorical Aspects of Topology and Analysis, volume 915 of LNM, pages 68--85. Springer, 1981.Google Scholar
- S. Goncharov, L. Schröder, and T. Mossakowski. Kleene monads: Handling iteration in a framework of generic effects. In CALCO, volume 5728 of LNCS, pages 18--33, 2009. Google ScholarDigital Library
- R. Hinze. Prolog's control constructs in a functional setting: Axioms and implementation. Intern. J. Found. Comput. Sci., 12(2):125--170, 2001.Google ScholarCross Ref
- C. A. R. Hoare. A couple of novelties in the propositional calculus. Z. Math. Logik Grundlag. Math., 31(2):173--178, 1985.Google ScholarCross Ref
- G. Hutton and D. Fulger. Reasoning about effects: Seeing the wood through the trees. In TFP, May 2008.Google Scholar
- M. Hyland and J. Power. The category theoretic understanding of universal algebra: Lawvere theories and monads. Electron. Notes Theoret. Comput. Sci., 172:437--458, 2007. Google ScholarDigital Library
- C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In LICS, pages 186--195, 1989. Google ScholarDigital Library
- F. W. Lawvere. The category of probabilistic mappings. Preprint - we haven't managed to obtain a copy of this manuscript, 1962.Google Scholar
- F. W. Lawvere. Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, 1963. Also available with commentary as textitTheory and Applications of Categories Reprint 5.Google ScholarCross Ref
- S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.Google ScholarCross Ref
- A. McIver and C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Springer Verlag, 2005. Google Scholar
- E. Moggi. Notions of computation and monads. Inform. & Comput., 93(1), 1991. Google ScholarDigital Library
- A. Nanevski, G. Morrisett, and L. Birkedal. Hoare Type Theory, polymorphism and separation. J. Funct. Prog., 18(5,6):865--911, 2008. Google ScholarDigital Library
- A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent types for imperative programs. In ICFP, pages 229--240, 2008. Google ScholarDigital Library
- P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In POPL, pages 268--280, 2004. Google ScholarDigital Library
- B. O'Sullivan, J. Goerzen, and D. Stewart. Real World Haskell. O'Reilly, 2008. Google ScholarDigital Library
- S. Peyton Jones. Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In T. Hoare, M. Broy, and R. Steinbrüggen, editors, Engineering Theories of Software Construction, volume 180 of NATO Science Series, pages 47--96. IOS Press, 2001.Google Scholar
- S. Peyton Jones. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.Google Scholar
- S. Peyton Jones and P. Wadler. Imperative functional programming. In POPL, pages 71--84, 1993. Google ScholarDigital Library
- G. Plotkin and J. Power. Notions of computation determine monads. In FOSSACS, volume 2303 of LNCS, pages 342--356, 2002. Google ScholarDigital Library
- G. Plotkin and J. Power. Algebraic operations and generic effects. Appl. Cat. Struct., 11(1):69--94, 2003.Google ScholarCross Ref
- G. D. Plotkin and M. Pretnar. Handlers of algebraic effects. In ESOP, volume 5502 of LNCS, pages 80--94, 2009. Google ScholarDigital Library
- N. Ramsey and A. Pfeffer. Stochastic lambda calculus and monads of probability distributions. In POPL, pages 154--165, 2002. Google ScholarDigital Library
- J. Rosenhouse. The Monty Hall Problem: The Remarkable Story of Math's Most Contentious Brain Teaser. Oxford University Press, 2009.Google Scholar
- L. Schröder and T. Mossakowski. HasCasl: Integrated higher-order specification and program development. Theoretical Comput. Sci., 410(12-13):1217--1260, 2009. Google ScholarDigital Library
- W. Swierstra. A Functional Specification of Effects. PhD thesis, University of Nottingham, November 2008.Google Scholar
- W. Swierstra. A Hoare logic for the state monad. In TPHOLs, volume 5674 of LNCS, pages 440--451. Springer-Verlag, 2009. Google ScholarDigital Library
- W. Swierstra and T. Altenkirch. Beauty in the beast. In Haskell Workshop, pages 25--36, 2007. Google ScholarDigital Library
- R. Tix. Continuous D-Cones: Convexity and Powerdomain Constructions. PhD thesis, Technische Universität Darmstadt, 1999.Google Scholar
- D. Varacca and G. Winskel. Distributing probability over non-determinism. Math. Struct. Comput. Sci., 16(1):87--113, 2006. Google ScholarDigital Library
- M. Vos Savant. Ask Marilyn. Parade Magazine, 9th September 1990. See also http://www.marilynvossavant.com/articles/gameshow.html.Google Scholar
- P. Wadler. A critique of Abelson and Sussman: Why calculating is better than scheming. SIGPLAN Not., 22(3):8, 1987. Google ScholarDigital Library
- P. Wadler. Comprehending monads. Math. Struct. Comput. Sci., 2(4):461--493, 1992.Google ScholarCross Ref
- P. Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi: Proceedings of the Marktoberdorf Summer School, 1992.Google Scholar
- A. Yakeley, textitet al. MonadPlus reform proposal. http://www.haskell.org/haskellwiki/MonadPlus_reform_proposal, Jan. 2006.Google Scholar
- W. Yi and K. G. Larsen. Testing probabilistic and nondeterministic processes. In Protocol Specification, Testing and Verification XII, pages 47--61, 1992. Google ScholarDigital Library
Index Terms
- Just do it: simple monadic equational reasoning
Recommendations
Just do it: simple monadic equational reasoning
ICFP '11One of the appeals of pure functional programming is that it is so amenable to equational reasoning. One of the problems of pure functional programming is that it rules out computational effects. Moggi and Wadler showed how to get round this problem by ...
Monad-independent Dynamic Logic in HasCasl
Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. In previous work, we have introduced a Hoare calculus for partial correctness of monadic programs. All this has been ...
Extensional Higher-Order Paramodulation in Leo-III
AbstractLeo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...
Comments