Home

Zipper-based file server/OS

We present a file server/OS where threading and exceptions are all realized via delimited continuations. We use zipper to navigate within any term. If the term in question is a finite map whose keys are strings and values are either strings or other finite maps, the zipper-based file system looks almost the same as the Unix file system. Unlike the latter, however, we offer: transactional semantics; undo of any file and directory operation; snapshots; statically guaranteed the strongest, repeatable read, isolation mode for clients; built-in traversal facility; and just the right behavior for cyclic directory references.



We can easily change our file server to support NFS or 9P or other distributed file system protocol. We can traverse richer terms than mere finite maps with string keys. In particular, we can use lambda-terms as our file system: one can cd into a lambda-term in bash.



The implementation of ZFS has no unsafe operations, no GHC let alone Unix threads, and no concurrency problems. Our threads cannot even do IO and cannot mutate any global state --- and the type system sees to it. We thus demonstrate how delimited continuations let us statically isolate effects even if the whole program eventually runs in an IO monad.

zfs-talk: Expanded talk with the demo. It was originally presented as an extra demo at the Haskell Workshop 2005

ZFS.tar.gz: The complete source code, with comments. It was tested with GHC 6.4 on FreeBSD and Linux


From: Zipper-based file server/OS


Neat, a referentially transparent filesystem with transactional semantics in 540 lines of Haskell. I can think of some interesting uses for this.

By shapr at 2005-10-08 10:10 | Fun | Functional | Implementation | Theory | other blogs | 39209 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Zipper?

What is a zipper?

By taral at Sat, 2005-10-08 18:41 | login or register to post comments

zipper

some explanation and example code (in OCaml): Using zippers to handle huge trees

By Olivier Andrieu at Sun, 2005-10-09 11:46 | login or register to post comments

These are a Good Start...

... but they're Huet's Zipper, which has to be instantiated per data structure that you wish to traverse. One of Oleg Kiselyov's advancements over that is that his zipper is polymorphic in the type of the traversal function, so if you have a consistent traversal interface, e.g. O'Caml's "iter" or C++'s "for_each," then you can have a generic Zipper for it. That's what I'm after, in O'Caml and C++. :-)

By Paul Snively at Wed, 2005-10-12 05:42 | login or register to post comments

To cite Oleg:

"Zipper is an updateable and yet pure functional cursor into a data structure. It lets us replace an item deep in a data structure, e.g., a tree or a term, without any mutation. The result will share as much of its components with the old structure as possible. The old data structure is still available, which is useful if we wish to 'undo' the operation later on.

Zipper is a delimited continuation reified as a data structure. Somehow that idea is not commonly discussed in the zipper literature. Because Scheme has first-class and delimited continuations, we can derive and use zipper far more easily."

Zipper in scheme

By Felicia Li Svilling at Sat, 2005-10-08 19:32 | login or register to post comments

Okasaki

Something quite well-known, but I'll say it anyway...

The great book by Chris Okasaki, "Purely Functional Data Structures", talks about something like this: "persistent" data structures, which have all their previous states available.

Simple example: a stack can be purely-functionally implemented as a list, push==cons, top==car, pop==cdr.

A more fun example: if we have a balanced tree with N elements, and need to insert/remove an element - the operation should return a new tree (because we're purely functional and can't mutate). However, it isn't too expensive to return a new tree! We only need O(log N) operations (just replace all the nodes on the path down), because the new tree can share the untouched subtrees of the old one.

On a side note... Tom Lord, author of the Arch source control system, criticizes the idea of using a purely functional data structure (also known as transactional FS) for implementing SCMs:

So here's the first mistake: the idea of a transactional FS is like a shiny new hammer. It's pretty natural to let it possess you and start running around looking for nails.

Also for the record, here's a reply to Tom's criticisms.

By Vladimir Slepnev at Sun, 2005-10-09 10:29 | login or register to post comments

Finger Trees

I believe that Paterson/Hinze's Finger Trees use a variant of zippers for maintenance of the structure. Parts of the tree are essentially held in a "uncomputed" state, via Haskell's normal lazy evaluation. Paterson has a PDF of the paper on his site; it is also very worthwhile to read through the presentation materials both have made available.

