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