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

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

My question now is, how does this generalize to fair scheduling of more than 2 streams?

]]>` F* A = mu X. A + F X `

. And `mu`

here indicates the initial algebra of

`X |-> A + F X`

.When F is the functor

` X |-> B -> X`

, ie the readermonad,

`F* A`

is the type of wellfounded trees(no infinite paths from the root) branching over B, with leaves

labelled by elements of A. Such a tree can be interpreted as a

program that reads a finite sequence of B’s, then terminates, yielding

an A. The wellfoundedness is here crucial to enforce termination.

I’m sorry, it wasn’t well explained. Moreover I’m not at all sure I’m

on the right track. (FP lunch is a venue where one can be a bit

unbuttoned…). I should have mentioned: besides

merge : (Str A > Str (A + B)

one needs a function

split : Str (A + B) -> (Str A >

to be left inverse. But the type of split is wrong. Its domain is really the set of

streams that have infinitely many inL’s and inR’s. My suggestion is that the

definition of this concept involves a nested fixpoint

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

where nu means: final coalgebra. So, mu’s nested inside nu’s.

By the way, I’m pretty sure there is a paper of David Park’s from the 70′s which (in part) discusses precisely this concept.

]]>I’m afraid I don’t understand what a “free monad over smtg” is..

But isn’t faire scheduling a simple matter of fair threads (coopĂ©rative threading) with no path of execution containing an infinity of progression steps before a call to the scheduler? I’ll have to re-read your article when the indentation is better ^^

P!

]]>