Hacker News Reader

Comment by juliangamble | Hacker News Reader

Some food for thought from Rich Hickey: "Statically typed programs and programmers can certainly be as correct about the outside world as any other program/programmers can, but the type system is irrelevant in that regard. The connection between the outside world and the premises will always be outside the scope of any type system." http://www.reddit.com/r/programming/comments/lirke/simple_ma...

View on HN

He seems to be saying "types are just a formal system; they are meaningless until given meaning by an interpretation". Which is, of course, true. But the same can be said of programming languages. They're just meaningless squiggles until interpreted by human or machine.

Assuming you have some sort of specification for your program, you can use a formal system (such as a static type system) to describe aspects of the specification. It's up to you to correctly model the requirements in the system, but it's similarly up to you to model the requirements of the system in your (far larger and more complex) program. The types ensure that the program fits the aspects of the specification you were able to describe with them.

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

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?

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.

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.

I was more convinced by someone who replied to that post (psnively). He seems to be saying that type systems can't model the world as we know it perfectly, in which case it sounds like a Nirvana fallacy - we can model a lot of things that we care about as programmers, so even though we can't model all of it, it still has merit. If what he is referring to is that type systems are somehow "separate" from the outside world, then it seems somewhat like saying that mathematics is a wholly abstract field. Still, though, applied mathematics has been incredibly successful.

After psnively's reply, Rich decides to throw a tantrum (read: "bow out").

Reply on news.ycombinator.com