Sketch of Udon (Version Control/Packaging system)

I’m kind of tired, so don’t expect this post to be entirely coherent. I just wanted to write a little bit about the project I started recently, called Udon.

The idea came to me as the common ground between several problems I have seen recently. I will not go into the intricate details of why I consider them problems worth addressing. They are:

  • The namespace problem on Hackage, CPAN, and related module collections. Specifically, ridding ourselves of the rigid, arbitrary taxonomy of packages without the root namespace getting uselessly polluted.
  • The fact that no popular DVCS allows moving files between projects while preserving history in a sane way.
  • The desire for a purely functional operating system.

Incidentally, these are programming culture problems #2,#3, and #4 on my list (#1 is, of course, FRP). I’m glad I took a break from FRP so I could see this common ground.

Udon stands for “Universal Distributed Object Notation”, with a tip o’ the hat to JSON. And yes, it is a system for serializing objects. It is a gigantic distributed store for inter-referential stateless objects, and would support a huge distributed data structure with no single computer containing all of it.

I’ll get to the implementation details in a minute. I’ll first address how it helps to solve the problems above.

It will help in the implementation of a DVCS that does support moving files between projects, by more or less eliminating the idea of a project. The versioning is all in commit objects, which refer to changes in some tree data structure (representing the directory tree of the project). This is how git works. The difference is that there is no restriction about what tree this is; it could be a tree “from another project”. Just picture how you would write git as pure Haskell, never having to touch the filesystem or anything, everything being objects in memory.

This DVCS, or something similar, helps to solve the namespace problem. A project could refer to the modules it uses by identity rather than name. So instead of the cabal file saying I depend on “binary”, the cabal file (well, data structure in the new model) would say I depend on “that thing over there”, and then import the modules from that package using an advanced import mechanism, which allows renaming or qualifying modules, etc. to avoid collisions.

After conceiving the idea, I realized that it is essentially the filesystem for a typed, purely functional operating system, which is another one of my fancies.

Okay, that’s probably more than enough vagueness for you math types.

The implementation is based on a flawed concept; the same flawed concept that all the DVCSes use, that the hash of an object is a unique identifier for that object. Basically we pretend that hash collisions don’t exist. Yuck. But I could not think of any other way to do it. (This may be the thing that prevents me from going very far with this project, since I am getting in the habit of proving my code correct, and I will never be able to do that with this code since it is not correct).

There is a special type called ExtRef. ExtRef a is semantically just a value of type a. The kicker is that it might be on someone else’s machine, on your usb drive, or even lost forever because nobody kept its data around. It is represented as data ExtRef a = ExtRef Hash (Maybe a). Hash is the “unique identifier” for the object, and you always have that. You might have an actual copy of the object too, but if not, the Hash is there so you can find it if you need it. This representation, and the whole Hashing idea, is hidden from the high-level interface, of course.

You work with ExtRefs through the External monad. It’s a coroutine monad (free monad over i × (o -> •)) which reports which ExtRefs need their associated objects to continue the computation. The low-level interface will allow implementation of a variety of ways to handle this. The simplest one is a local store of objects to be queried. As things get more mature, that could be expanded into one that looks at various remote network stores (based on some origin map or something), or asks the user where to look, etc.

And my hope is that the little Udon framework I’ve described here will be sufficient to model the DVCS and the hackage package system as if everything were just pure data structures in memory. Of course it won’t be quite as convenient (you need to annotate your data structures with some ExtRefs at least), but it would at least encourage pure modeling of these “real world” systems.

About these ads

