Nottingham FP Lab Blog

FP -vs- OO bialgebraically (“Expression Lemma”)

by Ondrej on February 22, 2008.
Tagged as: Lunches.

Today I showed how distributive laws of a monad over a comonad and adequacy results for bialgebraic operational semantics [Plotkin & Turi] can be used to formalize the correspondence between (certain) FP algebraic datatypes with functions (essentially implementations of abstract data types) and recursive OO structures (collections of classes with the same interface).

In short, given a functor $\Sigma$ standing for the signature of a datatype and a (finite) collection of functions $f_i\,:\,\mu\Sigma\rightarrow B_i\mu\Sigma$ (where $\mu\Sigma$ is the least fixed point of $\Sigma$ and each B_i is a functor), we can form the tupple $\langle f_i \rangle_i\,:\,\mu\Sigma\rightarrow(\Pi_i B_i)\mu\Sigma$ . Let be defined as the product $B\triangleq\Pi_i B_i$ . This arrow $\langle f_i \rangle_i$ is quite often a catamorphism whose algebra factors through a natural transformation $\lambda:\Sigma B \Rightarrow B \Sigma$ , thus $\langle f_i \rangle_i \;=\;\textsf{fold}(B \textsf{in}\circ\lambda)$ , where $\textsf{in}$ is the initial $\Sigma$ -algebra. Informally, $\lambda$ here combines recursive results from subterms and $B\textsf{in}$ packs recursive results into a new instance of $\mu\Sigma$ (for instance in a catamorphically defined map).

On the other hand, let us take the colagebraic view of objects [e.g. Jacobs] where interfaces are (certain) polynomial endofunctors, classes are coalgebras and object types are carriers of terminal coalgebras. Then a collection of classes with the same interface, , whose carriers are respectively given by the cases of the algebraic datatype functor $\Sigma$ are defined by a single coalgebra $\phi\,:\,\Sigma\nu B \rightarrow B\Sigma \nu B$ (where $\nu B$ is the greatest fixed point of , i.e. the carrier of the terminal -coalgebra). Let us take $\phi\,\triangleq\,\lambda\circ\Sigma\mathsf{out}$ . This corresponds to the classes recursively delegating to their subcomponents and then combining the resulting collection of behaviours into a behaviour on a collection.

Now $\mathsf{unfold}(\mathsf{fold}(B\mathsf{in}\circ\lambda))\;=\;\mathsf{fold}(\mathsf{unfold}(\lambda\circ\Sigma\mathsf{out}))\;:\;\mu\Sigma\rightarrow\nu B$ . This means that the functional program defined by a fold over an algebraic datatype, when wrapped up as an abstract datatype with interface , is bisimilar to the object constructed by folding a class constructor over a tree of object states. Note that in the latter case, each layer is first turned into a collection of objects (by $\mathsf{unfold}(\lambda\circ\Sigma\mathsf{out})$ ) which are then used to construct an object at the next level (as common in OO). In the first functional case, the functions are defined directly on an open datatype and the whole result is then interpreted as an abstract data type (object).

The situation generalizes straightforwardly for more general distributive laws of a monad over a comonad, in particular when the monad is free and comonad cofree. Thus $\lambda:T_\Sigma D_B \Rightarrow D_B T_\Sigma$ . This allows us to express a larger class of OO and FP programs while still preserving their bisimilarity.

A paper about this has been recently submitted for conference publication. The preliminary version and some relevant Haskell implementation can be found here.