More on OS design

I've been thinking a bit again about modern type systems with respect to operating system design and I think I can describe heuristically some of my old ideas and the open questions I still have. If there are comments or ideas, I'd love to hear them.

I like modern type systems. I also like capabilities. How can we combine them together? I used to think I had more solid leads on this question, but now I feel a little shaky. What I wanted to do was have a set of capabilities, essentially just indexes into some resource mapping in the kernel, be attached to each process. The actual access rights for each resource would be encoded as a phantom type in the capability. So for each resource type you'd have some set of operations that would have preconditions about the phantom types they would find acceptable. If you wanted to pass a capability to another process you can use provided functions for making a copy securely, giving any level of permissions less than or equivalent to your own.

Now there are some things that I think make sense here: the more we can shove questions of safety into the type system, the less we have to do at runtime and the better scalability you can have. Also, I think it encourages a very different UI experience. To see a resource you need to have a capability to it, but if you're dispatching over the type of capability then presumably you could do something like have the only shell commands available for that resource be the ones that match the type signature of the resource. I'm not sure how to actually implement a feature like that, but it seems like it should be feasible on a moral level.

I feel like there's three questions I have to answer in order to take the idea from "oh that's kinda cute" to something real. The first problem is bootstrapping and snapshotting of the OS. I haven't even begun to think about this, honestly.

Another issue is how the process and system call model would have to work. We'd want the system calls to be somehow typechecked for proper capability use. Again, I'm not sure of a good scheme for this that doesn't restrict execution to just the host language. Perhaps the bullet that has to be bitten involves making some form of FFI for each compiler that should target this system so that the system calls are made in the host language and then type checked at compilation.

The last issue that's still fuzzy in my head involves storing capabilities for a process. Now, it's all fine and dandy to say 'it's a set', but most data structures in a language such as Haskell are homogenous. What I need is a heterogenous container that doesn't completly lose type information, which means that using type classes and existentials is right out. I know Oleg Kiselyov has done work with thing like HList, but that's something I don't know much about.

Revisiting old concepts

In an old post I threw out the perspective that typeclasses & exokernels are similar ideas, but I explained it so pithily I think it was more or less incomprehensible. Honestly, even I had to sit & think for a minute to figure out what I meant over a year ago.

The idea wasn't really that profound, but did amuse me a little.

Let's say that you design a type class called Hardware, maybe even require that it be a monad or at least applicative, that includes all of the functionality you'd want from an exokernel, i.e. protection & raw handling of resources. You should also define a set of algebraic properties that you want all of these operations to satisfy in practice.

Any actual instance of this type class that satisfies all of our conditions is an implementation of an exokernel.

Then your libOS, the part that does all the nasty work of management of resources, can be polymorphic over the implementation and only work with the basic protection interface defined by the type class.

This whole business occurred to me a long time ago because of reading the original House paper and their discussion of the H monad. They don't quite take it in this direction, but I think that it seems feasible.

I'm being a little hand-wavy, though, because this isn't something I've
actually tried to make. It just seems like a compelling bit of imagery & possibly a good idea for organizing a kernel.