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