Hostname: page-component-8448b6f56d-dnltx Total loading time: 0 Render date: 2024-04-15T13:39:46.128Z Has data issue: false hasContentIssue false
  • English
  • Français

Interleaving data and effects

Part of: JFP Research Articles

Published online by Cambridge University Press:  20 November 2015

ROBERT ATKEY  and
PATRICIA JOHANN
ROBERT ATKEY
Affiliation:
University of Strathclyde, Glasgow, Scotland (e-mail: robert.atkey@strath.ac.uk)
PATRICIA JOHANN
Affiliation:
Appalachian State University, Boone, North Carolina, USA (e-mail: johannp@appstate.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The study of programming with and reasoning about inductive datatypes such as lists and trees has benefited from the simple categorical principle of initial algebras. In initial algebra semantics, each inductive datatype is represented by an initial f-algebra for an appropriate functor f. The initial algebra principle then supports the straightforward derivation of definitional principles and proof principles for these datatypes. This technique has been expanded to a whole methodology of structured functional programming, often called origami programming.

In this article we show how to extend initial algebra semantics from pure inductive datatypes to inductive datatypes interleaved with computational effects. Inductive datatypes interleaved with effects arise naturally in many computational settings. For example, incrementally reading characters from a file generates a list of characters interleaved with input/output actions, and lazily constructed infinite values can be represented by pure data interleaved with the possibility of non-terminating computation. Straightforward application of initial algebra techniques to effectful datatypes leads either to unsound conclusions if we ignore the possibility of effects, or to unnecessarily complicated reasoning because the pure and effectful concerns must be considered simultaneously. We show how pure and effectful concerns can be separated using the abstraction of initial f-and-m-algebras, where the functor f describes the pure part of a datatype and the monad m describes the interleaved effects. Because initial f-and-m-algebras are the analogue for the effectful setting of initial f-algebras, they support the extension of the standard definitional and proof principles to the effectful setting.

Initial f-and-m-algebras are originally due to Filinski and Støvring, who studied them in the category Cpo. They were subsequently generalised to arbitrary categories by Atkey, Ghani, Jacobs, and Johann in a FoSSaCS 2012 paper. In this article we aim to introduce the general concept of initial f-and-m-algebras to a general functional programming audience.

Type
Articles
Information
Journal of Functional Programming , Volume 25 , 2015 , e20
Copyright
Copyright © Cambridge University Press 2015 

References

Adámek, J., Bowler, N., Levy, P. B. & Milius, S. (2012) Coproducts of monads on set. In Dershowitz, N. (ed), Proceedings of the 27th Annual ACM/IEEE Symposium on Logic In Computer Science, LICS 2012, Dubrovnik, Croatia: ACM, pp. 45–54.CrossRefGoogle Scholar
Atkey, R., Ghani, N., Jacobs, B. & Johann, P. (2012) Fibrational induction meets effects. In Birkedal, L. (ed), Foundations of Software Science and Computational Structures, FoSSaCS 2012, Lecture Notes in Computer Science, vol. 7213, Tallinn, Estonia: Springer, pp. 42–57.Google Scholar
Barr, M. & Wells, C. (1990) Category Theory for Computing Science. Prentice Hall.Google Scholar
Benton, N., Hughes, J. & Moggi, E. (2000) Monads and effects. In Barthe, G., Dybjer, P., Pinto, L. & Saraiva, J. (eds), Proceedings of the Applied Semantics, International Summer School, APPSEM 2000. Lecture Notes in Computer Science, vol. 2395, Caminha, Portugal: Springer, pp. 42–122.Google Scholar
Bird, R. S. & de Moor, O. (1997) Algebra of Programming. Prentice Hall.Google Scholar
Crole, R. L. & Pitts, A. M. (1992) New foundations for fixpoint computations: Fix-hyperdoctrines and the fix-logic. Inform. Comput., no. 52, 171–210.Google Scholar
Danielsson, N. A., Hughes, J., Jansson, P. & Gibbons, J. (2006) Fast and loose reasoning is morally correct. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA: ACM, pp. 206–217.Google Scholar
Filinski, A. (1999) Representing layered monads. In Appel, A. W. & Aiken, A. (eds), Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999, San Antonio, Texas, USA: ACM, pp. 175–188.Google Scholar
Filinski, A. & Støvring, K. (2007) Inductive reasoning about effectful data types. In Hinze, R. & Ramsey, N. (eds), Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany: ACM, pp. 97–110.Google Scholar
Fokkinga, M. M. (1994) Monadic Maps and Folds for Arbitrary Datatypes. Technical Report Memoranda Informatica 94-28. University of Twente.Google Scholar
Ghani, N. & Johann, P. (2009) Short cut fusion of recursive programs with computational effects. In Proceedings of Trends in Functional Programming, TFP 2009, no. 9, Komarno, Solvakia: Kluwer, pp. 113–128.Google Scholar
Ghani, N. & Uustalu, T. (2004) Coproducts of ideal monads. Theoretical Informatics and Applications 38 (4), 321–342.CrossRefGoogle Scholar
Gibbons, J. (2003) Origami programming. In The Fun of Programming, Gibbons, J. & de Moor, O. (eds), Cornerstones in Computing. Palgrave.CrossRefGoogle Scholar
Goguen, J. A., Thatcher, J. & Wagner, E. (1978) An initial algebra approach to the specification, correctness and implementation of abstract data types. In Yeh, R. (ed), Current Trends in Programming Methodology, pp. 80–149.Google Scholar
Hyland, M., Plotkin, G. D. & Power, J. (2006) Combining effects: Sum and tensor. Theor. Comput. Sci. 357 (1–3), 70–99.CrossRefGoogle Scholar
Jacobs, B. & Rutten, J. (2011) A tutorial on (co)algebras and (co)induction. In Advanced Topics in Bisimulation and Coinduction, Sangiorgi, D. & Rutten, J. (eds), Tracts in Theoretical Computer Science, no. 52. Cambridge University Press, pp. 38–99.CrossRefGoogle Scholar
Jürgensen, C. (2002) Using Monads to Fuse Recursive Programs (Extended Abstract). Available at: citeseer.ist.psu.edu/543861.html.Google Scholar
Kiselyov, O. (2012) Iteratees. In Schrijvers, T. & Thiemann, P. (eds), Proceedings of the 11th International Symposium on Functional and Logic Programming, FLOPS 2012, Lecture Notes in Computer Science, vol. 7294, Kanazawa, Japan: Springer, pp. 166–181.Google Scholar
Lambek, J. (1968) A fixed point theorem for complete categories. Math. Z. 103, 151–161.CrossRefGoogle Scholar
Lehman, D. J. & Smyth, M. B. (1981) Algebraic specification of data types: A synthetic approach. Mathematical Systems Theory, no. 14, 97–139.CrossRefGoogle Scholar
Lüth, C. & Ghani, N. (2002) Composing monads using coproducts. In Wand, M. & Jones, SimonPeyton, L. (eds), Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, ICFP 2002, Pittsburgh, Pennsylvania, USA: ACM, pp. 133–144.Google Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics, no. 5. Springer-Verlag.Google Scholar
Meijer, E. & Jeuring, J. (1995) Merging moands and folds for functional programming. In Proceedings of the First International Summer School on Advanced Functional Programming, AFP 1995, vol. 925, Lecture Notes in Computer Science, Båstad, Sweden: Springer, pp. 228–266.Google Scholar
Moggi, E. (1991) Notions of computation and monads. Inform. Comput. 93 (1), 55–92.CrossRefGoogle Scholar
Mulry, P. S. (1995) Lifting theorems for Kleisli categories. In Mathematical Foundations of Programming Semantics, pp. 304–319.Google Scholar
Pardo, A. (2004) Combining datatypes and effects. In Vene, V. & Uustalu, T. (eds), Advanced Functional Programming, 5th International School, AFP 2004, Lecture Notes in Computer Science, vol. 3622, Tartu, Estonia: Springer, pp. 171–209.Google Scholar
Peyton Jones, S. L. & Wadler, P. (1993) Imperative functional programming. In Deusen, M. S. Van, & Lang, B. (eds), Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1993, Charleston, South Carolina, USA: ACM, pp. 71–84.Google Scholar
Piróg, M. & Gibbons, J. (2012) Tracing monadic computations and representing effects. In Chapman, J. & Levy, P. B. (eds), Proceedings 4th Workshop on Mathematically Structured Functional Programming, MSFP 2012, Electronic Proceedings in Theoretical Computer Science, vol. 76, Tallinn, Estonia: British Computer Society, pp. 90–111.Google Scholar
Pitts, A. M. (1996) Relational properties of domains. Inf. Comput. 127 (2), 66–90.CrossRefGoogle Scholar
Sheard, T. (1993a) Adding algebraic methods to traditional functional languages by using reflection. Algebraic Methods and Software Technology.Google Scholar
Sheard, T. (1993b) Type Parametric Programming with Compile-Time Reflection. Technical Report, Oregon Graduate Institute of Science and Technology.Google Scholar
Sheard, T. & Pasalic, E. (2004) Two-level types and parameterized modules. J. Funct. Program. 14 (5), 547–587.CrossRefGoogle Scholar
Swierstra, W. (2008) Data types à la carte. J. Funct. Program. 18 (4), 423–436.CrossRefGoogle Scholar
Swierstra, W. & Altenkirch, T. (2007) Beauty in the beast. In Keller, G. (ed), Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2007, Freiburg, Germany: ACM, pp. 25–36.Google Scholar
Voightländer, J. (2008) Asymptotic improvement of computations over free monads. In Proceedings of the 9th International Conference on Mathematics of Program Construction, MPC 2008, Luminy, France: Springer, pp. 388–403.Google Scholar
Wadler, P., Taha, W. & MacQueen, D. 1998 (September) How to add laziness to a strict language without even being odd. Proceedings of the ACM SIGPLAN Workshop on Standard ML, Baltimore, Maryland, USA: ACM.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.