This paper presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with effects, including mutable store, input and output, and probabilistic and non-deterministic computation as special cases of input. The FMC is derived from the lambda-calculus via two independent generalizations. One enables the encoding of effects into the calculus; the other provides control when they are executed, and encodes the imperative features of “sequencing” and “skip”.

These generalizations are particularly natural from the perspective of the FMC as an instruction language for a simple stack machine (a simplified Krivine Abstract Machine, and the “M” in “FMC”). The first generalization corresponds to allowing multiple stacks, which may represent storage cells and input and output streams to capture the operational semantics of effects. The second generalization gives composition of instruction sequences, and the empty sequence as a unit.

The FMC naturally encodes various previous approaches, including Plotkin’s Call-By-Value lambda-calculus, Moggi’s Computational Metalanguage, and Levy’s Call-By-Push-Value. The calculus is confluent, which is possible because beta-reduction encodes the evaluation of effects via their algebraic equations, not their operational semantics. Different evaluation strategies in the lambda-calculus are captured by different encodings into the FMC.

The FMC can be simply typed, and a simple, direct proof shows that types confer termination of the stack machine, or equivalently of weak head reduction. Types give a natural solution to the problem of types for higher-order store.