%\section{Proof isomorphism |Producer| and |Producer'|}
\section{Both Producer Representations are Isomorphic}
\label{app:proof-iso-mr}

We show the |Producer| case, an analogous strategy works for |Consumer|.

\begin{theorem}

The types |Producer' o| and |Producer o| are isomorphic.

\end{theorem}

\begin{proof}

We show this by using $\mu x.$ |G[x] = forall x. (G[x] -> x) -> x| \cite{Plotkin:1993:LPP:645891.671433}.

\begin{tabbing}
 = \= xx \= xx \kill
   \> |Producer' o| \\
 $=$ \> \> (see Appendix~\ref{app:proof-scott}) \\
   \> $\forall r.$ |SP o r| \\
 $=$ \> \> (def. |SP|) \\
   \> $\forall r. \mu x. $ |(o -> x -> r) -> r| \\
 $=$ \> \> (property $\mu$) \\
   \> $\forall r. \forall x.$ |(((o -> x -> r) -> r) -> x) -> x| \\
 $=$ \> \> (swap $\forall$) \\
   \> $\forall x. \forall r.$ |(((o -> x -> r) -> r) -> x) -> x| \\
 $=$ \> \> (property $\mu$) \\
   \> $\mu x. \forall r.$ |(o -> x -> r) -> r| \\
 $=$ \> \> (uncurry) \\
   \> $\mu x. \forall r.$ |((o, x) -> r) -> r| \\
 $=$ \> \> (property $\mu$) \\
   \> $\mu x. \mu r.$ |(o, x)| \\
 $=$ \> \> (drop unused $\mu$) \\
   \> $\mu x.$ |(o, x)| \\
 $=$ \> \> (def. |Producer|) \\
   \> |Producer o| \\
\end{tabbing}

\end{proof}

An isomorphism consists of two inverses, here |mr| and |mr'|, for which |mr' . mr = id| and |mr . mr' = id| holds.
Where |mr| is defined as:

< mr :: Producer x -> Producer' x
< mr (Producer o r) (ConsPar h) = h o (ProdPar (mr r))

And |mr'| is defined as:

< mr' :: Producer' x -> Producer x
< mr' f = f (ConsPar (\x p -> Producer x (helpermr' p)))
<
< helpermr' :: ProdPar x (Producer x) -> Producer x
< helpermr' (ProdPar f) = f (ConsPar (\x prod -> Producer x (helpermr' prod)))

We prove the first equation |mr' . mr = id|.

\begin{theorem}

|mr' . mr = id|.

\end{theorem}


\begin{proof}

We show this by equational reasoning.

