Yes, you can embed those semantics inside functional semantics, and even use the functional language to add more static verification at the type level via things like F-Star's Hoare logic. But you're still mostly going to shoving bits in specific places based on the result of a shallow pure function applied to bits you yanked from a specific place.
On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation (and which are hard to avoid categorically), so you'll need to work within an especially restrictive DSL. Definitely no lambdas or partial application. So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad". Where in this do you see any functional-ness, outside of the fact that you'll probably call your procedures functions?
> Many useful & powerful functional abstractions can be written to use constant space, even in Haskell.
Yes, but not to the degree that Atom's use cases require (where the program must allocate all memory ahead of time and therefore know a specific upper bound). This necessitates deviation from usual practices of any kind, including Haskell's.
The difference being that this "very fine imperative language" has much stronger type safety guarantees.
Maybe we can stop having ring0 buffer overflows some day when C programmer pride is sufficiently assuaged. I doubt it though... My experience with the linux kernel community is that it is a limitless void of insecurity and infighting.
> On top of that, you're not going to be able to abide the kind of allocations that functions in Haskell, OCaml, etc. can do with little provocation
OCaml does much better here (in fact, really quite amazingly well here, on part with some of the greatest common lisp distribution compilers which were stunningly good at it). But yeah, Haskell has a very poor focus on the needs of the "industry" when said industry is focused around extremely tight optimizations.
That said, I refuse to confuse a specific example of FP with a traditionally academic and research focus with the discipline as a whole. That's a dodge.
> So in the end you'll be in "Generic Stack-focused Pointer-pushing Procedural Imperative Language: The Monad".
Honest question: what's the problem with this if it offers additional safety and promotes the use of stateless functions? If it all compiles down to similar code, then it's fine. People act like monadic code is not functional, when it is in fact extremely functional code.
That's what's funny about all this: imperative programming is expressible succinctly and easily in functional languages.
Would you consider a C program transliterated into a representation of C inside a functional language and then annotated with proofs to be "functional"? My argument is what you get if you write a true kernel (no sitting on top of a runtime written in something else) is going to look a lot like that would.
Is that a result of the specific language, rather than FP?
That is: One could think about building a procedural language that had... well, I'm not sure it could have Hindley-Milner types, because I'm not sure it could have higher-kinded types, but it could come close, couldn't it?
And from the other side: Does FP require very strong types? Or can it be done with something equivalent to C/C++'s type system? Or Python's?
Here's a table of processes. We want it to be an array, rather than a linked list, for efficiency reasons. When a new process is created, we don't want to copy the array, also for efficiency reasons. So we mutate the array.
> So does every computer programmer though.
Not really.
Why do you think that FP doesn't have tools for this? Do you genuinely think that in 20+ years of research no one has thought of this? Have you investigated it?
I don't know. If you think that things like ST aren't suitable please say why (other than the larger problems with monad transformers, of course).
Are the FP tools as efficient as the direct, C-style approach? For an OS, that matters.
Are the FP tools as easy to reason about correctly (especially in a section you're not familiar with)? For an OS that's worked on by thousands of people, that matters.
In this context, what is "ST"? And, what are the larger problems with monad transformers?
I'm sorry, I decline to continue this conversation further.
In many ways the early MIT Lisp Machine morphed into a Flavors Machine in the early 80s.
Remember, Lisp is a multi-paradigm language.
At least in Linux, the table of processes is implemented as a (doubly) linked list.
Not really?
> A kernel (especially a microkernel) spends most of its time managing state.
So does every computer program though. The idea that functional languages can't support mutation is a strangely persistent myth even in the face of multiple counter-examples AND 20 years of improvement via research and practical work.
> but you won't be writing code that looks remotely functional.
Many useful & powerful functional abstractions can be written to use constant space, even in Haskell.