FP Lunch

From time to time, I try to put report things in this blog. If someone (local) can tell me how to put tags in so stuff like ASCII “art” comes out nice, I’d be grateful. It is beyond me. “code” doesn’t work.

This lunchtime was in 2 bits. First Hank spoke, about what he called “functional operating systems”. He seemed to mean combinations of continuous stream processing functions involving fair stream schedulers.

What is a fair stream scheduler? A function

m : Stream A -> Stream B -> Stream (A + B)

whose value always contains infinitely many inL’s and infinitely many inR’s.

Hank claimed that any such function could be represented by a program of type:

M = nu ((A->)* . (B ->)+. (A->))

where F* denotes the free monad over F, and F+ = F . F*.
He gave the constructors of (A->)* X the names Ret and Rd:

Ret : B -> (A->)* B
Rd : (A -> (A->)* B) -> (A ->)* B

The idea is as follows.

First, define

eat' : (A->)* (C) -> Str A -> ([A], C, Str A)
eat' (Ret c) as = ([],as)
eat' (Rd f) (a:as) = let (al,c,op) = eat (f a) in (a:al,c,op)

Now, let’s define

schd :  M -> Str A -> Str B -> Str (A +B)
schd m as bs = let
  t = elim m
  (al,f,as') = eat' t as : ([A], (B -> (B ->)* ((A ->) M)), Str A)
  t' = f (hd bs)
  (bl,g,bs') = eat' t' (tl bs) : ([B], (A ->) M, Str B)
  m' = g (hd as')
               in (map inL al)
                  ++ [inR (hd bs)]
                  ++ (map inR bl)
                  ++ [inL (hd as)]
                  ++ schd m' (tl as') bs'

In essence, m eats 0 or more A’s, then one or more B’s, then an A, then loops. As m reads things, we pass them through, appropriately
tagged to the output.

Hank asserted, in a voice of thunder, that the output of such a function contained infinitely many inR’s, and infinitely many inL’s; moreover that any such interleaving was the output of such function. He conjectured that

nu ((A->)* . (B ->)+. (A->))
= nu ((B->)* . (A ->)+. (B->))

and then began to talk rather obscurely about circuits

      /|      _________      |\\
     / |---->|    f    |---->| \\
    /  |      ---------      |  \\
+->    |      _________      | m  >-+
|   \\  |---->|    g    |---->|  /   |
|    \\ |      ---------      | /    |
|     \\|---->out      in---->|/     |
|                                   V
+<----------------------------------+

which "worked properly" for any choice of scheduler m, suggesting that at any rate he had made sense of the "for any", and that working
properly" might be, minimally, something like continuity (from in to out). He said this idea might help understanding delay-insensitive circuitry, or circuitry which is insensitive to buffering.

This all seemed to be in the context of the work Hank and Dirk and Neil had done some while ago in "stream eating". which represented continuous functions of type Str A -> Str B by nu ((A->)* (B \times)). There is a recent draft here.

This entry was posted on Saturday, March 8th, 2008 at 12:02 am and is filed under Lunches. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.