[Haskell-cafe] Well typed OS

[Jeffrey Brown]

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 <vanessa.mchale at iohk.io>
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 <yotam2206 at gmail.com> 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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181020/22d9d726/attachment.html>