Computability Theory is the foundation for computer software development. Our programming languages embody the techniques and models described by various theories of computation . The Turing Machine is the canonical example of the Imperative Model . Lambda Calculus is the canonical example of the Functional Model . Kleene’s Church–Turing Thesis asserts the equivalence of these two models . Programmers have come to believe that this represents all there is, and all there ever can be, to programming. There seem to be two problems with that belief. First, that everything we want to do with computers can be expressed as partial-recursive functions. And second, that our definition of functions in terms of a procedure used to compute them gives us license to include operations that cause effects. I hope to show counter-arguments to both.
At the highest level of abstraction, we are encouraged to think of programs as functions. They take a value from a domain of possible inputs and map it to a value from a co-domain of possible outputs. It is impossible, in general, to precisely define (for all programs) the input domain on which the output is defined (c.f.: the Halting Problem ). Therefore, we view a program as a partial function, with a defined mapping for some subset of a more-broad input domain, but undefined (divergent, or non-terminating) on some input values. This is well-understood territory and we have many powerful tools to help us reason about such programs.Even though it may not always be well-defined, our “functional” view of a program implies that the output value is strictly dependent on the input value. For a given input value, the output will always be the same. We have abstracted over time. The output value—in fact the entire functional machinery—is timeless. This yields wonderfully useful properties! Since time is irrelevant, concurrency and parallelism have no effect on the result. Programs can be composed from easier-to-compute sub-programs without introducing the possibility of interference between them. Unfortunately, in the real world, time matters. Useful programs interact with their environment, and especially with the people that use the program. Some languages have gone to Herculean efforts to stay within the functional model by defining their programs as a function of time (and state). Most cheat, weaken their notion of “function” to include time-variant values (e.g.: random, read, receive), and/or cause effects (e.g.: assign, write, send). These functional “impurities” are considered necessary to create practical programs, however they destroy many of the useful properties of pure-functional programming. Pure functional programming, defining values without causing side-effects, is extremely valuable. However, it is not sufficient, by itself, to capture the time-varying nature of interactions in the real world.
In the real world, time matters. Unlike the mathematical construction of pure timeless functional values, we have to consider events that occur over time and the effects they cause. By taking an imperative procedural view we focus on the steps of an algorithm and the effect each step has on the state of the system.It is useful to distinguish between the value computed by a function and the procedure used to compute that value. The output value has a timeless relationship to the input value. Defining that relationship constitutes defining the function. However, the procedure (or algorithm) used to compute the output value takes time (possibly abstracted to a sequence of steps) to execute . If the relationship is not well-defined for a given input value, then the procedure for computing it may never terminate. A Turing Machine specifies the computational procedure directly, defining the functional relationship only indirectly. If the machine halts (a big “If”), the final state of the machine represents the output value. Lambda Calculus specifies the computation as the process of reducing terms. If a unique (irreducible) normal form is reached, that is considered the output value. Of course, the reduction process may never terminate, representing an undefined result. In both Lambda Calculus and Turing Machines, the functional relationship between input and output is represented indirectly, through a process that takes (possibly infinite) time to complete. Since we envision computation of a value in terms of changes to an abstract machine, we are naturally tempted to include operations which either cause externally-visible effects or acknowledge externally-originated events. However, as soon as we allow this, we are no longer computing a pure-functional value. What we need is a way to separate timeless values from time-dependent effects which represent real-world interactions.
Values and Effects
Values are the domain of Functional Programming. By abstracting over time we achieve referential transparency and a strong equational theory. These are powerful tools for reasoning about the correctness of programs. We should not discard them lightly. Note however, we must also account for time in our systems. And in an Open System (one which interacts with its environment) this introduces unbounded non-determinism in the occurrence-ordering of events. The Actor Model of Computation gives us the tools to reason about open systems .Effects are the domain of Actor Programming. Effects are a partial ordering of events that occur over time. An event is represented by the delivery of a message to an actor, which invokes the actor’s behavior. A behavior describes the effects that are caused by the event. Effects are limited to:
- creating new actors
- sending new messages
- designating a behavior for the current actor to become 
The Humus programming language is built on the principle of separating values and effects. There are pure-functional expressions (values), and actor-oriented statements (effects). Expression evaluation cannot cause effects. Message contents are expressions. A behavior description is an expressions, whose value is a collection of statements. Evaluating a behavior expression is not the same as executing it. Execution causes effects. When an actor receives a message, its behavior is executed. Using expressions to describe, but not execute, behaviors gives us the full abstractive power of Lambda Calculus without polluting the functional purity of expressions.Let’s consider how a message reception event is handled by an actor. Recall that the message is a pure (immutable) value. The first thing we must do is determine the behavior to execute. Since we would like the behavior to be parameterized by the incoming message, we will assume that the actor maintains a function mapping messages to behaviors. Applying this behavior function to the message results in a behavior value, a description of the effects we want. Executing the behavior involves actually causing the described effects to occur. Execution changes the local state of the actor configuration; adding new actors, sending new messages, and potentially associating a new behavior function with the current actor. We can always trace the provenance of any given effect back to the event that caused it. The collection of effects caused by a given event are like an atomic transaction. Either all occur, or none occur. No actor in the system, including the one executing the behavior, can observe any effects until the behavior has completed.
LET sink_beh = \_. CREATE sink WITH sink_beh
Here we define a behavior function sink_beh that, when applied to any message, yields an empty statement block. The “
\” symbol represents lambda. The “
_” symbol is a wildcard that matches any message, but does not bind any identifiers. The behavior value is a statement block (with no statements) enclosed by “
[” and “
BECOMEstatements). This is trivially accomplished by wrapping a function around our message-to-behavior function.
LET once_beh = \cust.\msg.[ SEND msg TO cust BECOME sink_beh ] CREATE print_once WITH once_beh(println)
The definition of once_beh is parameterized by cust, yielding a function mapping msg to a statement block behavior value. The statement block contains two statements. A
SEND of msg to cust, and a
BECOME specifying that the actor’s subsequent behavior will be our previously-defined sink_beh (ignore all messages). When the print_once actor is created, println is bound to cust. When print_once receives a message, it forwards the message to println and ignores all subsequent messages.
f=\x.x” and “
f(x)=x” are equivalent ways of defining a function, we can rewrite behavior definitions to emphasize the separation between specification-time bindings and reception-time bindings. We place the specification-time (state) bindings on the left, and the reception-time (message) bindings on the right, under the lambda.
LET race_beh(list) = \(cust, req).[ CREATE once WITH once_beh(cust) send_to_all((once, req), list) ]
We define race_beh to arrange a concurrent race among a list of actors. A race actor expects a message consisting of a customer cust and a request req. We create a once actor to ensure that the customer cust receives only one answer. The original request req is sent to each actor in the list, with once specified as the proxy customer. It is important to note that send_to_all is not a statement. It is a function that produces a statement block, which is then executed.
LET send_to_all(msg, list) = [ CASE list OF () :  (first, rest) : [ SEND msg TO first send_to_all(msg, rest) ] (last) : [ SEND msg TO last ] END ]
The send_to_all function takes a message msg and a list of actors. We use a
CASE expression (not a statement) to conditionally compose the proper statement block, based on the structure of the list. If list is empty, we return an empty block. If list is a pair, we return a block that will send msg to first, and call sent_to_all recursively to construct a nested block based on the value of rest. Finally, if list is a singleton, we return a block that will just send msg to last.
CREATE stooge_race WITH race_beh(larry, curly, moe)” would evaluate to:
CREATE stooge_race WITH \(cust, req).[ CREATE once WITH once_beh(cust) [ SEND (once, req) TO larry [ SEND (once, req) TO curly [ SEND (once, req) TO moe ] ] ] ]
This is truly an executable specification. We can use the full power of functional abstraction to compute statement block behavior values. Computation of a statement block never causes any effects (it is just a value). Effects are caused by the execution of a block, which only happens in response to an actor receiving a message. The block is only a description of the desired effects.
Actor primitives are all about effects. However, an actor’s behavior description is a pure timeless value. By separating execution (causing effects) from evaluation (computing values), we can avoid polluting our functional expression language, yet still handle real-world Open System interactions. The Humus programming language demonstrates the facility of this approach.
- P. Van Roy, S. Haridi. Concepts, Techniques, and Models of Computer Programming. MIT Press, 2004.
- A. M. Turing. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. 2 42, 1937.
- A. Church. The Calculi of Lambda-Conversion. Princeton University Press, 1941.
- S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952.
- M. Davis. The Undecidable – Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Raven, New York, 1965. Reprint, Dover, 2004.
- E. A. Lee. Computing Needs Time, Communications of the ACM, 52(5):70-79, May 2009.
- C. Hewitt, P. de Jong. Analyzing the Roles of Descriptions and Actions in Open Systems. AI Memo 727, MIT, April, 1983.
- G. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, 1986.