<div dir="ltr"><div dir="ltr"><br><br><div class="gmail_quote"><div dir="ltr">On Fri, 5 Oct 2018 at 01:41, Joachim Durchholz <<a href="mailto:jo@durchholz.org">jo@durchholz.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Am 05.10.2018 um 06:36 schrieb Yotam Ohad:<br>
> Hi,<br>
> In the last couple of days, I've been toying with the thought of an <br>
> operating system in which programs (or more accurately, any process) has <br>
> a distinct type which limits<br>
> its use of the machine. For example, `echo` (String -> String) won't be <br>
> able to print an output without a second program which would handle <br>
> changing stdout.<br>
> <br>
> I think it could "break down" the IO monad into other structures that <br>
> are better at specifying what is changing: A file is read / memory <br>
> written / etc.<br>
> I do, however, not sure how to incorporate drivers (which handles IO and <br>
> external devices) into this. Giving them an `IO a` type feels like <br>
> cheating. I would be much cooler if there was a way<br>
> to treat them like the `echo` function from earlier.<br>
> <br>
> What are your thoughts/suggestions? I'll be happy to hear them.<br>
<br>
An OS needs to work for any programming language, so I'm not sure how to <br>
get from an IO-based approach to a working OS. Unless you plan to write <br>
the OS itself in Haskell and make it so that all programs are Haskell <br>
modules, but that's a huge task.<br></blockquote><div><br></div><div>He seems to suggest that he is playing around with the idea, more than proposing to write a whole OS.</div><div><br></div><div>For the sake of the exercise, it makes sense to assume that all programs will carry a type specification.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
The design approach you're after is called "Capabilities". It's not <br>
ordinarily described as a type system, and I'm not sure whether it's a <br>
good idea to use static types in the first place because there are <br>
situations where you want to grant or revoke them dynamically.<br></blockquote><div><br></div><div>In part, isn't specifying this up-front what iOS and Android do with permissions, or docker with capabilities?<br></div><div><br></div><div>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.</div><div><font size="2"><br></font></div><div><font size="2">The idea of using a less-than-IO mona</font><font size="2">d to limit possible IO effects is not uncommon. We briefly used it in [1, Section 7</font><font size="2">.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).</font><div><br></div></div><div>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).</div><div><br></div><div>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.</div><div><br></div><div>Best wishes,</div><div><br></div><div>Ivan</div><div><br></div><div>[1] <a href="https://dl.acm.org/citation.cfm?id=2976010">https://dl.acm.org/citation.cfm?id=2976010</a><br></div></div></div></div>