f :: Str A -> Str Bwhere A is called the input alphabet and B is called the output alphabet. Here
Str A denotes the type of streams (infinite lists) over
A. One should think of
Stras defined coinductively. I use Haskell notations, particularly `::' for typing. .
Many programs and scripts that are written to be `filters' in a Unix environment provide examples of functions on streams. For example, the function that copies the input through, except that lowercase characters are replaced by their uppercase equivalent is a stream processing function.
A continuous function is however something more than a function on streams: to produce the next character of output, it should be necessary to examine at most a finite prefix of the input. By providing longer and longer portions of the input, one can be sure of obtaining output eventually.
Note that the filter `grep p' is not continuous according to this definition: it need produce no output when there is no instance of pattern p in the input. Not all Unix filters are continuous. A continuous function is `productive' or non-null in a certain sense.
There is more than one way to skin a cat, or formulate the notion of continuity. One can express it by quantification over streams. The following formulation, which is the subject of this note uses inductive and coinductive definitions rather than quantification over streams.
The central operator is a binary operator on types which I shall write with an infix '&'.T A B = (mu X) B + (A -> X)The values of a type
A&Bare well-founded trees in which there are leaves of type B, and node-branches are indexed by
A. We can define a function which interprets such a tree as a program of a certain kind. We write this function with an infix `££':(££) :: T A B -> Str A -> (B, Str A) (inl b) ££ input = (b, input) (inr f) ££ (a:input') = (f a) ££ input'The program reads a prefix of the input stream, then emits an output character and stops, returning a value of B, paired with the unconsumed suffix of the input stream.
One should think of the definition as using induction over T(A,B). (A catamorphism.)
Now to model stream processing functions
Stream A -> Stream B, I propose the following coinductively defined type
Prog(A,B).Prog(A,B) = (nu X) T A (B,X)Such an program consumes some finite prefix of the input, then delivers a character and a new version of itself to apply to the unconsumed input. We express this with an infix `%':(%%) :: Prog(A,B) -> Str A -> Str B p %% input = let ((c,p'),input') = p ££ input in c : p' %% input'A continuous function
:: Str A -> Str Bis one which is obtained as the image of a program in Prog(A,B) under the interpretation
One should think of this definition as using co-induction into Str(B). (An anamorphism.)
It is interesting that the type
Prog(A,B)has both inductive and co-inductive aspects, with the former "inside" the latter.Prog(A,B) = (nu X)(mu Y)((B,X) + (A -> Y)
Note that the alphabets need not be finite. The cardinal of the alphabets plays no role above. However it may be interesting to look at the case when the input and output alphabets are finite, eg the binary digits. In that case we are looking at continuous functions over Cantor space. We have a (relatively well-known) inductive description of the functions from Str(2) to 2, and we use the trick above to describe the functions from Str(2) to Str(2).
There is a `piping' combinator on continuous programs that appears to reflect composition. A suitable operation is defined here in a Haskell program, written for the sake of type-checking the definition. That the operation reflects composition remains to be proved.
Peter G. Hancock Last modified: Thu Oct 30 09:38:47 GMT 2003