Home » forums » LtU Forum

sublanguages of CTM's Oz

I've been reading van Roy and Haridi's Concepts, Techniques, and Models of Computer Programming. It is an exciting and thought-provoking work. I have one major criticism of it that I thought LtU participants might be interested in discussing. While Oz does a great job of incorporating multiple programming models into a single language, to me what it lacks is a way of constraining oneself to a particular model or set of models, and demonstrating to others that these constraints have been met.

For example, I would like a way to assert that a function is declarative (i.e. is truly a function), and have this be enforced. I suppose this would have to be enforced at run-time to fit with the dynamically typed language design. Also, I'm not sure how this would be enforced; a conservative strategy would be to consider any use of NewCell or Exchange as non-declarative, but this would yield "false positives" in cases where state is used in a function that is still observationally declarative (e.g. is just using state for memoization).

Perhaps I want something more like monads in Haskell, where the fact that function that is not observationally declarative will be reflected in its type (and the way must be used). But this may be an inappropriate comparison because Haskell is a one-model language and is only simulating a stateful model via monads. And of course it is statically typed. In fact the CTM authors specifically mention (page xxi) that they disfavor the monadic approach to state because it is too explicit, violating modularity by making the use of state change the interface to a function (if I understand them correctly).

On the flip side, I'd say modularity is better supported by a language in which design contracts (e.g. do you use state) can be enforced. It all comes down to whether you think the use of state is a private or public manner, or perhaps under the choice of the programmer whether to make it private or public (and if the programmer chooses to keep that choice private, we are forced to make the conservative assumption that he did use state).

By bdenckla at 2006-03-20 02:20 | LtU Forum | previous forum topic | next forum topic | other blogs | 5737 reads

Comment viewing options

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

I dont think you can use

I dont think you can use state monads in haskel to implement memoization, without giving the memoizationing function a monadic (nonpure) type. And I guess thats one of the modularity violating aspects of monad based state, that they are talking about.

I also think that asserting that a function is observationally declarative even thought it has an imperative implementation is generally impossible. (perhaps if we demand that the function is memoized, and not involve anything non-funcional but second class cells (threads, continuations, exceptions...).)

By Felicia Li Svilling at Mon, 2006-03-20 04:06 | login or register to post comments

memoization

Right, the use of state in memoization could not be hidden in Haskell. I guess I'm kind of saying that is a good thing. I too, have a feeling that deciding observational declarativeness is impossible. So probably you'd have to do something conservative, and possibly that would be annoying if there were lots of false positives. Unless you're not trying to decide it and rather, you are somehow detecting it at runtime.

Also I have to think more about this observational declarativeness concept. I'll have to study CTM some more to figure out, for example, would a function using memoization be obs. decl. even if invoked from multiple threads? Would seem to depend on the atomicity of the updates to the data structure used for memoization.

By bdenckla at Mon, 2006-03-20 16:42 | login or register to post comments

Enforcing declarativeness

Section 4.1.4 of CTM (on pages 245-246) talks about "failure confinement": if you "leave the declarative model" by making nondeterminism visible, then one way to get back to the declarative model is by hiding the nondeterminism. This can be done by the programmer by making a local transformation to the program (not necessarily just at function boundaries, by the way). But we still have to prove that the transformed program does in fact hide the nondeterminism. For this example that's easy, but in general it can be harder.

The general problem, like you say, has two extreme solutions: a syntactic one and a semantic one. The syntactic one is easy: just forbid certain operations (more generally, make sure your program satisfies some simple rules that can be checked by a parser). The semantic one is more difficult: your program should be observationally equivalent to one written in a particular model. This opens the door to a whole series of techniques coming out of process calculus theory. My view would be to keep a clear goal in mind, namely *why* you want to enforce a particular model, and use some kind of "contracts" (with tool support?) to implement the goal.

By Peter Van Roy at Mon, 2006-03-20 17:56 | login or register to post comments