Lambda the Ultimate

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?