Just do It: Simple Monadic Equational Reasoning
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, leadin...
| Main Authors: | , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2011
|
| _version_ | 1797068785003266048 |
|---|---|
| author | Gibbons, J Hinze, R |
| author_facet | Gibbons, J Hinze, R |
| author_sort | Gibbons, J |
| collection | OXFORD |
| description | 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. Copyright © 2011 ACM. |
| first_indexed | 2024-03-06T22:15:06Z |
| format | Journal article |
| id | oxford-uuid:5320ebb8-53d0-47c2-ab30-32f5fab8826b |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T22:15:06Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:5320ebb8-53d0-47c2-ab30-32f5fab8826b2022-03-26T16:29:38ZJust do It: Simple Monadic Equational ReasoningJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:5320ebb8-53d0-47c2-ab30-32f5fab8826bEnglishSymplectic Elements at Oxford2011Gibbons, JHinze, ROne 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. Copyright © 2011 ACM. |
| spellingShingle | Gibbons, J Hinze, R Just do It: Simple Monadic Equational Reasoning |
| title | Just do It: Simple Monadic Equational Reasoning |
| title_full | Just do It: Simple Monadic Equational Reasoning |
| title_fullStr | Just do It: Simple Monadic Equational Reasoning |
| title_full_unstemmed | Just do It: Simple Monadic Equational Reasoning |
| title_short | Just do It: Simple Monadic Equational Reasoning |
| title_sort | just do it simple monadic equational reasoning |
| work_keys_str_mv | AT gibbonsj justdoitsimplemonadicequationalreasoning AT hinzer justdoitsimplemonadicequationalreasoning |