# Interleaving data and effects

## Publication Information

Robert Atkey and Patricia Johann.

*Interleaving data and effects*.

*Journal of Functional Programming* 25. 2015.

DOI:

10.1017/S0956796815000209## Abstract

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.

## Additional Information

This is a much extended version of a blog post about reasoning about stream processing in Haskell. This paper is intended as a more accessible version of the more theoretical paper Fibrational Induction Meets Effects by myself, Neil Ghani, Bart Jacobs, and Patricia Johann.