The Third Virtue

Ever since working with the Anygma team, the idea of a purely functional operating system has been stirring in my head: An operating system that stays denotational and composable all the way down to the device drivers. In this world, we have to make no sacrifices like IO to interface with the impure ideas around us. We can still communicate with the outside world by modeling them in a pure way.

Just to be clear: I will not be accepting comments about the feasibility of the idea itself (eg. don’t say “but the idea of an operating system is necessarily stateful” or any of that bull). Comments and criticisms about the approach I describe are more than welcome.

So this has been stirring away. Then at Thursday’s Boulder functional programmers group, somebody mentioned Squeak. I had seen Squeak a long time ago, and was amazed and impressed by the concept. There is no distinction between compile time and runtime, between source code and program. Everything is just objects floating around in the world. And of course this matches perfectly with the purely functional operating system idea.

It sucks to program with text. Programs are not text. Ultimately, programs are their denotation, but we need a representation. I say that representation is abstract syntax. Our program editors output abstract syntax, which the compiler turns into real objects. Text doesn’t have to enter the equation anywhere.

I don’t think this idea fits Haskell’s type system very well. We need something closer to dependent types, because types have to be objects floating around in the world too. So, while I’m at it, I think I’m going to make a pure language — pretty close to, but not exactly Haskell — which is the core abstraction language. Maybe something both expressive and barebones like PiSigma. But I’ll need a real-world language to go on top of that.

Hubris indeed.

So! What’s the large-scale plan? I am going to assume nobody will help me (other than to offer suggestions) in these early stages. This is a Grand Vision (TM), and I doubt anybody but me is going to get excited enough to contribute until it starts coming together at least a little. But I am completely excited, as this is the culmination of an idea that has been developing for years. Oh, and that was at the beginning of the large-scale plan because excitement is the top point in my book — engineering is secondary to motivation.

I don’t really know anything about drivers or hardware or any of that, and this undertaking is already way too huge for me. Therefore, I’m going to go the route of Squeak and implement an image-based sandbox — an OS inside an OS. I’ll start by choosing a core language and making a really slow proof-of-concept interactive text-based interpreter for it. At that point, many options open up, depending on what I’m inspired to do at any moment: improve the language frontend, work on graphical hooks, start work on a faster interpreter or JIT, start designing the FRP essentials, ….

As for the FRP essentials, why do I think they will be more possible in this new concept than in Haskell? Well, I have a sophisticated RTS extension that I think will handle that, which I will blog about riiiight… now! (And there are a few ways to compromise in case that idea doesn’t pan out)

Oh, btw, I’m calling this project Dana, after da man Dana Scott.

About these ads