Implementing them in Java was a head-stretching exercise, but very worthwhile. I didn't get the lazy behavior to work within my implementation, but I did get to learn why I wish I had an easy way of getting at it within Java.

By rossjudson at Mon, 2005-10-10 16:12 | login or register to post comments

Other Implementations

Boy, I'd love to see Kiselyov's Zipper (as opposed to Huet's) in O'Caml and C++! That's some amazing stuff. As far as I can see, to get there in C++ you'd have to use boost::lambda | boost::spirit::phoenix, and write your own continuation monad, or use FC++ 1.5 and its continuation monad. Then you'd have to emulate shift and reset using the continuation monad. Then you'd have to write the traversal-interface-based Zipper in terms of shift and reset. Hopefully it could be done in terms of for_each().

In O'Caml, the only thing you don't need is lambda; it's already there. You still need a continuation monad (maybe from the O'Caml Network Application Environment's "cf" libraries), you still need to emulate shift and reset, and you still need a polymorphic Zipper.

I'd be willing to collaborate on either or both of these implementations, if anyone else is interested.

By Paul Snively at Tue, 2005-10-11 14:15 | login or register to post comments

One of the explanations of zi

One of the explanations of zippers says they can be constructed using delimited continuations. That looked nice but what are they? They look like a way to add/remove handlers to continuation, is that right?

By Christopher Campbell at Thu, 2005-10-13 16:09 | login or register to post comments

Not Quite

That's not quite accurate. Instead, delimited continuations really do not make the entire "rest of the computation" available. Instead, they make some portion of it available, and these portions can be nested. So on one hand, in some attenuated sense, they're "simpler" than "full upward continuations" à la Scheme, but until relatively recently they've been perceived to require something "beyond full continuations" and/or "beyond monads" to implement. More recently, that's been proven not to be the case, apparently by multiple groups independently. Oleg Kiselyov's work here is important, as is the "A Monadic Framework for Subcontinuations" paper already alluded to.

What's also becoming somewhat apparent, at least to me, is that, just as theology is too important to be left to theologians, monads are too important to leave to category theorists and the Haskell community. Good monad implementations in other languages could only serve to demystify the beasts, which, after all, only consist of a type constructor and two higher-order functions that obey a few laws. Even Haskell can't enforce these laws, so the Monad class, "do" syntax, etc. in Haskell are just conveniences: there's nothing at all to prevent the same support from being provided in O'Caml or even C++ (see the other post in this thread about the "do" syntax extension in camlp4, for example).

So one of my goals in aiming for implementations of Kiselyov's Zipper in O'Caml and C++ is, of course, to have this great structure and supporting functions available for use. But another goal is to motivate the development and understanding of monads in O'Caml and C++ as well.

By Paul Snively at Fri, 2005-10-14 02:38 | login or register to post comments

Right on about monads

...until relatively recently they've been perceived to require something "beyond full continuations" and/or "beyond monads" to implement. More recently, that's been proven not to be the case, apparently by multiple groups independently. Oleg Kiselyov's work here is important, as is the "A Monadic Framework for Subcontinuations" paper already alluded to.

Ken Shan's was the first encoding of dynamic delimited continuations (control and prompt, for example) in terms of shift and reset---it was only dynamic delimited continuations that were "beyond continuations". Shift and reset were defined by CPS from the start.

But one only uses shift and reset anyway, not dynamic delimited continuations or the full "monadic framework for subcontinuations", to do things like the LogicT backtracking monad transformer or Oleg's zipper (his Scheme zipper; I'm not familiar enough with his zipper based FS).

Things like Oleg's zipper and the LogicT backtracking transformer are really rooted in CPS, after all, so it's not just a coincidence that they use static delimited continuations when written in direct style. I'll go even further: you may not ever need dynamic delimited continuations. The only compelling example where the extra expressive power of dynamic delimited continuations is used is the breadth first tree traversal examples of Biernacki and Danvy.

But you're right on about monads. What you should really want is call/cc in O'Caml, or better yet, a native implementation of shift and reset!

By Kevin Millikin at Fri, 2005-10-14 04:56 | login or register to post comments

Incremental transforms

