content: \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}
  