I had the fortunate opportunity to attend ACM's Symposium on Principles of Programming Languages (POPL) '09 earlier this year, including keynote addresses and open panel discussions by some of the field's most prominent and celebrated researchers. One issue that came up over and over again was the difficult problem of how to handle so-called "effects".
The functional programming community typically uses terms such as "effectful computation" or "side effects" to describe a broad class of things a computer program may do at runtime whose consequences may not be readily apparent from inspection of the program text itself. These may include memory references (e.g. as in the notoriously strange pointer semantics of C), I/O, interrupts, exceptions, and message passing. In certain quarters, there is a long history of concern over how to encapsulate these inevitabilities of useful programming within a language that somehow tames their unpredictability. This is no doubt a worthy motive; programs all of whose effects were perfectly and completely evident in their source code would make programming in general much easier and might even open the door to that elusive and often contentious goal of "formal program verification". A very substantial research effort has gone into solving the problem and the ideas put forward, which are far too numerous to survey here, show a dazzling sophistication. Even so, the fact that the problem of how to sensibly express computational effects is still an active concern of leading researchers is evidence that no work so far has decisively settled the issue.
To understand the difficulty, one must understand the curious notion of "functional purity". Functional programming languages are languages based on the Lambda Calculus, one of the three canonical (and interchangeable) paradigms of universal computation. The Lambda Calculus, originally due to Alonzo Church, expresses computations as the application three basic reduction rules to syntactic objects usually referred to as "lambda terms". Because the Lambda Calculus is a complete model of universal computation, any program that can be executed on a computer can, in theory, be expressed as a term in the calculus, with the "halt state" of the program equivalent in some sense to the fully-reduced form of the lambda term. The basic building block of a lambda term is a "lambda", which is nothing other than a function in the formal mathematical sense of the word "function". That is, a lambda specifies a rule according to which an input value is matched to a specific, well-defined output value. It would be ideal if programs behaved like lambdas, producing a well-defined output for each well-formed input, according to a specific and well-defined rule. Moreover, since lambda terms are composable into larger lambda terms, such programs could be modularly combined, according to traditional software engineering practice, to produce large and useful new programs from smaller, more basic ones, all while preserving the happy property that no program could have more than one output for any given input. This, in essence, is the goal of pure functional programming.
The significance of functional purity is that it leaves no room for unexpected effects. In theory, program execution should proceed according to nothing other than the well-defined reduction rules of the lambda calculus, whence each reduction has exactly one effect, namely, that specified by the appropriate reduction rule. This does not mean that a pure-functional program may not have bugs, only that source of bugs will be restricted to logical errors on the part of the programmer, rather than unexpected interactions between parts of the program. By contrast, a program in a more familiar and more organic language (such as C) may appear superficially correct but cause effects at runtime whose consequences ripple widely through the program with obscure and unintended consequences. However, the more attentive or skeptical reader may object: since any really useful programming language has a well-defined semantics that specifies what any given statement will do, separating a logical error in a pure functional language from a effect-caused bug in an impure language is a distinction without a difference. Any unexpected behavior of a program is a bug, regardless of its origin.
That's not to say that pure functions are not a useful organizing principle. Pure functions capture a basic intuition of how programs are "supposed to" work, producing no more than one possible output for any given input, and doing so according to a clearly specified rule whose deeper implementation mechanics are usually of no interest to the programmer. Moreover, the simple reductions of the lambda calculus make it relatively easy to foresee what a functional program will do, which is a notable contrast to the semantics of non-functional languages which, even though well-defined, may be forbiddingly complicated. It is very telling that even the illustrious Edsger Dijkstra, an unflinching champion of careful and semantically exact program composition, admitted that semantic analysis for even straightforward properties of trivial imperative programs seemed excessively complex[1]. (However, it's also noteworthy that Dijkstra did the analysis anyway.) The idea of a pure functional language certainly has virtues. It is, however, another matter whether these virtues are attainable in practice.
The best-developed and most successful pure functional language yet implemented is Haskell. Haskell enjoys a selection of stable compilers for every major platform, including the Glasgow Haskell Compiler (GHC), which is a commercial-grade compiler boasting numerous useful extensions and the capability to produce native machine code. Programs written in every major implementation of Haskell, however, suffer in most cases from serious performance deficits compared to similar programs in a non-imperative language. Even the official Haskell Wiki notes that "GHC doesn't have any credible competition in the performance department", and suggests that programs written in Haskell may keep pace with counterparts in other languages, but only with very aggressive tweeking and optimization. Haskell depends upon a very complex run-time system that is highly susceptible to memory leaks and greatly complicates formal verification of compiled Haskell code. One might argue, however, that for at least some applications this would be an acceptable price to pay for the straightforward semantics of a lambda calculus. Haskell's purity, however, is in name only.
Arguably, Haskell does not achieve purity at all, but only manages to localize all of its "impurities" to one place. This place is an essential Haskell construct known as the IO monad, where virtually all essential program behaviors take place. In essence, a Haskell program can only make system calls, catch or raise exceptions, or handle interrupts inside the IO monad. This allows the familiar Haskell type "IO a" to act as a wall separating the idyllic garden of pure functional delights made possible by the runtime system from the gritty details of how real programs execute on real machines. One of the chief architects of GHC, Simon Peyton-Jones, famously described the IO monad a giant "sin-bin, used whenever we want to do something that breaks the purely functional paradigm." [2] Peyton-Jones makes a reasonable argument in the same article that simply making the pure-impure distinction is useful in itself, but also acknowledges that contemporary attempts to more completely account for effects prove either too complicated or too inefficient to be practical. Haskell represents the end-product of a tremendous and concerted research effort by a large number of talented people and GHC is surely an impressive technical accomplishment. However, the sheer magnitude of the effort required to achieve even this modest gain toward the language enthusiasts' goal of functional purity makes its shortcomings that much more conspicuous.
There is, I think, a lesson in all this, and that lesson is that there is no promise in trying to capture all the effects. Computers are machines, and machines work via carefully a orchestrated cascade of predetermined physical causes and their expected effects. All computation is effectful computation. I realize that this may be an extremely controversial thing to say, but I feel that it stands on a well-founded principle. The difficulties and idiosyncracies of so-called "effects" all arise from the fact that computers have to be physically constructed, and thus must accommodate the protocols of the circuits that constitute them, must retain their data in some kind of physical memory, and must have some means to communicate with machines and components that are spatially separate. Trying to resist this fact by abstracting away such details is bound to end in abstractions of rapidly increasing complexity and rapidly decreasing practicality.
The motivations for abstraction via programming language are multifaceted and practically compelling. At the same time, not all abstractions are good abstractions. Church's calculus has proven a powerful and useful model of computation, and is theoretically interesting in its own right. However, it is telling that it was Alan Turing's eponymous and much more mechanical "machine" that became the conceptual basis of the first digital computers. The difficulty of a problem often depends upon its phrasing. We can't write programs that consist of causes with no effects. I admit that it's a very broad, very contentious, and very far-reaching claim, but the utter complexity and unusability of attempts so far to account for so-called "computational effects" suggests that perhaps we are trying to answer the wrong questions.
[1] Dijkstra, Edsger. "Notes on Structured Programming." T.H.-Report 70-WSK-03. 1970.
[2] Peyton-Jones, Simon. "Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell." Microsoft Research, Cambridge. 2001.
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment