[gargantuan]

Also what about protocols? Can type systems handle that. Things like:

  * open file
  * close file
  * read form file

That can be type checked up and down it will still be broken. Is that Rich Hickey meant? Here we are dealing with a real world -- a file. And it has a protocol to access it. So in a sense we want a protocol checker not a type checker in that case...?

[evincarofautumn]

Separation logic can handle that—it’s a program logic that subsumes typechecking and typestate, among other things. Your example, in pseudocode:

    // open : string -> file_mode -> (f : file) | f @ read * f @ close
    f = open "input.dat" Read

    // close : (f : file) | f @ read * f @ close -> ()
    close f

    // getline : (f : file) | f @ read -> string | f @ read
    s = getline f

“open” grants the “read” and “close” permissions to “f”; “close” revokes the “read” permission that “getline” requires, causing “getline” not to typecheck.

[salmonellaeater]

You could certainly handle that kind of error using a type system. There could be a scoping rule where certain kinds of operation (i.e. close file) put the reference to the object out of scope. The way Haskell chains I/O operations using monads is another way: the result of the 'close file' operation is basically a world that doesn't contain a reference to the file.

[mcosta]

I am pretty sure with a elaborate enough system with alias-forbidden types and resource managers you can do it.

with file.open as f do .... alias = f // fail done // autoclose

But then, is it really necessary?