{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T18:21:47Z","timestamp":1693851707702},"reference-count":36,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T00:00:00Z","timestamp":1447977600000},"content-version":"unspecified","delay-in-days":323,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 <jats:italic>f<\/jats:italic>-algebra for an appropriate functor <jats:italic>f<\/jats:italic>. 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.<\/jats:p><jats:p>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 <jats:italic>f<\/jats:italic>-and-<jats:italic>m<\/jats:italic>-algebras, where the functor <jats:italic>f<\/jats:italic> describes the pure part of a datatype and the monad <jats:italic>m<\/jats:italic> describes the interleaved effects. Because initial <jats:italic>f<\/jats:italic>-and-<jats:italic>m<\/jats:italic>-algebras are the analogue for the effectful setting of initial <jats:italic>f<\/jats:italic>-algebras, they support the extension of the standard definitional and proof principles to the effectful setting.<\/jats:p><jats:p>Initial <jats:italic>f<\/jats:italic>-and-<jats:italic>m<\/jats:italic>-algebras are originally due to Filinski and St\u00f8vring, 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 <jats:italic>f<\/jats:italic>-and-<jats:italic>m<\/jats:italic>-algebras to a general functional programming audience.<\/jats:p>","DOI":"10.1017\/s0956796815000209","type":"journal-article","created":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T09:58:33Z","timestamp":1448013513000},"source":"Crossref","is-referenced-by-count":7,"title":["Interleaving data and effects"],"prefix":"10.1017","volume":"25","author":[{"given":"ROBERT","family":"ATKEY","sequence":"first","affiliation":[]},{"given":"PATRICIA","family":"JOHANN","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,11,20]]},"reference":[{"key":"S0956796815000209_ref36","volume-title":"Proceedings of the ACM SIGPLAN Workshop on Standard ML","author":"Wadler","year":"1998"},{"key":"S0956796815000209_ref35","first-page":"388","volume-title":"Proceedings of the 9th International Conference on Mathematics of Program Construction, MPC 2008","author":"Voightl\u00e4nder","year":"2008"},{"key":"S0956796815000209_ref34","first-page":"25","volume-title":"Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2007","author":"Swierstra","year":"2007"},{"key":"S0956796815000209_ref33","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"S0956796815000209_ref31","unstructured":"Sheard T. (1993b) Type Parametric Programming with Compile-Time Reflection. Technical Report, Oregon Graduate Institute of Science and Technology."},{"key":"S0956796815000209_ref30","unstructured":"Sheard T. (1993a) Adding algebraic methods to traditional functional languages by using reflection. Algebraic Methods and Software Technology."},{"key":"S0956796815000209_ref29","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"S0956796815000209_ref28","first-page":"90","volume-title":"Proceedings 4th Workshop on Mathematically Structured Functional Programming, MSFP 2012","author":"Pir\u00f3g","year":"2012"},{"key":"S0956796815000209_ref27","first-page":"71","volume-title":"Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1993","author":"Peyton Jones","year":"1993"},{"key":"S0956796815000209_ref25","unstructured":"Mulry P. S. (1995) Lifting theorems for Kleisli categories. In Mathematical Foundations of Programming Semantics, pp. 304\u2013319."},{"key":"S0956796815000209_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0956796815000209_ref23","first-page":"228","volume-title":"Proceedings of the First International Summer School on Advanced Functional Programming, AFP 1995","author":"Meijer","year":"1995"},{"key":"S0956796815000209_ref22","volume-title":"Categories for the Working Mathematician","author":"Mac Lane","year":"1998"},{"key":"S0956796815000209_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BF01752392"},{"key":"S0956796815000209_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"key":"S0956796815000209_ref18","first-page":"166","volume-title":"Proceedings of the 11th International Symposium on Functional and Logic Programming, FLOPS 2012","author":"Kiselyov","year":"2012"},{"key":"S0956796815000209_ref16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.003"},{"key":"S0956796815000209_ref12","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2004016"},{"key":"S0956796815000209_ref11","first-page":"113","volume-title":"Proceedings of Trends in Functional Programming, TFP 2009","author":"Ghani","year":"2009"},{"key":"S0956796815000209_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291168"},{"key":"S0956796815000209_ref21","first-page":"133","volume-title":"Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming, ICFP 2002","author":"L\u00fcth","year":"2002"},{"key":"S0956796815000209_ref14","unstructured":"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\u2013149."},{"key":"S0956796815000209_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680300488X"},{"key":"S0956796815000209_ref1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.16"},{"key":"S0956796815000209_ref10","unstructured":"Fokkinga M. M. (1994) Monadic Maps and Folds for Arbitrary Datatypes. Technical Report Memoranda Informatica 94-28. University of Twente."},{"key":"S0956796815000209_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-349-91518-7"},{"key":"S0956796815000209_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"S0956796815000209_ref17","unstructured":"J\u00fcrgensen C. (2002) Using Monads to Fuse Recursive Programs (Extended Abstract). Available at: citeseer.ist.psu.edu\/543861.html."},{"key":"S0956796815000209_ref26","first-page":"171","volume-title":"Advanced Functional Programming, 5th International School, AFP 2004","author":"Pardo","year":"2004"},{"key":"S0956796815000209_ref8","first-page":"175","volume-title":"Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1999","author":"Filinski","year":"1999"},{"key":"S0956796815000209_ref2","first-page":"42","volume-title":"Foundations of Software Science and Computational Structures, FoSSaCS 2012","author":"Atkey","year":"2012"},{"key":"S0956796815000209_ref3","volume-title":"Category Theory for Computing Science","author":"Barr","year":"1990"},{"key":"S0956796815000209_ref5","volume-title":"Algebra of Programming","author":"Bird","year":"1997"},{"key":"S0956796815000209_ref4","first-page":"42","volume-title":"Proceedings of the Applied Semantics, International Summer School, APPSEM 2000","author":"Benton","year":"2000"},{"key":"S0956796815000209_ref6","unstructured":"Crole R. L. & Pitts A. M. (1992) New foundations for fixpoint computations: Fix-hyperdoctrines and the fix-logic. Inform. Comput., no. 52, 171\u2013210."},{"key":"S0956796815000209_ref7","first-page":"206","volume-title":"Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006","author":"Danielsson","year":"2006"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796815000209","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T02:30:04Z","timestamp":1559874604000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796815000209\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":36,"alternative-id":["S0956796815000209"],"URL":"https:\/\/doi.org\/10.1017\/s0956796815000209","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"article-number":"e20"}}