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 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:

1. A stream, representing ”how to get here from above”.

2. An infinite (rooted) tree, representing the stuff below where we are.

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)