[Haskell-cafe] Well typed OS

[Joachim Durchholz]

Am 05.10.2018 um 06:36 schrieb Yotam Ohad:
> Hi,
> In the last couple of days, I've been toying with the thought of an 
> operating system in which programs (or more accurately, any process) has 
> a distinct type which limits
> its use of the machine. For example, `echo` (String -> String) won't be 
> able to print an output without a second program which would handle 
> changing stdout.
> 
> I think it could "break down" the IO monad into other structures that 
> are better at specifying what is changing: A file is read / memory 
> written / etc.
> I do, however, not sure how to incorporate drivers (which handles IO and 
> external devices) into this. Giving them an `IO a` type feels like 
> cheating. I would be much cooler if there was a way
> to treat them like the `echo` function from earlier.
> 
> What are your thoughts/suggestions? I'll be happy to hear them.

An OS needs to work for any programming language, so I'm not sure how to 
get from an IO-based approach to a working OS. Unless you plan to write 
the OS itself in Haskell and make it so that all programs are Haskell 
modules, but that's a huge task.

The design approach you're after is called "Capabilities". It's not 
ordinarily described as a type system, and I'm not sure whether it's a 
good idea to use static types in the first place because there are 
situations where you want to grant or revoke them dynamically.
See https://en.wikipedia.org/wiki/Capability-based_security . This 
article also has a link to other security models; capabilities are 
pretty famous, but it's quite possible that a different one would be a 
better fit.

HTH
Jo