\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 { MSF m a b -> StateTransition m a b (MSF m a b) 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 m a b -> MSF m a b finality (Coalg s state s -> StateTransition m a b s step) = StateTransition m a b (MSF m a b) -> MSF m a b forall (m :: * -> *) a b. StateTransition m a b (MSF m a b) -> MSF m a b MSF (StateTransition m a b (MSF m a b) -> MSF m a b) -> StateTransition m a b (MSF m a b) -> MSF m a b forall a b. (a -> b) -> a -> b $ \a a -> do (b b, s state') <- s -> StateTransition m a b s step s state a a (b, MSF m a b) -> m (b, MSF m a b) forall (m :: * -> *) a. Monad m => a -> m a return (b b, Coalg m a b -> MSF m a b forall (m :: * -> *) a b. Monad m => Coalg m a b -> MSF m a b finality (Coalg m a b -> MSF m a b) -> Coalg m a b -> MSF m a b forall a b. (a -> b) -> a -> b $ s -> (s -> StateTransition m a b s) -> Coalg m a b forall s (m :: * -> *) a b. s -> (s -> StateTransition m a b s) -> Coalg m a b Coalg s state' s -> StateTransition m a b s 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 m a b -> MSF m a b finalityC Cell { s s -> a -> m (b, s) cellStep :: () cellState :: () cellStep :: s -> a -> m (b, s) cellState :: s .. } = StateTransition m a b (MSF m a b) -> MSF m a b forall (m :: * -> *) a b. StateTransition m a b (MSF m a b) -> MSF m a b MSF (StateTransition m a b (MSF m a b) -> MSF m a b) -> StateTransition m a b (MSF m a b) -> MSF m a b forall a b. (a -> b) -> a -> b $ \a a -> do (b b, s cellState') <- s -> a -> m (b, s) cellStep s cellState a a (b, MSF m a b) -> m (b, MSF m a b) forall (m :: * -> *) a. Monad m => a -> m a return (b b, Cell m a b -> MSF m a b forall (m :: * -> *) a b. Monad m => Cell m a b -> MSF m a b finalityC (Cell m a b -> MSF m a b) -> Cell m a b -> MSF m a b forall a b. (a -> b) -> a -> b $ s -> (s -> a -> m (b, s)) -> Cell m a b forall (m :: * -> *) a b s. Data s => s -> (s -> a -> m (b, s)) -> Cell m a b Cell s cellState' s -> a -> m (b, s) 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 m a b -> Coalg m a b coalgebra MSF m a b msf = MSF m a b -> (MSF m a b -> StateTransition m a b (MSF m a b)) -> Coalg m a b forall s (m :: * -> *) a b. s -> (s -> StateTransition m a b s) -> Coalg m a b Coalg MSF m a b msf MSF m a b -> StateTransition m a b (MSF m a b) forall (m :: * -> *) a b. MSF m a b -> StateTransition m a b (MSF m a b) 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 m a b -> Cell m a b coalgebraC MSF m a b msf = MSF m a b -> (MSF m a b -> a -> m (b, MSF m a b)) -> Cell m a b forall (m :: * -> *) a b s. Data s => s -> (s -> a -> m (b, s)) -> Cell m a b Cell MSF m a b msf MSF m a b -> a -> m (b, MSF m a b) forall (m :: * -> *) a b. MSF m a b -> StateTransition m a b (MSF m a b) 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 m a b -> Alg m a b algMSF MSF m a b msf = MSF m a b -> AlgStructure m a b (MSF m a b) -> Alg m a b forall s (m :: * -> *) a b. s -> AlgStructure m a b s -> Alg m a b Alg MSF m a b msf AlgStructure m a b (MSF m a b) forall (m :: * -> *) a b. StateTransition m a b (MSF m a b) -> MSF m a b 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 m a b s -> MSF m a b -> s initiality AlgStructure m a b s algStructure = MSF m a b -> s go where go :: MSF m a b -> s go MSF m a b msf = AlgStructure m a b s algStructure AlgStructure m a b s -> AlgStructure m a b s forall a b. (a -> b) -> a -> b $ \a a -> (MSF m a b -> s) -> (b, MSF m a b) -> (b, s) forall (a :: * -> * -> *) b c d. Arrow a => a b c -> a (d, b) (d, c) second MSF m a b -> s go ((b, MSF m a b) -> (b, s)) -> m (b, MSF m a b) -> m (b, s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> MSF m a b -> StateTransition m a b (MSF m a b) forall (m :: * -> *) a b. MSF m a b -> StateTransition m a b (MSF m a b) unMSF MSF m a b msf a a \end{code} \end{comment}