6 ms·
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
by 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 agoI 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 agoSeparation 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 agoYou 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.