Lambda the Ultimate

Neel - note the department assignments when you post!

The end result in both cases is serialization of the code, i.e. it's becomes viable to reason about side effects if they are executed in a well-known order. Isn't it so?

I'm glad some people started talking about the actual paper. =)

I am a big fan of finding ways to loosen up evaluation order.

But, from looking at it, each region in \lambda_wit^reg basically just takes the role of a multiple-reader single-writer lock with an enforced access protocol. While the reachability condition allows you to 'fan out' reads and do them in any order, if you ever want to write to any location in that region again you have to join all the witnesses for all the reads that occurred against it in order to meet the witness race freedom condition. Otherwise, you won't be able to construct another write to anything in that region. Thats kind of an ugly global property to have to reason about.

I do like the fact that it tackles the kinds of commutative actions that monads address so poorly, but it does so at the expense of equational reasoning, and the lambda_wit^reg confluence checking algorithm doesn't work in a call-by-need setting, so as designed it seems like an interesting direction, but as implemented its not quite an ideal solution.

I am not sure I fully appreciate the application of this paper but in terms of LAP there might be another approach that does not involve built in language features. The writers and readers of the reference data need a "contract" governing there exchange. In this case there might be a unique situation reference, as well as the other references. Each write would also contain its situation. The readers would be responsible for selecting and using the data correctly based on the situation. Situations also must terminate somehow.

This is just for the sake of a thought experiment or discussion.

This approach, while attractive, seems quite complicated. Adding monads to a purely functional language seems comparatively simpler. Am I wrong here?

This approach sounds very much like uniqueness types in the Clean programming language. From what I understand, in Clean, all type declarations, you can add an '*' to indicate that a particular parameter must be 'unique', meaning that the variable reference for that parameter must be the *only* reference to that variable in the system. This way, a destructive function consumes the one-and-only reference to that variable, making it impossible to call the function with that reference again, thus maintaining referential transparency. There are probably some other details, but that's the gist of it.