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`.