by Hancock on March 8, 2008.
Tagged as: Lunches.
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.