Der Blog

(In response to Gimbo.)

Speaking of Unix, I have thought that there is a pretty close connection between lazy evaluation and Unix pipelines. On the xmonad home page there's an example for using dzen that looks like this:

while true ; do
    date +"%H.%M %a %b %d"
    sleep 60
done | dzen2 -ta r -fg '#a8a3f7' -bg '#3f3c6d'

Of course, if that was strictly/eagerly evaluated, dzen would never run, because of the infinite loop. But what actually happens is that the two commands, joined together by a pipe (indicated by the | character), are executed in parallel; the while loop runs date, producing some output, which it writes to a pipe (just a first-in-first-out buffer shared by the two processes); it sleeps for 60 seconds; then it runs date again; sleeps again; ..., ad infinitum. Meanwhile, dzen reads its output, until there is none left, then blocks until the loop provides more.

But that's just like a lazily evaluated stream. Suppose we had an IO action getTimeString, then we could do:

statusBarContents :: IO [String]
statusBarContents = do
    sleep 60
    now <- getTimeString
    then <- unsafeInterleaveIO statusBarContents
    return (now:then)

statusBar = dzen statusBarContents

Again, it looks like statusBarContents would never terminate because it calls itself, and not even in an inductive manner with a base case where it bottoms out. In contrast to the above, this is all done in one thread; but the unsafeInterleaveIO says "only evaluate this when it's asked for" - so it manages to produce one time string, which dzen uses; then dzen asks for the next one, and the sleep in statusBarContents makes it block.

(For the mathematically minded, this kind of non-inductive recursion producing infinte amounts of data is called corecursion. I intend to do a SUCS talk on the topic someday.)