Interleaving Data and Effects
Patricia Johann, Neil Ghani, Bart Jacobs and myself have just submitted a paper on interleaving pure data types with effects. This is a much more detailed version of the blog post I wrote back in January on reasoning about stream processing with effects.
Here is the 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. Straightforward application of initial algebra techniques to effectful datatypes leads to unnecessarily complicated reasoning, because the pure and effectful concerns must be considered simultaneously. We show how these concerns can be separated 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. Because initial f-and-m-algebras separate pure and effectful concerns, they support the direct transfer of definitions and proofs from the pure setting to the effectful setting.
Initial f-and-m-algebras are originally due to Filinski and Støvring, and were subsequently generalised to arbitrary categories by the authors of this article. In this article, we aim to introduce the concept of initial f-and-m-algebras to a general functional programming audience.
The actual paper is available here.