I always felt, as a C++ programmer, that Haskell was just restricting me, without providing me any real benefits (of course, other people's opinion can vary!) -- on the other hand, Idris provides tools I can see as useful, things like checking at compile time all file handles are correctly opened before use, and closed after use (that's a very simple example, but just one type of thing you can do)
Also, you can already do half of what you described in Haskell. Just require the functions that work over open files to require an Open type which the open function would return.
Not quite. The problem is that values can be copied (AKA used "non-linearly"), for example:
open :: FilePath -> IO Open
readFile :: Open -> IO String
close :: Open -> IO Closed
main = do
-- Open a file handle
o <- open "/tmp/foo"
-- Close "o"
c <- close o
-- Try reading from "o"
s <- readFile o
putStr s
With linear types, we can make "Open" and "Closed" linear. It's a type error to use a linearly-typed value more than once, which rules out the above double-usage of "o :: Open". It's also a type error to create a linearly-typed value and not use it at all; we can use this when designing an API, e.g. to make a function like:
withFile :: (Open -> (Closed, a)) -> IO a
> things like checking at compile time all file handles are correctly opened before use, and closed after use
Using distinct `Open` and `Closed` types, as you say, doesn't help at all with ensuring file handles are closed after use.
They also don't ensure that handles are correctly opened before use, as I showed with my example `open "/tmp/foo" >>= (\o -> close o >> readFile o >>= putStr)`.
I can't think of a way to ensure both of these things, without using linear or dependent types to track state machines in types.
I can think of ways to ensure one of these things:
- To ensure files are correctly opened, we can remove the ability to close them. My above example would then work correctly, since `close o` would be a no-op, and `readFile` would succeed.
- To ensure all handles get closed, we can remove the ability to open them.
Separating handles into `Open` and `Closed` varieties does nothing more than provide documentation hints to programmers; it cannot automatically check whether handles are used correctly, it requires programmers to consciously avoid language features (like using variables multiple times), be careful about the way they compose functions, and write test suites to check if things are working. In other words, it provides none of the benefits of static typing, and is more akin to documentation in a dynamically typed language.
There was some discussion previously on HN about this https://news.ycombinator.com/item?id=12350273
AFAIK that sounds like unique/linear types, which Idris doesn't provide at this point, it's an experimental/work in progress feature: http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
There's a tutorial on just this sort of thing here: http://docs.idris-lang.org/en/latest/st/index.html
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?
-- Simon Peyton Jones
Although I understand why Idris is strict by default, there is a part of me that dies a little from that understanding :(
Haskell's laziness undoubtedly works and is useful; you might say it was Haskell's strictness that needed improving.
Just like other languages are strict by default, but can be made lazy via sequences, streams, generators,...
It is just a matter which defaults might be better for a given application.
Feel free to point if I've got any of the above wrong.
Update: Thanks for the replies, people.
In Haskell, the primary mechanism for inducing evaluation is the case expression (if/then/else and pattern matching are syntactic sugar for case).
Thunks (lazy expressions) in Haskell are created with let and then forced with case. It's very straightforward at the most basic level, there's just a lot of abstraction built on top of it that can obscure what's going on.
def foo(a: Bar)(b: a.Baz) = ...