\begin{tabbing}
 = \= xx \= xx \kill
   \> |mr' . mr| \\
 $=$ \> \> (eta-expansion) \\
   \> |\x -> mr' (mr x)| \\
 $=$ \> \> (def. |mr|) \\
   \> |\x -> mr' (case x of (Producer o r) -> \(ConsPar h) -> h o (ProdPar (mr r)))| \\
 $=$ \> \> (case analysis on |x|) \\
   \> |\(Producer o r) -> mr' (\(ConsPar h) -> h o (ProdPar (mr r)))| \\
 $=$ \> \> (def. |mr'|) \\
   \> |\(Producer o r) -> (\(ConsPar h) ->| \\
   \> \> |h o (ProdPar (mr r))) (ConsPar (\x p -> Producer x (helpermr' p)))| \\
 $=$ \> \> (beta-reduction) \\
   \> |\(Producer o r) -> Producer o (helpermr' (ProdPar (mr r)))| \\
 $=$ \> \> (def. |helpermr'|) \\
   \> |\(Producer o r) -> Producer o (mr r (ConsPar (\x prod -> Producer x (helpermr' prod))))| \\
 $=$ \> \> (def. |mr'|) \\
   \> |\(Producer o r) -> Producer o (mr' (mr r))| \\
 $=$ \> \> (coinduction hypothesis) \\
   \> |\(Producer o r) -> Producer o r| \\
 $=$ \> \> (def. |id|) \\
   \> |id| \\
\end{tabbing}

\end{proof}

The second equation |mr . mr' = id| is more complicated since we cannot do case analysis
on |Producer'|, which is the function type |forall a. ConsPar o a -> a|.
We assume that values of this type can always be written using the constructor function |output'|.
Where |output'| is defined as:

< output' :: o -> Producer' o -> Producer' o
< output' o prod = \(ConsPar cons) -> cons o (ProdPar prod)


\begin{conjecture}
\label{conj1}

Values of |Producer'| can always be written in the form |output' o r|.

\end{conjecture}

This allows us to do a similar step to case analysis and complete the proof.

\begin{theorem}

|mr . mr' = id|.

\end{theorem}

\begin{proof}

We show this by equational reasoning.

\begin{tabbing}
 = \= xx \= xx \kill
   \> |mr . mr'| \\
 $=$ \> \> (eta-expansion) \\
   \> |\x -> mr (mr' x)| \\
 $=$ \> \> (def. |mr'|) \\
   \> |\x -> mr (x (ConsPar (\x p -> Producer x (helpermr' p))))| \\
 $=$ \> \> (Conjecture~\ref{conj1}) \\
   \> |\(output' o r) -> mr ((output' o r) (ConsPar (\x p -> Producer x (helpermr' p))))| \\
 $=$ \> \> (def. |output'|) \\
   \> |\(output' o r) -> mr ((\(ConsPar cons) ->| \\
   \> \> |cons o (ProdPar r)) (ConsPar (\x p -> Producer x (helpermr' p))))| \\
 $=$ \> \> (beta-reduction) \\
   \> |\(output' o r) -> mr ((\x p -> Producer x (helpermr' p)) o (ProdPar r))| \\
 $=$ \> \> (beta-reduction) \\
   \> |\(output' o r) -> mr (Producer o (helpermr' (ProdPar r)))| \\
 $=$ \> \> (def. |helpermr'|) \\
   \> |\(output' o r) -> mr (Producer o (r (ConsPar (\x prod -> Producer x (helpermr' prod)))))| \\
 $=$ \> \> (def. |mr'|) \\
   \> |\(output' o r) -> mr (Producer o (mr' r))| \\
 $=$ \> \> (def. |mr|) \\
   \> |\(output' o r) -> \(ConsPar h) -> h o (ProdPar (mr (mr' r)))| \\
 $=$ \> \> (coinduction hypothesis) \\
   \> |\(output' o r) -> \(ConsPar h) -> h o (ProdPar r)| \\
 $=$ \> \> (def. |output'|) \\
   \> |\(output' o r) -> output' o r| \\
 $=$ \> \> (def. |id|) \\
   \> |id| \\
\end{tabbing}

\end{proof}


\section{Connect Implementation}

\label{app:connect}

Connect implementation which also handles the return case by keeping track of the left |InCont| continuation and the right |OutCont| continuation impurely in |IORef|s. Then, the appropriate continuation is read in the interpretation of the return continuation.

> connect_CP2 :: ContPipe i x m a -> ContPipe x o m a -> ContPipe i o m a
> connect_CP2 p q = MakePipe $ \ k k_i k_o -> unsafePerformIO $ do
>   ref_o <- newIORef k_o
>   ref_i <- newIORef k_i
>   let  p' = runPipe p (\ a ik' _ -> unsafePerformIO $ do ok' <- readIORef ref_o ; return (k a ik' ok'))
>        q' = runPipe q (\ a _ ok' -> unsafePerformIO $ do ik' <- readIORef ref_i ; return (k a ik' ok'))
>        modp ik ok = p' (keepRefI ref_i ik) ok
>        modq ik ok = q' ik (keepRefO ref_o ok)
>   return $ modq (MakeInCont (\ k'_o -> modp k_i k'_o)) k_o
>   where
>     keepRefI :: IORef (InCont i a) -> InCont i a -> InCont i a
>     keepRefI ref_i (MakeInCont f) = MakeInCont $ \ (MakeOutCont g) -> f $ MakeOutCont $ \ i ik ->
>       unsafePerformIO $ do
>         modifyIORef' ref_i (\ _ -> ik)
>         return (g i (keepRefI ref_i ik))
>     keepRefO :: IORef (OutCont o a) -> OutCont o a -> OutCont o a
>     keepRefO ref_o (MakeOutCont f) = MakeOutCont $ \ o (MakeInCont g) -> f o $ MakeInCont $ \ ok ->
>       unsafePerformIO $ do
>         modifyIORef' ref_o (\ _ -> ok)
>         return (g (keepRefO ref_o ok))

%\section{|Producer'| is representationally equal to |forall a. SP o a|}
\section{Relation to Scott Encoding}
\label{app:proof-scott}

We show the |Producer| case, an analogous strategy works for |Consumer|.

\begin{theorem}

The representation |Producer'| is |rel_equal| (representationally equivalent) to |forall a. SP o a|.

\end{theorem}

The relevant definitions for the proof are:

< newtype ConsPar  x a = ConsPar  (x -> ProdPar x a -> a)
< newtype ProdPar  x a = ProdPar  (ConsPar x a -> a)
< newtype SP o a = SP ((o -> SP o a -> a) -> a)
< type Producer'  o  = forall a. ConsPar o a -> a

\begin{proof}

First, we show that |ConsPar o a -> a rel_equal SP o a|.

\begin{tabbing}
 = \= xx \= xx \kill
   \> |ConsPar o a -> a| \\
 $\sim_{R}$ \> \> (def. |ConsPar|) \\
   \> |(o -> ProdPar o a -> a) -> a| \\
 $\sim_{R}$ \> \> (def. |ProdPar|) \\
   \> |(o -> (ConsPar o a -> a) -> a) -> a| \\
 $\sim_{R}$ \> \> (coinduction hypothesis) \\
   \> |(o -> SP o a -> a) -> a| \\
 $\sim_{R}$ \> \> (def. |SP|) \\
   \> |SP o a| \\
\end{tabbing}

Then,

\begin{tabbing}
 = \= xx \= xx \kill
   \> |Producer' o| \\
 $\sim_{R}$ \> \> (def. |Producer'|) \\
   \> |forall a. ConsPar o a -> a| \\
 $\sim_{R}$ \> \> (proven above) \\
   \> |forall a. SP o a| \\
\end{tabbing}

\end{proof}
