Re: [Haskell-cafe] Well typed OS

I don't know whether this is helpful, but Purescript provides a way to specify the kinds of IO a monad can do. For instance, the Extensible Effects section[1] of Purescript by Example includes this code snippet: > :type main forall eff. Eff (console :: CONSOLE, random :: RANDOM | eff) Unit [1] https://leanpub.com/purescript/read#leanpub-auto-extensible-effects On Fri, Oct 19, 2018 at 8:11 PM Vanessa McHale wrote:

There's a lot of other stuff going on too, not just binary sizes - GHC's runtime, a dynamic memory allocator, etc. I would hesitate to use Haskell in the embedded context or for hardware-level stuff. I presume GHC's approach to laziness has a role in this.

I don't have much experience with OCaml but my experience with ATS is that it's very much possible to have functional, ML-style programming without a runtime or even dynamic memory allocation.

On 10/19/18 4:02 PM, Andreas Reuleaux wrote:

...

While this may not be an answer to your specific question, you may want to have a look at MirageOS, the Operating System written in Ocaml by Anil Madhavapeddy el., https://mirage.io/

We had discussed this some while ago in our seminar, and I learned that Ocaml may be a better fit for writing an operating system than Haskell, due to Ocaml's ability to produce small binaries, smaller than Haskell binaries in any case usually. - Being involved with Haskell personally, I would like to be proven wrong, of course (ie. I would like to see small Haskell binaries), and I have heard of some former efforts of writing an OS in Haskell as well (but I would have to search for links).

just my 2 cents, Andreas

Yotam Ohad writes:

...

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.

Yotam _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

---

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- Jeff Brown | Jeffrey Benjamin Brown Website https://msu.edu/~brown202/ | Facebook https://www.facebook.com/mejeff.younotjeff | LinkedIn https://www.linkedin.com/in/jeffreybenjaminbrown(spammy, so I often miss messages here) | Github https://github.com/jeffreybenjaminbrown