C++ (if not used as C with classes) is built around RAII and will also enforce file handles to be opened before use and automatically closed when leaving scope (no longer in use).
Now std::ifstream isn't 100% idiomatic RAII (because constructor sets error state instead of throwing and it also provides open/close-methods) but generally you should be able to encode a safe file handle into the c++ type system. Here is how i would compare it to what idris describes in https://media.readthedocs.org/pdf/idris/latest/idris.pdf
* It is necessary to open a file for reading before reading it
> Enforced by RAII, create file handle(variable) is equivalent to opening file
* Opening may fail, so the programmer should check whether opening was successful
> If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle.
* A file which is open for reading must not be written to, and vice versa
> Can be enforced with different types for reading and writing (ifstream vs ofstream).
* When finished, an open file handle should be closed
> fstream is automatically closed when variable goes out of scope.
* When a file is closed, its handle should no longer be used
> Here it's actually the other way around, the correct way to close a file is to get rid of the last handle refering to it.
> Hence a handle can't be used to write to a closed file since such a handle cannot exist in the first place.
> If opening file fails, exception is thrown when the handle is created, it is impossible to create/use an unopened handle.
Unfortunately C++ offers no way to track which exceptions any given function might throw and/or enforce that they are handled.
> fstream is automatically closed when variable goes out of scope.
That works for the simple case where the variable exists on the stack of a single function. C++ does not offer safety in the general case where you pass a handle to/from functions, store it in data structures and so on. (You have the option of runtime checks via shared_ptr etc, but at that point you have very little assurance the file ever actually gets closed).
Checked exceptions would be neat but still, if you don't catch the exception it will be propagated further up the chain, so the claim that it is impossible to create an unopened file handle still holds :)
Yes, object lifetime management is not provably safe in c++, due to lack of borrow checker, but that's a general problem for all types of objects, not specifically file management.
> Checked exceptions would be neat but still, if you don't catch the exception it will be propagated further up the chain, so the claim that it is impossible to create an unopened file handle still holds :)
True, but introducing invisible partiality to essentially all functions is a pretty stiff cost.
> Yes, object lifetime management is not provably safe in c++, due to lack of borrow checker, but that's a general problem for all types of objects, not specifically file management.
Well, that's a question of language design philosophy. Object management is so much more frequent than any other kind of resource management that it may be worth treating as a special case, as most languages other than C++ do.
Be that as it may, the point is that the really cool thing about Idris is that its type system is powerful enough to let you implement borrow-checker-like functionality in "userspace" rather than needing it built into the language. In theory one could use that (in an Idris-like language with a different record feature, standard library and so on) to have Rust-style manual-but-safe memory management for all objects, though I suspect that might be too cumbersome to be practical.
But you either have to use unique ptr (then passing the pointer around is a pain), or shared ptr (then you pay a runtime cost of counting). In idris the type system deals with these things better.
See https://github.com/isocpp/CppCoreGuidelines/blob/master/CppC...