21 thoughts on “The Third Virtue

  1. First of all, woot! I’m all for this project.

    eg. don’t say “but the idea of an operating system is necessarily stateful” or any of that bull

    I take such statements as nothing more than entrenched mental habit. I like Gandhi’s statement, “Do not confuse what is natural with what is habitual.”

    Ultimately, programs are their denotation, but we need a representation.

    I’d like to hear more about what purposes are served by a representation other than the denotation itself.
    Having purposes in mind may help making conscious (non-habitual) choices of representations.

  2. “This is a Grand Vision (TM), and I doubt anybody but me is going to get excited enough to contribute until it starts coming together at least a little.”

    Don’t assume so much. :) I’ve been tossing these ideas around in my head for a couple years now as well, including a Squeak-like environment and a new, dependently-typed language. My ideas still need more development before I even try writing a single line of code toward them though.

    If you blog regularly about your progress then things might “come together” enough for me and others to “get excited enough to contribute.” ;)

  3. Sounds like fun, when you get it working. One comment I’ll put in is about something I’ve always hated in Squeak. While it’s nice to throw everything together in the sandbox, it’s also good to be able to keep things separate (or at least separable). In particular, developing an application and running it should be distinct (dependent typery aside).

    Rather than the all-in-one image of Squeak, consider something more like a Darcsian patch soup. That way you can roll back some changes (e.g. running the program) without rolling everything back to a fixed timepoint (e.g. loosing the programming you were doing interactively). Similarly, the ontological space in which things are defined should have some sort of permissions model so that the developer can lock code down before shipping (or users can lock configurations down, or…)

    Implementing the actual version control and permissions stuff can wait a while, just so long as you have these ideas in mind when structuring the overall implementation.

  4. wren: Thanks for the tip. The whole image/sandbox idea is a mixed blessing; I see that it’s a cool way to develop and provides a neat world view. But, and this is the uneasiness I’ve been trying to address with Udon, it’s still a finite sandbox. Why is there a distinction between different worlds — it should all be one world that comes in chunks.

    Don’t forget that it’s a purely functional project from the ground up. “roll-backs” are not really necessary, since nothing can have side-effects.

    Although something you were working on might go out of scope in your development context (still working out what that exactly means, but roughly, a lot of development is actually occurring underneath a bunch of lambdas), in which case you might want to go back and get it.

    But thanks for pointing me at possible showstoppers. These are definitely things that need to be considered at the early stages of development.

  5. How does your blogware language compare to Agda? Given that Adga is close in spirit to Haskell and dependently types I assume it will be a good starting point.

  6. Jason: It’s a reference to the three virtues of a great programmer, from Perl culture: “Laziness, Impatience, and Hubris”.

    Josef: I’ve picked ΠΣ as the core language. Agda isn’t a good starting point because it is too complex; ΠΣ is in the same spirit as Agda but much simpler. It’s also partial, which is a positive when you want to make something rather than prove something. Basically with a small core calculus I can experiment with my own implementation without too much effort, and tweak things here and there as it becomes necessary.

    Also ΠΣ will be benefiting from my work, since I’ll be one of its first users, and implementing an interpreter for it (which it presently has only in a very limited form).

  7. So, I’ve briefly looked at the ΠΣ paper and I can understand why it was rejected. While I can understand why you find it appealing I think it is also pretty brave to use. In particular they don’t prove a single theorem about the language in the paper. In a typed programming language one thing that you would like to have is subject reduction. But because of their use of boxes it is not at all clear that ΠΣ actually enjoys subject reduction. In Agda they have had exactly this problem when dealing with coinduction. Thierry Coquand has come up with a new core calculus for Agda which solves these problems though. But it just goes to show just how subtle these things can be, and I would recommend trying to use something a little bit more well studied.

  8. Josef: That is a good idea. But I’m going going to do it. I like ΠΣ because I can understand it and have a hope of implementing it. Through implementation I will gain understanding, and perhaps this will lead me to study it more; so I can not just hear that it might not be a good choice, but either see it fail or gain the understanding necessary to prove some of these properties.

    I am quite happy with it in practice. We’ll see if it holds up.

  9. authorize me too `woot` too =]

    your whole article is like a duplicate of my mind, I can’t help much except follow your publications here and wish you the best.

  10. Hey, the idea is definitely very exciting. I have had an almost identical (or maybe really identical :-) vision for the future of computing in my head for many years.

    Unfortunately for me, I had no functional programming background, so my vision wasn’t quite so refined as it is now.

    I think it is fascinating how we reached the same vision but coming from completely opposite ends. For me, this idea of computing was inspired by Jonathan Edwards’ Subtext, as well as Vapor (Language safety as basis of OS security, rather than hardware protections). I had this crazy idea, that Jonathan Edwards’ code editor can really be a complete desktop interface, unifying the programmer and user interface! It can also unify edit, compile and run times!

    When I started implementing my vision, I had used Python as my implementation language, and implemented a limited form of FRP on top of that (I had to reinvent FRP, and without a functional background, and in a language like Python, I had great difficulty in seeing how to represent the input events functionally). This led me to learn Haskell, in order to implement my vision.

    I recently decided that I finally know enough Haskell to start, and that I won’t wait for Reactive to be ready anymore, and have started by implementing a purely functional widget set, on top of which I intend to implement the live code editor that edits Haskell.

    I disagree that dependent types are a must (as you can represent arbitrary type sums and products and nicely present them to the user), but they are definitely a plus. I do think that whatever can be deferred to later (e.g OS drivers) should be.

    Bottom line: I would love to collaborate with you on this project!

    P.S: I have also toyed with OS programming, but I don’t think running on the bare metal is that important at the moment.

  11. Eyal: Great! I’d be glad to have your help. You can fork the repo on github if you care, though there isn’t much there yet. I have to make a roadmap for the grant proposal, so that will identify places that support independent work. At first glance, there is a lot of opportunity for parallelization even at such an early stage.

    I’m curious why you don’t think dependent types are necessary. My whole plan is built around the possibility of dependent quotation, which endows the user the ability to compose arbitrary components.

    You just built a lambda in your editor of type forall a. a -> a, now you have a box representing that function (together with whatever extra info it needs). You had a box with a Nat in it from before. How do you know you can apply them? Once you do, how do you apply them, without resorting to unsafeCoerce?

    Or am I making assumptions that you don’t share?

  12. I agree that runtime type information is going to have to exist, and then type checking is going to be used (I was hoping existing libraries could do this), and then only type-safe expressions are allowed to be created. I think that this leaves open several possibilities:

    A. Use Haskell types, Haskell type checkers, and unsafeCoerce.

    B. Write a small typed language on top of Haskell, use type checkers on this language, no unsafeCoerce necessary.

    C. Same as B, but the language is not so small and is dependently typed.

    If I understand correctly, you’re choosing C, which I think is a great choice in the long term. But I think in the short term, B is probably the easiest to implement, but A can allow porting existing code to this new platform more easily.

  13. Luke, this is Bruce from the FPUG. I really like your idea. It’s very similar to mine, except that I have been working on it full-time for many years and I am putting on the final touches. I know that if I met someone who was almost done with what I was just starting I would have a lot of strong feelings about having my idea and motivation stolen. (Then I’d get over it:) ) The thing is, it was MUCH harder than I ever thought it would be and I had to learn and invent a lot of mathematics. I also found some really cool things that will totally change the way we interact with computers; e.g., an almost perfect map from the mathematical model of information to natural languages. I also found that what I was doing was really discovery and that there is very close to one way to do it.

    If you look at infomage.com, the language is called “Proteus”, the “command line interface” is the proteus “core” and the GUI (which uses openGL/Cairo to render sound and video) is the “slypstreem engine.” The global distributed model is the “slypstreem”

    Whether your goal is the journey or the end result, we should have a beer and talk. Either way, one of us can help the other.

    Cheers!

  14. Bruce, I looked briefly at infomage.com, and posted a forum question (FURST!!). Sounds great… do you know of anywhere that has beer and blackboards? :-)

  15. Somewhere in Boulder there has GOT to be a place with beer and blackboards. Instead of going to watch a live band, people go to watch scientists and mathematicians plot. :)

  16. You could write something on top of HALVM then as you got more ambitious you would start to formally prove or replace parts of XEN. That way you could work on it incrementally.

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