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).
See https://github.com/isocpp/CppCoreGuidelines/blob/master/CppC...
See https://github.com/isocpp/CppCoreGuidelines/blob/master/CppC...
* 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.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).
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.
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.
You must track files by some type already right?