Home

Witnessing Side-Effects

Witnessing Side-Effects, Tachio Terauchi and Alex Aiken. ICFP 2005.

We present a new approach to the old problem of adding side effects to purely functional languages. Our idea is to extend the language with “witnesses,” which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient.We also give a static checking algorithm that makes use of a network flow property equivalent to the semantic condition.

If I understand the idea in this paper correctly, you take a functional language with a possibly non-deterministic or parallel execution model, and then add references to it. To keep this from being impossible to reason about, you add dataflow tokens to each reference operation (assignment, allocation, reading) to ensure that they don't happen until each op's predecessors have happened -- and you make the tokens first class, so that the programmer can directly specify the amount of serial execution needed. Then you can do an analysis to ensure that the reduction is confluent, which means that you have no races.

By neelk at 2007-09-28 19:38 | Functional | other blogs | 14280 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Departments

Neel - note the department assignments when you post!

By Ehud Lamm at Fri, 2007-09-28 19:47 | login or register to post comments

Thanks for the reminder

It's been fixed.

By neelk at Fri, 2007-09-28 20:17 | login or register to post comments

More courtesy please.

Ehud, I want to point out that this post (and others you have made in the past to other contributors) can come across as having a somewhat scolding tone. Using the word "please", and avoiding the use of unwarranted exclamation points, will go great lengths to soften such suggestions.

By cdiggins at Sat, 2007-09-29 18:32 | login or register to post comments

He is scolding!


By Derek Elkins at Sat, 2007-09-29 20:37 | login or register to post comments

Isn't that counterproductive?

Isn't that counterproductive? I would think that a public scolding rather than a gentle reminder would discourage people from making posts to the front page.

By cdiggins at Sat, 2007-09-29 23:53 | login or register to post comments

neelk should know better

neelk should know better (hence scolding) and I'm sure he can take it. Not everyone is equal on LtU.

By Derek Elkins at Sun, 2007-09-30 00:09 | login or register to post comments

That said, an example of

That said, an example of that inequality might be that other contributors find it awkward. I'm guessing that's more the point than leaping to neelk's defence.

By Philippa Cowderoy at Sun, 2007-09-30 01:09 | login or register to post comments

courtesy

@cdiggins
I find Ehud comment terse and to the point, not uncourteous.
Since you raised the subject of courtesy I would like to present my own claim about courtesy.
I find political correctness overly dumb and irritating, could you have the courtesy not to ask for political correctness as I am extremely resentfull of such demands :-)

Thanks.

By Jean-Luc Delatre at Sat, 2007-09-29 20:52 | login or register to post comments

cursity

I find Ehud comment terse and to the point, not uncourteous.

This seems accurate to me. That's clearly the case if you read the original comment without projecting an emotional interpretation onto it.

In any case, neelk certainly doesn't deserve scolding — he's one of LtU's most active contributing editors, for which we should all be grateful. Thanks Neel! That said, remember to classify your stories by department, you ignorant slut!

By Anton van Straaten at Sun, 2007-09-30 00:57 | login or register to post comments

I agree re Ehud's comment.

I agree re Ehud's comment. Discourtesy would be introducing the spectre of political correctness to a disagreement about terseness, no?

By Philippa Cowderoy at Sun, 2007-09-30 01:07 | login or register to post comments

Isn't it practically the same result with monads?

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?

By Achilleas Margaritis at Tue, 2007-10-02 10:26 | login or register to post comments

This and nothing else

I think I agree. But I would put it this way. If a side effect has a known behavior the program as a whole can be modeled. The issue from a functional point of view seems to be whether I can look at the code and prove that the behavior of the effect is what I want it to be. Isn't this a matter of how I write the code? I need to say that it does this and nothing else. An automata has this property. In the paper we are dealing with a system, but the possibility of races means it isn't properly written. It needs to be rewritten so that there are provably no races. Monads might be a way to do this, but I would like to see a proof that using monads can prevent races. Is it only a matter of monads, or is there still a design issue?

By Hank Thediek at Tue, 2007-10-02 12:30 | login or register to post comments

There's still a design issue

There's still a design issue - you need to have the right monads.

By Philippa Cowderoy at Tue, 2007-10-02 13:10 | login or register to post comments

Regions as locks

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.

By Edward Kmett at Tue, 2007-10-02 14:50 | login or register to post comments

Communicative acts semantics

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.

By Hank Thediek at Wed, 2007-10-03 13:07 | login or register to post comments

Language implementator point of view

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

By naasking at Wed, 2007-10-10 02:08 | login or register to post comments

Uniqueness types

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.

By C Rebert at Sun, 2007-11-25 07:58 | login or register to post comments