\begin{comment} \begin{code} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RecordWildCards #-} module LiveCoding.Coalgebra where -- base import Control.Arrow (second) import Data.Data -- essence-of-live-coding import LiveCoding.Cell \end{code} \end{comment} \section{Monadic stream functions and final coalgebras} \label{sec:msfs and final coalgebras} \mintinline{haskell}{Cell}s mimick Dunai's \cite{Dunai} monadic stream functions (\mintinline{haskell}{MSF}s) closely. But can they fill their footsteps completely in terms of expressiveness? If not, which programs exactly can be represented as \mintinline{haskell}{MSF}s and which can't? To find the answer to these questions, let us reexamine both types. With the help of a simple type synonym, the \mintinline{haskell}{MSF} definition can be recast in explicit fixpoint form: \begin{code} type StateTransition m a b s = a -> m (b, s) data MSF m a b = MSF { unMSF :: StateTransition m a b (MSF m a b) } \end{code} This definition tells us that monadic stream functions are so-called \emph{final coalgebras} of the \mintinline{haskell}{StateTransition} functor (for fixed \mintinline{haskell}{m}, \mintinline{haskell}{a}, and \mintinline{haskell}{b}). An ordinary coalgebra for this functor is given by some type \mintinline{haskell}{s} and a coalgebra structure map: \begin{code} data Coalg m a b where Coalg :: s -> (s -> StateTransition m a b s) -> Coalg m a b \end{code} But hold on, the astute reader will intercept, is this not simply the definition of \mintinline{haskell}{Cell}? Alas, it is not, for it lacks the type class restriction \mintinline{haskell}{Data s}, which we need so dearly for the type migration. Any cell is a coalgebra, but only those coalgebras that satisfy this type class are a cell. Oh, if only there were no such distinction. By the very property of the final coalgebra, we can embed every coalgebra therein: \begin{code} finality :: Monad m => Coalg m a b -> MSF m a b finality (Coalg state step) = MSF $\a -> do (b, state') <- step state a return (b, finality$ Coalg state' step) \end{code} And analogously, every cell can be easily made into an \mintinline{haskell}{MSF} without loss of information: \begin{code} finalityC :: Monad m => Cell m a b -> MSF m a b finalityC Cell { .. } = MSF $\a -> do (b, cellState') <- cellStep cellState a return (b, finalityC$ Cell cellState' cellStep) \end{code} And the final coalgebra is of course a mere coalgebra itself: \begin{code} coalgebra :: MSF m a b -> Coalg m a b coalgebra msf = Coalg msf unMSF \end{code} But we miss the abilty to encode \mintinline{haskell}{MSF}s as \mintinline{haskell}{Cell}s by just the \mintinline{haskell}{Data} type class: \begin{code} coalgebraC :: Data (MSF m a b) => MSF m a b -> Cell m a b coalgebraC msf = Cell msf unMSF \end{code} We are out of luck if we would want to derive an instance of \mintinline{haskell}{Data (MSF m a b)}. Monadic stream functions are, well, functions, and therefore have no \mintinline{haskell}{Data} instance. The price of \mintinline{haskell}{Data} is loss of higher-order state. Just how big this loss is will be demonstrated in the following section. \begin{comment} \subsection{Initial algebras} \begin{code} type AlgStructure m a b s = StateTransition m a b s -> s data Alg m a b where Alg :: s -> AlgStructure m a b s -> Alg m a b algMSF :: MSF m a b -> Alg m a b algMSF msf = Alg msf MSF -- TODO Could explain better why this is simpler in the coalgebra case initiality :: Functor m => AlgStructure m a b s -> MSF m a b -> s initiality algStructure = go where go msf = algStructure $\a -> second go <$> unMSF msf a \end{code} \end{comment}