-- The power of infinity

Infinite streams are great. For one thing, they can be used to record
or "memo-ise" the values of a function whose domain is the natural
numbers, so you can look up a value by indexing into the sequence, and
so avoid recomputation of values.  In fact, as Thorsten Altenkirch and
Ralf Hinze have pointed out, lazily infinite objects of kinds other
than streams are useful for memoising functions on any concrete
(ie. first-order) datatype.

The program below illustrates the usefulness of final coalgebras for
functors other than the one which gives us infinite streams.  It makes
two applications of final coalgebras, as a type of states of a "tape"
mechanism of some kind.  There are two kinds of tape. 

1. A Turing machine tapes.  Such a tape is doubly infinite (like the 
integers).  The tape is represented as an infinitary object in a
final coalgebra.  The object is in fact a Moore machine.  The remainder
of the Turing machine. ie. the finite automaton or control unit, which
may be represented by an association list is a Mealey machine,
modulo some beaurocracy concerning halting states.

2. A further example gives a wierd kind of "infinitely bifurcating
tape".  The inspiration for the representation of this tape
is Gerard Huet's zipper structure for representing linear
contexts in data structures.  There's an extra twist though,
as we are \emph{infinitely} in our data structure.  The
twist here can obviously be generalised to quite a lot of 
data structures (beyond regular ones - we could even have
the data structure be an non-wellfounded, rootless, countably
branching tree). 

The most general type of "tape" is a client process, which computes a
"latest" command, paired with a function which dispatches on responses
to the command.  In the case of a genuine tape, the commands are to
rewrite the current command and/or move to a next position, where a
new command is stored.  We think of the commands as "spread out in
space", in a memory which is accessed "locally", with respect to a
current position -- "PC relative".

-- Mealy and Moore functors

> newtype MealyF cmd rsp state = MealyF (cmd -> (rsp,state))
> instance Functor (MealyF cmd rsp) where
>   fmap f (MealyF g) = MealyF g' 
>                       where g' c = let (r,s') = g c in (r, f s') 

> newtype MooreF cmd rsp state = MooreF (cmd,rsp -> state) 
> instance Functor (MooreF cmd rsp) where
>   fmap f (MooreF (c,k)) = MooreF (c,f . k)

-- greatest and least fixed points

> data Functor f => Mu f = Mu (f (Mu f))
> data Functor f => Nu f = Nu (f (Nu f))

> unMu (Mu t) = t
> unNu (Nu t) = t

-- iteration, coiteration

> iter :: (Functor f) => (f a -> a) -> Mu f -> a
> coit :: (Functor f) => (a -> f a) -> a -> Nu f
> iter alg        = alg . fmap (iter alg) . unMu 
> coit coa        = Nu  . fmap (coit coa) . coa

-- recursion , corecursion

This is a slightly more complicated form of iteration
and coiteration, that brings product types in (negatively)
to iteration, and sum types in (positively) to coiteration.

> rec :: (Functor f) => (f (Mu f,a) -> a) -> Mu f -> a
> cor :: (Functor f) => (a -> f (Either (Nu f) a)) -> a -> Nu f
> rec ih = ih . fmap (id `conj` rec ih) . unMu
> cor hi = Nu . fmap (id `either` cor hi) . hi

> conj :: (c -> a) -> (c -> b) -> c -> (a,b) 
> conj a b = \c -> (a c, b c) 

-- back to our example

Here Char is being used as a set of "commands" from the tape to
the finite state automaton, and Rsp is a set of responses from this
automaton, which cause the automaton to roll left, roll right, or 
overwrite the current cell with a given character.

> type Cmd = Char
> data Rsp = GoLeft | GoRight | Write Char

We first define an coalgebra for MooreF.  The states are like those
for an editor, with a stream of characters before the cursor, and
a stream of characters after it. 

> type State = (Str Char, Str Char) 

> tape_co :: State -> MooreF Cmd Rsp State
> tape_co (bef@(Str b bef'),aft@(Str a aft')) 
>              = MooreF (a,\r -> case r of 
>                            GoLeft  -> (bef',Str b aft)
>                            GoRight -> (Str a bef,aft') 
>                            Write d -> (bef,Str d aft'))

This gives us, by coiteration, a map from initial states to elements
of the final coalgebra for MooreF

> tape :: State -> Nu (MooreF Cmd Rsp)
> tape = coit tape_co 

We make the coalgebra into a pointed coalgebra, with a distinguished
initial tape which is empty. 

> empty :: State
> empty = let blanks = bang ' ' in (blanks,blanks)

Now we can define the tape as an element of the final coalgebra.

> emptyTape :: Nu (MooreF Cmd Rsp) 
> emptyTape = tape empty

At this point it would be good to define a Turing machine
automaton as a coalgebra for the corresponding Mealy functor.

-- General things

Type of infinite streams.

> data Str a      = Str a (Str a) 

> bang :: a -> Str a
> bang a = let x = Str a x in x 

> fight :: Nu (MooreF c r) -> Nu (MealyF c r) -> Str (c,r)
> fight (Nu (MooreF (c,g))) (Nu (MealyF f)) 
>       = Str (c,r) (fight (g r) me')
>         where (r,me') = f c 

-- Another kind of "tape"

The idea here is that we navigate around in the "middle" of a
infinite, rootless binary tree.  We represent the position by a pair
of two things:

\begin{enumerate}
\item A stream, representing "how to get here from above". 
\item An infinite (rooted) tree, representing the stuff below where
  we are. 
\end{enumerate}

> data Tree    = Tree Char Tree Tree -- non wf binary tree
> type Cmd2    = Char
> data Rsp2    = GoDownL | GoDownR | Up | Write2 Char
> type State2  = (Str (Char,Either Tree Tree), Tree)

The coalgebra, which lets us navigate around, and change
the content of nodes.

> co2 :: State2 -> MooreF Cmd2 Rsp2 State2
> co2 (above@(Str (ca,lrt) above'),t@(Tree c belowL belowR) )
>              = MooreF (c,\r -> case r of 
>                         GoDownL -> (Str (c,Left belowR) above, belowL)
>                         GoDownR -> (Str (c,Right belowL)  above, belowR)
>                         Up      -> case lrt of 
>                                       Left t'  -> (above', Tree ca t t')
>                                       Right t' -> (above', Tree ca t' t)
>                         Write2 c' -> (above,Tree c' belowL belowR))

> tape2 = coit co2

> blankTree = Tree ' ' blankTree blankTree
> blankTape2 = let above = (' ', Left blankTree)
>              in  (above,blankTree)