[Haskell-cafe] Well typed OS

[Ivan Perez]

On Fri, 5 Oct 2018 at 01:41, Joachim Durchholz <jo at durchholz.org> wrote:

> 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.
>

He seems to suggest that he is playing around with the idea, more than
proposing to write a whole OS.

For the sake of the exercise, it makes sense to assume that all programs
will carry a type specification.


>
> 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.
>

In part, isn't specifying this up-front what iOS and Android do with
permissions, or docker with capabilities?

As an exercise, I think this could be nice. And my intuition would be to
use specific effects/monads as well, both to provide the capabilities
themselves and to encode the idea that that permission or effect is needed.
Type inference might be able to tell you whether a permission may be needed
at all or not, so this seems like a potentially good idea.

The idea of using a less-than-IO monad to limit possible IO effects is not
uncommon. We briefly used it in [1, Section 7.3 - Limiting the Impact of
IO] and I seem to recall Thorsten Altenkirsch talking about this (I don't
remember if there's a paper and could not find one right now).

There's two parts to this problem: can I write Haskell programs with
limited-IO type specifications, and I think the answer is yes, and can I
ensure that programs will not use resources not declared in their type, and
I think the answer depends on kernel and, possibly, hardware support (even
if you restrict this to Haskell).

Because the type is not included in the program, it would not be included
with the executable. It would be interesting to output that too in some
form during compilation. This would seem also useful for DSLs.

Best wishes,

Ivan

[1] https://dl.acm.org/citation.cfm?id=2976010
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181005/f87c736e/attachment.html>