11 thoughts on “Sketch of Udon (Version Control/Packaging system)

  1. I am intrigued by this sentence:

    It’s a coroutine monad (free monad over i × (o -> •))

    Could you perhaps point me to some papers or other resources so I can understand that notation? I believe I understand what a coroutine is (like a cooperative multitasking OS), and I understand monads enough to write code that uses them. I suspect I can google “free monad”, but I don’t know where to start with that notation.

  2. It’s from category theory, I think. I’ve only passively seen it, so I may be using it wrong, but it’s pretty straightforward so it’s probably correct. The bullet is a shorthand for a parameter. So “i × (o -> •)” is the functor “F a = i × (o -> a)”. i and o here are just types. I’m using the mathy forms of product (a × b = (a,b)) and coproduct (a + b = Either a b).

    A free monad M over a functor F is “M a = a + F (M a)”. Or in Haskell notation:

    data FreeMonad f a
    = Return a
    | Free (f (FreeMonad f a))

    This is always a monad when f is a functor, and if you’re not that good at making monads, it’s a good exercise to try to make it one.

    So! The coroutine monad I refer to is:

    data Suspension i o a = Suspension i (o -> a)
    type Coroutine i o = FreeMonad (Suspension i o)

    Or, stated more friendlily:

    data Coroutine i o a
    = Return a
    | Suspend i (o -> Coroutine i o a)

    That is, a coroutine either says “I’m done, here’s the result”, or it “asks a question of type i, and waits for an answer of type o” before continuing. It can ask as many of these questions as it likes. The essential function which asks such questions is:

    suspend :: i -> Coroutine i o o
    suspend i = Suspend i Return

    This is a very useful little construction. It gives you the ability to separate purity from effects in a lot of complex scenarios, where you would otherwise be riddling your whole program with IO.

  3. Thanks for your quick response!

    The notation makes some sense. I had guessed what ‘+’ and ‘×’ do from context; I’ve heard people refer to “sumtypes” when describing basically what I would call a [discriminated] union in C. It’s nice to get a confirmation.

    I do not immediately understand why (a + b) is called a “coproduct” rather than a “sum”. Nor do I understand comonads, coalgebras, codata, or any other co-things I keep running across in the haskellian blogosphere at this point. My day job is boring C++, and I just play with haskell after hours for fun.

    Armed with a better understanding of that type notation, I should revisit those papers about how you can somehow symbolically derive a zipper type from some other structure.

    The word “free” is so widely overloaded that I wasn’t sure what to make of it in this context. It seems like “free” refers to the fact that if we’ve got a functor F, we can always apply this formula and pop out some monad “for free”.

    I must admit I don’t fully grok the type recursion here; I suspect won’t get it until I try to write some actual code that uses it. My first thought is that it reminds me of a list with the functor as a kind of cons cell. The Return constructor of the free monad is like Nil.

  4. Regarding coproduct: I’m no category theorist (though I have been trying), but I love thinking about this stuff, so here’s my guess. Let’s look at the product in terms of its projections.

    The product of two types X and Y is an type X × Y with two functions: π1 : X × Y → X and π2 : X × Y → Y.

    There’s another property which is a little compilcated, but interesting and important. Intuitively it says that X × Y is the “most general” pair of Xs and Ys.

    Say you have a type A and two functions f : A → X and g : A -→ Y. Then there is a unique function c : A → X × Y (in Haskell we call this f &&& g, from Control.Arrow), such that f = π1 ° c and g = π2 ° c. This is just the property the “obvious” function with this type has.

    I will summarize, then we’ll form the coproduct by reversing all the arrows.

    π1 : X × Y → X
    π2 : X × Y → Y
    Given f : A → X and g : A → Y:
    f &&& g : A → X × Y.
    f = π1 ° (f &&& g)
    g = π2 ° (f &&& g)

    Now let’s do some renaming and reverse the arrows:

    π’1 : X → X + Y
    π’2 : Y → X + Y
    Given f : X → A and g : Y → A
    f ||| g : X + Y → A
    f = (f ||| g) ° π’1
    g = (f ||| g) ° π’2

    And these are exactly the rules for Either. So we formalized a product, reversed all the arrows (which is what “co-” means in category theory) and got Either. Thus, Either = coproduct.

    I don’t know if you followed that, but I sure enjoyed exploring it. In fact, I just learned why commutative diagrams are cool. If you phrase your theorems in terms of commutative diagrams, then you can just reverse the arrows in those to get the corresponding cotheorems (as we did for the last two lines in the list of properties above).

  5. Oh, as long as I’m procrastinating, I might as well explain a few other things you mentioned.

    For comonads, I could not do better than this excellent introduction by Dan Piponi. This is where I learned about them.

    I don’t really know the categorical underpinnings of “algebra” and “coalgebra”. The way it is used in everyday culture though is pretty straightforward. Algebras X are just types with a bunch of functions returning X. Coalgebras Y are just types with a bunch of functions taking Y as an argument (and returning other stuff). Classes in OO are coalgebras, since every method takes the object as an argument.

    Here is another great article, again by Dan Piponi, explaining codata.

    The zipper derivative stuff you mentioned, Conor McBride’s work, is one of the most hauntingly beautiful correspondences I know of. But nobody seems to know why it occurs.

    Haskell culture’s obsession with deep theory is one of the reasons I love the language. Enjoy your exploration!

  6. Seems like you could prove all your code correct “modulo uniqueness”, that is to say, assuming that the hash/uuid function provides a unique identifier. Then you can say that your program is correct, except in a case which occurs only once out of 2^512 (or whatever).

  7. Luke,

    Thanks for that explanation about co-things reversing arrows. I had a feeling there was some satisfying relationship like that, but I didn’t know how to express it well enough to research it much further.

    Category theory always seems elusive to me, because I have a hard time finding entry-level stuff for people who aren’t grad students. Haskell obviously helps here, since it lets you at least get a programmer’s-eye-view of monads/functors/arrows/etc.

    Haskell culture’s obsession with deep theory is one of the reasons I love the language.

    Agreed!

    The downside of all this fun stuff is that my poor girlfriend has to deal with countless printouts of functional programming papers littering up the house. “You and your damn monads!” ;-)

  8. Craig,

    Strictly speaking, the free monad is a least-fixed-point. In the case of the “coroutine” monad, it means that the sequence of Q&As is finite. A return value will eventually drop out. Of course, since Haskell muddles data and codata (some prefer to think of this as Haskell providing only the greatest-fixed-point), there is in fact no such guarantee.

    “Freeness” as a piece of math jargon doesn’t quite mean gratis in the commercial sense. It’s more in the ideal of “freedom”, as in least fettered. When something is called a “free Y”, some restrictions were made to get it to become Y. We want just those restrictions that we explicitly impose and no other, sometimes a tough act to get right. Why this insistence on purity? Because in some math ideas are hard to pin down, a definite linguistic limitation. Without some care, we end up missing the big picture.

    (That by the way, is one of the best reasons I’ve heard to do math: fight for your language freedoms.)

    Sorry for being so waffly here. The cognoscenti are probably rolling their eyes right now at this crude attempt at explaining “freeness”.

  9. Craig,

    Here’s a specific example of free-ness: suppose we have the free set-theoretic monoid generated over a single element x. In other words, we have a set S comprising all sequences (including the null sequence) of x’s. Suppose now that I tell you that the x’s were really a representation of unary clock arithmetic, and therefore 13 of them is equal to just one x.

    You could then say, “But wait, then S is not free.” And you would be right.

  10. rajan: Ah yes, of course! I remember seeing the “free group” when studying the Banach-Tarski theorem.

    So in what way is the free monad free? There are monads which are not free over any functor, right? (e.g. the Const monad)

  11. My guess is that the free monad is free in that whereas “mu X. A + F(X)” always gives you a monad via substitution, the free monad is the most general (i.e. least restrictive) formulation of the substitution.

    There are no hidden equations in the free monad.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s