I've been looking for something like this for a while. My idea goes like this:
  1. Get a tree data structure that allows updates via some kind of cursor, or better yet multiple cursors.
  2. Define a small set of operators, maybe just fold, map and filter. Given an existing tree, each of these operators creates a new tree that is incrementally updated along with the original. So if I have a tree of X and a map (X->Y) to turn it into a tree of Y, then adding a new X will automatically add the corresponding Y. Similarly for fold and filter. The new tree will be the same base type as the original, so you can daisy chain operations.
  3. Hence it should be possible to define a document data type as a tree of document elements, a bit like HaXML. Then define the transform from the document tree to a screen representation in graphical primitives using the map, filter and fold operations. Hey presto: a document editor.

Am I making sense, or just totally deluded.

Paul.

By Paul Johnson at Tue, 2005-10-11 21:34 | login or register to post comments

Huet's Zipper

You're making sense, that was the original use of The Zipper by Huet. He used it for a structure editor.

By shapr at Tue, 2005-10-11 21:43 | login or register to post comments

A Monadic Framework for Subcontinuations

The implementation appears to use A Monadic Framework for Subcontinuations

It's nice to have a specific example with working source code - allows one to play with it. Maybe this time I will finally grok that monadic framework...

By Andris Birkmanis at Wed, 2005-10-12 13:46 | login or register to post comments

Graydon Hoare Got it Right

"Monads are one of those things like pointers or closures. You bang your head against them for a year or two, then one day your brain's resistance to the concept just breaks, and in its new broken state they make perfect sense."

I've read the paper. Several times now. I suspect that I'm just going to have to start with someone else's existing monad example in O'Caml and see if I can get their "implementation approach #2" (CPS) to work by evolving the example monad for O'Caml. It'll also be interesting to try to implement the two operators that have to be "syntactic" due to order-of-evaluation issues in terms of camlp4.

Then, on the basis of that experience, maybe I can use FC++'s monads to do the same in C++. Whee.

By Paul Snively at Wed, 2005-10-12 20:03 | login or register to post comments

Monads in Ocaml

If you are prepared to wait just a bit (a week?), I will be releasing an update to our (Oleg, Lydia van Dijk and I) campl4 extension for a multi-monad 'do' notation for Ocaml (and MetaOCaml too). Oleg and I have used it extensively now, and it definitely helps, especially when you are writing CPS code!

By Jacques Carette at Thu, 2005-10-13 13:32 | login or register to post comments

Excellent News!

I'll be looking forward to the new extension. :-)

By Paul Snively at Fri, 2005-10-14 02:20 | login or register to post comments

Finally here - pa_monad

Ok, so it was way more than a week, but it is finally here, the official release of the syntax extension for monads in Ocaml. Enjoy!

By Jacques Carette at Wed, 2006-06-07 22:03 | login or register to post comments

Awesome!

Has anyone tried it with Oleg's monadic delimited continuations yet?

By Paul Snively at Thu, 2006-06-08 03:57 | login or register to post comments

Oleg, Lydia, and Jacques Rock

At my request, Oleg revised pa_monad to support his monadic delimited continuation framework, and Lydia revised it to work with findlib. The result, pa_monad 1.1 is now available at Jacques' site. This means that one can now use delimited continuations, and so presumably delimited dynamic binding, in native-code O'Caml as well as bytecode O'Caml, and without the syntax being too ungainly. Thanks, Oleg, Lydia, and Jacques!

By Paul Snively at Sat, 2006-06-24 02:32 | login or register to post comments

Some ideas

I've been thinking a little about zippers recently. You guys might remember Oleg's other paper on various kinds of collection interfaces, where he demonstrates that streams/generators/iterators are just inside-out super-folds. He then uses call/cc to perform this inversion automatically.

This duality between streams and traversal functions made me think of the inside-outing that Oleg also does in his generic zipper code. So, what if you have a stream-style interface to your data type instead of a traversal function? Then you just need a zipper for streams (which is simple) and you essentially get your generic zipper for free. Maybe streams are the "natural" interface for zippers and the delimited continuations only appear in Oleg's because he needs to turn the traversal function inside out a la his collections interface paper?

Anyway, this approach is extremely intuitive and works quite well in dynamically-typed languages like Scheme, but I don't think it would be as nice in Haskell. Thoughts?

Edit: Fixed some typos.

By Per Vognsen at Thu, 2006-07-13 10:13 | login or register to post comments