Reference. Interleaving data and effects
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.
Cite
Cites 33 works (0 here)
External (33)
- Coproducts of Monads on Set (2012)
- Fibrational induction meets effects (2012)
- Iteratees (2012)
- An introduction to (co)algebra and (co)induction (2011)
- Short cut fusion of recursive programs with computational effects (2009)
- Data types à la carte (2008)
- Inductive reasoning about effectful data types (2007)
- Beauty in the beast (2007)
- Combining effects: Sum and tensor (2006)
- Fast and loose reasoning is morally correct (2006)
- Combining datatypes and effects (2005)
- Coproducts of Ideal Monads (2004)
- Two-level types and parameterized modules (2004)
- Origami programming (2003)
- Monads and effects (2002)
- Composing monads using coproducts (2002)
- Representing layered monads (1999)
- Categories for the Working Mathematician (2nd edn.) (1998)
- How to add laziness to a strict language without even being odd (1998)
- Algebra of Programming (1997)
- Relational Properties of Domains (1996)
- Merging monads and folds for functional programming (1995)
- Monadic maps and folds for arbitrary datatypes (tech report) (1994)
- Lifting theorems for Kleisli categories (1994)
- Imperative functional programming (1993)
- Adding algebraic methods to traditional functional languages by using reflection (1993)
- Type parametric programming with compile-time reflection (tech report) (1993)
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic (1992)
- Notions of computation and monads (1991)
- Category Theory for Computing Science (1990)
- Algebraic specification of data types: A synthetic approach (1981)
- An initial algebra approach to the specification, correctness and implementation of abstract data types (1978)
- A fixpoint theorem for complete categories (1968)