4 ms·

I'm not sure that is quite a simple example actually. Sounds kind of complex to prove that all file handles are closed after use (how soon after use?) in the ge

• lgas 10y ago
  If you search for the "File Management" section in this doc, you can see an example of what he's talking about. https://media.readthedocs.org/pdf/idris/latest/idris.pdf https://media.readthedocs.org/pdf/idris/latest/idris.pdf
• chriswarbo 10y ago
  > 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 This program will type-check, since "o" has type "Open", so it's a valid input to "close" and to "readFile". The problem is that the type system has no idea that calling (the IO action returned by) "close o" makes subsequent uses of "o" invalid, even though it still has type "Open". 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 The only way to call this function is to provide it with a function of type `Open -> (Closed, a)`. If we've encapsulated our implementation details, then the only way to write a function which returns a `Closed` is to have it call `close :: Open -> Close`. Since values of type `Open` can't be re-used, this must either be its argument or the return value of some call, e.g. `readFile :: Open -> (Open, String)` or `writeFile :: String -> Open -> IO Open`, which in turn require an `Open` argument, and so on; forcing a chain of operations, culminating in a `close`.
  • pdexter 10y ago
    I said half.
    • chriswarbo 10y ago
      Yes, but your approach doesn't actually solve any of the requirements: > 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.