3 ms·

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/pro

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_made_easy_by_rich_hickey_video/c2u1fgc http://www.reddit.com/r/programming/comments/lirke/simple_ma...

Dewie 12y ago
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").
gargantuan 12y ago
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...?
- mcosta 12y ago
  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?
- evincarofautumn 12y ago
  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 12y ago
  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.
pinealservo 12y ago
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.

Dewie 12y ago

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").

gargantuan 12y ago

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

mcosta 12y ago
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?
evincarofautumn 12y ago
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 12y ago
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.

pinealservo 12y ago

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.