> What happens if a dependency adds a system call something?
AFAIK, in Haskell, any function that returns IO must indicate it in the type signature.
If you could find a way to take that idea, expand upon it with much more fine-grained types, then you could build an ecosystem where any system call, external network call, use of env variables, etc is baked into the type signature of every function and package. If you could do that, you could build pretty trivial checks to ensure that a given package doesn't perform any kind of system call.
So sort of like the types of permissions we assign to apps on Android, but represented (and enforced) directly in the type system.
It would be difficult to make something like this ergonomic but could be pretty cool.
This works in Haskell because it is a purely functional language, and the IO monad is an intrusion into that to allow for useful computation. Rust is not purely functional, so there is no way to enforce something like this in the compiler. You could add an IO monad, but it would be easy for someone further down the chain of packages to ignore it and make a syscall.
Anything similar in rust would have to be enforced through code auditing tools, either forking the compiler, using some of its code as a basis or starting from scratch.
Yes, it is a shame that no version of that purely functional Haskell ideal has been created that could reasonably be used for kernel development. Using the type system to constrain side effects of code in the way you suggest would eliminate massive classes of security vulnerabilities and crashes.
IO is necessary because of purity, but it's in no way enabled by it. You don't need purity to have the IO monad, and you don't need purity to enforce that IO is defined in a type signature.
I feel like effect systems like the ones in unison and koka (or haskell with extensible effects / freer libraries like polysemy or eff) get pretty close to that. I feel like there's a lot of effort needed to make the idea "mainstream" and to get a good implementation going though (I think a lot of implementations use delimited continuations, but I'm not sure so don't quote me on that. At least it's the design for haskell's new primops to make that kind of library better)
If you're going to pick a "counterexample" just say unsafePerformIO, or the aptly named accursedUnutterablePerformIO[0]. (There are quite a few variants.)
Everybody knows that there are escape hatches because they are actually sometimes absolutely required for asymptotics or just plainly because it may be too hard to "prove" that your code is safe to the compiler.
That isn't a gotcha -- you know exactly what code you need to audit extra carefully.
[0] That one's actually in ByteString to technically not standard Haskell, but I just like the name.
AFAIK, in Haskell, any function that returns IO must indicate it in the type signature.
If you could find a way to take that idea, expand upon it with much more fine-grained types, then you could build an ecosystem where any system call, external network call, use of env variables, etc is baked into the type signature of every function and package. If you could do that, you could build pretty trivial checks to ensure that a given package doesn't perform any kind of system call.
So sort of like the types of permissions we assign to apps on Android, but represented (and enforced) directly in the type system.
It would be difficult to make something like this ergonomic but could be pretty cool.