3 ms·

> Languages that use types for elaborate proofs always seem to me like they only prove the most uninteresting properties of programs, namely the parts that deal

> Languages that use types for elaborate proofs always seem to me like they only prove the most uninteresting properties of programs, namely the parts that deal with data transformations. > At the end of the day, programs are written for their side effects The reason for such a focus on data transformation is that it's very easy to do in these purely functional languages (Agda included). It's so easy, in fact, that "other" things, like side effects, event handling, etc. are represented as data transformations. This is most obvious in Haskell, since laziness decouples definition from computation; eg. making it trivial to represent event streams as infinite lists. > What I'm most interested in is proofs that, say, in a concurrent environment, a function that closes a socket will never be called as long as there are pending tasks to write to the socket. The usual approach is to define a datatype of operations you might want to perform (eg. `Write String`, `Read Length`, etc.). Next you define a datatype which can combine these operations together in ways you may want (eg. something like a rose tree, if you want threads firing off threads). This forms an "embedded domain-specific language". We then write a bunch of helper functions for manipulating these datastructures (eg. a "combinator library"), then we use these to write down what we actually want as a combination of operations. Next we write an interpreter function which opens a socket, performs all of the operations in the tree (possibly in multiple threads), waits for them to finish then closes the socket. > Or, because I write concurrent data structures, I'm interested to prove that a certain function will eventually release all locks it acquires. Are there any such languages? You can do the same thing as with the socket example, except you can strengthen the type of your program (operation-combining) datastructure to enforce that locks are released. As a simplified example, we can force a serial computation to release locks by only allowing AQUIRE and RELEASE to be inserted together: data Op = Foo | Bar | Aquire ID | Release ID data SafeOp = SFoo | SBar data Program : Type where NoOp : Program -- Empty Program WithLock : Program -> Program -- Add lock ops to a Program PrefixOp : SafeOp -> Program -> Program -- Add a non-lock Op to a Program Interleave : Program -> Program -> Program -- Combine two Programs -- Part of the interpreter, not exposed to the world progToOps : Program -> [Op] progToOps NoOp = [] progToOps (WithLock id p) = [Aquire id] ++ progToOps p ++ [Release id] progToOps (PrefixOp SFoo p) = [Foo] ++ progToOps p progToOps (PrefixOp SBar p) = [Bar] ++ progToOps p progToOps (Interleave p1 p2) = interleave (progToOps p1) (progToOps p2) interleave [] ys = ys interleave (x:xs) ys = [x] ++ interleave ys xs Notice that progToOps can never output a list containing Aquire without also containing a Release with the same ID. Also notice that we can define arbitrary combinations of the other ops: [] is NoOp [Foo, Bar] is PrefixOp SFoo (PrefixOp SBar NoOp) [Foo, Aquire A, Bar, Aquire B, Release A, Foo, Release B] is Interleave (PrefixOp SFoo (PrefixOp SBar NoOp)) (Interleave (WithLock A NoOp) (WithLock B (PrefixOp SFoo NoOp))) Of course these datastructures would be build up by helper functions instead of by hand, would be tree-like for concurrency, would probably provide guarantees per sub-tree, would allow arbitrary functions (of some suitable type) in place of Foo, Bar, etc.

pron 12y ago
But in your example the program doesn't represent the code itself but a program written in some new language. I said that current type systems are good for writing compilers, but not so good at describing their own behavior other than data transformations.
- art-w 12y ago
  It's not reasonable to embed every possible language constructs, semantic and logic into a theorem prover. So the trick is to make the host generic enough to be able to embed your needs as a domain specific language: your critic becomes a library problem. Which implies that you only need to trust the host logic/implementation; and many people can work, collaborate and profit from the same core. Also, we kind of know how a generic logic can be done, but the domain specific logic are more controversial (because everyone needs are different.) The fact that your DSL is represented as an immutable datastructure by the host is really not important. Any code you write is going to be turned into a datastructure at some point. The immutability should be read as "the context in which this result is valid has been made fully explicit", where "context" includes "things that mutate over time". You don't loose in expressivity, you just can't forget to handle special cases.
  - pron 12y ago
    I think this is a type system limitation that every type describing side effects -- i.e. the core of every interesting program other than a compiler/interpreter -- can only be used in the context of a compiler/interpreter. Checker (Java 8's pluggable intersection type-system framework) is able to do that (define side-effect types), but isn't a single general type system. I.e. you need to write a different type system for each property (of course, they can all work together). Maybe that's the only known way to do that. Searching for more general solutions, I've come up empty handed (the problem is well known, but the solutions are all in early stages of research). The idea of such a type system needs to be something like: each function has a set of types associated with it, and a function's type interacts with the types of the functions it calls in some ways. So the most primitive example is, of course, checked exceptions, where the type of a function is a simple union of the types of its callees. But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.

pron 12y ago

But in your example the program doesn't represent the code itself but a program written in some new language. I said that current type systems are good for writing compilers, but not so good at describing their own behavior other than data transformations.

art-w 12y ago
It's not reasonable to embed every possible language constructs, semantic and logic into a theorem prover. So the trick is to make the host generic enough to be able to embed your needs as a domain specific language: your critic becomes a library problem. Which implies that you only need to trust the host logic/implementation; and many people can work, collaborate and profit from the same core. Also, we kind of know how a generic logic can be done, but the domain specific logic are more controversial (because everyone needs are different.) The fact that your DSL is represented as an immutable datastructure by the host is really not important. Any code you write is going to be turned into a datastructure at some point. The immutability should be read as "the context in which this result is valid has been made fully explicit", where "context" includes "things that mutate over time". You don't loose in expressivity, you just can't forget to handle special cases.
- pron 12y ago
  I think this is a type system limitation that every type describing side effects -- i.e. the core of every interesting program other than a compiler/interpreter -- can only be used in the context of a compiler/interpreter. Checker (Java 8's pluggable intersection type-system framework) is able to do that (define side-effect types), but isn't a single general type system. I.e. you need to write a different type system for each property (of course, they can all work together). Maybe that's the only known way to do that. Searching for more general solutions, I've come up empty handed (the problem is well known, but the solutions are all in early stages of research). The idea of such a type system needs to be something like: each function has a set of types associated with it, and a function's type interacts with the types of the functions it calls in some ways. So the most primitive example is, of course, checked exceptions, where the type of a function is a simple union of the types of its callees. But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc.