Stream processors in Haskell. 
============================
Tue Sep  2 23:55:26 BST 2003

By a stream processor, I mean a continuous function from streams of
characters in an input alphabet to streams of characters in an output
alphabet. By continuity, I mean that a finite prefix of the input
stream suffices to obtain the next character of output (and so and
desired prefix of the output. So I exclude programs that produce no
output, however much of the input is made available.  A program can
refuse to produce output only as long as sufficient input is not yet
available to it.  For example, the unix program that simply absorbs
its input and produces no output is not a stream processor by this
definition.  Stream processors are filters that possess a certain kind
of liveness, or productivity.

One can formulate the notion of continuity  using quantification
over input streams: to obtain a desired amount of the output,
it suffices to feed the program with a certain amount of the input.

One can however also formulate the notion of continuity in a different
way that replaces quantification over streams with an inductive
definition, combined with a coinductive definition.

Infinite streams are `co-data'.  We intend here the greatest fixed
point.

> data Str a   = Str a (Str a) 
> -- Str both constructor and type operator

The following type operator takes two types, and returns the data type
of well-founded trees with leaves in b, branching over a.  We intend
here the _least_ fixed point.

> data T a b   = Ret b | Inp (a -> T a b) 

We can interpret trees of this kind as imperative programs which read
a stream of a's, and eventually terminate with a single output
`character' in b together with the unconsumed suffix of the input
stream.

The leaves represent constant functions, that consume no input.
The internal nodes represent reading a character, and dispatching based
on its value.  Note the definition is by recursion on the tree.

> (££) :: T a b -> Str a -> (b, Str a) 
> Ret b  ££  as          = (b,as)
> Inp f  ££  Str a as    = f a ££ as           -- reading

T is monadic in its second argument.  I don't _think_ I've used this,
but it may be implicit.

> instance Functor (T a) where
>  fmap f (Ret b) = Ret (f b) 
>  fmap f (Inp g) = Inp (\ a -> fmap f (g a))
> instance Monad (T a) where
>  return a     = Ret a
>  Ret a >>= f  = f a
>  Inp g >>= f  = Inp (\a-> g a >>= f) 

The following co-data type is for continuous programs which read a
stream of as and write a stream of bs.  We intend here the greatest
fixed point.

> data P a b   = P (T a (b,P a b))
> unP (P x)    = x 

These are infinite objects (co-data).  They can be interpreted as
programs to read a stream of as and write a stream of bs.

> (%%) :: P a b -> Str a -> Str b 
> p  %%  bs = let ((a,p'),bs') = unP p ££ bs 
>             in  Str a (p' %% bs')

The problem now is to define composition.  This reminds me of 
cut elimination, in the hiding of internal communications.

> pipe :: P a b -> P b c -> P a c 
> alpha `pipe` beta = 
>   case (unP beta) of 
>     Ret (c,beta') -> P (Ret (c,alpha `pipe` beta'))      -- output 
>     Inp f         -> case (unP alpha) of 
>                        Ret (b,alpha') 
>                               -> alpha' `pipe` P (f b)   -- hiding internal communication
>                        Inp g  -> let h a = P (g a) `pipe` beta 
>                                  in P (Inp (unP . h))    -- input

One needs a unit for composition.  The following just copies any input
straight through unaltered as and when it appears.

> skip :: P a a   
> skip = P (Inp (\a->Ret (a,skip))) 

One should now try to prove that (perhaps reverse (.))

     ((p `pipe` q) %%) = (q %%) . (p %%)
     (skip %%) = id 
  

Question: is P monadic in its second argument?

> instance Functor (P a) where
>  fmap = fmap9

> fmap9 :: (a -> b) -> P c a -> P c b 
> fmap9 f  (P (Ret (b,p'))) = P (Ret (f b,fmap9 f p'))
> fmap9 f  (P (Inp g))      = P (Inp (\a->unP (fmap9 f (P (g a)))))

> unit9 :: b -> P a b
> unit9 b = let x = P(Ret (b,x)) in x 

> bind9 :: P a b -> (b -> P a c) -> P a c
> bind9 (P (Ret (b,p'))) m = m b    -- seems odd to throw away p'