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.