A survey and discussion of taming effects

My previous post dealt with the advantages of referential transparency, and those advantages are lost without properly taming effects. In designing my language, I've waffled back and forth on the purity argument: whether to follow SML's example and just adopt a call-by-value semantics and effects, or whether to adopt a slightly safer, more disciplined stance and maintain referential transparency.

I've researched many different approaches to taming effects in the hope of maintaining referential transparency, and I will summarize and link to those works here.

The two predominant techniques are obviously monads as in Haskell, and linear types as in Clean.

Monads are somewhat attractive as they can be expressed in Hindley/Milner type systems, and are relatively straightforward to use once you understand the basic idea. However, monads require the developer to ensure he satisfies various algebraic properties, which can be difficult to understand. There has been some advancement in simplifying the development of monads via the Unimo framework (first seen on LTU here). Unimo abstracts the core monad logic into a common structure, and allows the developer to define monads via operations instead of the usual denotations. It further defines an observer function which enforces the monad laws, so the result is more heavily checked than if you had defined the monad yourself. Unfortunately, Unimo requires rank-2 types and other sophistication, which I doubt I'll provide.

Further, monads also carry efficiency concerns. A purported partial solution is Monadic Reflection (talk slides for Monadic Reflection in Haskell, whose paper doesn't seem available). Monadic reflection involves transforming the core of Haskell's monads to use mutable state and continuations to gain efficiency; essentially, continuations and mutation are the most general effects, and they can be used to simulate other effects. I'm still trying to figure this one out. :-)

F# has recently introduced "computation expressions", which that post describes as a general monadic syntax. I haven't been able to find a paper describing computation expressions, so any links would be appreciated. As a balance of usability against safety, something like this might present quite a good tradeoff.

"Witness types" recently made an appearance on LTU. They provide a framework strictly more expressive than either linear types or monads. The core lambda calculus is extended with references whose operations take an additional "witness" parameter, and these witness can be used to sequence operations. They also provide a type system to ensure witness race freedom. This looks interesting, but the system seems quite complicated. Additionally, managing the extra witness parameters seems like it might be a tad cumbersome.

The final approach I've come across is based on modal logic: A Logical View of Effects (or is A Modal Language for Effects newer?). It syntactically distinguishes terms which denote values and expressions which denote computations; control effects can appear only in terms, and world effects only in expressions. This looks interesting, but it also seems to be fairly new work so I'm not exactly sure how well developed it is or what sort of impact it has on a language.

I'm also curious as to whether the Orc orchestration language can be used to tame effects; it has explicit sequencing constructs, so order of operations is defined, and it is internally referentially transparent. Simon Peyton Jones has a noted a connection between Orc's primitives and Haskell's List monad, but the Haskell implementation of Orc does not seem publicly available anymore so I haven't been able to pursue this further. Since my language will feature concurrency, it would be nice to be able to provide concurrency primitives and tame effects with only a single addition. As others have noted, concurrency violates referential transparency as well, so there may be something here.

I'm interested in any views or experiences people may have with these various approaches to taming effects. Also, is there any other relevant research that I have not mentioned?

Effect systems

The most direct approach would be to use an effect typing system. This is related to the others you've mentioned (in fact they are all interrelated). Wadler's A Marriage of Effects and Monads illustrates how monads are related to effect typing systems. Googling for "effect systems", "effect typing" and such and following the references will give you things to read about it. One of the benefits (or arguably not) of effect typing is that the terms are the same any impure language only the types reveal whether an effect is present or not. This means there is no need to write in, for example, a "monadic style".

By Derek Elkins at Sun, 2007-11-25 02:53 | login or register to post comments

Comparing effect systems

As Derek Elkins mentioned, type and effect systems are a convenient way to present effects in a programming language. The work you surveyed can be considered as different possible choices of the semantics for an effect system. In choosing the right effect system for your language, I think it's useful to look at a couple of different dimensions:

How an expression's effects are described in its interface (i.e., the type-effect annotation).
How usage of effects constrains the possible valid implementations of a program (this is useful for optimization).

For example, using the Haskell IO monad causes a program's type to include "IO _". Composing multiple monad transfomers can give us more detailed effect information (dimension 1). In terms of behavior, the IO monad has to sequence actions, even if their order doesn't matter to the program. On the other hand, uniqueness types allow us to use dataflow to determine the true sequential dependencies (dimension 2).

You could examine the different systems in more detail according to these and other criteria to help find what works best for you. Here's another idea that I think can also help better frame the problem:

As you mentioned, there is a very close relationship between effects and concurrency, since an effect can be viewed as communication between a program and its evaluation context. Both the program and the context may either be monolithic or composed of multiple concurrent processes. From that perspective, the denotation of a program is no longer its result value as a function of its inputs, but rather a set of possible interaction traces as a function of its evaluation context. The type-effect of a program expression is then an observable abstraction of its possible interaction traces, rather than an abstraction (namely, the type) of its result value. Designing an effect system amounts to finding an abstraction that makes the right compromise between expressivity and tractability of effect analysis.

By Sameer Sundresh at Sun, 2007-11-25 05:58 | login or register to post comments

It should be noted that

It should be noted that monads don't necessarily prevent the dataflow approach - and uniqueness types don't necessarily gain anything. Not every monad has strict semantics, for example.

By Philippa Cowderoy at Sun, 2007-11-25 06:26 | login or register to post comments

Don't know why I had

Don't know why I neglected to mention type and effect systems; probably because all the work I had seen on them dealt with region-based memory management and not general effects. I'm particularly partial to Makholm's imperative region calculus, and he provides a handy approach for adding regions to any language. I'll have to do some more reading on effect systems and see how it can be used for general effects instead of just regions.

I had some questions about effect systems and concurrency, but managed to fine Nielson and Nielson's Type and Effect Systems paper, which extends a core calculus with references and concurrency primitives ala Concurrent ML. I still have questions with regard to distribution, but I'll save those until I've processed this. Anybody know anything about the Type and Effect Systems: Behaviours for Concurrency book?

I've already learned quite a bit from Nielson's paper: types are a data flow analysis, where effect systems are a control flow analysis. He further mentions that effects can be used to track exception propagation. In my post on purity I had discussed totality and how unchecked exceptions as found in OCaml and C# are detrimental to correctness; I then described a transformation to turn partial functions, like division, into total functions. Effects present an alternate technique to accomplish the same by using effects to track unhandled exceptions. The program's type just has to ensure that no exception escapes by specifying the 0 effect, and this will achieve a similar effect. Interesting! Much to digest here. :-)

Even more interesting will be the further development of the partiality monad. Making partiality an effect paves a "straightforward" path to useful total programming checked by types and effects, which would be quite significant!

[Edit: Nielson's paper also states that effect systems are eager; is that necessarily the case?]

By naasking at Sun, 2007-11-25 17:56 | login or register to post comments

What's the point of effect systems?

What's the point of effect systems? A quote from Nielson's paper:

It is then important to ensure that whenever a program can be typed in the original type system then there also exists a type in the type and effect system, and whenever there exists a type in the type and effect system then the program can also be typed in the original type system.

Isn't the point of adding a new level of static checking to rule out a larger class of erroneous programs? Given the above statement, I can see the use of type and effect systems in the optimization phase of a compiler to ensure valid transformations, but if effect annotations are exposed to the user, Nielson's statement doesn't seem correct.

For instance, I can specify map as accepting a function from 'a -> 'b, and enforce that it's effect is '0', ie. purely functional. This composition has a valid typing in the original, effect-less system, but not in the effect-ful one. Unless Neilson's meaning of "type" excludes the effect component. Hmm, on another reading he may just be referring to the inference algorithm producing valid typings. Any clarification is appreciated!

By naasking at Mon, 2007-11-26 16:23 | login or register to post comments

Full and faithful embedding

Unless Neilson's meaning of "type" excludes the effect component.

That's how I read that sentence. In technical terms, he seems to be saying that the type and effects systems needs to be a "conservative extention" of the base type system without effects.

(Incidentally, I think this also relates to some of the discussion here, at least in my mental model. ;-) )

By Marc Hamann at Mon, 2007-11-26 18:29 | login or register to post comments

Call-by-value given, what about call-by-name?

Nielson's paper assumes a call-by-value semantics, so that referencing any variable has no effect; I suspect this is just a simplification. Has there been any type and effect system developed with call-by-name/need semantics? Given the connection with monads, I'm sure it's possible.

By naasking at Wed, 2007-11-28 13:58 | login or register to post comments

Filinski's dissertation

A purported partial solution is Monadic Reflection (talk slides for Monadic Reflection in Haskell, whose paper doesn't seem available).

I don't know if, by "paper", you mean the first link but that is Filinski's thesis, not an ordinary paper. It's available here. It's not difficult or very long, and it contains (as I recall) a complete implementation in SML/NJ.

Thanks for the survey. These things are always useful.

By Frank Atanassow at Wed, 2007-11-28 04:28 | login or register to post comments

Systems programming

I very much like the way operating systems make effects manageable. Strong dynamic invariants like the isolation between Unix processes are great.

By Luke Gorrie at Wed, 2007-11-28 12:41 | login or register to post comments

The Monad Laws

naasking: However, monads require the developer to ensure he satisfies various algebraic properties, which can be difficult to understand.

This is true in the "popular" (on LtU, anyway) languages in which you can easily write monadic code: Haskell, OCaml, Standard ML... but not true necessarily, by which I mean that with a rich enough type system, you can enforce the monad laws. See here for details. :-)

Update: Here is actually the post that I originally had in mind when I wrote this. It's somewhat more concise than the one linked above.

By Paul Snively at Wed, 2007-11-28 14:59 | login or register to post comments

with a rich enough type

with a rich enough type system, you can enforce the monad laws.

Indeed, and enforcing the monad laws via rank-2 types is more or less what Unimo does. Unfortunately, adding such sophistication to my language is beyond me at the moment. :-(

By naasking at Wed, 2007-11-28 15:19 | login or register to post comments

"We donâ€™t need no stinking modules!"

Although you didn't refer to this aspect of it, that is the title of your second link..

Any comments on this aspect of Coq's type system?

I know barely anything about Coq, but its an interesting thought that the design of "module systems" may be missing the mark (i.e. its a non-problem).

By dbfaken at Wed, 2007-11-28 17:49 | login or register to post comments

I'm Not Positive...

...but I believe the point refers to the common (?) use of modules in the Standard ML or OCaml sense of "module system" to leverage the observation that "Abstract Types Have Existential Type." In Coq, "there exists some type y with property P" is spelled "{y | P y}," literally "there exists some type y such that P y holds."

So the use of modules to provide abstract types so that you have existential types is one particular use of modules that might be a "non-problem" given actual existential types. But it's not the only use of modules, so I'm sure modules are here to stay.

By Paul Snively at Wed, 2007-11-28 18:35 | login or register to post comments

But it's not the only use of

But it's not the only use of modules, so I'm sure modules are here to stay.

If a language can express first-class modules, what other uses for explicit second-class modules are there?

By naasking at Wed, 2007-11-28 19:24 | login or register to post comments

Lambda the Ultimate

User login

Navigation